<?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 time;
clock energy;
// to run the sender and freequecny
broadcast chan run_sender;
bool run_sender_s = true;
broadcast chan run_frequency;
bool run_frequency_s = true;

// to suspend the sender and freequecny
broadcast chan suspend_sender;
bool suspend_sender_s = false;
broadcast chan suspend_frequency;
bool suspend_frequency_s = false;

//broadcast chan time;
broadcast chan reply;

/*
declaration for frequency changes
*/
const int z_max = 4096;
typedef int[0, 32] Phase_t;
Phase_t phase;

/*
declarions for receiver
*/ 

typedef int[0, 32] Freq_t;
Freq_t freq; // frequency scanning on (0 = not scanning)
typedef int[0, 3] R_t;
R_t r;  // locate state ( 0 = sleep, 1 = scan, 2 = reply, 3 = radom delay)


/*
declarations for sender
*/
const int mrep = 128; // maximum number of replies
const int mrec = 128; // number of repetitions of each frequency sequence

typedef int[0,2] S_t;
S_t s = 0; // local state, 1 = sending, 2 = listenling

typedef int[1, 16] F_t;
F_t f;  // current frequency modulo 16

typedef int[0, 1] O_t;
O_t o; // calculates current frequency( actural frequence = f + o * 16)

typedef int[1, 16] C_t;
C_t c;  // used to work out frequency sequence

typedef int[1, mrec] Rep_t;
Rep_t rep; // number of repctitions of current sequence

typedef int[0, mrep] Rec_t;
Rec_t rec; // number of replies received
</declaration>
	<template>
		<name x="5" y="5">Sender</name>
		<declaration>// Place local declarations here.


clock t;

bool hear_reply()
{
    return freq == f + 16 * o;
}

bool c_odd()
{
    return c % 2 == 1;
}

bool f_odd()
{
    return f % 2 == 1;
}

void update_2_1()
{
    if (rep &lt; mrep)
    {
        o := (f == c)? o: 1 - o;        
    }
    else if (rep == mrep)
    {
        o := (c_odd())? o: 1 - o;
    }
    c := (c == 16)? 1: c + 1;
    f := 1;
}</declaration>
		<location id="id0" x="-704" y="0">
			<name x="-712" y="8">s_sleep_wait</name>
			<label kind="invariant" x="-760" y="8">s == 0</label>
		</location>
		<location id="id1" x="-704" y="-424">
			<name x="-744" y="-456">s2_c</name>
			<committed/>
		</location>
		<location id="id2" x="-544" y="-192">
			<name x="-560" y="-224">s1_c</name>
			<committed/>
		</location>
		<location id="id3" x="-328" y="-192">
			<name x="-320" y="-224">s2</name>
			<label kind="invariant" x="-320" y="-184">t &lt;= 1 &amp;&amp; s == 2</label>
		</location>
		<location id="id4" x="-704" y="-192">
			<name x="-728" y="-232">s1</name>
			<label kind="invariant" x="-864" y="-224">s == 1 &amp;&amp; t &lt;= 1</label>
		</location>
		<init ref="id0"/>
		<transition>
			<source ref="id4"/>
			<target ref="id0"/>
			<label kind="synchronisation" x="-696" y="-136">suspend_sender?</label>
			<label kind="assignment" x="-696" y="-120">t := 0,
s := 0,
run_sender_s := true</label>
		</transition>
		<transition>
			<source ref="id3"/>
			<target ref="id0"/>
			<label kind="synchronisation" x="-544" y="0">suspend_sender?</label>
			<label kind="assignment" x="-544" y="16">t := 0,
s := 0,
run_sender_s := true</label>
			<nail x="-328" y="0"/>
		</transition>
		<transition>
			<source ref="id0"/>
			<target ref="id4"/>
			<label kind="synchronisation" x="-912" y="-80">run_sender?</label>
			<label kind="assignment" x="-912" y="-64">t := 0,
