<?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>// Place global declarations here.
clock gc;
// maximum and minimum delays
// fast
const int rc_fast_max = 85;
const int rc_fast_min = 76;
//slow
const int rc_slow_max = 167;
const int rc_slow_min = 159;
// delay caused by the wire length
const int delay = 30;
const int delay_min = 5;

// probability of choosing fast or slow
const int fast = 20;
const int slow = 80;
const int FAST[2]={99,1};
const int SLOW[2]={1,99};

// clocks for node1 and node2
clock tx[2];

// clocks for wire12 and wire21
clock t1[2];
clock t2[2];

//
broadcast chan snd_idle[2];
broadcast chan snd_req[2];
broadcast chan snd_ack[2];
broadcast chan rec_idle[2];
broadcast chan rec_req[2];
broadcast chan rec_ack[2];

// this boolean variable is used for shake-hand
bool rec_idle_s[2];
bool rec_req_s[2];
bool rec_ack_s[2];
/*
broadcast chan rec_idle12;
broadcast chan rec_req12;
broadcast chan rec_ack12;

broadcast chan rec_idle21;
broadcast chan rec_req21;
broadcast chan rec_ack21;
*/</declaration>
	<template>
		<name x="5" y="5">Node</name>
		<parameter>int id</parameter>
		<declaration>// Place local declarations here.
int s = 0;

int getID(int x)
{
    return 1 - x;
}</declaration>
		<location id="id0" x="624" y="8">
			<name x="640" y="-16">s8</name>
			<label kind="invariant" x="664" y="-16">s == 8 &amp;&amp;
tx[id] &lt;= rc_slow_max</label>
		</location>
		<location id="id1" x="392" y="8">
			<name x="360" y="8">s6</name>
			<label kind="invariant" x="336" y="24">s == 6</label>
		</location>
		<location id="id2" x="-374" y="-95">
			<name x="-406" y="-119">s7</name>
			<label kind="invariant" x="-520" y="-88">s == 7 &amp;&amp;
tx[id] &lt;= rc_slow_max</label>
		</location>
		<location id="id3" x="160" y="160">
			<name x="176" y="160">s5</name>
			<label kind="invariant" x="152" y="176">s == 5 &amp;&amp;
tx[id] &lt;= rc_slow_max</label>
		</location>
		<location id="id4" x="160" y="-96">
			<name x="128" y="-128">s4</name>
			<label kind="invariant" x="152" y="-144">s == 4 &amp;&amp;
tx[id] &lt;= rc_fast_max</label>
		</location>
		<location id="id5" x="-200" y="160">
			<name x="-224" y="128">s3</name>
			<label kind="invariant" x="-304" y="160">s == 3 &amp;&amp;
tx[id] &lt;= rc_slow_max</label>
		</location>
		<location id="id6" x="-200" y="-96">
			<name x="-216" y="-128">s2</name>
			<label kind="invariant" x="-192" y="-144">s == 2 &amp;&amp;
tx[id] &lt;= rc_fast_max</label>
		</location>
		<location id="id7" x="-64" y="96">
			<name x="-74" y="66">s1</name>
			<label kind="invariant" x="-80" y="104">s == 1</label>
		</location>
		<location id="id8" x="-64" y="8">
			<name x="-64" y="-24">s0</name>
			<label kind="invariant" x="-48" y="8">s == 0</label>
			<urgent/>
		</location>
		<branchpoint id="id9" x="160" y="96">
		</branchpoint>
		<branchpoint id="id10" x="-200" y="8">
		</branchpoint>
		<init ref="id8"/>
		<transition>
			<source ref="id0"/>
			<target ref="id0"/>
			<label kind="guard" x="584" y="80">tx[id] &lt; rc_slow_min</label>
			<nail x="656" y="80"/>
			<nail x="592" y="80"/>
		</transition>
		<transition>
			<source ref="id2"/>
			<target ref="id2"/>
			<label kind="guard" x="-584" y="-128">tx[id] &lt; rc_slow_min</label>
			<nail x="-448" y="-128"/>
			<nail x="-448" y="-72"/>
		</transition>
		<transition>
			<source ref="id3"/>
			<target ref="id3"/>
			<label kind="guard" x="96" y="264">tx[id] &lt;= rc_slow_min</label>
			<nail x="216" y="264"/>
			<nail x="104" y="264"/>
		</transition>
		<transition>
			<source ref="id5"/>
			<target ref="id5"/>
			<label kind="guard" x="-272" y="256">tx[id] &lt; rc_slow_min</label>
			<nail x="-160" y="256"/>
			<nail x="-256" y="256"/>
		</transition>
		<transition>
			<source ref="id3"/>
			<target ref="id1"/>
			<label kind="guard" x="408" y="104">tx[id] &gt;= rc_slow_min</label>
			<label kind="synchronisation" x="408" y="120">snd_req[id]!</label>
			<label kind="assignment" x="408" y="144">s := 6,
