<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.5//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_5.dtd'>
<nta>
	<declaration>broadcast chan head, tail;

</declaration>
	<template>
		<name>Coin</name>
		<parameter>broadcast chan &amp;flip, const int headw, const int tailw</parameter>
		<location id="id0" x="-76" y="-25">
			<committed/>
		</location>
		<location id="id1" x="42" y="17">
			<name x="25" y="34">Tail</name>
			<committed/>
		</location>
		<location id="id2" x="42" y="-76">
			<name x="32" y="-110">Head</name>
			<committed/>
		</location>
		<location id="id3" x="-153" y="-25">
			<name x="-187" y="-59">Idle</name>
		</location>
		<branchpoint id="id4" x="-25" y="-25"/>
		<init ref="id3"/>
		<transition id="id5">
			<source ref="id0"/>
			<target ref="id4"/>
		</transition>
		<transition id="id6">
			<source ref="id1"/>
			<target ref="id3"/>
			<label kind="synchronisation" x="-75" y="0">tail!</label>
			<nail x="-153" y="17"/>
		</transition>
		<transition id="id7">
			<source ref="id2"/>
			<target ref="id3"/>
			<label kind="synchronisation" x="-75" y="-93">head!</label>
			<nail x="-153" y="-76"/>
		</transition>
		<transition id="id8">
			<source ref="id4"/>
			<target ref="id1"/>
			<label kind="probability" x="17" y="-17">tailw</label>
		</transition>
		<transition id="id9">
			<source ref="id4"/>
			<target ref="id2"/>
			<label kind="probability" x="17" y="-51">headw</label>
		</transition>
		<transition id="id10">
			<source ref="id3"/>
			<target ref="id0"/>
			<label kind="synchronisation" x="-136" y="-42">flip?</label>
		</transition>
	</template>
	<template>
		<name x="5" y="5">Dice</name>
		<parameter>broadcast chan &amp;flip, int &amp;val</parameter>
		<declaration>// Place local declarations here.</declaration>
		<location id="id11" x="476" y="331">
			<name x="466" y="297">Six</name>
		</location>
		<location id="id12" x="382" y="331">
		</location>
		<location id="id13" x="476" y="263">
			<name x="466" y="229">Five</name>
		</location>
		<location id="id14" x="476" y="187">
			<name x="466" y="153">Four</name>
		</location>
		<location id="id15" x="382" y="221">
		</location>
		<location id="id16" x="297" y="332">
			<name x="287" y="298">TT</name>
			<urgent/>
		</location>
		<location id="id17" x="297" y="221">
			<name x="287" y="187">TH</name>
			<urgent/>
		</location>
		<location id="id18" x="476" y="136">
			<name x="466" y="102">Three</name>
		</location>
		<location id="id19" x="476" y="51">
			<name x="466" y="17">Two</name>
		</location>
		<location id="id20" x="382" y="93">
		</location>
		<location id="id21" x="476" y="-25">
			<name x="466" y="-59">One</name>
		</location>
		<location id="id22" x="382" y="-25">
		</location>
		<location id="id23" x="221" y="272">
		</location>
		<location id="id24" x="297" y="93">
			<name x="287" y="59">HT</name>
			<urgent/>
		</location>
		<location id="id25" x="297" y="-26">
			<name x="287" y="-60">HH</name>
			<urgent/>
		</location>
		<location id="id26" x="220" y="34">
		</location>
		<location id="id27" x="127" y="272">
			<name x="117" y="238">T</name>
			<urgent/>
		</location>
		<location id="id28" x="127" y="34">
			<name x="102" y="8">H</name>
			<urgent/>
		</location>
		<location id="id29" x="42" y="136">
		</location>
		<location id="id30" x="-51" y="136">
			<urgent/>
		</location>
		<init ref="id30"/>
		<transition id="id31">
			<source ref="id12"/>
			<target ref="id27"/>
			<label kind="synchronisation" x="145" y="365">tail?</label>
			<nail x="382" y="382"/>
			<nail x="127" y="382"/>
		</transition>
		<transition id="id32">
			<source ref="id12"/>
			<target ref="id11"/>
			<label kind="synchronisation" x="400" y="314">head?</label>
			<label kind="assignment" x="400" y="331">val=6</label>
		</transition>
		<transition id="id33">
			<source ref="id16"/>
			<target ref="id12"/>
			<label kind="synchronisation" x="315" y="314">flip!</label>
		</transition>
		<transition id="id34">
			<source ref="id15"/>
			<target ref="id13"/>
			<label kind="synchronisation" x="400" y="225">tail?</label>
			<label kind="assignment" x="400" y="242">val=5</label>
		</transition>
		<transition id="id35">
			<source ref="id15"/>
			<target ref="id14"/>
			<label kind="synchronisation" x="400" y="187">head?</label>
			<label kind="assignment" x="400" y="204">val=4</label>
		</transition>
		<transition id="id36">
			<source ref="id17"/>
			<target ref="id15"/>
			<label kind="synchronisation" x="315" y="204">flip!</label>
		</transition>
		<transition id="id37">
			<source ref="id23"/>
			<target ref="id16"/>
			<label kind="synchronisation" x="229" y="306">tail?</label>
		</transition>
		<transition id="id38">
			<source ref="id23"/>
			<target ref="id17"/>
			<label kind="synchronisation" x="221" y="221">head?</label>
		</transition>
		<transition id="id39">
			<source ref="id20"/>
			<target ref="id18"/>
			<label kind="synchronisation" x="400" y="106">tail?</label>
			<label kind="assignment" x="400" y="123">val=3</label>
		</transition>
		<transition id="id40">
			<source ref="id20"/>
			<target ref="id19"/>
			<label kind="synchronisation" x="400" y="55">head?</label>
			<label kind="assignment" x="400" y="72">val=2</label>
		</transition>
		<transition id="id41">
			<source ref="id24"/>
			<target ref="id20"/>
			<label kind="synchronisation" x="315" y="76">flip!</label>
		</transition>
		<transition id="id42">
			<source ref="id22"/>
			<target ref="id21"/>
			<label kind="synchronisation" x="400" y="-42">tail?</label>
			<label kind="assignment" x="400" y="-25">val=1</label>
		</transition>
		<transition id="id43">
			<source ref="id22"/>
			<target ref="id28"/>
			<label kind="synchronisation" x="145" y="-93">head?</label>
			<nail x="382" y="-76"/>
			<nail x="127" y="-76"/>
		</transition>
		<transition id="id44">
			<source ref="id25"/>
			<target ref="id22"/>
			<label kind="synchronisation" x="315" y="-42">flip!</label>
		</transition>
		<transition id="id45">
			<source ref="id27"/>
			<target ref="id23"/>
			<label kind="synchronisation" x="145" y="255">flip!</label>
		</transition>
		<transition id="id46">
			<source ref="id26"/>
			<target ref="id24"/>
			<label kind="synchronisation" x="229" y="68">tail?</label>
		</transition>
		<transition id="id47">
			<source ref="id26"/>
			<target ref="id25"/>
			<label kind="synchronisation" x="221" y="-17">head?</label>
		</transition>
		<transition id="id48">
			<source ref="id28"/>
			<target ref="id26"/>
			<label kind="synchronisation" x="145" y="17">flip!</label>
		</transition>
		<transition id="id49">
			<source ref="id29"/>
			<target ref="id27"/>
			<label kind="synchronisation" x="51" y="221">tail?</label>
		</transition>
		<transition id="id50">
			<source ref="id29"/>
			<target ref="id28"/>
			<label kind="synchronisation" x="42" y="68">head?</label>
		</transition>
		<transition id="id51">
			<source ref="id30"/>
			<target ref="id29"/>
			<label kind="synchronisation" x="-16" y="119">flip!</label>
		</transition>
	</template>
	<template>
		<name x="5" y="5">DiceSimulator</name>
		<parameter>const int headw, const int tailw, int &amp;val</parameter>
		<declaration>// Place local declarations here.</declaration>
		<location id="id52" x="476" y="323">
			<name x="466" y="289">Six</name>
		</location>
		<location id="id53" x="476" y="255">
			<name x="466" y="221">Five</name>
		</location>
		<location id="id54" x="476" y="187">
			<name x="466" y="153">Four</name>
		</location>
		<location id="id55" x="297" y="324">
			<name x="287" y="290">TT</name>
			<urgent/>
		</location>
		<location id="id56" x="297" y="221">
			<name x="287" y="187">TH</name>
			<urgent/>
		</location>
		<location id="id57" x="476" y="127">
			<name x="466" y="93">Three</name>
		</location>
		<location id="id58" x="476" y="59">
			<name x="466" y="25">Two</name>
		</location>
		<location id="id59" x="476" y="-8">
			<name x="466" y="-42">One</name>
		</location>
		<location id="id60" x="297" y="93">
			<name x="287" y="59">HT</name>
			<urgent/>
		</location>
		<location id="id61" x="297" y="-9">
			<name x="287" y="-43">HH</name>
			<urgent/>
		</location>
		<location id="id62" x="127" y="272">
			<name x="117" y="238">T</name>
			<urgent/>
		</location>
		<location id="id63" x="127" y="34">
			<name x="102" y="8">H</name>
			<urgent/>
		</location>
		<location id="id64" x="-34" y="136">
			<urgent/>
		</location>
		<branchpoint id="id65" x="382" y="323"/>
		<branchpoint id="id66" x="382" y="221"/>
		<branchpoint id="id67" x="221" y="272"/>
		<branchpoint id="id68" x="382" y="93"/>
		<branchpoint id="id69" x="382" y="-8"/>
		<branchpoint id="id70" x="221" y="34"/>
		<branchpoint id="id71" x="34" y="136"/>
		<init ref="id64"/>
		<transition id="id72">
			<source ref="id65"/>
			<target ref="id62"/>
			<label kind="probability" x="145" y="374">tailw</label>
			<nail x="382" y="374"/>
			<nail x="127" y="374"/>
		</transition>
		<transition id="id73">
			<source ref="id65"/>
			<target ref="id52"/>
			<label kind="assignment" x="400" y="306">val=6</label>
			<label kind="probability" x="400" y="323">headw</label>
		</transition>
		<transition id="id74">
			<source ref="id55"/>
			<target ref="id65"/>
		</transition>
		<transition id="id75">
			<source ref="id66"/>
			<target ref="id53"/>
			<label kind="assignment" x="400" y="238">val=5</label>
			<label kind="probability" x="399" y="255">tailw</label>
			<nail x="382" y="255"/>
		</transition>
		<transition id="id76">
			<source ref="id66"/>
			<target ref="id54"/>
			<label kind="assignment" x="400" y="170">val=4</label>
			<label kind="probability" x="400" y="187">headw</label>
			<nail x="382" y="187"/>
		</transition>
		<transition id="id77">
			<source ref="id56"/>
			<target ref="id66"/>
		</transition>
		<transition id="id78">
			<source ref="id67"/>
			<target ref="id55"/>
			<label kind="probability" x="229" y="323">tailw</label>
			<nail x="221" y="323"/>
		</transition>
		<transition id="id79">
			<source ref="id67"/>
			<target ref="id56"/>
			<label kind="probability" x="229" y="221">headw</label>
			<nail x="221" y="221"/>
		</transition>
		<transition id="id80">
			<source ref="id62"/>
			<target ref="id67"/>
		</transition>
		<transition id="id81">
			<source ref="id68"/>
			<target ref="id57"/>
			<label kind="assignment" x="400" y="110">val=3</label>
			<label kind="probability" x="400" y="127">tailw</label>
			<nail x="382" y="127"/>
		</transition>
		<transition id="id82">
			<source ref="id68"/>
			<target ref="id58"/>
			<label kind="assignment" x="399" y="42">val=2</label>
			<label kind="probability" x="399" y="59">headw</label>
			<nail x="382" y="59"/>
		</transition>
		<transition id="id83">
			<source ref="id60"/>
			<target ref="id68"/>
		</transition>
		<transition id="id84">
			<source ref="id69"/>
			<target ref="id63"/>
			<label kind="probability" x="170" y="-59">headw</label>
			<nail x="382" y="-59"/>
			<nail x="127" y="-59"/>
		</transition>
		<transition id="id85">
			<source ref="id69"/>
			<target ref="id59"/>
			<label kind="assignment" x="399" y="-25">val=1</label>
			<label kind="probability" x="399" y="-8">tailw</label>
		</transition>
		<transition id="id86">
			<source ref="id61"/>
			<target ref="id69"/>
		</transition>
		<transition id="id87">
			<source ref="id70"/>
			<target ref="id60"/>
			<label kind="probability" x="229" y="93">tailw</label>
			<nail x="221" y="93"/>
		</transition>
		<transition id="id88">
			<source ref="id70"/>
			<target ref="id61"/>
			<label kind="probability" x="229" y="-8">headw</label>
			<nail x="221" y="-8"/>
		</transition>
		<transition id="id89">
			<source ref="id63"/>
			<target ref="id70"/>
		</transition>
		<transition id="id90">
			<source ref="id71"/>
			<target ref="id62"/>
			<label kind="probability" x="42" y="272">tailw</label>
			<nail x="34" y="272"/>
		</transition>
		<transition id="id91">
			<source ref="id71"/>
			<target ref="id63"/>
			<label kind="probability" x="42" y="34">headw</label>
			<nail x="34" y="34"/>
		</transition>
		<transition id="id92">
			<source ref="id64"/>
			<target ref="id71"/>
		</transition>
	</template>
	<template>
		<name>Norm</name>
		<parameter>int &amp;val, int &amp;out</parameter>
		<declaration>clock x;</declaration>
		<location id="id93" x="136" y="0">
		</location>
		<location id="id94" x="0" y="0">
			<label kind="invariant" x="-10" y="17">x&lt;=1</label>
		</location>
		<init ref="id94"/>
		<transition id="id95">
			<source ref="id94"/>
			<target ref="id93"/>
			<label kind="guard" x="25" y="-17">x&gt;0</label>
			<label kind="assignment" x="25" y="0">out=2*val-7</label>
		</transition>
	</template>
	<system>broadcast chan fairflip, badflip;