s := 1,
suspend_sender_s := true</label>
			<nail x="-776" y="-48"/>
			<nail x="-776" y="-128"/>
		</transition>
		<transition>
			<source ref="id3"/>
			<target ref="id3"/>
			<label kind="synchronisation" x="-264" y="-248">reply?</label>
			<label kind="assignment" x="-264" y="-232">rec := (hear_reply() &amp;&amp; rec &lt; mrec)? rec + 1: rec,
suspend_sender_s := true</label>
			<nail x="-272" y="-224"/>
			<nail x="-272" y="-192"/>
		</transition>
		<transition>
			<source ref="id1"/>
			<target ref="id4"/>
			<label kind="guard" x="-1088" y="-360">!f_odd() &amp;&amp; f != 16</label>
			<label kind="assignment" x="-1088" y="-336">s := 1,
f := f + 1,
o := (f == c)? 1 - o: o,
rep := (rep == mrep)? 1: rep + 1,
suspend_sender_s := true</label>
			<nail x="-880" y="-424"/>
			<nail x="-880" y="-192"/>
		</transition>
		<transition>
			<source ref="id1"/>
			<target ref="id4"/>
			<label kind="guard" x="-856" y="-360">f == 16</label>
			<label kind="assignment" x="-856" y="-344">s := 1,
update_2_1(),
suspend_sender_s := true</label>
		</transition>
		<transition>
			<source ref="id1"/>
			<target ref="id3"/>
			<label kind="guard" x="-320" y="-416">f_odd()</label>
			<label kind="assignment" x="-320" y="-400">f := f + 1,
o := (f == c)? 1 - o: o,
suspend_sender_s := true</label>
			<nail x="-328" y="-424"/>
		</transition>
		<transition>
			<source ref="id3"/>
			<target ref="id1"/>
			<label kind="guard" x="-552" y="-344">t == 1</label>
			<label kind="assignment" x="-552" y="-328">t := 0</label>
			<nail x="-472" y="-328"/>
		</transition>
		<transition>
			<source ref="id2"/>
			<target ref="id3"/>
			<label kind="guard" x="-504" y="-272">f_odd()</label>
			<label kind="assignment" x="-504" y="-256">t := 0,
f := f + 1,
s := 2,
suspend_sender_s := true</label>
		</transition>
		<transition>
			<source ref="id2"/>
			<target ref="id4"/>
			<label kind="guard" x="-672" y="-304">!f_odd()</label>
			<label kind="assignment" x="-672" y="-288">t := 0,
f := f - 1,
suspend_sender_s := true</label>
			<nail x="-584" y="-216"/>
			<nail x="-672" y="-216"/>
		</transition>
		<transition>
			<source ref="id4"/>
			<target ref="id2"/>
			<label kind="guard" x="-672" y="-192">t == 1</label>
			<label kind="assignment" x="-672" y="-168">o := (f == c - 1)? 1 - o: o</label>
			<nail x="-672" y="-168"/>
			<nail x="-584" y="-168"/>
		</transition>
	</template>
	<template>
		<name>Receiver</name>
		<declaration>clock y;

// the time slot is 0.3125 ms
// so the sleep state is 2012 time slots, scan is 36 time slots, respond is 2 time slots
// it takes too many time, so I change the constant
const int T_sleep = 2012;
const int T_scan = 36;
const int T_resp = 2;
const int T_wait = 2;
const int N_wait = 127;

