repositories / mc1516the.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
working exercise2
[mc1516the.git] / uppaal / 2.xml
diff --git a/uppaal/2.xml b/uppaal/2.xml
index e45b155..0f68e2c 100644 (file)
--- a/uppaal/2.xml
+++ b/uppaal/2.xml
@@ -6,8 +6,10 @@
 //const int N=13;
 // Advanced
 //const int N = 7;
-//easy test puzzle
-const int N=3;
+//hard from website 1
+const int N=13;
+//hard from website 2
+//const int N=9;
 
 typedef int[0, N-1] id_c;
 
@@ -106,7 +108,7 @@ x:=x+1</label>
                        <label kind="guard" x="-170" y="153">y&gt;0 &amp;&amp; !grid[x][y-1]</label>\r
                        <label kind="synchronisation" x="-119" y="119">down[id]!</label>\r
                        <label kind="assignment" x="-221" y="51">grid[x][y-1]:=true,
-grid[x][y+length-1]:=true,
+grid[x][y+length-1]:=false,
 y:=y-1</label>\r
                        <nail x="-153" y="42"/>\r
                        <nail x="-34" y="42"/>\r
@@ -163,10 +165,10 @@ bool done = 0;</declaration>
     grid[x][3] = true;
     grid[x+1][3] = true;
 }</declaration>\r
-               <location id="id9" x="238" y="34">\r
+               <location id="id9" x="42" y="136">\r
                        <urgent/>\r
                </location>\r
-               <location id="id10" x="221" y="-153">\r
+               <location id="id10" x="59" y="-238">\r
                        <urgent/>\r
                </location>\r
                <location id="id11" x="493" y="-51">\r
@@ -181,23 +183,45 @@ bool done = 0;</declaration>
                <branchpoint id="id15" x="187" y="-85">\r
                </branchpoint>\r
                <init ref="id14"/>\r
+               <transition>\r
+                       <source ref="id9"/>\r
+                       <target ref="id12"/>\r
+                       <label kind="guard" x="67" y="38">x &lt;= 0 || grid[x-1][3]</label>\r
+                       <nail x="93" y="8"/>\r
+               </transition>\r
+               <transition>\r
+                       <source ref="id10"/>\r
+                       <target ref="id12"/>\r
+                       <label kind="guard" x="93" y="-187">x+2 &gt;= 6 || grid[x+2][3]</label>\r
+                       <nail x="102" y="-127"/>\r
+               </transition>\r
                <transition>\r
                        <source ref="id10"/>\r
                        <target ref="id12"/>\r
+                       <label kind="guard" x="-136" y="-161">x+2 &lt; 6 &amp;&amp; !grid[x+2][3]</label>\r
+                       <label kind="synchronisation" x="-68" y="-144">rightRed!</label>\r
+                       <label kind="assignment" x="-85" y="-212">grid[x][3]:=false,
+grid[x+2][3]:=true,
+x:=x+1</label>\r
                </transition>\r
                <transition>\r
                        <source ref="id9"/>\r
                        <target ref="id12"/>\r
+                       <label kind="guard" x="-144" y="-25">x &gt; 0 &amp;&amp; !grid[x-1][3]</label>\r
+                       <label kind="synchronisation" x="-93" y="0">leftRed!</label>\r
+                       <label kind="assignment" x="-144" y="25">grid[x+1][3]:=false,
+grid[x-1][3]:=true,
+x:=x-1</label>\r
                </transition>\r
                <transition>\r
                        <source ref="id15"/>\r
                        <target ref="id9"/>\r
-                       <label kind="probability" x="212" y="-25">1</label>\r
+                       <label kind="probability" x="127" y="34">1</label>\r
                </transition>\r
                <transition>\r
                        <source ref="id15"/>\r
                        <target ref="id10"/>\r
-                       <label kind="probability" x="204" y="-119">3</label>\r
+                       <label kind="probability" x="178" y="-127">3</label>\r
                </transition>\r
                <transition>\r
                        <source ref="id12"/>\r
@@ -209,28 +233,6 @@ bool done = 0;</declaration>
                        <label kind="guard" x="416" y="-93">x == 4</label>\r
                        <label kind="synchronisation" x="416" y="-76">finish!</label>\r
                </transition>\r
