From: pimjager <pim@pimjager.nl>
Date: Thu, 16 Jun 2016 09:36:44 +0000 (+0200)
Subject: Woep woep, 2 works for small example
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=fc8b6c60a2187cb452e91441b3cd18e116d86d2e;p=mc1516the.git

Woep woep, 2 works for small example
---

diff --git a/uppaal/2.xml b/uppaal/2.xml
index e45b155..25de23c 100644
--- a/uppaal/2.xml
+++ b/uppaal/2.xml
@@ -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>
 			<label kind="synchronisation" x="-119" y="119">down[id]!</label>
 			<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>
 			<nail x="-153" y="42"/>
 			<nail x="-34" y="42"/>
@@ -163,10 +163,10 @@ bool done = 0;</declaration>
     grid[x][3] = true;
     grid[x+1][3] = true;
 }</declaration>
-		<location id="id9" x="238" y="34">
+		<location id="id9" x="42" y="136">
 			<urgent/>
 		</location>
-		<location id="id10" x="221" y="-153">
+		<location id="id10" x="59" y="-238">
 			<urgent/>
 		</location>
 		<location id="id11" x="493" y="-51">
@@ -181,23 +181,45 @@ bool done = 0;</declaration>
 		<branchpoint id="id15" x="187" y="-85">
 		</branchpoint>
 		<init ref="id14"/>
+		<transition>
+			<source ref="id9"/>
+			<target ref="id12"/>
+			<label kind="guard" x="67" y="38">x &lt;= 0 || grid[x-1][3]</label>
+			<nail x="93" y="8"/>
+		</transition>
+		<transition>
+			<source ref="id10"/>
+			<target ref="id12"/>
+			<label kind="guard" x="93" y="-187">x+2 &gt;= 6 || grid[x+2][3]</label>
+			<nail x="102" y="-127"/>
+		</transition>
 		<transition>
 			<source ref="id10"/>
 			<target ref="id12"/>
+			<label kind="guard" x="-136" y="-161">x+2 &lt; 6 &amp;&amp; !grid[x+2][3]</label>
+			<label kind="synchronisation" x="-68" y="-144">rightRed!</label>
+			<label kind="assignment" x="-85" y="-212">grid[x][3]:=false,
+grid[x+2][3]:=true,
+x:=x+1</label>
 		</transition>
 		<transition>
 			<source ref="id9"/>
 			<target ref="id12"/>
+			<label kind="guard" x="-144" y="-25">x &gt; 0 &amp;&amp; !grid[x-1][3]</label>
+			<label kind="synchronisation" x="-93" y="0">leftRed!</label>
+			<label kind="assignment" x="-144" y="25">grid[x+1][3]:=false,
+grid[x-1][3]:=true,
+x:=x-1</label>
 		</transition>
 		<transition>
 			<source ref="id15"/>
 			<target ref="id9"/>
-			<label kind="probability" x="212" y="-25">1</label>
+			<label kind="probability" x="127" y="34">1</label>
 		</transition>
 		<transition>
 			<source ref="id15"/>
 			<target ref="id10"/>
-			<label kind="probability" x="204" y="-119">3</label>
+			<label kind="probability" x="178" y="-127">3</label>
 		</transition>
 		<transition>
 			<source ref="id12"/>
@@ -209,28 +231,6 @@ bool done = 0;</declaration>
 			<label kind="guard" x="416" y="-93">x == 4</label>
 			<label kind="synchronisation" x="416" y="-76">finish!</label>
 		</transition>
-		<transition>
-			<source ref="id12"/>
-			<target ref="id12"/>
-			<label kind="guard" x="0" y="161">x &gt; 0 &amp;&amp; !grid[x-1][3]</label>
-			<label kind="synchronisation" x="25" y="119">leftRed!</label>
-			<label kind="assignment" x="-85" y="85">grid[x+1][3]:=false,
-grid[x-1][3]:=true,
-x:=x-1</label>
-			<nail x="-25" y="42"/>
-			<nail x="178" y="51"/>
-		</transition>
-		<transition>
-			<source ref="id12"/>
-			<target ref="id12"/>
-			<label kind="guard" x="-17" y="-255">x+2 &lt; 6 &amp;&amp; !grid[x+2][3]</label>
-			<label kind="synchronisation" x="25" y="-221">rightRed!</label>
-			<label kind="assignment" x="-85" y="-187">grid[x][3]:=false,
-grid[x+2][3]:=true,
-x:=x+1</label>
-			<nail x="-17" y="-144"/>
-			<nail x="144" y="-136"/>
-		</transition>
 		<transition>
 			<source ref="id13"/>
 			<target ref="id12"/>