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

diff --git a/uppaal/2.xml b/uppaal/2.xml
index ad68966..dcbd6c3 100644
--- a/uppaal/2.xml
+++ b/uppaal/2.xml
@@ -2,64 +2,263 @@
 <!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>
 <nta>
 	<declaration>// Place global declarations here.
+// Intermediate
+//const int N=13;
+// Advanced
+//const int N = 7;
+//hard from website 1
+const int N=13;
+//hard from website 2
+//const int N=9;
 
-const int N = 13;
-typedef int[0,N-1] id_c;
+typedef int[0, N-1] id_c;
 
-chan up[N], down[N], left[N], right[N];</declaration>
+broadcast chan up[N], down[N], left[N], right[N], start, leftRed, rightRed;
+
+chan reg, finish;
+
+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>
-		<declaration>// Place local declarations here.</declaration>
-		<location id="id0" x="-212" y="-76">
+		<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+i][y] = true;
+    } 
+}</declaration>
+		<location id="id0" x="-425" y="-51">
+		</location>
+		<location id="id1" x="-535" y="-136">
+			<urgent/>
+		</location>
+		<location id="id2" x="-212" y="-76">
 		</location>
-		<init ref="id0"/>
+		<init ref="id1"/>
 		<transition>
 			<source ref="id0"/>
+			<target ref="id2"/>
+			<label kind="synchronisation" x="-407" y="-80">start?</label>
+		</transition>
+		<transition>
+			<source ref="id1"/>
 			<target ref="id0"/>
-			<label kind="guard" x="-288" y="-68">x&gt;0</label>
-			<label kind="synchronisation" x="-288" y="-51">down[id]!</label>
-			<label kind="assignment" x="-288" y="-34">x:=x-1</label>
+			<label kind="synchronisation" x="-517" y="-110">reg!</label>
+			<label kind="assignment" x="-517" y="-93">register()</label>
+		</transition>
+		<transition>
+			<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="-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>
 			<nail x="-306" y="8"/>
 			<nail x="-136" y="0"/>
 		</transition>
 		<transition>
-			<source ref="id0"/>
-			<target ref="id0"/>
-			<label kind="guard" x="-306" y="-204">x+length &lt; 6</label>
-			<label kind="synchronisation" x="-314" y="-153">up[id]!</label>
-			<label kind="assignment" x="-306" y="-178">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="-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>
 			<nail x="-323" y="-102"/>
 			<nail x="-195" y="-178"/>
 			<nail x="-110" y="-102"/>
 		</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>
-		<location id="id1" x="-102" y="-34">
+		<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][y+i] = true;
+    }
+}
+</declaration>
+		<location id="id3" x="-314" y="-34">
 		</location>
-		<init ref="id1"/>
+		<location id="id4" x="-416" y="-76">
+			<urgent/>
+		</location>
+		<location id="id5" x="-102" y="-34">
+		</location>
+		<init ref="id4"/>
 		<transition>
-			<source ref="id1"/>
-			<target ref="id1"/>
-			<label kind="guard" x="-135" y="8">y&gt;0</label>
-			<label kind="synchronisation" x="-135" y="25">left[id]!</label>
-			<label kind="assignment" x="-135" y="42">y:=y-1</label>
+			<source ref="id3"/>
+			<target ref="id5"/>
+			<label kind="synchronisation" x="-246" y="-59">start?</label>
+		</transition>
+		<transition>
+			<source ref="id4"/>
+			<target ref="id3"/>
+			<label kind="synchronisation" x="-374" y="-110">reg!</label>
+			<label kind="assignment" x="-374" y="-76">register()</label>
+			<nail x="-255" y="-85"/>
+		</transition>
+		<transition>
+			<source ref="id5"/>
+			<target ref="id5"/>
+			<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"/>
 			<nail x="-34" y="42"/>
 		</transition>
 		<transition>
-			<source ref="id1"/>
-			<target ref="id1"/>
-			<label kind="guard" x="-160" y="-102">y+length &lt; 6</label>
-			<label kind="synchronisation" x="-160" y="-85">right[id]!</label>
-			<label kind="assignment" x="-160" y="-68">y:=y+1</label>
+			<source ref="id5"/>
+			<target ref="id5"/>
+			<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"/>
 			<nail x="-34" y="-102"/>
 		</transition>
 	</template>