tx[id] := 0,
rec_ack_s[getID(id)] := true,
rec_req_s[getID(id)] := true</label>
			<nail x="392" y="160"/>
		</transition>
		<transition>
			<source ref="id4"/>
			<target ref="id1"/>
			<label kind="guard" x="352" y="-136">tx[id] &gt;= rc_fast_min</label>
			<label kind="synchronisation" x="352" y="-120">snd_req[id]!</label>
			<label kind="assignment" x="400" y="-104">s := 6,
tx[id] := 0,
rec_ack_s[getID(id)] := true,
rec_req_s[getID(id)] := true</label>
			<nail x="392" y="-96"/>
		</transition>
		<transition>
			<source ref="id3"/>
			<target ref="id5"/>
			<label kind="synchronisation" x="-104" y="200">rec_req[getID(id)]?</label>
			<label kind="assignment" x="-104" y="216">s := 3,
rec_idle_s[getID(id)] := true</label>
			<nail x="104" y="200"/>
			<nail x="-144" y="200"/>
		</transition>
		<transition>
			<source ref="id1"/>
			<target ref="id0"/>
			<label kind="synchronisation" x="424" y="-16">rec_ack[getID(id)]?</label>
			<label kind="assignment" x="424" y="8">s := 8,
rec_req_s[getID(id)] := false</label>
		</transition>
		<transition>
			<source ref="id1"/>
			<target ref="id8"/>
			<label kind="synchronisation" x="32" y="8">rec_req[getID(id)]?</label>
			<label kind="assignment" x="176" y="8">s := 0,
rec_idle_s[id] := true,
rec_ack_s[getID(id)] := false</label>
		</transition>
		<transition>
			<source ref="id0"/>
			<target ref="id0"/>
			<label kind="guard" x="592" y="-104">tx[id] &gt;= rc_slow_min</label>
			<label kind="assignment" x="592" y="-88">tx[id] := 0</label>
			<nail x="648" y="-64"/>
			<nail x="584" y="-64"/>
		</transition>
		<transition>
			<source ref="id2"/>
			<target ref="id2"/>
			<label kind="guard" x="-438" y="-191">tx[id] &gt;= rc_slow_min</label>
			<label kind="assignment" x="-438" y="-175">tx[id] := 0</label>
			<nail x="-342" y="-159"/>
			<nail x="-406" y="-159"/>
		</transition>
		<transition>
			<source ref="id4"/>
			<target ref="id6"/>
			<label kind="synchronisation" x="-40" y="-64">rec_req[getID(id)]?</label>
			<label kind="assignment" x="-40" y="-48">s := 2,
rec_idle_s[getID(id)] := true</label>
			<nail x="120" y="-64"/>
			<nail x="-160" y="-64"/>
		</transition>
		<transition>
			<source ref="id5"/>
			<target ref="id3"/>
			<label kind="synchronisation" x="-160" y="136">rec_idle[getID(id)]?</label>
			<label kind="assignment" x="-32" y="120">s := 5,
rec_req_s[getID(id)] := true</label>
		</transition>
		<transition>
			<source ref="id5"/>
			<target ref="id2"/>
			<label kind="guard" x="-488" y="32">tx[id] &gt;= rc_slow_min</label>
			<label kind="synchronisation" x="-488" y="48">snd_ack[id]!</label>
			<label kind="assignment" x="-488" y="64">tx[id] := 0,
s := 7,
rec_idle_s[getID(id)] := false</label>
			<nail x="-376" y="160"/>
		</transition>
		<transition>
			<source ref="id6"/>
			<target ref="id2"/>
			<label kind="guard" x="-296" y="-168">tx[id] &gt;= rc_fast_min</label>
			<label kind="synchronisation" x="-296" y="-152">snd_ack[id]!</label>
			<label kind="assignment" x="-344" y="-152">s := 7,
tx[id] := 0,
rec_idle_s[getID(id)] := false</label>
		</transition>
		<transition>
			<source ref="id6"/>
			<target ref="id4"/>
			<label kind="synchronisation" x="-48" y="-152">rec_idle[getID(id)]?</label>
			<label kind="assignment" x="-48" y="-136">s := 4,
