Uppaal Model

<?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.

urgent chan u;

</declaration>
	<template>
		<name x="5" y="5">UrgentChannel</name>
		<declaration>// Place local declarations here.</declaration>
		<location id="id0" x="0" y="0">
		</location>
		<init ref="id0"/>
		<transition>
			<source ref="id0"/>
			<target ref="id0"/>
			<label kind="synchronisation" x="0" y="-51">u!</label>
			<nail x="-25" y="-34"/>
			<nail x="34" y="-34"/>
		</transition>
	</template>
	<template>
		<name>P1</name>
		<location id="id1" x="-68" y="-51">
			<name x="-78" y="-85">start</name>
		</location>
		<location id="id2" x="59" y="-51">
			<name x="49" y="-85">goal</name>
		</location>
		<init ref="id1"/>
		<transition>
			<source ref="id1"/>
			<target ref="id2"/>
			<label kind="synchronisation" x="-8" y="-76">u?</label>
		</transition>
	</template>
	<template>
		<name>P2</name>
		<location id="id3" x="0" y="0">
		</location>
		<init ref="id3"/>
		<transition>
			<source ref="id3"/>
			<target ref="id3"/>
			<nail x="-25" y="-25"/>
			<nail x="25" y="-25"/>
		</transition>
	</template>
	<system>// Place template instantiations here.

// List one or more processes to be composed into a system.
system UrgentChannel, P1, P2;
    </system>
	<queries>
		<query>
			<formula>P1.start --&gt; P1.goal</formula>
			<comment></comment>
		</query>
	</queries>
</nta>