<?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>// Place global declarations here.
</declaration>
	<template>
		<name x="5" y="5">Foo</name>
		<declaration>// Place local declarations here.
clock x;</declaration>
		<location id="id0" x="112" y="-16">
			<name x="136" y="-32">D</name>
			<label kind="invariant" x="152" y="-32">x'==2</label>
			<label kind="exponentialrate" x="136" y="-16">2</label>
		</location>
		<location id="id1" x="112" y="-80">
			<name x="136" y="-96">C</name>
			<label kind="invariant" x="152" y="-96">x'==4</label>
			<label kind="exponentialrate" x="136" y="-80">1</label>
		</location>
		<location id="id2" x="112" y="-112">
			<name x="136" y="-128">B</name>
			<label kind="invariant" x="152" y="-128">x'==3</label>
			<label kind="exponentialrate" x="136" y="-112">2</label>
		</location>
		<location id="id3" x="112" y="-176">
			<name x="136" y="-192">A</name>
			<label kind="invariant" x="152" y="-192">x'==3</label>
			<label kind="exponentialrate" x="136" y="-176">1</label>
		</location>
		<location id="id4" x="-32" y="-48">
			<name x="-42" y="-78">Bottom</name>
			<label kind="invariant" x="-42" y="-33">x'==2</label>
			<label kind="exponentialrate" x="-40" y="-16">3</label>
		</location>
		<location id="id5" x="-32" y="-144">
			<name x="-42" y="-174">Top</name>
			<label kind="invariant" x="-40" y="-128">x'==1</label>
			<label kind="exponentialrate" x="-40" y="-112">2</label>
		</location>
		<location id="id6" x="-176" y="-96">
			<name x="-186" y="-126">Init</name>
			<label kind="invariant" x="-200" y="-80">x'==0</label>
			<label kind="exponentialrate" x="-200" y="-64">1</label>
		</location>
		<branchpoint id="id7" x="48" y="-48"/>
		<branchpoint id="id8" x="48" y="-144"/>
		<branchpoint id="id9" x="-96" y="-96"/>
		<init ref="id6"/>
		<transition id="id10">
			<source ref="id4"/>
			<target ref="id7"/>
		</transition>
		<transition id="id11">
			<source ref="id7"/>
			<target ref="id0"/>
			<label kind="probability" x="56" y="-32">20</label>
		</transition>
		<transition id="id12">
			<source ref="id7"/>
			<target ref="id1"/>
			<label kind="probability" x="56" y="-80">30</label>
		</transition>
		<transition id="id13">
			<source ref="id8"/>
			<target ref="id2"/>
			<label kind="probability" x="56" y="-128">20</label>
		</transition>
		<transition id="id14">
			<source ref="id8"/>
			<target ref="id3"/>
			<label kind="probability" x="56" y="-176">30</label>
		</transition>
		<transition id="id15">
			<source ref="id5"/>
			<target ref="id8"/>
		</transition>
		<transition id="id16">
			<source ref="id9"/>
			<target ref="id4"/>
			<label kind="probability" x="-88" y="-80">20</label>
		</transition>
		<transition id="id17">
			<source ref="id9"/>
			<target ref="id5"/>
			<label kind="probability" x="-88" y="-128">30</label>
		</transition>
		<transition id="id18">
			<source ref="id6"/>
			<target ref="id9"/>
		</transition>
	</template>
	<lsc>
		<name>LscTemplate</name>
		<type>Universal</type>
		<mode>Invariant</mode>
		<declaration>// Place local declarations here.
</declaration>
		<yloccoord number="0" y="0"/>
		<yloccoord number="1" y="220"/>
		<instance id="id19" x="0" y="0">
			<name x="0" y="0">Instance</name>
		</instance>
	</lsc>
	<system>system Foo;
</system>
	<queries>
		<query>
			<formula>E[&lt;=100; 200](max:Foo.x)</formula>
			<comment/>
		</query>
		<query>
			<formula>Pr[#&lt;=4](&lt;&gt; Foo.A)	</formula>
			<comment/>
		</query>
		<query>
			<formula>Pr[#&lt;=4](&lt;&gt; Foo.B)</formula>
			<comment/>
		</query>
		<query>
			<formula>Pr[#&lt;=4](&lt;&gt; Foo.C)	</formula>
			<comment/>
		</query>
		<query>
			<formula>Pr[#&lt;=4](&lt;&gt; Foo.D)</formula>
			<comment/>
		</query>
	</queries>
</nta>
