From: pimjager <pim@pimjager.nl>
Date: Tue, 14 Jun 2016 10:16:50 +0000 (+0200)
Subject: mend
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=4ab4904ff6f4de986c0306008dc5e9f12322aec5;p=mc1516the.git

mend
---

diff --git a/uppaal/2.xml b/uppaal/2.xml
index 153e6b9..862ab1e 100644
--- a/uppaal/2.xml
+++ b/uppaal/2.xml
@@ -9,20 +9,20 @@ const int N = 13;
 
 typedef int[0,N-1] id_c;
 
-broadcast chan up[N], down[N], left[N], right[N], start;
+broadcast chan up[N], down[N], left[N], right[N], start, leftRed, rightRed;
 
 chan reg;
 
 bool grid[6][6];</declaration>
 	<template>
-		<name x="5" y="5">VertCar</name>
-		<parameter>int[2,3] length, const id_c id, int[0,5] x, const int[0,4] y</parameter>
+		<name x="5" y="5">HorzCar</name>
+		<parameter>int[2,3] length, const id_c id, int[0,4] x, const int[0,5] y</parameter>
 		<declaration>// Place local declarations here.
 
 void register() {
     int i;
     for (i=0; i&lt;length; i++) {
-        grid[x][y+1] = true;
+        grid[x+i][y] = true;
     } 
 }</declaration>
 		<location id="id0" x="-425" y="-51">
@@ -65,12 +65,12 @@ void register() {
 		</transition>
 	</template>
 	<template>
-		<name>HorzCar</name>
-		<parameter>int[2,3] length, const id_c id, const int[0,4] x, int[0,5] y</parameter>
+		<name>VertCar</name>
+		<parameter>int[2,3] length, const id_c id, const int[0,5] x, int[0,4] y</parameter>
 		<declaration>void register() {
     int i;
     for(i=0; i&lt;length; i++){
-        grid[x+i][y] = true;
+        grid[x][y+i] = true;
     }
 }
 </declaration>
@@ -115,7 +115,6 @@ void register() {
 	</template>
 	<template>
 		<name>Player</name>
-		<parameter>Template red</parameter>
 		<declaration>int[0,N] registered;</declaration>
 		<location id="id6" x="-680" y="-246">
 		</location>
@@ -138,6 +137,51 @@ void register() {
 			<nail x="-765" y="-314"/>
 		</transition>
 	</template>
+	<template>
+		<name>RedCar</name>
+		<parameter>const id_c id, int[0,5] x</parameter>
+		<declaration>void register() {
+    grid[x][3] = true;
+    grid[x+1][3] = true;
+}</declaration>
+		<location id="id8" x="51" y="-59">
+		</location>
+		<location id="id9" x="-93" y="-68">
+		</location>
+		<location id="id10" x="-204" y="-68">
+			<urgent/>
+		</location>
+		<init ref="id10"/>
+		<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>
+			<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>
+			<nail x="-17" y="-144"/>
+			<nail x="144" y="-136"/>
+		</transition>
+		<transition>
+			<source ref="id9"/>
+			<target ref="id8"/>
+			<label kind="synchronisation" x="-75" y="-80">start?</label>
+		</transition>
+		<transition>
+			<source ref="id10"/>
+			<target ref="id9"/>
+			<label kind="synchronisation" x="-186" y="-85">reg!</label>
+			<label kind="assignment" x="-186" y="-68">register()</label>
+		</transition>
+	</template>
 	<system>// Place template instantiations here.
 
 // Intermediate puzzle