bool hear()
{
    return (s == 1) &amp;&amp; (freq == f + o * 16);
}</declaration>
		<location id="id5" x="-64" y="128">
			<name x="-88" y="136">wait_3</name>
			<label kind="invariant" x="-74" y="143">energy' == 0</label>
			<committed/>
		</location>
		<location id="id6" x="160" y="48">
			<name x="176" y="32">wait_2</name>
			<label kind="invariant" x="150" y="63">energy' == 0</label>
			<committed/>
		</location>
		<location id="id7" x="160" y="128">
			<name x="144" y="136">wait_1</name>
			<label kind="invariant" x="150" y="143">energy' == 0</label>
			<committed/>
		</location>
		<location id="id8" x="-296" y="-184">
			<name x="-306" y="-214">scan_2</name>
			<label kind="invariant" x="-306" y="-169">energy' == 0</label>
			<committed/>
		</location>
		<location id="id9" x="-296" y="-272">
			<name x="-306" y="-302">scan_3</name>
			<label kind="invariant" x="-306" y="-257">energy' == 0</label>
			<committed/>
		</location>
		<location id="id10" x="-64" y="-184">
			<name x="-48" y="-208">scan_1</name>
			<label kind="invariant" x="-74" y="-169">energy' == 0</label>
			<committed/>
		</location>
		<location id="id11" x="-288" y="72">
			<name x="-312" y="40">sleep_3</name>
			<label kind="invariant" x="-298" y="87">energy' == 0</label>
			<committed/>
		</location>
		<location id="id12" x="-280" y="-40">
			<name x="-290" y="-70">sleep_2</name>
			<label kind="invariant" x="-290" y="-25">energy' == 0</label>
			<committed/>
		</location>
		<location id="id13" x="-456" y="-40">
			<name x="-472" y="-72">sleep_1</name>
			<label kind="invariant" x="-512" y="-24">energy' == 0</label>
			<committed/>
		</location>
		<location id="id14" x="384" y="128">
			<name x="376" y="144">wait</name>
			<label kind="invariant" x="400" y="120">energy'==1 &amp;&amp; r == 3 &amp;&amp; y &lt;= N_wait * T_wait</label>
		</location>
		<location id="id15" x="384" y="-40">
			<name x="368" y="-72">Reply</name>
			<label kind="invariant" x="400" y="-48">energy'==3 &amp;&amp; r == 2 &amp;&amp; y &lt;= T_resp</label>
		</location>
		<location id="id16" x="-64" y="-40">
			<name x="-104" y="-72">scan</name>
			<label kind="invariant" x="-56" y="-64">energy'==2 &amp;&amp; r == 1 &amp;&amp; y &lt;= T_scan</label>
		</location>
		<location id="id17" x="-520" y="-184">
			<name x="-560" y="-216">sleep</name>
			<label kind="invariant" x="-616" y="-200">energy' == 0 &amp;&amp; r == 0 &amp;&amp;