rec_req_s[getID(id)] := true</label>
		</transition>
		<transition>
			<source ref="id7"/>
			<target ref="id8"/>
			<label kind="synchronisation" x="-32" y="32">rec_req[id]?</label>
			<label kind="assignment" x="-32" y="48">s := 0,
rec_idle_s[id] := true</label>
			<nail x="-32" y="56"/>
		</transition>
		<transition>
			<source ref="id9"/>
			<target ref="id3"/>
			<label kind="assignment" x="176" y="104">s := 5,
tx[id] := 0,
rec_req_s[getID(id)] := true</label>
			<label kind="probability" x="176" y="88">SLOW[id]</label>
		</transition>
		<transition>
			<source ref="id9"/>
			<target ref="id4"/>
			<label kind="assignment" x="168" y="-64">s := 4,
tx[id] := 0,
rec_req_s[getID(id)] := true</label>
			<label kind="probability" x="168" y="-80">FAST[id]</label>
		</transition>
		<transition>
			<source ref="id7"/>
			<target ref="id9"/>
			<label kind="synchronisation" x="16" y="72">snd_idle[id]!</label>
			<label kind="assignment" x="-32" y="96">rec_req_s[getID(id)] := false</label>
		</transition>
		<transition>
			<source ref="id8"/>
			<target ref="id7"/>
			<label kind="synchronisation" x="-192" y="16">rec_idle[id]?</label>
			<label kind="assignment" x="-192" y="32">s := 1,
rec_req_s[id] := true,
rec_idle_s[getID(id)] := false</label>
			<nail x="-96" y="56"/>
		</transition>
		<transition>
			<source ref="id10"/>
			<target ref="id5"/>
			<label kind="assignment" x="-328" y="56">s:=3,
tx[id]:=0,
rec_idle_s[getID(id)] := true</label>
			<label kind="probability" x="-320" y="40">SLOW[id] //slow</label>
		</transition>
		<transition>
			<source ref="id10"/>
			<target ref="id6"/>
			<label kind="assignment" x="-328" y="-64">s := 2,
tx[id] := 0,
rec_idle_s[getID(id)] := true</label>
			<label kind="probability" x="-328" y="-80">FAST[id] //fast</label>
		</transition>
		<transition>
			<source ref="id8"/>
			<target ref="id10"/>
			<label kind="synchronisation" x="-152" y="-32">snd_idle[id]!</label>
		</transition>
	</template>
	<template>
		<name>Wire</name>
		<parameter>int id</parameter>
		<declaration>int w;</declaration>
		<location id="id11" x="400" y="288">
			<name x="390" y="258">w9</name>
			<label kind="invariant" x="360" y="296">w == 9 &amp;&amp;
t1[id] &lt;= delay</label>
		</location>
		<location id="id12" x="-424" y="-96">
			<name x="-440" y="-128">w6</name>
			<label kind="invariant" x="-528" y="-80">w == 6 &amp;&amp;
t1[id] &lt;= delay</label>
		</location>
		<location id="id13" x="424" y="-432">
			<name x="440" y="-448">w7</name>
			<label kind="invariant" x="440" y="-432">w == 7 &amp;&amp; t1[id] &lt;= delay</label>
		</location>
		<location id="id14" x="224" y="152">
			<name x="240" y="120">w4</name>
			<label kind="invariant" x="240" y="136">w == 4 &amp;&amp;
t1[id] &lt;= delay</label>
		</location>
		<location id="id15" x="-312" y="-88">
			<name x="-304" y="-120">w8</name>
			<label kind="invariant" x="-296" y="-96">w == 8 &amp;&amp;
t1[id] &lt;= delay</label>
		</location>
		<location id="id16" x="224" y="-280">
			<name x="214" y="-310">w2</name>
			<label kind="invariant" x="240" y="-296">w == 2 &amp;&amp;
t1[id] &lt;= delay</label>
		</location>
		<location id="id17" x="-96" y="152">
			<name x="-112" y="120">w5</name>
			<label kind="invariant" x="-192" y="152">w == 5 &amp;&amp; 
t2[id] &lt;= delay</label>
		</location>
		<location id="id18" x="224" y="-56">
			<name x="190" y="-81">w3</name>
			<label kind="invariant" x="128" y="-112">w == 3 &amp;&amp;
