X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=uppaal%2F2.xml;h=dcbd6c3fa8407b0143f20d8c60941afcf1ccc383;hb=ed285902eb72f2b491b64c82c3bed5a24a50b3b0;hp=0f68e2cef3ed30cc91fac2b316665df4d9332006;hpb=9fb20990d15588f3042851886b4dd4b6b662d0d4;p=mc1516the.git

diff --git a/uppaal/2.xml b/uppaal/2.xml
index 0f68e2c..dcbd6c3 100644
--- a/uppaal/2.xml
+++ b/uppaal/2.xml
@@ -52,7 +52,7 @@ void register() {
 			<source ref="id2"/>
 			<target ref="id2"/>
 			<label kind="guard" x="-280" y="8">x&gt;0 &amp;&amp; !grid[x-1][y]</label>
-			<label kind="synchronisation" x="-246" y="102">left[id]!</label>
+			<label kind="synchronisation" x="-153" y="-42">left[id]!</label>
 			<label kind="assignment" x="-340" y="34">grid[x+length-1][y]:=false,
 grid[x-1][y]:=true,
 x:=x-1</label>
@@ -63,7 +63,7 @@ x:=x-1</label>
 			<source ref="id2"/>
 			<target ref="id2"/>
 			<label kind="guard" x="-306" y="-263">x+length &lt; 6 &amp;&amp; !grid[x+length][y]</label>
-			<label kind="synchronisation" x="-221" y="-204">right[id]!</label>
+			<label kind="synchronisation" x="-170" y="-170">right[id]!</label>
 			<label kind="assignment" x="-331" y="-229">grid[x][y]:=false,
 grid[x+length][y]:=true,
 x:=x+1</label>
@@ -93,7 +93,7 @@ x:=x+1</label>
 		<transition>
 			<source ref="id3"/>
 			<target ref="id5"/>
-			<label kind="synchronisation" x="-228" y="-72">start?</label>
+			<label kind="synchronisation" x="-246" y="-59">start?</label>
 		</transition>
 		<transition>
 			<source ref="id4"/>
@@ -105,9 +105,9 @@ x:=x+1</label>
 		<transition>
 			<source ref="id5"/>
 			<target ref="id5"/>
-			<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,
+			<label kind="guard" x="-153" y="153">y&gt;0 &amp;&amp; !grid[x][y-1]</label>
+			<label kind="synchronisation" x="-153" y="119">down[id]!</label>
+			<label kind="assignment" x="-153" y="51">grid[x][y-1]:=true,
 grid[x][y+length-1]:=false,
 y:=y-1</label>
 			<nail x="-153" y="42"/>
@@ -116,9 +116,9 @@ y:=y-1</label>
 		<transition>
 			<source ref="id5"/>
 			<target ref="id5"/>
-			<label kind="guard" x="-204" y="-221">y+length &lt; 6 &amp;&amp; !grid[x][y+length]</label>
-			<label kind="synchronisation" x="-127" y="-195">up[id]!</label>
-			<label kind="assignment" x="-263" y="-161">grid[x][y+length]:=true,
+			<label kind="guard" x="-161" y="-204">y+length &lt; 6 &amp;&amp; !grid[x][y+length]</label>
+			<label kind="synchronisation" x="-161" y="-178">up[id]!</label>
+			<label kind="assignment" x="-161" y="-153">grid[x][y+length]:=true,
 grid[x][y]:=false,
 y:=y+1</label>
 			<nail x="-178" y="-102"/>
@@ -129,33 +129,33 @@ y:=y+1</label>
 		<name>Player</name>
 		<declaration>int[0,N] registered;
 bool done = 0;</declaration>
-		<location id="id6" x="-493" y="-255">
+		<location id="id6" x="-476" y="-459">
 		</location>
-		<location id="id7" x="-680" y="-246">
+		<location id="id7" x="-663" y="-450">
 		</location>
-		<location id="id8" x="-799" y="-246">
+		<location id="id8" x="-782" y="-450">
 		</location>
 		<init ref="id8"/>
 		<transition>
 			<source ref="id7"/>
 			<target ref="id6"/>
-			<label kind="synchronisation" x="-629" y="-272">finish?</label>
-			<label kind="assignment" x="-662" y="-250">done := 1</label>
+			<label kind="synchronisation" x="-612" y="-476">finish?</label>
+			<label kind="assignment" x="-645" y="-454">done := 1</label>
 		</transition>
 		<transition>
 			<source ref="id8"/>
 			<target ref="id7"/>
-			<label kind="guard" x="-781" y="-280">registered == N</label>
-			<label kind="synchronisation" x="-781" y="-263">start!</label>
+			<label kind="guard" x="-764" y="-484">registered == N</label>
+			<label kind="synchronisation" x="-764" y="-467">start!</label>
 		</transition>
 		<transition>
 			<source ref="id8"/>
 			<target ref="id8"/>
-			<label kind="synchronisation" x="-875" y="-365">reg?</label>
-			<label kind="assignment" x="-926" y="-382">registered := registered+1</label>
-			<nail x="-892" y="-263"/>
-			<nail x="-833" y="-331"/>
-			<nail x="-765" y="-314"/>
+			<label kind="synchronisation" x="-833" y="-561">reg?</label>
+			<label kind="assignment" x="-909" y="-578">registered := registered+1</label>
+			<nail x="-875" y="-467"/>
+			<nail x="-816" y="-535"/>
+			<nail x="-748" y="-518"/>
 		</transition>
 	</template>
 	<template>
@@ -216,7 +216,7 @@ x:=x-1</label>
 		<transition>
 			<source ref="id15"/>
 			<target ref="id9"/>
-			<label kind="probability" x="127" y="34">1</label>
+			<label kind="probability" x="161" y="-34">1</label>
 		</transition>
 		<transition>
 			<source ref="id15"/>