y &lt;= T_sleep</label>
		</location>
		<init ref="id17"/>
		<transition>
			<source ref="id5"/>
			<target ref="id16"/>
			<label kind="guard" x="-56" y="40">s == 0 || suspend_frequency_s</label>
			<label kind="synchronisation" x="-56" y="56">suspend_frequency!</label>
			<label kind="assignment" x="-56" y="72">suspend_sender_s := false</label>
		</transition>
		<transition>
			<source ref="id6"/>
			<target ref="id16"/>
			<label kind="guard" x="96" y="-32">s == 0 || suspend_sender_s</label>
			<label kind="synchronisation" x="96" y="-16">suspend_sender!</label>
			<label kind="assignment" x="96" y="0">suspend_sender_s := false</label>
		</transition>
		<transition>
			<source ref="id7"/>
			<target ref="id6"/>
			<label kind="guard" x="168" y="64">s == 0 || suspend_frequency_s</label>
			<label kind="synchronisation" x="168" y="80">suspend_frequency!</label>
			<label kind="assignment" x="168" y="96">suspend_frequency_s := false</label>
		</transition>
		<transition>
			<source ref="id7"/>
			<target ref="id5"/>
			<label kind="guard" x="-32" y="128">s == 0 || suspend_sender_s</label>
			<label kind="synchronisation" x="-32" y="144">suspend_sender!</label>
			<label kind="assignment" x="-32" y="160">suspend_sender_s := false</label>
		</transition>
		<transition>
			<source ref="id10"/>
			<target ref="id9"/>
			<label kind="guard" x="-240" y="-328">s == 0 || suspend_sender_s</label>
			<label kind="synchronisation" x="-240" y="-312">suspend_sender!</label>
			<label kind="assignment" x="-240" y="-296">suspend_sender_s := false</label>
			<nail x="-64" y="-272"/>
		</transition>
		<transition>
			<source ref="id10"/>
			<target ref="id8"/>
			<label kind="guard" x="-272" y="-184">s == 0 || suspend_frequency_s</label>
			<label kind="synchronisation" x="-272" y="-168">suspend_frequency!</label>
			<label kind="assignment" x="-272" y="-152">suspend_frequency_s := false</label>
		</transition>
		<transition>
			<source ref="id8"/>
			<target ref="id17"/>
			<label kind="guard" x="-496" y="-184">s == 0 || suspend_sender_s</label>
			<label kind="synchronisation" x="-496" y="-168">suspend_sender!</label>
			<label kind="assignment" x="-496" y="-152">suspend_sender_s := false</label>
		</transition>
		<transition>
			<source ref="id9"/>
			<target ref="id17"/>
			<label kind="guard" x="-504" y="-328">s == 0 || suspend_frequency_s</label>
			<label kind="synchronisation" x="-504" y="-312">suspend_frequency!</label>
			<label kind="assignment" x="-504" y="-296">suspend_frequency_s := false</label>
			<nail x="-520" y="-272"/>
		</transition>
		<transition>
			<source ref="id12"/>
			<target ref="id16"/>
			<label kind="guard" x="-256" y="-40">run_sender_s</label>
			<label kind="synchronisation" x="-256" y="-24">run_sender!</label>
			<label kind="assignment" x="-256" y="-8">run_sender_s := false</label>
		</transition>
		<transition>
			<source ref="id11"/>
			<target ref="id16"/>
			<label kind="guard" x="-272" y="72">run_frequency_s</label>
			<label kind="synchronisation" x="-272" y="88">run_frequency!</label>
			<label kind="assignment" x="-272" y="104">run_frequency_s := false</label>
			<nail x="-152" y="72"/>
		</transition>
		<transition>
			<source ref="id13"/>
			<target ref="id11"/>
			<label kind="guard" x="-456" y="72">run_sender_s</label>
			<label kind="synchronisation" x="-456" y="88">run_sender!</label>
			<label kind="assignment" x="-456" y="104">run_sender_s := false</label>
			<nail x="-456" y="72"/>
		</transition>
		<transition>
			<source ref="id13"/>
			<target ref="id12"/>
			<label kind="guard" x="-440" y="-40">run_frequency_s</label>
			<label kind="synchronisation" x="-440" y="-24">run_frequency!</label>
			<label kind="assignment" x="-440" y="-8">run_frequency_s := false</label>
		</transition>
		<transition>
			<source ref="id16"/>
			<target ref="id10"/>
			<label kind="guard" x="-56" y="-144">y == T_scan &amp;&amp; !hear()</label>
			<label kind="assignment" x="-56" y="-120">r := 0,
y := 0</label>
		</transition>
		<transition>
			<source ref="id14"/>
			<target ref="id7"/>
			<label kind="guard" x="272" y="136">y &gt; 0</label>
			<label kind="assignment" x="272" y="152">r := 1,
y := 0</label>
		</transition>
		<transition>
			<source ref="id15"/>
			<target ref="id14"/>
			<label kind="guard" x="392" y="0">y == T_resp</label>
			<label kind="synchronisation" x="392" y="16">reply!</label>
			<label kind="assignment" x="392" y="32">y := 0,
r := 3</label>
		</transition>
		<transition>
			<source ref="id16"/>
			<target ref="id15"/>
			<label kind="guard" x="104" y="-96">hear()</label>
			<label kind="assignment" x="104" y="-80">r := 2,
y := 0</label>
		</transition>
		<transition>
			<source ref="id17"/>
			<target ref="id13"/>
			<label kind="guard" x="-608" y="-136">y == T_sleep</label>
			<label kind="assignment" x="-608" y="-120">y := 0,
r := 1,
freq := phase</label>
			<nail x="-520" y="-40"/>
		</transition>
	</template>
	<template>
		<name>Frequency</name>
		<declaration>clock z;
clock t;</declaration>
		<location id="id18" x="-256" y="0">
			<name x="-288" y="-16">f0</name>
		</location>
		<location id="id19" x="0" y="0">
			<name x="0" y="-32">f1</name>
			<label kind="invariant" x="48" y="-56">t &lt;= 1 &amp;&amp;
