<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>
<nta>
	<declaration>const int NODES = 4;  // number of nodes in the network
const int SLOTS = 5; // number of slots in a frame
const int frame = SLOTS;
const int maxk = 3; // max number of frames to wait for initially

typedef int[0,NODES-1] nodeid_t;// used to identify node
typedef int[-1,NODES-1] node_t; // used to transfer node info where -1 means no node
typedef int[0,SLOTS-1] slotid_t;// used to identify slot
typedef int[-1,SLOTS-1] slot_t; // used to transfer slot info where -1 means no slot
typedef int[0, maxk] frame_t;
typedef int weight_t[frame_t];
typedef bool topology_t[nodeid_t][nodeid_t];
typedef int power_t[nodeid_t];

const weight_t expw = {4, 2, 1, 1};
const weight_t uni = {1, 1, 1, 1};

const topology_t ring =
{//   0  1  2  3
    { 0, 1, 1, 0}, // 0
    { 1, 0, 0, 1}, // 1
    { 1, 0, 0, 1}, // 2
    { 0, 1, 1, 0}  // 3
};

const topology_t chain =
{//   0  1  2  3
    { 0, 1, 1, 0}, // 0
    { 1, 0, 0, 1}, // 1
    { 1, 0, 0, 0}, // 2
    { 0, 1, 0, 0}  // 3
};

const weight_t weight = expw;
const topology_t can_hear = ring;

// Medium model with variables that contain data sent from a node;
broadcast chan  sendWM;
nodeid_t aux_node; // the sender id
slot_t aux_slot; // id of slot that had collision (-1 means no collision)
    
typedef bool used_slot_t[slotid_t];

const used_slot_t zero_vec = { 0, 0, 0, 0, 0};
const used_slot_t max_vec =  { 1, 1, 1, 1, 1};

// neighbor information for how nodes use slots
used_slot_t first[nodeid_t];
used_slot_t second[nodeid_t]; 

slot_t slot_no[nodeid_t]={0,-1,-1,-1}; // currently used slot by a node
</declaration>
	<template>
		<name x="5" y="5">Node</name>
		<parameter>const nodeid_t id</parameter>
		<declaration>clock t;
int[-1, maxk*SLOTS] counter;

slot_t curr=-1, detected=-1, col=-1;

used_slot_t aux_vec;
used_slot_t rec_vec;

bool got_info=0;
bool sent_info=0;

void acc(used_slot_t&amp; usage, const used_slot_t&amp; info) 
{
    for(i: nodeid_t) usage[i] |= info[i];
}</declaration>
		<location id="id0" x="-384" y="808">
			<name x="-408" y="824">sending</name>
			<committed/>
		</location>
		<location id="id1" x="32" y="808">
			<name x="16" y="840">sent</name>
			<label kind="invariant" x="16" y="824">t&lt;=2</label>
		</location>
		<location id="id2" x="144" y="808">
			<name x="136" y="840">done</name>
			<label kind="invariant" x="134" y="823">t&lt;=2</label>
		</location>
		<location id="id3" x="496" y="624">
			<name x="512" y="608">rec_one</name>
			<label kind="invariant" x="512" y="624">t&lt;=2</label>
		</location>
		<location id="id4" x="280" y="624">
			<name x="240" y="576">listening</name>
			<label kind="invariant" x="248" y="592">t&lt;=2</label>
		</location>
		<location id="id5" x="88" y="624">
			<name x="24" y="624">Normal</name>
			<committed/>
		</location>
		<location id="id6" x="-384" y="624">
			<name x="-400" y="576">ready</name>
			<label kind="invariant" x="-400" y="592">t&lt;=1</label>
		</location>
		<location id="id7" x="88" y="472">
			<name x="112" y="464">choice</name>
			<committed/>
		</location>
		<location id="id8" x="-120" y="384">
			<name x="-144" y="336">done0</name>
			<label kind="invariant" x="-144" y="352">t&lt;=2</label>
		</location>
		<location id="id9" x="88" y="336">
			<label kind="invariant" x="104" y="344">t&lt;=2</label>
			<committed/>
		</location>
		<location id="id10" x="-408" y="232">
			<name x="-424" y="184">rec_one0</name>
			<label kind="invariant" x="-424" y="200">t&lt;=2</label>
		</location>
		<location id="id11" x="88" y="232">
			<name x="8" y="232">listening0</name>
			<label kind="invariant" x="8" y="248">t&lt;=2</label>
		</location>
		<location id="id12" x="88" y="136">
			<name x="104" y="120">waiting</name>
			<label kind="invariant" x="104" y="136">t&lt;=2*counter</label>
		</location>
		<location id="id13" x="-160" y="-40">
			<label kind="invariant" x="-216" y="-48">t&lt;=1</label>
		</location>
		<location id="id14" x="88" y="-40">
			<label kind="invariant" x="112" y="-48">t&lt;=1</label>
		</location>
		<location id="id15" x="88" y="-160">
			<name x="78" y="-190">initial</name>
		</location>
		<location id="id16" x="-64" y="-160">
			<committed/>
		</location>
		<branchpoint id="id17" x="88" y="40">
		</branchpoint>
		<init ref="id16"/>
		<transition>
			<source ref="id5"/>
			<target ref="id17"/>
			<label kind="guard" x="-416" y="512">curr==slot_no[id] &amp;&amp; first[id]==zero_vec &amp;&amp; id!=0</label>
			<label kind="assignment" x="-416" y="528">counter=-1, detected=-1, slot_no[id]=-1,
