<?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>/** Case-study used in
 * Rewrite-Based Statistical Model Checking of WMTL.
 * Peter Bulychev, Alexandre David, Kim G. Larsen, Axel Legay,
 * Guangyan Li, and Danny Bøgsted Poulsen.
 * Runtime Verification 2012, pages 260-275, LNCS 7687.
 */

//const int N=10; // CORRECT
const int N=2; // INCORRECT

clock time;

typedef int[0,N-1] id_t;

broadcast chan ready;
broadcast chan go;

broadcast chan a;

bool isTransmitting[N];

const int macMaxCSMABackoffs = 4; // CORRECT
//const int macMaxCSMABackoffs = 1; // INCORRECT

// approved consts
const int aUnitBackoffPeriod = 20;
const int CCA_duration = 8; // CORRECT
const int aTurnaroundTime = 12; // CORRECT
const int ACK_time = 88;
const int aMaxFrameRetries = 3; // CORRECT

const int macMinBE = 3; // CORRECT
const int macMaxBE = 5; // CORRECT

//const int macMinBE = 0; // INCORRECT
//const int macMaxBE = 0; // INCORRECT

//const int minDataLength = 15*8; // CORRECT
//const int maxDataLength = 6*8; // CORRECT
const int data_length = 35*8; // CORRECT 35*8 25*8 - is for header 
//const int data_length = maxDataLength;

//const int data_length = 3; // INCORRECT
//const int aTurnaroundTime = 2; // INCORRECT
//const int CCA_duration = 10; // INCORRECT

//const int max_waking_delay=6000;  for sound speed is 300 m/s
//const int max_waking_delay=10;  //CORRECT for something else
const int max_waking_delay=data_length;  //CORRECT for something else
//const int max_waking_delay=aTurnaroundTime;  //CORRECT to show that is_disrete_waiting qualitatively affects the model // exist
//const int max_waking_delay=aTurnaroundTime + data_length + CCA_duration;  //CORRECT to show that is_disrete_waiting qualitatively affects the model // forall

const int aMinLIFSPeriod = 40; // CORRECT

const bool is_discrete_waiting = false;
const bool acknowledgment_supported = true;
const bool recover_from_failures = false;

const int wait_after_failure = 0;</declaration>
	<template>
		<name x="5" y="5">Process</name>
		<parameter>const id_t id</parameter>
		<declaration>// Place local declarations here.

int be;
int nb; 
int nretries;

int backoff;

int waking_delay;



clock x;

bool cca_passed := false;
bool collision_occured := false;

bool is_busy() {
    int i;
    for(i=0; i&lt;N; i++) {
        if (isTransmitting[i])
            return true;
    }
    return false;
}

void start_sending() {
    isTransmitting[id] = true;
}

void finish_sending() {
    isTransmitting[id] = false;
}

