<?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>
/* Example used in
 * Checking &amp; Distributing Statistical Model Checking.
 * Peter Bulychev, Alexandre David, Kim G. Larsen,
 * Axel Legay, Marius Mikucionis, and Danny Bøgsted Poulsen.
 * 4th NASA Formal Methods Symposium, 2012, pages 449-463,
 * LNCS 7226, Springer.
 */

const int N = 20;
clock time;
clock steps;
clock runs;
int t=0;

broadcast chan add, sub;</declaration>
	<template>
		<name x="5" y="5">Runner</name>
		<parameter>int[1,N] id</parameter>
		<declaration>// Place local declarations here.
clock x;</declaration>
		<location id="id0" x="160" y="-128">
			<committed/>
		</location>
		<location id="id1" x="-32" y="-128">
			<committed/>
		</location>
		<location id="id2" x="-32" y="-32">
			<name x="-72" y="-80">NOK</name>
			<label kind="invariant" x="-80" y="-64">x&lt;=2</label>
		</location>
		<location id="id3" x="160" y="-32">
			<name x="168" y="-80">OK</name>
			<label kind="invariant" x="168" y="-64">x&lt;=2</label>
			<urgent/>
		</location>
		<location id="id4" x="64" y="-128">
			<committed/>
		</location>
		<branchpoint id="id5" x="64" y="-32">
		</branchpoint>
		<init ref="id4"/>
		<transition>
			<source ref="id0"/>
			<target ref="id4"/>
			<label kind="synchronisation" x="104" y="-144">sub!</label>
			<label kind="assignment" x="80" y="-128">runs=++t</label>
		</transition>
		<transition>
			<source ref="id1"/>
			<target ref="id4"/>
			<label kind="synchronisation" x="0" y="-144">add!</label>
			<label kind="assignment" x="-16" y="-128">runs=++t</label>
		</transition>
		<transition>
			<source ref="id3"/>
			<target ref="id0"/>
		</transition>
		<transition>
			<source ref="id2"/>
			<target ref="id1"/>
			<label kind="guard" x="-72" y="-104">time&gt;=100</label>
		</transition>
		<transition>
			<source ref="id3"/>
			<target ref="id3"/>
			<label kind="assignment" x="176" y="-24">x=0</label>
			<nail x="176" y="0"/>
			<nail x="144" y="0"/>
		</transition>
		<transition>
			<source ref="id2"/>
			<target ref="id2"/>
			<label kind="guard" x="-16" y="-16">time&lt;100</label>
			<label kind="assignment" x="-80" y="-24">x=0</label>
			<nail x="-16" y="0"/>
			<nail x="-48" y="0"/>
		</transition>
		<transition>
			<source ref="id5"/>
			<target ref="id2"/>
			<label kind="assignment" x="8" y="-56">x=0</label>
			<label kind="probability" x="16" y="-72">58</label>
		</transition>
		<transition>
			<source ref="id5"/>
			<target ref="id3"/>
			<label kind="assignment" x="96" y="-56">x=0</label>
			<label kind="probability" x="96" y="-72">42</label>
		</transition>
		<transition>
			<source ref="id4"/>
			<target ref="id5"/>
			<label kind="assignment" x="72" y="-104">time=0</label>
		</transition>
	</template>
	<template>
		<name>Global</name>
		<location id="id6" x="0" y="0">
			<label kind="invariant" x="-10" y="15">runs'==0</label>
		</location>
		<init ref="id6"/>
	</template>
	<template>
		<name>dum</name>
		<location id="id7" x="0" y="-64">
		</location>
		<location id="id8" x="0" y="0">
			<label kind="invariant" x="-10" y="15">steps'==0</label>
		</location>
		<init ref="id8"/>
		<transition>
			<source ref="id7"/>
			<target ref="id8"/>
			<nail x="48" y="-64"/>
			<nail x="48" y="0"/>
		</transition>
		<transition>
			<source ref="id7"/>
			<target ref="id8"/>
			<nail x="-56" y="-64"/>
			<nail x="-56" y="0"/>
		</transition>
		<transition>
			<source ref="id8"/>
			<target ref="id7"/>
		</transition>
	</template>
	<template>
		<name>Master</name>
		<declaration>int r;</declaration>
		<location id="id9" x="-120" y="0">
			<name x="-130" y="-30">H0</name>
		</location>
		<location id="id10" x="120" y="0">
			<name x="112" y="-32">H1</name>
		</location>
		<location id="id11" x="0" y="0">
		</location>
		<init ref="id11"/>
		<transition>
			<source ref="id11"/>
			<target ref="id9"/>
			<label kind="guard" x="-88" y="-32">r&lt;-1192</label>
			<label kind="synchronisation" x="-88" y="-16">sub?</label>
			<label kind="assignment" x="-88" y="0">r=r-87</label>
		</transition>
		<transition>
			<source ref="id11"/>
			<target ref="id10"/>
			<label kind="guard" x="32" y="-32">r&gt;=1192</label>
			<label kind="synchronisation" x="32" y="-16">add?</label>
			<label kind="assignment" x="32" y="0">r=r+87</label>
		</transition>
		<transition>
			<source ref="id11"/>
			<target ref="id11"/>
			<label kind="guard" x="-120" y="-104">r&gt;-1192</label>
			<label kind="synchronisation" x="-104" y="-88">sub?</label>
			<label kind="assignment" x="-112" y="-72">r=r-87</label>
			<nail x="-32" y="-96"/>
			<nail x="-64" y="-96"/>
		</transition>
		<transition>
			<source ref="id11"/>
			<target ref="id11"/>
			<label kind="guard" x="64" y="-104">r&lt;1192</label>
			<label kind="synchronisation" x="64" y="-88">add?</label>
			<label kind="assignment" x="64" y="-72">r=r+87</label>
			<nail x="32" y="-96"/>
			<nail x="64" y="-96"/>
		</transition>
	</template>
	<system>// Place template instantiations here.


// List one or more processes to be composed into a system.
system Runner, Master, Global;</system>
	<queries>
		<query>
			<formula>Pr[steps&lt;=20000](&lt;&gt; Master.H1)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[runs&lt;=420](&lt;&gt; Master.H0)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[runs&lt;=20000](&lt;&gt; Master.H1)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[#&lt;=20000](&lt;&gt; Master.H0)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[#&lt;=80000](&lt;&gt; Master.H1)
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt;P.OK)
			</formula>
			<comment>
			</comment>
		</query>
	</queries>
</nta>