t2[id] &lt;= delay</label>
		</location>
		<location id="id19" x="-96" y="-280">
			<name x="-72" y="-304">w1</name>
			<label kind="invariant" x="-200" y="-320">w == 1 &amp;&amp;
t1[id] &lt;= delay</label>
		</location>
		<location id="id20" x="-96" y="-56">
			<name x="-128" y="-80">w0</name>
			<label kind="invariant" x="-152" y="-64">w == 0</label>
		</location>
		<init ref="id20"/>
		<transition>
			<source ref="id11"/>
			<target ref="id18"/>
			<label kind="guard" x="408" y="48">rec_idle_s[id] &amp;&amp;
t1[id] &gt;= delay_min</label>
			<label kind="synchronisation" x="408" y="32">rec_idle[id]!</label>
			<label kind="assignment" x="408" y="80">w := 3,
rec_idle_s[id] := false</label>
			<nail x="400" y="264"/>
			<nail x="400" y="24"/>
		</transition>
		<transition>
			<source ref="id15"/>
			<target ref="id15"/>
			<label kind="synchronisation" x="-408" y="-144">snd_idle[id]?</label>
			<nail x="-344" y="-120"/>
			<nail x="-344" y="-48"/>
		</transition>
		<transition>
			<source ref="id15"/>
			<target ref="id17"/>
			<label kind="guard" x="-400" y="-24">rec_req_s[id] &amp;&amp;
t1[id] &gt;= delay_min</label>
			<label kind="synchronisation" x="-400" y="8">rec_req[id]!</label>
			<label kind="assignment" x="-400" y="24">w := 5,
rec_req_s[id] := false</label>
			<nail x="-312" y="80"/>
		</transition>
		<transition>
			<source ref="id13"/>
			<target ref="id19"/>
			<label kind="guard" x="104" y="-504">rec_ack_s[id] &amp;&amp; t1[id] &gt;= delay_min</label>
			<label kind="synchronisation" x="104" y="-488">rec_ack[id]!</label>
			<label kind="assignment" x="104" y="-472">w := 1,
rec_ack_s[id] := false</label>
			<nail x="112" y="-432"/>
		</transition>
		<transition>
			<source ref="id13"/>
			<target ref="id13"/>
			<label kind="synchronisation" x="384" y="-496">snd_req[id]?</label>
			<nail x="392" y="-472"/>
			<nail x="456" y="-472"/>
		</transition>
		<transition>
			<source ref="id12"/>
			<target ref="id19"/>
			<label kind="guard" x="-560" y="-328">rec_idle_s[id] &amp;&amp;
t1[id] &gt;= delay_min</label>
			<label kind="synchronisation" x="-560" y="-296">rec_idle[id]!</label>
			<label kind="assignment" x="-560" y="-280">w := 1,
rec_idle_s[id] := false</label>
			<nail x="-424" y="-280"/>
		</transition>
		<transition>
			<source ref="id12"/>
			<target ref="id12"/>
			<label kind="synchronisation" x="-568" y="-112">snd_req[id]?</label>
			<nail x="-488" y="-120"/>
			<nail x="-488" y="-80"/>
		</transition>
		<transition>
			<source ref="id17"/>
			<target ref="id11"/>
			<label kind="synchronisation" x="64" y="248">snd_ack[id]?</label>
			<label kind="assignment" x="64" y="264">w := 9</label>
			<nail x="64" y="288"/>
		</transition>
		<transition>
			<source ref="id17"/>
			<target ref="id12"/>
			<label kind="synchronisation" x="-504" y="104">snd_req[id]?</label>
			<label kind="assignment" x="-504" y="120">w := 6</label>
			<nail x="-424" y="152"/>
		</transition>
		<transition>
			<source ref="id17"/>
			<target ref="id20"/>
			<label kind="guard" x="-64" y="-8">rec_idle_s[id] &amp;&amp;
t2[id] &gt;= delay_min</label>
			<label kind="synchronisation" x="-64" y="32">rec_idle[id]!</label>
			<label kind="assignment" x="-64" y="48">w := 0,
t1[id] := 0,
t2[id] := 0,
rec_idle_s[id] := false</label>
			<nail x="-72" y="104"/>
			<nail x="-72" y="-8"/>
		</transition>
		<transition>
			<source ref="id17"/>
			<target ref="id17"/>
			<label kind="synchronisation" x="-128" y="216">snd_idle[id]?</label>
			<nail x="-72" y="192"/>
			<nail x="-96" y="224"/>
		</transition>
		<transition>
			<source ref="id14"/>
			<target ref="id17"/>
			<label kind="guard" x="-32" y="128">rec_ack_s[id] &amp;&amp; t1[id] &gt;= delay_min</label>
			<label kind="synchronisation" x="-32" y="152">rec_ack[id]!</label>
			<label kind="assignment" x="-32" y="168">w := 5,