bool is_conflict() {
    bool f = false;
    int i;
    for(i=0; i&lt;N; i++) {
        if (isTransmitting[i]) {
            if (f)
                return true;
            else 
                f = true;
        }
    }
    return false;
}</declaration>
		<location id="id0" x="-2536" y="-184">
			<urgent/>
		</location>
		<location id="id1" x="-2240" y="-320">
			<name x="-2224" y="-328">failure</name>
		</location>
		<location id="id2" x="-2376" y="-264">
			<label kind="invariant" x="-2408" y="-240">x&lt;=wait_after_failure</label>
		</location>
		<location id="id3" x="-1872" y="-272">
			<urgent/>
		</location>
		<location id="id4" x="-1968" y="-312">
			<urgent/>
		</location>
		<location id="id5" x="-2704" y="-264">
			<label kind="invariant" x="-2714" y="-249">x&lt;=waking_delay</label>
		</location>
		<location id="id6" x="-2792" y="-96">
			<urgent/>
		</location>
		<location id="id7" x="-2536" y="-144">
			<label kind="invariant" x="-2584" y="-128">x&lt;=aMinLIFSPeriod</label>
		</location>
		<location id="id8" x="-2536" y="-248">
			<name x="-2536" y="-280">start</name>
			<urgent/>
		</location>
		<location id="id9" x="-2768" y="-328">
			<label kind="invariant" x="-2784" y="-304">x&lt;=max_waking_delay</label>
		</location>
		<location id="id10" x="-2440" y="-72">
			<name x="-2450" y="-102">ok</name>
		</location>
		<location id="id11" x="-2288" y="-160">
			<urgent/>
		</location>
		<location id="id12" x="-2280" y="-376">
			<urgent/>
		</location>
		<location id="id13" x="-2416" y="-376">
			<urgent/>
		</location>
		<location id="id14" x="-1912" y="-328">
			<urgent/>
		</location>
		<location id="id15" x="-1928" y="24">
			<label kind="invariant" x="-2136" y="48">x&lt;=aTurnaroundTime + ACK_time</label>
		</location>
		<location id="id16" x="-2192" y="-224">
			<name x="-2216" y="-264">transmit_ack</name>
			<label kind="invariant" x="-2224" y="-176">x&lt;=ACK_time</label>
		</location>
		<location id="id17" x="-1992" y="-224">
			<label kind="invariant" x="-2096" y="-264">x&lt;=aTurnaroundTime</label>
		</location>
		<location id="id18" x="-1912" y="-480">
			<name x="-1922" y="-510">transmit</name>
			<label kind="invariant" x="-1896" y="-496">x&lt;=data_length</label>
		</location>
		<location id="id19" x="-2192" y="-480">
			<name x="-2224" y="-512">vulnerable</name>
			<label kind="invariant" x="-2248" y="-560">x&lt;=aTurnaroundTime</label>
		</location>
		<location id="id20" x="-2320" y="-480">
			<name x="-2328" y="-512">cca</name>
			<label kind="invariant" x="-2384" y="-464">x&lt;=CCA_duration</label>
		</location>
		<location id="id21" x="-2536" y="-480">
			<name x="-2672" y="-488">waiting_backoff</name>
			<label kind="invariant" x="-2784" y="-512">x&lt;=backoff*aUnitBackoffPeriod</label>
		</location>
		<location id="id22" x="-2536" y="-344">
			<name x="-2664" y="-344">set_backoff</name>
			<urgent/>
		</location>
		<init ref="id6"/>
		<transition>
			<source ref="id0"/>
			<target ref="id1"/>
			<label kind="guard" x="-2448" y="-250">nretries == (aMaxFrameRetries-1)</label>
			<nail x="-2240" y="-240"/>
		</transition>
		<transition>
			<source ref="id0"/>
			<target ref="id8"/>
			<label kind="guard" x="-2596" y="-254">nretries &lt; (aMaxFrameRetries-1)</label>
			<label kind="assignment" x="-2596" y="-224">nretries = nretries + 1</label>
		</transition>
		<transition>
			<source ref="id12"/>
			<target ref="id1"/>
			<label kind="guard" x="-2264" y="-360">!acknowledgment_supported or !recover_from_failures</label>
		</transition>
		<transition>
			<source ref="id2"/>
			<target ref="id8"/>
			<label kind="guard" x="-2520" y="-256">x==wait_after_failure</label>
		</transition>
		<transition>
			<source ref="id12"/>
			<target ref="id2"/>
			<label kind="guard" x="-2464" y="-312">acknowledgment_supported &amp;&amp; recover_from_failures</label>
			<label kind="assignment" x="-2336" y="-288">x:=0</label>
			<nail x="-2272" y="-256"/>
		</transition>
		<transition>
			<source ref="id4"/>
			<target ref="id10"/>
			<label kind="guard" x="-2216" y="-40">!collision_occured</label>
			<nail x="-1968" y="-8"/>
			<nail x="-2440" y="-16"/>
		</transition>
		<transition>
			<source ref="id4"/>
			<target ref="id12"/>
			<label kind="guard" x="-2232" y="-392">collision_occured</label>
			<nail x="-2056" y="-368"/>
		</transition>
		<transition>
			<source ref="id14"/>
			<target ref="id4"/>
			<label kind="guard" x="-2032" y="-344">!acknowledgment_supported</label>
		</transition>
		<transition>
			<source ref="id14"/>
			<target ref="id3"/>
			<label kind="guard" x="-1936" y="-312">acknowledgment_supported</label>
		</transition>
		<transition>
			<source ref="id5"/>
			<target ref="id8"/>
			<label kind="guard" x="-2688" y="-280">x==waking_delay</label>
		</transition>
		<transition>
			<source ref="id6"/>
			<target ref="id5"/>
			<label kind="select" x="-2784" y="-232">_waking_delay : int[0, max_waking_delay]</label>
			<label kind="guard" x="-2768" y="-200">is_discrete_waiting</label>
			<label kind="assignment" x="-2776" y="-184">waking_delay:=_waking_delay</label>
		</transition>
		<transition>
			<source ref="id6"/>
			<target ref="id9"/>
			<label kind="guard" x="-2872" y="-256">!is_discrete_waiting</label>
		</transition>
		<transition>
			<source ref="id7"/>
			<target ref="id0"/>
			<label kind="guard" x="-2584" y="-176">x==aMinLIFSPeriod</label>
		</transition>
		<transition>
			<source ref="id9"/>
			<target ref="id8"/>
			<nail x="-2552" y="-272"/>
		</transition>
		<transition>
			<source ref="id8"/>
			<target ref="id22"/>
			<label kind="assignment" x="-2528" y="-304">be:=macMinBE, nb:=0</label>
		</transition>
		<transition>
			<source ref="id20"/>
			<target ref="id20"/>
			<label kind="synchronisation" x="-2344" y="-648">a?</label>
			<label kind="assignment" x="-2368" y="-624">cca_passed:=false</label>
			<nail x="-2416" y="-632"/>
			<nail x="-2192" y="-632"/>
		</transition>
		<transition>
			<source ref="id16"/>
			<target ref="id11"/>
			<label kind="guard" x="-2300" y="-222">x==ACK_time</label>
			<label kind="assignment" x="-2300" y="-192">finish_sending()</label>
		</transition>
		<transition>
			<source ref="id13"/>
			<target ref="id12"/>
			<label kind="guard" x="-2360" y="-416">nb == macMaxCSMABackoffs</label>
		</transition>
		<transition>
			<source ref="id13"/>
			<target ref="id22"/>
			<label kind="guard" x="-2496" y="-344">nb &lt; macMaxCSMABackoffs</label>
			<label kind="assignment" x="-2496" y="-360">be:= (be+1 &gt; macMaxBE ? macMaxBE: be+1)</label>
		</transition>
		<transition>
			<source ref="id16"/>
			<target ref="id16"/>
			<label kind="synchronisation" x="-2120" y="-336">a?</label>
			<label kind="assignment" x="-2152" y="-304">collision_occured:=true</label>
			<nail x="-2056" y="-312"/>
			<nail x="-2168" y="-312"/>
		</transition>
		<transition>
			<source ref="id3"/>
			<target ref="id17"/>
			<label kind="guard" x="-2048" y="-280">!collision_occured</label>
		</transition>
		<transition>
			<source ref="id15"/>
			<target ref="id7"/>
			<label kind="guard" x="-2544" y="16">x == aTurnaroundTime + ACK_time</label>
			<label kind="assignment" x="-2340" y="40">x=0</label>
			<nail x="-2632" y="16"/>
			<nail x="-2656" y="-136"/>
		</transition>
		<transition>
			<source ref="id3"/>
			<target ref="id15"/>
			<label kind="guard" x="-1912" y="-240">collision_occured</label>
			<nail x="-1904" y="-144"/>
		</transition>
		<transition>
			<source ref="id18"/>
			<target ref="id18"/>
			<label kind="synchronisation" x="-1776" y="-480">a?</label>
			<label kind="assignment" x="-1848" y="-400">collision_occured:=true</label>
			<nail x="-1724" y="-445"/>
			<nail x="-1812" y="-365"/>
		</transition>
		<transition>
			<source ref="id11"/>
			<target ref="id10"/>
			<label kind="guard" x="-2280" y="-128">!collision_occured</label>
			<nail x="-2296" y="-48"/>
		</transition>
		<transition>
			<source ref="id11"/>
			<target ref="id7"/>
			<label kind="guard" x="-2448" y="-208">collision_occured</label>
			<label kind="assignment" x="-2384" y="-168">x=0</label>
		</transition>
		<transition>
			<source ref="id17"/>
			<target ref="id16"/>
			<label kind="guard" x="-2144" y="-208">x==aTurnaroundTime</label>
			<label kind="synchronisation" x="-2080" y="-248">a!</label>
			<label kind="assignment" x="-2184" y="-200">x:=0, collision_occured:=is_busy(), start_sending()</label>
		</transition>
		<transition>
			<source ref="id18"/>
			<target ref="id14"/>
			<label kind="guard" x="-2056" y="-424">x==data_length</label>
			<label kind="assignment" x="-2096" y="-400">x:=0, finish_sending()</label>
		</transition>
		<transition>
			<source ref="id19"/>
			<target ref="id18"/>
			<label kind="guard" x="-2144" y="-504">x==aTurnaroundTime</label>
			<label kind="synchronisation" x="-2148" y="-495">a!</label>
			<label kind="assignment" x="-2240" y="-464">x:=0, collision_occured:=is_busy(), start_sending()</label>
		</transition>
		<transition>
			<source ref="id20"/>
			<target ref="id19"/>
			<label kind="guard" x="-2312" y="-528">(x==CCA_duration) &amp;&amp; (cca_passed)</label>
			<label kind="assignment" x="-2272" y="-496">x:=0</label>
		</transition>
		<transition>
			<source ref="id20"/>
			<target ref="id13"/>
			<label kind="guard" x="-2432" y="-440">(x == CCA_duration) &amp;&amp; !cca_passed</label>
			<label kind="assignment" x="-2428" y="-428">nb = nb+1</label>
		</transition>
		<transition>
			<source ref="id21"/>
			<target ref="id20"/>
			<label kind="guard" x="-2672" y="-544">(x==backoff*aUnitBackoffPeriod)</label>
			<label kind="assignment" x="-2520" y="-504">x:=0, cca_passed:=!is_busy()</label>
		</transition>
		<transition>
			<source ref="id22"/>
			<target ref="id21"/>
			<label kind="select" x="-2736" y="-448">tbackoff : int [0, (1&lt;&lt;macMaxBE)-1]</label>
			<label kind="assignment" x="-2760" y="-432">backoff := tbackoff % (1&lt;&lt;be), x:=0</label>
		</transition>
	</template>
	<system>// Place template instantiations here.

system Process;</system>
	<queries>
		<query>
			<formula>E&lt;&gt; exists (i : id_t) ((time &lt;= 92) &amp;&amp; Process(i).ok)</formula>
			<comment>For N=2 expect unsatisfied within 15s</comment>
		</query>
		<query>
			<formula>Pr[time&lt;=5000] (&lt;&gt; forall (i : id_t) Process(i).ok)</formula>
			<comment/>
		</query>
		<query>
			<formula>Pr[time&lt;=data_length*5] (&lt;&gt; exists (i : id_t) Process(i).ok)</formula>
			<comment/>
		</query>
		<query>
			<formula>Pr[&lt;=10000] (&lt;&gt; exists (i : id_t) Process(i).ok)</formula>
			<comment/>
		</query>
	</queries>
</nta>