-               <transition>\r
-                       <source ref="id12"/>\r
-                       <target ref="id12"/>\r
-                       <label kind="guard" x="0" y="161">x &gt; 0 &amp;&amp; !grid[x-1][3]</label>\r
-                       <label kind="synchronisation" x="25" y="119">leftRed!</label>\r
-                       <label kind="assignment" x="-85" y="85">grid[x+1][3]:=false,
-grid[x-1][3]:=true,
-x:=x-1</label>\r
-                       <nail x="-25" y="42"/>\r
-                       <nail x="178" y="51"/>\r
-               </transition>\r
-               <transition>\r
-                       <source ref="id12"/>\r
-                       <target ref="id12"/>\r
-                       <label kind="guard" x="-17" y="-255">x+2 &lt; 6 &amp;&amp; !grid[x+2][3]</label>\r
-                       <label kind="synchronisation" x="25" y="-221">rightRed!</label>\r
-                       <label kind="assignment" x="-85" y="-187">grid[x][3]:=false,
-grid[x+2][3]:=true,
-x:=x+1</label>\r
-                       <nail x="-17" y="-144"/>\r
-                       <nail x="144" y="-136"/>\r
-               </transition>\r
                <transition>\r
                        <source ref="id13"/>\r
                        <target ref="id12"/>\r
@@ -248,13 +250,15 @@ x:=x+1</label>
 
 
 //easy test puzzle
+/*
 RED = RedCar(0,2);
 V1 = VertCar(2, 1, 4, 3);
 V2 = VertCar(3, 2, 5, 2);
 system RED, V1, V2, Player;
+*/
 
 // Intermediate puzzle
-/*
+
 H1 = HorzCar(2, 0, 0, 5);
 H2 = HorzCar(2, 1, 2, 5);
 V3 = VertCar(2, 2, 4, 4);
@@ -269,7 +273,7 @@ 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, RED, V9, HA, VB, HC, HD, Player;
-*/
+
 
 // Advanced puzzle
 /*
@@ -277,12 +281,44 @@ H1 = HorzCar(2, 0, 0, 5);
 V2 = VertCar(2, 1, 2, 4);
 V3 = VertCar(3, 2, 3, 3);
 V4 = VertCar(3, 3, 0, 2);
-H5 = HorzCar(2, 4, 1, 3);
+RED = RedCar(4, 1);
 H6 = HorzCar(3, 5, 1, 2);
 H7 = HorzCar(3, 6, 3, 0);
-system H1, V2, V3, V4, H5, H6, H7
+system H1, V2, V3, V4, RED, H6, H7, Player;
 */
-    </system>\r
+
+//Hard from website 1
+//Can not be solved
+/*
+V1 = VertCar(2, 0, 0, 3);
+V2 = VertCar(2, 1, 1, 0);
+V3 = VertCar(2, 2, 2, 1);
+V4 = VertCar(2, 3, 3, 4);
+V5 = VertCar(3, 4, 4, 3);
+V6 = VertCar(3, 5, 5, 3);
+H7 = HorzCar(2, 6, 0, 2);
+H8 = HorzCar(3, 7, 0, 5);
+H85= HorzCar(3,12, 1, 4); 
+H9 = HorzCar(2, 8, 2, 0);
+RED = RedCar(9, 2);
+HB = HorzCar(2,10, 4, 0);
+HC = HorzCar(2,11, 4, 1);
+system V1, V2, V3, V4, V5, V6, H7, H8, H85, H9, RED, HB, HC, Player;
+*/
+
+//Hard from website 2
+/*
+V1 = VertCar(2, 0, 0, 0);
+V2 = VertCar(3, 1, 2, 3);
+V3 = VertCar(3, 2, 3, 0);
+V4 = VertCar(3, 3, 5, 3);
+H5 = HorzCar(2, 4, 1, 1);
+RED = RedCar(5, 3);
+H7 = HorzCar(2, 6, 3, 5);
+H8 = HorzCar(2, 7, 4, 0);
+H9 = HorzCar(2, 8, 4, 2);
+system V1, V2, V3, V4, H5, RED, H7, H8, H9, Player;
+*/</system>\r
        <queries>\r
                <query>\r
                        <formula>E&lt;&gt; Player.done == 1\r