rec_ack_s[id] := false</label>
		</transition>
		<transition>
			<source ref="id14"/>
			<target ref="id14"/>
			<label kind="synchronisation" x="200" y="200">snd_idle[id]?</label>
			<nail x="248" y="200"/>
			<nail x="192" y="200"/>
		</transition>
		<transition>
			<source ref="id18"/>
			<target ref="id13"/>
			<label kind="synchronisation" x="440" y="-288">snd_req[id]?</label>
			<label kind="assignment" x="440" y="-272">w := 7,
t2[id] := 0</label>
			<nail x="424" y="-200"/>
		</transition>
		<transition>
			<source ref="id18"/>
			<target ref="id14"/>
			<label kind="synchronisation" x="232" y="40">snd_idle[id]?</label>
			<label kind="assignment" x="232" y="56">w := 4,
t2[id] := 0</label>
		</transition>
		<transition>
			<source ref="id18"/>
			<target ref="id20"/>
			<label kind="guard" x="-48" y="-48">rec_ack_s[id] &amp;&amp; t2[id] &gt;= delay_min</label>
			<label kind="synchronisation" x="72" y="-24">rec_ack[id]!</label>
			<label kind="assignment" x="72" y="-8">w := 0,
t1[id] := 0,
t2[id] := 0,
rec_ack_s[id] := false</label>
			<nail x="168" y="-24"/>
			<nail x="-48" y="-24"/>
		</transition>
		<transition>
			<source ref="id18"/>
			<target ref="id18"/>
			<label kind="synchronisation" x="310" y="-65">snd_ack[id]?</label>
			<nail x="302" y="-81"/>
			<nail x="302" y="-41"/>
		</transition>
		<transition>
			<source ref="id16"/>
			<target ref="id18"/>
			<label kind="guard" x="232" y="-240">rec_req_s[id] &amp;&amp;
t1[id] &gt;= delay_min</label>
			<label kind="synchronisation" x="232" y="-208">rec_req[id]!</label>
			<label kind="assignment" x="232" y="-192">w := 3,
rec_req_s[id] := false</label>
		</transition>
		<transition>
			<source ref="id16"/>
			<target ref="id16"/>
			<label kind="synchronisation" x="200" y="-352">snd_ack[id]?</label>
			<nail x="264" y="-328"/>
			<nail x="184" y="-328"/>
		</transition>
		<transition>
			<source ref="id19"/>
			<target ref="id15"/>
			<label kind="synchronisation" x="-368" y="-232">snd_idle[id]?</label>
			<label kind="assignment" x="-368" y="-216">w := 8</label>
			<nail x="-312" y="-200"/>
		</transition>
		<transition>
			<source ref="id19"/>
			<target ref="id16"/>
			<label kind="synchronisation" x="32" y="-320">snd_ack[id]?</label>
			<label kind="assignment" x="32" y="-304">w := 2</label>
		</transition>
		<transition>
			<source ref="id19"/>
			<target ref="id20"/>
			<label kind="guard" x="-232" y="-232">rec_req_s[id] &amp;&amp;
t1[id] &gt;= delay_min</label>
			<label kind="synchronisation" x="-232" y="-200">rec_req[id]!</label>
			<label kind="assignment" x="-232" y="-184">w := 0,
t1[id] := 0,
t2[id] := 0,
rec_req_s[id] := false</label>
		</transition>
		<transition>
			<source ref="id19"/>
			<target ref="id19"/>
			<label kind="synchronisation" x="-120" y="-376">snd_req[id]?</label>
			<nail x="-120" y="-352"/>
			<nail x="-64" y="-352"/>
		</transition>
		<transition>
			<source ref="id20"/>
			<target ref="id17"/>
			<label kind="synchronisation" x="-224" y="8">snd_idle[id]?</label>
			<label kind="assignment" x="-224" y="24">w := 5,
t1[id] := 0,
t2[id] := 0</label>
			<nail x="-144" y="-8"/>
			<nail x="-144" y="96"/>
		</transition>
		<transition>
			<source ref="id20"/>
			<target ref="id18"/>
			<label kind="synchronisation" x="0" y="-128">snd_ack[id]?</label>
			<label kind="assignment" x="0" y="-112">w := 3,
