From: pimjager <pim@pimjager.nl>
Date: Tue, 14 Jun 2016 09:29:58 +0000 (+0200)
Subject: kut rushhour spelletje
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=36c699606f794bcbe31bf2a1fd5eeaa7d97226d7;p=mc1516the.git

kut rushhour spelletje
---

diff --git a/uppaal/2.xml b/uppaal/2.xml
new file mode 100644
index 0000000..ad68966
--- /dev/null
+++ b/uppaal/2.xml
@@ -0,0 +1,81 @@
+<?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.
+
+const int N = 13;
+typedef int[0,N-1] id_c;
+
+chan up[N], down[N], left[N], right[N];</declaration>
+	<template>
+		<name x="5" y="5">VertCar</name>
+		<parameter>int[2,3] length, const id_c id, int[0,5] x, const int[0,4] y</parameter>
+		<declaration>// Place local declarations here.</declaration>
+		<location id="id0" x="-212" y="-76">
+		</location>
+		<init ref="id0"/>
+		<transition>
+			<source ref="id0"/>
+			<target ref="id0"/>
+			<label kind="guard" x="-288" y="-68">x&gt;0</label>
+			<label kind="synchronisation" x="-288" y="-51">down[id]!</label>
+			<label kind="assignment" x="-288" y="-34">x:=x-1</label>
+			<nail x="-306" y="8"/>
+			<nail x="-136" y="0"/>
+		</transition>
+		<transition>
+			<source ref="id0"/>
+			<target ref="id0"/>
+			<label kind="guard" x="-306" y="-204">x+length &lt; 6</label>
+			<label kind="synchronisation" x="-314" y="-153">up[id]!</label>
+			<label kind="assignment" x="-306" y="-178">x:=x+1</label>
+			<nail x="-323" y="-102"/>
+			<nail x="-195" y="-178"/>
+			<nail x="-110" y="-102"/>
+		</transition>
+	</template>
+	<template>
+		<name>HorzCar</name>
+		<parameter>int[2,3] length, const id_c id, const int[0,4] x, int[0,5] y</parameter>
+		<location id="id1" x="-102" y="-34">
+		</location>
+		<init ref="id1"/>
+		<transition>
+			<source ref="id1"/>
+			<target ref="id1"/>
+			<label kind="guard" x="-135" y="8">y&gt;0</label>
+			<label kind="synchronisation" x="-135" y="25">left[id]!</label>
+			<label kind="assignment" x="-135" y="42">y:=y-1</label>
+			<nail x="-153" y="42"/>
+			<nail x="-34" y="42"/>
+		</transition>
+		<transition>
+			<source ref="id1"/>
+			<target ref="id1"/>
+			<label kind="guard" x="-160" y="-102">y+length &lt; 6</label>
+			<label kind="synchronisation" x="-160" y="-85">right[id]!</label>
+			<label kind="assignment" x="-160" y="-68">y:=y+1</label>
+			<nail x="-178" y="-102"/>
+			<nail x="-34" y="-102"/>
+		</transition>
+	</template>
+	<system>// Place template instantiations here.
+H1 = HorzCar(2, 0, 0, 5);
+H2 = HorzCar(2, 1, 2, 5);
+V3 = VertCar(2, 2, 4, 4);
+V4 = VertCar(2, 3, 2, 3);
+V5 = VertCar(3, 4, 5, 2);
+V6 = VertCar(2, 5, 1, 3);
+H7 = HorzCar(2, 6, 3, 4);
+H8 = HorzCar(2, 7, 3, 2);
+V9 = VertCar(3, 8, 0, 0);
+HA = HorzCar(2, 9, 1, 0);
+VB = VertCar(2, 10, 3, 0);
+HC = HorzCar(2, 11, 4, 1);
+HD = HorzCar(2, 12, 4, 0);
+// List one or more processes to be composed into a system.
+system H1, H2, V3, V4, V5, V6, H7, H8, V9, HA, VB, HC, HD;
+    </system>
+	<queries>
+	</queries>
+</nta>