aux_vec=zero_vec, first[id]=zero_vec, 
sent_info=0</label>
			<nail x="-72" y="544"/>
			<nail x="-464" y="544"/>
			<nail x="-464" y="40"/>
		</transition>
		<transition>
			<source ref="id6"/>
			<target ref="id0"/>
			<label kind="guard" x="-440" y="696">t==1</label>
			<label kind="assignment" x="-440" y="712">aux_node=id,
aux_slot=detected</label>
		</transition>
		<transition>
			<source ref="id0"/>
			<target ref="id1"/>
			<label kind="synchronisation" x="-236" y="793">sendWM!</label>
			<label kind="assignment" x="-236" y="808">detected=-1,
sent_info=1</label>
			<label kind="comments" x="-236" y="838">Broadcast information about collisions if any</label>
		</transition>
		<transition>
			<source ref="id1"/>
			<target ref="id5"/>
			<label kind="guard" x="-48" y="744">t==2</label>
			<label kind="assignment" x="-48" y="760">curr=(curr+1)%frame,
first[id]=zero_vec,
t=0</label>
			<nail x="88" y="736"/>
		</transition>
		<transition>
			<source ref="id2"/>
			<target ref="id5"/>
			<label kind="guard" x="128" y="744">t==2</label>
			<label kind="assignment" x="128" y="760">curr=(curr+1)%frame,
t=0</label>
			<nail x="88" y="736"/>
		</transition>
		<transition>
			<source ref="id3"/>
			<target ref="id2"/>
			<label kind="guard" x="216" y="776">can_hear[id][aux_node]</label>
			<label kind="synchronisation" x="216" y="792">sendWM?</label>
			<label kind="assignment" x="216" y="808">detected=(detected&lt;0)?curr:detected,
rec_vec=zero_vec</label>
			<label kind="comments" x="260" y="746">detected two messages in one slot: record the collision</label>
			<nail x="496" y="808"/>
		</transition>
		<transition>
			<source ref="id4"/>
			<target ref="id5"/>
			<label kind="guard" x="128" y="640">t==2</label>
			<label kind="assignment" x="128" y="648">curr=(curr+1)%frame,
first[id][curr]=0,
t=0</label>
			<nail x="280" y="664"/>
			<nail x="112" y="664"/>
		</transition>
		<transition>
			<source ref="id3"/>
			<target ref="id5"/>
			<label kind="guard" x="168" y="680">t==2 &amp;&amp;
col!=slot_no[id]</label>
			<label kind="assignment" x="168" y="712">curr=(curr+1)%frame,
t=0,
rec_vec=zero_vec</label>
			<nail x="488" y="712"/>
			<nail x="136" y="712"/>
		</transition>
		<transition>
			<source ref="id3"/>
			<target ref="id11"/>
			<label kind="guard" x="392" y="304">t==2 &amp;&amp;
(col==slot_no[id] || 
(rec_vec[slot_no[id]] &amp;&amp; !sent_info))</label>
			<label kind="assignment" x="392" y="352">counter=0,
curr=(curr+1)%frame,
col=-1,
detected=-1,
slot_no[id]=-1,
first[id]=zero_vec,
sent_info=0,
rec_vec=zero_vec,
t=0</label>
			<label kind="comments" x="232" y="458">Reported colision on our slot</label>
			<nail x="496" y="232"/>
		</transition>
		<transition>
			<source ref="id4"/>
			<target ref="id3"/>
			<label kind="guard" x="296" y="592">can_hear[id][aux_node]==1</label>
			<label kind="synchronisation" x="296" y="608">sendWM?</label>
			<label kind="assignment" x="296" y="624">col=aux_slot,