int fairvalue, badvalue, simvalue, normalized=-10;

faircoin = Coin(fairflip, 1, 1);
fairdice = Dice(fairflip, fairvalue);

badcoin = Coin(badflip, 1, 2);
baddice = Dice(badflip, badvalue);

simdice = DiceSimulator(1, 1, simvalue);

norm = Norm(simvalue, normalized); // normalize around 0

system faircoin, fairdice, badcoin, baddice, simdice, norm;
    </system>
	<queries>
		<query>
			<formula>simulate [&lt;=2] { fairvalue, badvalue, simvalue, normalized }
			</formula>
			<comment/>
		</query>
		<query>
			<formula>Pr[#&lt;=1000] (&lt;&gt; fairvalue&gt;0)</formula>
			<comment/>
		</query>
		<query>
			<formula>E[&lt;=2; 10000] (max: fairvalue)
			</formula>
			<comment/>
		</query>
		<query>
			<formula>E[&lt;=2; 10000] (max: badvalue)
			</formula>
			<comment/>
		</query>
		<query>
			<formula>E[&lt;=2; 10000] (max: simvalue)
			</formula>
			<comment/>
		</query>
		<query>
			<formula>E[&lt;=2; 10000] (max: normalized)
			</formula>
			<comment/>
		</query>
		<query>
			<formula>E[#&lt;=10; 10000] (max:fairvalue)</formula>
			<comment/>
		</query>
	</queries>
</nta>
