Woep woep, 2 works for small example
authorpimjager <pim@pimjager.nl>
Thu, 16 Jun 2016 09:36:44 +0000 (11:36 +0200)
committerpimjager <pim@pimjager.nl>
Thu, 16 Jun 2016 09:36:44 +0000 (11:36 +0200)
uppaal/2.xml

index e45b155..25de23c 100644 (file)
@@ -106,7 +106,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 +163,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 +181,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 +231,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