first[id][curr]=1,
rec_vec=sent_info?
  zero_vec : first[aux_node]</label>
		</transition>
		<transition>
			<source ref="id5"/>
			<target ref="id4"/>
			<label kind="guard" x="112" y="608">curr!=slot_no[id]</label>
		</transition>
		<transition>
			<source ref="id5"/>
			<target ref="id6"/>
			<label kind="guard" x="-328" y="608">curr==slot_no[id] &amp;&amp; (first[id]!=zero_vec || id==0)</label>
		</transition>
		<transition>
			<source ref="id7"/>
			<target ref="id5"/>
			<label kind="select" x="24" y="496">slot: int[0,frame-1]</label>
			<label kind="guard" x="24" y="512">!aux_vec[slot] &amp;&amp;
aux_vec != zero_vec</label>
			<label kind="assignment" x="24" y="544">slot_no[id]=slot,
aux_vec=zero_vec</label>
		</transition>
		<transition>
			<source ref="id16"/>
			<target ref="id6"/>
			<label kind="guard" x="-336" y="-176">id==0</label>
			<label kind="assignment" x="-336" y="-160">curr=0</label>
			<label kind="comments" x="-284" y="262">Gateway uses slot #0 and initiates the communication.</label>
			<nail x="-488" y="-160"/>
			<nail x="-488" y="624"/>
		</transition>
		<transition>
			<source ref="id7"/>
			<target ref="id17"/>
			<label kind="guard" x="-416" y="440">aux_vec==max_vec || aux_vec==zero_vec</label>
			<label kind="assignment" x="-416" y="456">counter=-1, aux_vec=zero_vec,
first[id]=zero_vec, second[id]=zero_vec,
detected=-1</label>
			<label kind="comments" x="28" y="286">All slots taken, reset the neighbour information.</label>
			<nail x="-440" y="472"/>
			<nail x="-440" y="40"/>
		</transition>
		<transition>
			<source ref="id9"/>
			<target ref="id7"/>
			<label kind="guard" x="32" y="400">counter&gt;=frame-1</label>
			<label kind="assignment" x="32" y="416">aux_vec=first[id],
acc(aux_vec,second[id]),
second[id]=zero_vec</label>
		</transition>
		<transition>
			<source ref="id8"/>
			<target ref="id9"/>
			<label kind="guard" x="-96" y="368">t==2</label>
			<label kind="assignment" x="-96" y="384">curr=(curr+1)%frame,
t=0</label>
			<nail x="24" y="384"/>
		</transition>
		<transition>
			<source ref="id10"/>
			<target ref="id9"/>
			<label kind="guard" x="-288" y="272">t==2</label>
			<label kind="assignment" x="-288" y="288">curr=(curr+1)%frame,
acc(second[id], rec_vec),
rec_vec=zero_vec,
t=0</label>
			<nail x="-328" y="304"/>
			<nail x="8" y="304"/>
		</transition>
		<transition>
			<source ref="id10"/>
			<target ref="id8"/>
			<label kind="guard" x="-400" y="352">can_hear[id][aux_node]</label>
			<label kind="synchronisation" x="-400" y="368">sendWM?</label>
			<label kind="assignment" x="-400" y="384">detected=(detected&lt;0)?curr:detected,
rec_vec=zero_vec</label>
			<label kind="comments" x="-324" y="338">Collision detected</label>
			<nail x="-408" y="384"/>
		</transition>
		<transition>
			<source ref="id11"/>
			<target ref="id9"/>
			<label kind="guard" x="160" y="264">t==2</label>
			<label kind="assignment" x="160" y="280">curr=(curr+1)%frame,
t=0</label>
			<nail x="192" y="256"/>
			<nail x="192" y="320"/>
		</transition>
		<transition>
			<source ref="id9"/>
			<target ref="id11"/>
			<label kind="guard" x="32" y="264">counter&lt;frame-1</label>
			<label kind="assignment" x="32" y="280">counter++</label>
		</transition>
		<transition>
			<source ref="id11"/>
			<target ref="id10"/>
			<label kind="guard" x="-176" y="200">can_hear[id][aux_node]</label>
			<label kind="synchronisation" x="-176" y="216">sendWM?</label>
			<label kind="assignment" x="-176" y="232">rec_vec=first[aux_node],
first[id][curr]=1</label>
		</transition>
		<transition>
			<source ref="id12"/>
			<target ref="id11"/>
			<label kind="guard" x="32" y="160">t==2*counter</label>
			<label kind="assignment" x="32" y="176">counter=0,
t=0</label>
		</transition>
		<transition>
			<source ref="id17"/>
			<target ref="id12"/>
			<label kind="select" x="24" y="48">k:frame_t</label>
			<label kind="assignment" x="24" y="80">counter=k*frame,