t1[id] := 0,
t2[id] := 0</label>
		</transition>
		<transition>
			<source ref="id20"/>
			<target ref="id19"/>
			<label kind="synchronisation" x="-56" y="-200">snd_req[id]?</label>
			<label kind="assignment" x="-56" y="-184">w := 1,
t1[id] := 0,
t2[id] := 0</label>
			<nail x="-64" y="-96"/>
			<nail x="-64" y="-232"/>
		</transition>
	</template>
	<system>// Place template instantiations here.
node1 = Node(0);
node2 = Node(1);
//node2 = Node(idx, snd_idle21, rec_idle12, snd_req21, rec_req12, snd_ack21, rec_ack12);
wire12 = Wire(0);
wire21 = Wire(1);
//wire21 = Wire(tz1, tz2, snd_idle21, rec_idle21, snd_req21, rec_req21, snd_ack21, rec_ack21);
// List one or more processes to be composed into a system.
system node1, node2, wire12, wire21;</system>
	<queries>
		<query>
			<formula>E&lt;&gt; ( node1.s == 7 &amp;&amp; node2.s == 8 ) 
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>E&lt;&gt; (!( node1.s == 8 &amp;&amp; node2.s == 7 || node1.s == 7 &amp;&amp; node2.s == 8) &amp;&amp; gc &gt;= 1500)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>A&lt;&gt; (( node1.s == 8 &amp;&amp; node2.s == 7 || node1.s == 7 &amp;&amp; node2.s == 8) || gc &lt; 100)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;= 100] (&lt;&gt; node1.s == 7 &amp;&amp; node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;= 150] (&lt;&gt; node1.s == 7 &amp;&amp; node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;= 200] (&lt;&gt; node1.s == 7 &amp;&amp; node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;= 250] (&lt;&gt; node1.s == 7 &amp;&amp; node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;= 300] (&lt;&gt; node1.s == 7 &amp;&amp; node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;= 400] (&lt;&gt; node1.s == 7 &amp;&amp; node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;= 500] (&lt;&gt; node1.s == 7 &amp;&amp; node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;= 600] (&lt;&gt; node1.s == 7 &amp;&amp; node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;= 700] (&lt;&gt; node1.s == 7 &amp;&amp; node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;= 800] (&lt;&gt; node1.s == 7 &amp;&amp; node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[ &lt;= 900] (&lt;&gt; node1.s == 7 &amp;&amp; node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[ &lt;= 1000] (&lt;&gt; node1.s == 7 &amp;&amp; node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[ &lt;= 1000] (&lt;&gt; node1.s == 8 &amp;&amp; node2.s == 7 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[ &lt;= 1500] (&lt;&gt; node1.s == 7 &amp;&amp; node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[ &lt;= 1500] (&lt;&gt; node1.s == 8 &amp;&amp; node2.s == 7 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[ &lt;= 1500] (&lt;&gt; node1.s == 8 &amp;&amp; node2.s == 7 || node1.s == 7 &amp;&amp; node2.s == 8)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[ &lt;= 1500] (&lt;&gt; node1.s == 8 &amp;&amp; node2.s == 7 ) &gt;= Pr[ &lt;= 1500] (&lt;&gt; node1.s == 7 &amp;&amp; node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[ &lt;= 1500] (&lt;&gt; node1.s == 7 &amp;&amp; node2.s == 8 ) &gt;= Pr[ &lt;= 1500] (&lt;&gt; node1.s == 8 &amp;&amp; node2.s == 7 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[ &lt;= 1500] (&lt;&gt; node1.s == 8 || node1.s == 7 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[ &lt;= 1500] (&lt;&gt; node2.s == 7 || node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[ &lt;= 1500] (&lt;&gt; node1.s == 7 || node1.s == 8 ) &gt;= Pr[ &lt;= 1500] (&lt;&gt; node2.s == 7 || node2.s == 8 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[ &lt;= 1500] (&lt;&gt; node1.s == 7 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula> Pr[ &lt;= 1500] (&lt;&gt; node2.s == 7 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[ &lt;= 1500] (&lt;&gt; node2.s == 7 ) &gt;= Pr[ &lt;= 1500] (&lt;&gt; node1.s == 7 )
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>A[] not deadlock
			</formula>
			<comment>node 2 is the root and node 1 is the child
			</comment>
		</query>
	</queries>
</nta>
