<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.5//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_5.dtd'>
<nta>
	<declaration>//Insert declarations of global clocks, variables, constants and channels.

const int N = 4;
const int M = N*2;
const int MINDELAY = 1;
const int MAXDELAY = 5;
const int DDELAY = MAXDELAY-MINDELAY;
const int TDELAY = 6;
const int TO = 10;

clock time;

typedef int[0,N-1] id_t;
typedef int[0,M-1] id_m;
typedef struct
{
  id_t src;
  id_t dst;
  id_t leader;
  int[0,N] hops;
} msg_t;

void setMsg(msg_t &amp;msg, id_t src, id_t dst, id_t leader, int[0,N] hops)
{
  msg.src = src;
  msg.dst = dst;
  msg.leader = leader;
  msg.hops = hops;
}

broadcast chan send;
broadcast chan receive[N];
msg_t shared;

int linked[N][N];

bool link(id_t n, id_t m) {
    return (m == ((m+1)%N)) or (m == (n+1)%N);
}

void reset(msg_t &amp;msg)
{
  msg.src = msg.dst = msg.leader = msg.hops = 0;
}

bool used[M];</declaration>
	<template>
		<name x="5" y="5">Message</name>
		<parameter>const id_m id</parameter>
		<declaration>//Insert local declarations of clocks, variables and constants.

clock x;
msg_t msg;

bool mayUse()
{
  int i = 0;
  while (i &lt; id)
  {
    if(!used[i])
      return false;
    i++;
  }
  return true;
}