z &lt;= z_max</label>
		</location>
		<init ref="id18"/>
		<transition>
			<source ref="id19"/>
			<target ref="id18"/>
			<label kind="synchronisation" x="-224" y="-64">suspend_frequency?</label>
			<label kind="assignment" x="-224" y="-48">run_frequency_s := true</label>
			<nail x="-56" y="-24"/>
			<nail x="-216" y="-24"/>
		</transition>
		<transition>
			<source ref="id18"/>
			<target ref="id19"/>
			<label kind="synchronisation" x="-248" y="24">run_frequency?</label>
			<label kind="assignment" x="-248" y="40">t := 0,
z := 0,
suspend_frequency_s := true</label>
			<nail x="-216" y="24"/>
			<nail x="-56" y="24"/>
		</transition>
		<transition>
			<source ref="id19"/>
			<target ref="id19"/>
			<label kind="guard" x="112" y="-8">z == z_max</label>
			<label kind="assignment" x="112" y="8">z := 0,
suspend_frequency_s := true</label>
			<nail x="104" y="32"/>
			<nail x="104" y="-24"/>
		</transition>
		<transition>
			<source ref="id19"/>
			<target ref="id19"/>
			<label kind="guard" x="-32" y="72">t &lt;= 1</label>
			<label kind="assignment" x="-32" y="88">phase := (phase &lt; 32)? phase + 1: 1,
t := 0,
suspend_frequency_s := true</label>
			<nail x="48" y="72"/>
			<nail x="-40" y="72"/>
		</transition>
		<transition>
			<source ref="id19"/>
			<target ref="id19"/>
			<label kind="synchronisation" x="-40" y="-136">reply?</label>
			<label kind="assignment" x="-40" y="-120">phase := (phase &lt; 32)? phase + 1: 1,
t := 0,
suspend_frequency_s := true</label>
			<nail x="48" y="-64"/>
			<nail x="-48" y="-64"/>
		</transition>
	</template>
	<system>// Place template instantiations here.
sender1 = Sender();
receiver1 = Receiver();
frequency1 = Frequency();
// List one or more processes to be composed into a system.
system sender1, receiver1, frequency1;</system>
	<queries>
		<query>
			<formula>Pr[&lt;=500000] (&lt;&gt; energy&gt;=500)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=5000](&lt;&gt; receiver1.Reply)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=10000](&lt;&gt; receiver1.Reply)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=15000](&lt;&gt; receiver1.Reply)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=20000](&lt;&gt; receiver1.Reply)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=25000](&lt;&gt; receiver1.Reply)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=30000](&lt;&gt; receiver1.Reply)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=35000](&lt;&gt; receiver1.Reply)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=40000](&lt;&gt; receiver1.Reply)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=45000](&lt;&gt; receiver1.Reply)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=50000](&lt;&gt; receiver1.Reply)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=55000](&lt;&gt; receiver1.Reply)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=60000](&lt;&gt; receiver1.Reply)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=65000](&lt;&gt; receiver1.Reply)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=70000](&lt;&gt; receiver1.Reply)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[energy&lt;=500] (&lt;&gt; time&gt;=10000)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[energy&lt;=1000] (&lt;&gt; time&gt;=70000)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[energy&lt;=2500] (&lt;&gt; time&gt;=70000)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[energy&lt;=4000] (&lt;&gt; time&gt;=70000)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>E&lt;&gt;(time &lt;= 500 &amp;&amp; energy &gt;= 1000)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=500000] (&lt;&gt; energy&gt;=500)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>E[&lt;=10000; 10000] (max: receiver1.energy)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[#&lt;=1000](&lt;&gt;rep ==mrep)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[#&lt;=1000](&lt;&gt;rep ==mrep)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[#&lt;=14012] (&lt;&gt; rep &gt;=12)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>E&lt;&gt;rep &gt;=2
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[# &lt;= 50] (&lt;&gt; (freq == f + o * 16 &amp;&amp; s== 1))
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>E&lt;&gt;rep &gt;= 2
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>E&lt;&gt; receiver1.wait
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>E&lt;&gt; receiver1.Reply
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>E&lt;&gt; receiver1.scan
			</formula>
			<comment>
			</comment>
		</query>
	</queries>
</nta>