t=0</label>
			<label kind="comments" x="28" y="118">Choice of frame</label>
			<label kind="probability" x="24" y="64">weight[k]</label>
		</transition>
		<transition>
			<source ref="id14"/>
			<target ref="id17"/>
			<label kind="guard" x="32" y="-24">t==1</label>
			<label kind="assignment" x="32" y="-8">curr=(curr+1)%frame,
t=0</label>
		</transition>
		<transition>
			<source ref="id13"/>
			<target ref="id15"/>
			<label kind="guard" x="-32" y="-128">t==1</label>
			<label kind="assignment" x="-32" y="-112">t=0</label>
		</transition>
		<transition>
			<source ref="id14"/>
			<target ref="id13"/>
			<label kind="guard" x="-88" y="-72">can_hear[id][aux_node]</label>
			<label kind="synchronisation" x="-88" y="-56">sendWM?</label>
		</transition>
		<transition>
			<source ref="id15"/>
			<target ref="id14"/>
			<label kind="guard" x="96" y="-134">can_hear[id][aux_node]</label>
			<label kind="synchronisation" x="96" y="-119">sendWM?</label>
			<label kind="assignment" x="96" y="-104">curr=slot_no[aux_node],
t=0</label>
		</transition>
		<transition>
			<source ref="id16"/>
			<target ref="id15"/>
			<label kind="guard" x="-32" y="-176">id!=0</label>
		</transition>
	</template>
	<system>clock time;

system Node;
</system>
	<queries>
		<query>
			<formula>A[] not deadlock</formula>
			<comment>The most basic formula is freedom from deadlocks			</comment>
		</query>
		<query>
			<formula>A[] forall(i: nodeid_t) forall(j: nodeid_t) (Node(i).t==1 imply Node(j).t==1)</formula>
			<comment>Nodes should be synchronised halfway the duration of a slot, since at this time they will send and receive information. Prove for each pair (i, j) of first-order neighbours</comment>
		</query>
		<query>
			<formula>A&lt;&gt; (slot_no[0]!=slot_no[1] and slot_no[0]&gt;=0 and slot_no[1]&gt;=0)</formula>
			<comment>Eventually node 0 and 1 allocate different slots? Answer: yes</comment>
		</query>
		<query>
			<formula>A&lt;&gt; (slot_no[0]!=slot_no[2] and slot_no[0]&gt;=0 and slot_no[2]&gt;=0)</formula>
			<comment>Eventually node 0 and 2 allocate different slots? Answer: yes</comment>
		</query>
		<query>
			<formula>A&lt;&gt; (slot_no[0]!=slot_no[3] and slot_no[0]&gt;=0 and slot_no[3]&gt;=0)</formula>
			<comment>Eventually node 0 and 3 allocate different slots? Answer: NO (strange)</comment>
		</query>
		<query>
			<formula>A&lt;&gt; (slot_no[1]!=slot_no[2] and slot_no[1]&gt;=0 and slot_no[2]&gt;=0)</formula>
			<comment>Eventually node 1 and 2 allocate different slots? Answer: NO (strange)</comment>
		</query>
		<query>
			<formula>A&lt;&gt; (slot_no[1]!=slot_no[3] and slot_no[1]&gt;=0 and slot_no[3]&gt;=0)</formula>
			<comment>Eventually node 1 and 3 allocate different slots? Answer: NO (strange)</comment>
		</query>
		<query>
			<formula>A&lt;&gt; (slot_no[2]!=slot_no[3] and slot_no[2]&gt;=0 and slot_no[3]&gt;=0)</formula>
			<comment>Eventually node 2 and 3 allocate different slots? Answer: NO (maybe OK)</comment>
		</query>
		<query>
			<formula>A&lt;&gt; forall(i: nodeid_t) forall(j: nodeid_t) (i==j || (slot_no[i]&gt;=0 &amp;&amp; slot_no[j]&gt;=0 &amp;&amp; slot_no[i]!=slot_no[j]))</formula>
			<comment>Eventually all nodes allocate different slots? Answer: NO (strange)</comment>
		</query>
		<query>
			<formula>sup: Node(0).detected, Node(1).detected, Node(2).detected, Node(3).detected</formula>
			<comment></comment>
		</query>
		<query>
			<formula>E&lt;&gt; exists(i:nodeid_t) Node(i).detected&gt;=0</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Pr[&lt;=100] (&lt;&gt; exists(i:nodeid_t) Node(i).detected&gt;=0)</formula>
			<comment></comment>
		</query>
	</queries>
</nta>