const int mtype = 3;</declaration>
		<location id="id0" x="360" y="216">
			<label kind="invariant" x="352" y="232">x&lt;=1</label>
		</location>
		<location id="id1" x="168" y="216">
			<label kind="invariant" x="120" y="232">x&lt;=DDELAY/2</label>
		</location>
		<location id="id2" x="480" y="-216">
			<label kind="invariant" x="464" y="-248">x&lt;=DDELAY/6</label>
		</location>
		<location id="id3" x="408" y="-216">
			<label kind="invariant" x="360" y="-248">x&lt;=DDELAY/6</label>
		</location>
		<location id="id4" x="344" y="-216">
			<label kind="invariant" x="296" y="-272">x&lt;=DDELAY/6</label>
		</location>
		<location id="id5" x="272" y="-216">
			<label kind="invariant" x="224" y="-248">x&lt;=DDELAY/6</label>
		</location>
		<location id="id6" x="192" y="-216">
			<label kind="invariant" x="120" y="-248">x&lt;=DDELAY/6</label>
		</location>
		<location id="id7" x="104" y="-216">
			<label kind="invariant" x="16" y="-248">x&lt;=DDELAY/6</label>
		</location>
		<location id="id8" x="352" y="-120">
			<label kind="invariant" x="344" y="-152">x&lt;=DDELAY/3</label>
		</location>
		<location id="id9" x="264" y="-120">
			<label kind="invariant" x="232" y="-152">x&lt;=DDELAY/3</label>
		</location>
		<location id="id10" x="176" y="-120">
			<label kind="invariant" x="120" y="-152">x&lt;=DDELAY/3</label>
		</location>
		<location id="id11" x="344" y="32">
			<label kind="invariant" x="312" y="0">x&lt;=DDELAY/2</label>
		</location>
		<location id="id12" x="216" y="32">
			<label kind="invariant" x="192" y="0">x&lt;=DDELAY/2</label>
		</location>
		<location id="id13" x="280" y="104">
			<label kind="invariant" x="240" y="72">x&lt;=DDELAY</label>
		</location>
		<location id="id14" x="280" y="144">
			<label kind="invariant" x="232" y="160">x&lt;=DDELAY/2</label>
		</location>
		<location id="id15" x="432" y="104">
			<urgent/>
		</location>
		<location id="id16" x="64" y="104">
			<urgent/>
		</location>
		<location id="id17" x="-88" y="104">
			<label kind="invariant" x="-224" y="72">x&lt;=MINDELAY</label>
		</location>
		<location id="id18" x="240" y="328">
		</location>
		<init ref="id18"/>
		<transition id="id19">
			<source ref="id0"/>
			<target ref="id15"/>
		</transition>
		<transition id="id20">
			<source ref="id1"/>
			<target ref="id0"/>
			<label kind="guard" x="208" y="192">x==DDELAY/2</label>
			<label kind="assignment" x="220" y="216">x:=0</label>
		</transition>
		<transition id="id21">
			<source ref="id16"/>
			<target ref="id1"/>
			<label kind="guard" x="40" y="160">mtype==0</label>
		</transition>
		<transition id="id22">
			<source ref="id2"/>
			<target ref="id15"/>
		</transition>
		<transition id="id23">
			<source ref="id3"/>
			<target ref="id2"/>
			<label kind="assignment" x="424" y="-216">x=0</label>
		</transition>
		<transition id="id24">
			<source ref="id4"/>
			<target ref="id3"/>
			<label kind="assignment" x="360" y="-216">x=0</label>
		</transition>
		<transition id="id25">
			<source ref="id5"/>
			<target ref="id4"/>
			<label kind="assignment" x="288" y="-216">x=0</label>
		</transition>
		<transition id="id26">
			<source ref="id6"/>
			<target ref="id5"/>
			<label kind="assignment" x="216" y="-216">x=0</label>
		</transition>
		<transition id="id27">
			<source ref="id7"/>
			<target ref="id6"/>
			<label kind="assignment" x="136" y="-208">x=0</label>
		</transition>
		<transition id="id28">
			<source ref="id16"/>
			<target ref="id7"/>
			<label kind="guard" x="0" y="-80">mtype==5</label>
		</transition>
		<transition id="id29">
			<source ref="id17"/>
			<target ref="id16"/>
			<label kind="guard" x="-56" y="80">x==MINDELAY</label>
			<label kind="assignment" x="-16" y="104">x=0</label>
		</transition>
		<transition id="id30">
			<source ref="id8"/>
			<target ref="id15"/>
		</transition>
		<transition id="id31">
			<source ref="id9"/>
			<target ref="id8"/>
			<label kind="assignment" x="296" y="-120">x=0</label>
		</transition>
		<transition id="id32">
			<source ref="id10"/>
			<target ref="id9"/>
			<label kind="assignment" x="200" y="-120">x=0</label>
		</transition>
		<transition id="id33">
			<source ref="id16"/>
			<target ref="id10"/>
			<label kind="guard" x="104" y="-32">mtype==4</label>
		</transition>
		<transition id="id34">
			<source ref="id12"/>
			<target ref="id11"/>
			<label kind="assignment" x="256" y="32">x=0</label>
		</transition>
		<transition id="id35">
			<source ref="id11"/>
			<target ref="id15"/>
		</transition>
		<transition id="id36">
			<source ref="id16"/>
			<target ref="id12"/>
			<label kind="guard" x="112" y="32">mtype==3</label>
		</transition>
		<transition id="id37">
			<source ref="id13"/>
			<target ref="id15"/>
		</transition>
		<transition id="id38">
			<source ref="id16"/>
			<target ref="id13"/>
			<label kind="guard" x="136" y="80">mtype==2</label>
		</transition>
		<transition id="id39">
			<source ref="id14"/>
			<target ref="id15"/>
			<label kind="guard" x="336" y="136">x==DDELAY/2</label>
		</transition>
		<transition id="id40">
			<source ref="id16"/>
			<target ref="id14"/>
			<label kind="guard" x="120" y="128">mtype == 1</label>
		</transition>
		<transition id="id41">
			<source ref="id15"/>
			<target ref="id18"/>
			<label kind="synchronisation" x="520" y="184">receive[msg.dst]!</label>
			<label kind="assignment" x="520" y="208">shared = msg,
reset(msg),
used[id] = false</label>
			<nail x="512" y="104"/>
			<nail x="512" y="328"/>
		</transition>
		<transition id="id42">
			<source ref="id18"/>
			<target ref="id17"/>
			<label kind="guard" x="-264" y="160">mayUse()</label>
			<label kind="synchronisation" x="-264" y="176">send?</label>
			<label kind="assignment" x="-264" y="192">x = 0,
msg = shared,
reset(shared),
used[id] = true</label>
			<nail x="-136" y="328"/>
			<nail x="-136" y="104"/>
		</transition>
	</template>
	<template>
		<name>Node</name>
		<parameter>const id_t id</parameter>
		<declaration>
id_t leader = id;
int[0,N] hops;
clock x;
int[0,N] i;
id_t src;

void set(id_t l, int[0,N] h)
{
  leader = l;
  hops = h;
}

int[0,N] next(int[0,N] i,int[0,N] src)
{
  while (i  &lt; N &amp;&amp; (!link(id, i) || i == src))
  {
    i++;
  }
  return i;
}

int[0,1000] timeout()
{
  if (hops &gt; 0)
    return TO + TDELAY + hops * MAXDELAY;
  return TO;
}

