From: pimjager <pim@pimjager.nl>
Date: Tue, 14 Jun 2016 08:23:50 +0000 (+0200)
Subject: Uppaalmodel of train gate
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=8fda60e79520d70eb130ba08ef48f67df9b60886;p=mc1516the.git

Uppaalmodel of train gate
---

diff --git a/uppaal/traingate.xml b/uppaal/traingate.xml
new file mode 100644
index 0000000..33f0fde
--- /dev/null
+++ b/uppaal/traingate.xml
@@ -0,0 +1,176 @@
+<?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.
+clock x, y, z;
+
+chan approach, in, out, ex, lower, raise, down, up;</declaration>
+	<template>
+		<name x="5" y="5">Train</name>
+		<declaration>// Place local declarations here.</declaration>
+		<location id="id0" x="-119" y="17">
+			<name x="-187" y="-17">safe</name>
+			<label kind="invariant" x="-187" y="17">x&lt;=5</label>
+		</location>
+		<location id="id1" x="8" y="17">
+			<name x="-2" y="-17">unsafe</name>
+			<label kind="invariant" x="-2" y="34">x&lt;=5</label>
+		</location>
+		<location id="id2" x="0" y="-110">
+			<name x="-10" y="-144">aproaching</name>
+			<label kind="invariant" x="25" y="-136">x&lt;=5</label>
+		</location>
+		<location id="id3" x="-127" y="-102">
+			<name x="-137" y="-136">initial</name>
+		</location>
+		<init ref="id3"/>
+		<transition>
+			<source ref="id0"/>
+			<target ref="id3"/>
+			<label kind="synchronisation" x="-119" y="-59">ex!</label>
+		</transition>
+		<transition>
+			<source ref="id1"/>
+			<target ref="id0"/>
+			<label kind="synchronisation" x="-101" y="0">out!</label>
+		</transition>
+		<transition>
+			<source ref="id2"/>
+			<target ref="id1"/>
+			<label kind="guard" x="4" y="-80">x&gt;2</label>
+			<label kind="synchronisation" x="4" y="-63">in!</label>
+		</transition>
+		<transition>
+			<source ref="id3"/>
+			<target ref="id2"/>
+			<label kind="synchronisation" x="-102" y="-127">approach!</label>
+			<label kind="assignment" x="-93" y="-102">x:=0</label>
+		</transition>
+	</template>
+	<template>
+		<name>Stupid</name>
+		<location id="id4" x="0" y="0">
+		</location>
+		<init ref="id4"/>
+		<transition>
+			<source ref="id4"/>
+			<target ref="id4"/>
+			<label kind="synchronisation" x="-119" y="-59">in?</label>
+			<nail x="-68" y="-85"/>
+			<nail x="-85" y="-8"/>
+		</transition>
+		<transition>
+			<source ref="id4"/>
+			<target ref="id4"/>
+			<label kind="synchronisation" x="93" y="-17">out?</label>
+			<nail x="93" y="-59"/>
+			<nail x="85" y="42"/>
+		</transition>
+		<transition>
+			<source ref="id4"/>
+			<target ref="id4"/>
+			<label kind="synchronisation" x="-67" y="4">down?</label>
+			<nail x="-85" y="42"/>
+			<nail x="25" y="68"/>
+		</transition>
+		<transition>
+			<source ref="id4"/>
+			<target ref="id4"/>
+			<label kind="synchronisation" x="1" y="-85">up?</label>
+			<nail x="-17" y="-68"/>
+			<nail x="68" y="-68"/>
+		</transition>
+	</template>
+	<template>
+		<name>Gate</name>
+		<location id="id5" x="-204" y="-25">
+			<name x="-246" y="0">raising</name>
+			<label kind="invariant" x="-274" y="-33">y&lt;=2</label>
+		</location>
+		<location id="id6" x="-42" y="-25">
+			<name x="-34" y="8">lowered</name>
+		</location>
+		<location id="id7" x="-42" y="-161">
+			<name x="-52" y="-195">lowering</name>
+			<label kind="invariant" x="-25" y="-161">y&lt;=1</label>
+		</location>
+		<location id="id8" x="-204" y="-161">
+			<name x="-214" y="-195">raised</name>
+		</location>
+		<init ref="id8"/>
+		<transition>
+			<source ref="id5"/>
+			<target ref="id8"/>
+			<label kind="guard" x="-191" y="-127">y&gt;=1</label>
+			<label kind="synchronisation" x="-178" y="-110">up!</label>
+		</transition>
+		<transition>
+			<source ref="id6"/>
+			<target ref="id5"/>
+			<label kind="synchronisation" x="-160" y="-42">raise?</label>
+			<label kind="assignment" x="-160" y="-25">y:=0</label>
+		</transition>
+		<transition>
+			<source ref="id7"/>
+			<target ref="id6"/>
+			<label kind="synchronisation" x="-42" y="-110">down!</label>
+		</transition>
+		<transition>
+			<source ref="id8"/>
+			<target ref="id7"/>
+			<label kind="synchronisation" x="-160" y="-178">lower?</label>
+			<label kind="assignment" x="-160" y="-161">y:=0</label>
+		</transition>
+	</template>
+	<template>
+		<name>Controller</name>
+		<location id="id9" x="187" y="-68">
+			<name x="177" y="-102">trainComing</name>
+			<label kind="invariant" x="229" y="-76">z&lt;=1</label>
+		</location>
+		<location id="id10" x="-153" y="-76">
+			<name x="-229" y="-51">trainLeaving</name>
+			<label kind="invariant" x="-221" y="-85">z &lt;= 1</label>
+		</location>
+		<location id="id11" x="-8" y="-76">
+		</location>
+		<init ref="id11"/>
+		<transition>
+			<source ref="id10"/>
+			<target ref="id11"/>
+			<label kind="synchronisation" x="-143" y="-178">raise!</label>
+			<nail x="-161" y="-161"/>
+			<nail x="-17" y="-161"/>
+		</transition>
+		<transition>
+			<source ref="id11"/>
+			<target ref="id10"/>
+			<label kind="synchronisation" x="-135" y="-93">ex?</label>
+			<label kind="assignment" x="-135" y="-76">z:=0</label>
+		</transition>
+		<transition>
+			<source ref="id9"/>
+			<target ref="id11"/>
+			<label kind="guard" x="10" y="-22">z==1</label>
+			<label kind="synchronisation" x="10" y="-5">lower!</label>
+			<nail x="187" y="17"/>
+			<nail x="-8" y="8"/>
+		</transition>
+		<transition>
+			<source ref="id11"/>
+			<target ref="id9"/>
+			<label kind="synchronisation" x="10" y="-89">approach?</label>
+			<label kind="assignment" x="10" y="-72">z:=0</label>
+		</transition>
+	</template>
+	<system>// Place template instantiations here.
+T = Train();
+G = Gate();
+C = Controller();
+Gezeik = Stupid();
+// List one or more processes to be composed into a system.
+system T, G, C, Gezeik;
+    </system>
+	<queries>
+	</queries>
+</nta>