+	<template>
+		<name>Player</name>
+		<declaration>int[0,N] registered;
+bool done = 0;</declaration>
+		<location id="id6" x="-476" y="-459">
+		</location>
+		<location id="id7" x="-663" y="-450">
+		</location>
+		<location id="id8" x="-782" y="-450">
+		</location>
+		<init ref="id8"/>
+		<transition>
+			<source ref="id7"/>
+			<target ref="id6"/>
+			<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="-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="-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>
+		<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="id9" x="42" y="136">
+			<urgent/>
+		</location>
+		<location id="id10" x="59" y="-238">
+			<urgent/>
+		</location>
+		<location id="id11" x="493" y="-51">
+		</location>
+		<location id="id12" x="51" y="-59">
+		</location>
+		<location id="id13" x="-93" y="-68">
+		</location>
+		<location id="id14" x="-204" y="-68">
+			<urgent/>
+		</location>
+		<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="161" y="-34">1</label>
+		</transition>
+		<transition>
+			<source ref="id15"/>
+			<target ref="id10"/>
+			<label kind="probability" x="178" y="-127">3</label>
+		</transition>
+		<transition>
+			<source ref="id12"/>
+			<target ref="id15"/>
+		</transition>
+		<transition>
+			<source ref="id12"/>
+			<target ref="id11"/>
+			<label kind="guard" x="416" y="-93">x == 4</label>
+			<label kind="synchronisation" x="416" y="-76">finish!</label>
+		</transition>
+		<transition>
+			<source ref="id13"/>
+			<target ref="id12"/>
+			<label kind="synchronisation" x="-75" y="-80">start?</label>
+		</transition>
+		<transition>
+			<source ref="id14"/>
+			<target ref="id13"/>
+			<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.
+
+
+
+//easy test puzzle
+/*
+RED = RedCar(0,2);
+V1 = VertCar(2, 1, 4, 3);
+V2 = VertCar(3, 2, 5, 2);
+system RED, V1, V2, Player;
+*/
+
+// Intermediate puzzle
+
 H1 = HorzCar(2, 0, 0, 5);
 H2 = HorzCar(2, 1, 2, 5);
 V3 = VertCar(2, 2, 4, 4);
@@ -67,15 +266,65 @@ 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);
+RED = RedCar(7, 2); //RED
 V9 = VertCar(3, 8, 0, 0);
 HA = HorzCar(2, 9, 1, 0);
 VB = VertCar(2, 10, 3, 0);
 HC = HorzCar(2, 11, 4, 1);
 HD = HorzCar(2, 12, 4, 0);
-// List one or more processes to be composed into a system.
-system H1, H2, V3, V4, V5, V6, H7, H8, V9, HA, VB, HC, HD;
-    </system>
+system H1, H2, V3, V4, V5, V6, H7, RED, V9, HA, VB, HC, HD, Player;
+
+
+// Advanced puzzle
+/*
+H1 = HorzCar(2, 0, 0, 5);
+V2 = VertCar(2, 1, 2, 4);
+V3 = VertCar(3, 2, 3, 3);
+V4 = VertCar(3, 3, 0, 2);
+RED = RedCar(4, 1);
+H6 = HorzCar(3, 5, 1, 2);
+H7 = HorzCar(3, 6, 3, 0);
+system H1, V2, V3, V4, RED, H6, H7, Player;
+*/
+
+//Hard from website 1
+//Can not be solved
+/*
+V1 = VertCar(2, 0, 0, 3);
+V2 = VertCar(2, 1, 1, 0);
+V3 = VertCar(2, 2, 2, 1);
+V4 = VertCar(2, 3, 3, 4);
+V5 = VertCar(3, 4, 4, 3);
+V6 = VertCar(3, 5, 5, 3);
+H7 = HorzCar(2, 6, 0, 2);
+H8 = HorzCar(3, 7, 0, 5);
+H85= HorzCar(3,12, 1, 4); 
+H9 = HorzCar(2, 8, 2, 0);
+RED = RedCar(9, 2);
+HB = HorzCar(2,10, 4, 0);
+HC = HorzCar(2,11, 4, 1);
+system V1, V2, V3, V4, V5, V6, H7, H8, H85, H9, RED, HB, HC, Player;
+*/
+
+//Hard from website 2
+/*
+V1 = VertCar(2, 0, 0, 0);
+V2 = VertCar(3, 1, 2, 3);
+V3 = VertCar(3, 2, 3, 0);
+V4 = VertCar(3, 3, 5, 3);
+H5 = HorzCar(2, 4, 1, 1);
+RED = RedCar(5, 3);
+H7 = HorzCar(2, 6, 3, 5);
+H8 = HorzCar(2, 7, 4, 0);
+H9 = HorzCar(2, 8, 4, 2);
+system V1, V2, V3, V4, H5, RED, H7, H8, H9, Player;
+*/</system>
 	<queries>
+		<query>
+			<formula>E&lt;&gt; Player.done == 1
+			</formula>
+			<comment>
+			</comment>
+		</query>
 	</queries>
 </nta>