From 53484c4fd63f80db558d9c0a4f00b3e8e61f2db2 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 14 Jun 2016 13:10:06 +0200
Subject: [PATCH] ding

---
 uppaal/2.xml | 111 +++++++++++++++++++++++++++++++++------------------
 1 file changed, 73 insertions(+), 38 deletions(-)

diff --git a/uppaal/2.xml b/uppaal/2.xml
index 862ab1e..29e4e8f 100644
--- a/uppaal/2.xml
+++ b/uppaal/2.xml
@@ -11,7 +11,7 @@ typedef int[0,N-1] id_c;
 
 broadcast chan up[N], down[N], left[N], right[N], start, leftRed, rightRed;
 
-chan reg;
+chan reg, finish;
 
 bool grid[6][6];</declaration>
 	<template>
@@ -47,18 +47,22 @@ void register() {
 		<transition>
 			<source ref="id2"/>
 			<target ref="id2"/>
-			<label kind="guard" x="-288" y="-68">x&gt;0 &amp;&amp; !grid[x-1][y]</label>
-			<label kind="synchronisation" x="-288" y="-51">down[id]!</label>
-			<label kind="assignment" x="-288" y="-34">x:=x-1</label>
+			<label kind="guard" x="-280" y="8">x&gt;0 &amp;&amp; !grid[x-1][y]</label>
+			<label kind="synchronisation" x="-246" y="102">down[id]!</label>
+			<label kind="assignment" x="-340" y="34">grid[x+length-1][y]:=false,
+grid[x-1][y]:=true,
+x:=x-1</label>
 			<nail x="-306" y="8"/>
 			<nail x="-136" y="0"/>
 		</transition>
 		<transition>
 			<source ref="id2"/>
 			<target ref="id2"/>
-			<label kind="guard" x="-306" y="-204">x+length &lt; 6 &amp;&amp; !grid[x+length][y]</label>
-			<label kind="synchronisation" x="-314" y="-153">up[id]!</label>
-			<label kind="assignment" x="-306" y="-178">x:=x+1</label>
+			<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">up[id]!</label>
+			<label kind="assignment" x="-331" y="-229">grid[x][y]:=false,
+grid[x+length][y]:=true,
+x:=x+1</label>
 			<nail x="-323" y="-102"/>
 			<nail x="-195" y="-178"/>
 			<nail x="-110" y="-102"/>
@@ -97,39 +101,52 @@ void register() {
 		<transition>
 			<source ref="id5"/>
 			<target ref="id5"/>
-			<label kind="guard" x="-135" y="8">y&gt;0 &amp;&amp; !grid[x][y-1]</label>
-			<label kind="synchronisation" x="-135" y="25">left[id]!</label>
-			<label kind="assignment" x="-135" y="42">y:=y-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">left[id]!</label>
+			<label kind="assignment" x="-221" y="51">grid[x][y-1]:=true,
+grid[x][y+length-1]:=true,
+y:=y-1</label>
 			<nail x="-153" y="42"/>
 			<nail x="-34" y="42"/>
 		</transition>
 		<transition>
 			<source ref="id5"/>
 			<target ref="id5"/>
-			<label kind="guard" x="-160" y="-102">y+length &lt; 6 &amp;&amp; !grid[x][y+length]</label>
-			<label kind="synchronisation" x="-160" y="-85">right[id]!</label>
-			<label kind="assignment" x="-160" y="-68">y:=y+1</label>
+			<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">right[id]!</label>
+			<label kind="assignment" x="-263" y="-161">grid[x][y+length]:=true,
+grid[x][y]:=false,
+y:=y+1</label>
 			<nail x="-178" y="-102"/>
 			<nail x="-34" y="-102"/>
 		</transition>
 	</template>
 	<template>
 		<name>Player</name>
-		<declaration>int[0,N] registered;</declaration>
-		<location id="id6" x="-680" y="-246">
+		<declaration>int[0,N] registered;
+bool done = 0;</declaration>
+		<location id="id6" x="-493" y="-255">
 		</location>
-		<location id="id7" x="-799" y="-246">
+		<location id="id7" x="-680" y="-246">
 		</location>
-		<init ref="id7"/>
+		<location id="id8" x="-799" y="-246">
+		</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>
+		</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>
 		</transition>
 		<transition>
-			<source ref="id7"/>
-			<target ref="id7"/>
+			<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"/>
@@ -144,40 +161,52 @@ void register() {
     grid[x][3] = true;
     grid[x+1][3] = true;
 }</declaration>
-		<location id="id8" x="51" y="-59">
+		<location id="id9" x="493" y="-51">
 		</location>
-		<location id="id9" x="-93" y="-68">
+		<location id="id10" x="51" y="-59">
 		</location>
-		<location id="id10" x="-204" y="-68">
+		<location id="id11" x="-93" y="-68">
+		</location>
+		<location id="id12" x="-204" y="-68">
 			<urgent/>
 		</location>
-		<init ref="id10"/>
+		<init ref="id12"/>
 		<transition>
-			<source ref="id8"/>
-			<target ref="id8"/>
-			<label kind="guard" x="-7" y="-42">x &gt; 0 &amp;&amp; grid[x-1][3]</label>
-			<label kind="synchronisation" x="-7" y="-25">leftRed!</label>
-			<label kind="assignment" x="-7" y="-8">x := x-1, grid[x+1][3] := false, grid[x-1][3] := true</label>
+			<source ref="id10"/>
+			<target ref="id9"/>
+			<label kind="guard" x="416" y="-93">x == 4</label>
+			<label kind="synchronisation" x="416" y="-76">finish!</label>
+		</transition>
+		<transition>
+			<source ref="id10"/>
+			<target ref="id10"/>
+			<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="id8"/>
-			<target ref="id8"/>
-			<label kind="guard" x="1" y="-135">x+2 &lt; 6 &amp;&amp; grid[x+2][3]</label>
-			<label kind="synchronisation" x="1" y="-118">rightRed!</label>
-			<label kind="assignment" x="1" y="-101">x := x+1, grid[x][3] := false, grid[x+2][3] := true</label>
+			<source ref="id10"/>
+			<target ref="id10"/>
+			<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-1][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="id9"/>
-			<target ref="id8"/>
+			<source ref="id11"/>
+			<target ref="id10"/>
 			<label kind="synchronisation" x="-75" y="-80">start?</label>
 		</transition>
 		<transition>
-			<source ref="id10"/>
-			<target ref="id9"/>
+			<source ref="id12"/>
+			<target ref="id11"/>
 			<label kind="synchronisation" x="-186" y="-85">reg!</label>
 			<label kind="assignment" x="-186" y="-68">register()</label>
 		</transition>
@@ -192,7 +221,7 @@ V4 = VertCar(2, 3, 2, 3);
 V5 = VertCar(3, 4, 5, 2);
 V6 = VertCar(2, 5, 1, 3);
 H7 = HorzCar(2, 6, 3, 4);
-H8 = HorzCar(2, 7, 3, 2);
+H8 = RedCar(7, 2); //RED
 V9 = VertCar(3, 8, 0, 0);
 HA = HorzCar(2, 9, 1, 0);
 VB = VertCar(2, 10, 3, 0);
@@ -216,5 +245,11 @@ system H1, V2, V3, V4, H5, H6, H7
 
     </system>
 	<queries>
+		<query>
+			<formula>E&lt;&gt; Player.done == 1
+			</formula>
+			<comment>
+			</comment>
+		</query>
 	</queries>
 </nta>
-- 
2.20.1