kut rushhour spelletje
authorpimjager <pim@pimjager.nl>
Tue, 14 Jun 2016 09:29:58 +0000 (11:29 +0200)
committerpimjager <pim@pimjager.nl>
Tue, 14 Jun 2016 09:29:58 +0000 (11:29 +0200)
uppaal/2.xml [new file with mode: 0644]

diff --git a/uppaal/2.xml b/uppaal/2.xml
new file mode 100644 (file)
index 0000000..ad68966
--- /dev/null
@@ -0,0 +1,81 @@
+<?xml version="1.0" encoding="utf-8"?>\r
+<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>\r
+<nta>\r
+       <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>\r
+       <template>\r
+               <name x="5" y="5">VertCar</name>\r
+               <parameter>int[2,3] length, const id_c id, int[0,5] x, const int[0,4] y</parameter>\r
+               <declaration>// Place local declarations here.</declaration>\r
+               <location id="id0" x="-212" y="-76">\r
+               </location>\r
+               <init ref="id0"/>\r
+               <transition>\r
+                       <source ref="id0"/>\r
+                       <target ref="id0"/>\r
+                       <label kind="guard" x="-288" y="-68">x&gt;0</label>\r
+                       <label kind="synchronisation" x="-288" y="-51">down[id]!</label>\r
+                       <label kind="assignment" x="-288" y="-34">x:=x-1</label>\r
+                       <nail x="-306" y="8"/>\r
+                       <nail x="-136" y="0"/>\r
+               </transition>\r
+               <transition>\r
+                       <source ref="id0"/>\r
+                       <target ref="id0"/>\r
+                       <label kind="guard" x="-306" y="-204">x+length &lt; 6</label>\r
+                       <label kind="synchronisation" x="-314" y="-153">up[id]!</label>\r
+                       <label kind="assignment" x="-306" y="-178">x:=x+1</label>\r
+                       <nail x="-323" y="-102"/>\r
+                       <nail x="-195" y="-178"/>\r
+                       <nail x="-110" y="-102"/>\r
+               </transition>\r
+       </template>\r
+       <template>\r
+               <name>HorzCar</name>\r
+               <parameter>int[2,3] length, const id_c id, const int[0,4] x, int[0,5] y</parameter>\r
+               <location id="id1" x="-102" y="-34">\r
+               </location>\r
+               <init ref="id1"/>\r
+               <transition>\r
+                       <source ref="id1"/>\r
+                       <target ref="id1"/>\r
+                       <label kind="guard" x="-135" y="8">y&gt;0</label>\r
+                       <label kind="synchronisation" x="-135" y="25">left[id]!</label>\r
+                       <label kind="assignment" x="-135" y="42">y:=y-1</label>\r
+                       <nail x="-153" y="42"/>\r
+                       <nail x="-34" y="42"/>\r
+               </transition>\r
+               <transition>\r
+                       <source ref="id1"/>\r
+                       <target ref="id1"/>\r
+                       <label kind="guard" x="-160" y="-102">y+length &lt; 6</label>\r
+                       <label kind="synchronisation" x="-160" y="-85">right[id]!</label>\r
+                       <label kind="assignment" x="-160" y="-68">y:=y+1</label>\r
+                       <nail x="-178" y="-102"/>\r
+                       <nail x="-34" y="-102"/>\r
+               </transition>\r
+       </template>\r
+       <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>\r
+       <queries>\r
+       </queries>\r
+</nta>\r