<?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>// Fischer's mutual exclusion protocol.

typedef int[1,6] id_t;
int id;</declaration>
	<template>
		<name x="16" y="-8">P</name>
		<parameter>const id_t pid</parameter>
		<declaration>clock x;
const int k = 2;</declaration>
		<location id="id0" x="216" y="176">
			<name x="216" y="192">wait</name>
			<label kind="exponentialrate" x="232" y="168">1</label>
		</location>
		<location id="id1" x="216" y="48">
			<name x="216" y="16">req</name>
			<label kind="invariant" x="240" y="32">x&lt;=k</label>
		</location>
		<location id="id2" x="64" y="48">
			<name x="54" y="18">A</name>
			<label kind="exponentialrate" x="40" y="40">1</label>
		</location>
		<location id="id3" x="64" y="176">
			<name x="56" y="192">cs</name>
			<label kind="exponentialrate" x="40" y="168">1</label>
		</location>
		<init ref="id2"/>
		<transition id="id4">
			<source ref="id2"/>
			<target ref="id1"/>
			<label kind="guard" x="88" y="24">id== 0</label>
			<label kind="assignment" x="160" y="24">x = 0</label>
		</transition>
		<transition id="id5">
			<source ref="id1"/>
			<target ref="id0"/>
			<label kind="guard" x="144" y="72">x&lt;=k</label>
			<label kind="assignment" x="144" y="104">x = 0,
id = pid</label>
		</transition>
		<transition id="id6">
			<source ref="id0"/>
			<target ref="id1"/>
			<label kind="guard" x="264" y="120">id== 0</label>
			<label kind="assignment" x="264" y="88">x = 0</label>
			<nail x="251" y="146"/>
			<nail x="251" y="82"/>
		</transition>
		<transition id="id7">
			<source ref="id0"/>
			<target ref="id3"/>
			<label kind="guard" x="96" y="184">x&gt;k &amp;&amp; id==pid</label>
		</transition>
		<transition id="id8">
			<source ref="id3"/>
			<target ref="id2"/>
			<label kind="assignment" x="8" y="80">id = 0</label>
		</transition>
	</template>
	<system>system P;</system>
	<queries>
		<query>
			<formula>Pr[&lt;=300](&lt;&gt; P(1).cs)</formula>
			<comment>Fischer's mutual exclusion protocol.
			</comment>
		</query>
		<query>
			<formula>A[] forall (i:id_t) forall (j:id_t) P(i).cs &amp;&amp; P(j).cs imply i == j</formula>
			<comment>Mutex requirement.
			</comment>
		</query>
		<query>
			<formula>A[] not deadlock</formula>
			<comment>The system is deadlock free.
			</comment>
		</query>
		<query>
			<formula>P(1).req --&gt; P(1).wait</formula>
			<comment>Whenever P(1) requests access to the critical section it will eventually enter the wait state.
			</comment>
		</query>
	</queries>
</nta>
