mend

diff --git a/uppaal/2.xml b/uppaal/2.xml
index 153e6b9..862ab1e 100644 (file)
--- a/uppaal/2.xml
+++ b/uppaal/2.xml
@@ -9,20 +9,20 @@ const int N = 13;
 
 typedef int[0,N-1] id_c;
 
-broadcast chan up[N], down[N], left[N], right[N], start;
+broadcast chan up[N], down[N], left[N], right[N], start, leftRed, rightRed;
 
 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
+               <name x="5" y="5">HorzCar</name>\r
+               <parameter>int[2,3] length, const id_c id, int[0,4] x, const int[0,5] y</parameter>\r
                <declaration>// Place local declarations here.
 
 void register() {
     int i;
     for (i=0; i&lt;length; i++) {
-        grid[x][y+1] = true;
+        grid[x+i][y] = true;
     } 
 }</declaration>\r
                <location id="id0" x="-425" y="-51">\r
@@ -65,12 +65,12 @@ void register() {
                </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
+               <name>VertCar</name>\r
+               <parameter>int[2,3] length, const id_c id, const int[0,5] x, int[0,4] y</parameter>\r
                <declaration>void register() {
     int i;
     for(i=0; i&lt;length; i++){
-        grid[x+i][y] = true;
+        grid[x][y+i] = true;
     }
 }
 </declaration>\r
@@ -115,7 +115,6 @@ void register() {
        </template>\r
        <template>\r
                <name>Player</name>\r
-               <parameter>Template red</parameter>\r
                <declaration>int[0,N] registered;</declaration>\r
                <location id="id6" x="-680" y="-246">\r
                </location>\r
@@ -138,6 +137,51 @@ void register() {
                        <nail x="-765" y="-314"/>\r
                </transition>\r
        </template>\r
+       <template>\r
+               <name>RedCar</name>\r
+               <parameter>const id_c id, int[0,5] x</parameter>\r
+               <declaration>void register() {
+    grid[x][3] = true;
+    grid[x+1][3] = true;
+}</declaration>\r
+               <location id="id8" x="51" y="-59">\r
+               </location>\r
+               <location id="id9" x="-93" y="-68">\r
+               </location>\r
+               <location id="id10" x="-204" y="-68">\r
+                       <urgent/>\r
+               </location>\r
+               <init ref="id10"/>\r
+               <transition>\r
+                       <source ref="id8"/>\r
+                       <target ref="id8"/>\r
+                       <label kind="guard" x="-7" y="-42">x &gt; 0 &amp;&amp; grid[x-1][3]</label>\r
+                       <label kind="synchronisation" x="-7" y="-25">leftRed!</label>\r
+                       <label kind="assignment" x="-7" y="-8">x := x-1, grid[x+1][3] := false, grid[x-1][3] := true</label>\r
+                       <nail x="-25" y="42"/>\r
+                       <nail x="178" y="51"/>\r
+               </transition>\r
+               <transition>\r
+                       <source ref="id8"/>\r
+                       <target ref="id8"/>\r
+                       <label kind="guard" x="1" y="-135">x+2 &lt; 6 &amp;&amp; grid[x+2][3]</label>\r
+                       <label kind="synchronisation" x="1" y="-118">rightRed!</label>\r
+                       <label kind="assignment" x="1" y="-101">x := x+1, grid[x][3] := false, grid[x+2][3] := true</label>\r
+                       <nail x="-17" y="-144"/>\r
+                       <nail x="144" y="-136"/>\r
+               </transition>\r
+               <transition>\r
+                       <source ref="id9"/>\r
+                       <target ref="id8"/>\r
+                       <label kind="synchronisation" x="-75" y="-80">start?</label>\r
+               </transition>\r
+               <transition>\r
+                       <source ref="id10"/>\r
+                       <target ref="id9"/>\r
+                       <label kind="synchronisation" x="-186" y="-85">reg!</label>\r
+                       <label kind="assignment" x="-186" y="-68">register()</label>\r
+               </transition>\r
+       </template>\r
        <system>// Place template instantiations here.
 
 // Intermediate puzzle