bool worse(const msg_t &amp;msg)
{ 
  return msg.leader &gt; leader || msg.leader == leader &amp;&amp; msg.hops &gt; hops;
}</declaration>
		<location id="id43" x="360" y="400">
			<committed/>
		</location>
		<location id="id44" x="168" y="400">
			<committed/>
		</location>
		<location id="id45" x="168" y="96">
			<committed/>
		</location>
		<location id="id46" x="168" y="256">
			<label kind="invariant" x="-8" y="248">x &lt;= timeout() + TDELAY</label>
		</location>
		<init ref="id46"/>
		<transition id="id47">
			<source ref="id43"/>
			<target ref="id46"/>
			<label kind="guard" x="240" y="232">i == N</label>
			<label kind="assignment" x="288" y="232">i = src = 0</label>
			<nail x="360" y="256"/>
		</transition>
		<transition id="id48">
			<source ref="id43"/>
			<target ref="id43"/>
			<label kind="guard" x="424" y="344">i &lt; N</label>
			<label kind="synchronisation" x="416" y="360">send!</label>
			<label kind="assignment" x="416" y="376">setMsg(shared, id, i, leader, hops),
i = next(i+1, src)</label>
			<nail x="408" y="344"/>
			<nail x="408" y="400"/>
		</transition>
		<transition id="id49">
			<source ref="id44"/>
			<target ref="id43"/>
			<label kind="guard" x="208" y="400">!worse(shared)</label>
			<label kind="assignment" x="208" y="416">src = shared.src,
set(shared.leader, shared.hops + 1),
i = next(0, src),
x = 0</label>
		</transition>
		<transition id="id50">
			<source ref="id44"/>
			<target ref="id46"/>
			<label kind="guard" x="176" y="296">worse(shared)</label>
			<label kind="assignment" x="176" y="312">reset(shared)</label>
		</transition>
		<transition id="id51">
			<source ref="id46"/>
			<target ref="id44"/>
			<label kind="synchronisation" x="24" y="304">receive[id]?</label>
			<nail x="112" y="288"/>
			<nail x="112" y="400"/>
		</transition>
		<transition id="id52">
			<source ref="id45"/>
			<target ref="id46"/>
			<label kind="guard" x="240" y="120">i == N</label>
			<label kind="assignment" x="240" y="144">i = 0</label>
			<nail x="232" y="96"/>
			<nail x="232" y="232"/>
		</transition>
		<transition id="id53">
			<source ref="id45"/>
			<target ref="id45"/>
			<label kind="guard" x="112" y="-24">i &lt; N</label>
			<label kind="synchronisation" x="112" y="-8">send!</label>
			<label kind="assignment" x="112" y="8">setMsg(shared, id, i, leader, hops),
i = next(i + 1, N)</label>
			<nail x="120" y="48"/>
			<nail x="208" y="48"/>
		</transition>
		<transition id="id54">
			<source ref="id46"/>
			<target ref="id45"/>
			<label kind="guard" x="16" y="152">x &gt; timeout()</label>
			<label kind="assignment" x="16" y="168">set(id, 0),
i = next(0, N),
x = 0</label>
			<nail x="112" y="216"/>
			<nail x="112" y="96"/>
		</transition>
	</template>
	<system>//Insert process assignments.

//Edit system definition.
system Message, Node; </system>
	<queries>
		<query>
			<formula>Pr[&lt;=(TO + TDELAY + (N-1)*MAXDELAY)](&lt;&gt; forall (i : id_t) Node(i).leader==0)</formula>
			<comment/>
		</query>
		<query>
			<formula>Pr[&lt;=(TO + TDELAY + (N-8)*MAXDELAY)](&lt;&gt; forall (i : id_t) Node(i).leader==0)</formula>
			<comment/>
		</query>
		<query>
			<formula>A[] (time &gt;= (TO + TDELAY + (N-1)*MAXDELAY) imply ( forall (i : id_t) Node(i).leader==0) )</formula>
			<comment/>
		</query>
		<query>
			<formula>A[] (time &gt;  (TO + TDELAY + (N-1)*MAXDELAY) imply ( forall (i : id_t) Node(i).leader==0) )</formula>
			<comment/>
		</query>
		<query>
			<formula>Pr[&lt;=(TO + TDELAY + N*MAXDELAY)/2](&lt;&gt; forall (i : id_t) Node(i).leader==0)</formula>
			<comment/>
		</query>
		<query>
			<formula>A[] not deadlock</formula>
			<comment/>
		</query>
	</queries>
</nta>
