Gaat de goede kant op

diff --git a/uppaal/2.xml b/uppaal/2.xml
index 7091457..153e6b9 100644 (file)
--- a/uppaal/2.xml
+++ b/uppaal/2.xml
@@ -9,27 +9,54 @@ const int N = 13;
 
 typedef int[0,N-1] id_c;
 
-chan up[N], down[N], left[N], right[N];</declaration>\r
+broadcast chan up[N], down[N], left[N], right[N], start;
+
+chan reg;
+
+bool grid[6][6];</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
+               <declaration>// Place local declarations here.
+
+void register() {
+    int i;
+    for (i=0; i&lt;length; i++) {
+        grid[x][y+1] = true;
+    } 
+}</declaration>\r
+               <location id="id0" x="-425" y="-51">\r
+               </location>\r
+               <location id="id1" x="-535" y="-136">\r
+                       <urgent/>\r
                </location>\r
-               <init ref="id0"/>\r
+               <location id="id2" x="-212" y="-76">\r
+               </location>\r
+               <init ref="id1"/>\r
                <transition>\r
                        <source ref="id0"/>\r
+                       <target ref="id2"/>\r
+                       <label kind="synchronisation" x="-407" y="-80">start?</label>\r
+               </transition>\r
+               <transition>\r
+                       <source ref="id1"/>\r
                        <target ref="id0"/>\r
-                       <label kind="guard" x="-288" y="-68">x&gt;0</label>\r
+                       <label kind="synchronisation" x="-517" y="-110">reg!</label>\r
+                       <label kind="assignment" x="-517" y="-93">register()</label>\r
+               </transition>\r
+               <transition>\r
+                       <source ref="id2"/>\r
+                       <target ref="id2"/>\r
+                       <label kind="guard" x="-288" y="-68">x&gt;0 &amp;&amp; !grid[x-1][y]</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
+                       <source ref="id2"/>\r
+                       <target ref="id2"/>\r
+                       <label kind="guard" x="-306" y="-204">x+length &lt; 6 &amp;&amp; !grid[x+length][y]</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
@@ -40,22 +67,46 @@ chan up[N], down[N], left[N], right[N];</declaration>
        <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
+               <declaration>void register() {
+    int i;
+    for(i=0; i&lt;length; i++){
+        grid[x+i][y] = true;
+    }
+}
+</declaration>\r
+               <location id="id3" x="-314" y="-34">\r
                </location>\r
-               <init ref="id1"/>\r
+               <location id="id4" x="-416" y="-76">\r
+                       <urgent/>\r
+               </location>\r
+               <location id="id5" x="-102" y="-34">\r
+               </location>\r
+               <init ref="id4"/>\r
                <transition>\r
-                       <source ref="id1"/>\r
-                       <target ref="id1"/>\r
-                       <label kind="guard" x="-135" y="8">y&gt;0</label>\r
+                       <source ref="id3"/>\r
+                       <target ref="id5"/>\r
+                       <label kind="synchronisation" x="-228" y="-72">start?</label>\r
+               </transition>\r
+               <transition>\r
+                       <source ref="id4"/>\r
+                       <target ref="id3"/>\r
+                       <label kind="synchronisation" x="-374" y="-110">reg!</label>\r
+                       <label kind="assignment" x="-374" y="-76">register()</label>\r
+                       <nail x="-255" y="-85"/>\r
+               </transition>\r
+               <transition>\r
+                       <source ref="id5"/>\r
+                       <target ref="id5"/>\r
+                       <label kind="guard" x="-135" y="8">y&gt;0 &amp;&amp; !grid[x][y-1]</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
+                       <source ref="id5"/>\r
+                       <target ref="id5"/>\r
+                       <label kind="guard" x="-160" y="-102">y+length &lt; 6 &amp;&amp; !grid[x][y+length]</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
@@ -64,9 +115,28 @@ chan up[N], down[N], left[N], right[N];</declaration>
        </template>\r
        <template>\r
                <name>Player</name>\r
-               <location id="id2" x="-476" y="-178">\r
+               <parameter>Template red</parameter>\r
+               <declaration>int[0,N] registered;</declaration>\r
+               <location id="id6" x="-680" y="-246">\r
+               </location>\r
+               <location id="id7" x="-799" y="-246">\r
                </location>\r
-               <init ref="id2"/>\r
+               <init ref="id7"/>\r
+               <transition>\r
+                       <source ref="id7"/>\r
+                       <target ref="id6"/>\r
+                       <label kind="guard" x="-781" y="-280">registered == N</label>\r
+                       <label kind="synchronisation" x="-781" y="-263">start!</label>\r
+               </transition>\r
+               <transition>\r
+                       <source ref="id7"/>\r
+                       <target ref="id7"/>\r
+                       <label kind="synchronisation" x="-875" y="-365">reg?</label>\r
+                       <label kind="assignment" x="-926" y="-382">registered := registered+1</label>\r
+                       <nail x="-892" y="-263"/>\r
+                       <nail x="-833" y="-331"/>\r
+                       <nail x="-765" y="-314"/>\r
+               </transition>\r
        </template>\r
        <system>// Place template instantiations here.
 
@@ -84,7 +154,7 @@ HA = HorzCar(2, 9, 1, 0);
 VB = VertCar(2, 10, 3, 0);
 HC = HorzCar(2, 11, 4, 1);
 HD = HorzCar(2, 12, 4, 0);
-system H1, H2, V3, V4, V5, V6, H7, H8, V9, HA, VB, HC, HD;
+system H1, H2, V3, V4, V5, V6, H7, H8, V9, HA, VB, HC, HD, Player;
 
 // Advanced puzzle
 /*