From: pimjager <pim@pimjager.nl>
Date: Thu, 16 Jun 2016 09:28:08 +0000 (+0200)
Subject: 2.xml voor prop weight op RedCar
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=0aa0c8c76d10a27e689c139203923943ae07460b;p=mc1516the.git

2.xml voor prop weight op RedCar
---

diff --git a/uppaal/2.xml b/uppaal/2.xml
index 29e4e8f..e45b155 100644
--- a/uppaal/2.xml
+++ b/uppaal/2.xml
@@ -3,11 +3,13 @@
 <nta>
 	<declaration>// Place global declarations here.
 // Intermediate
-const int N = 13;
+//const int N=13;
 // Advanced
-//const int N = 7
+//const int N = 7;
+//easy test puzzle
+const int N=3;
 
-typedef int[0,N-1] id_c;
+typedef int[0, N-1] id_c;
 
 broadcast chan up[N], down[N], left[N], right[N], start, leftRed, rightRed;
 
@@ -48,7 +50,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">down[id]!</label>
+			<label kind="synchronisation" x="-246" y="102">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>
@@ -59,7 +61,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">up[id]!</label>
+			<label kind="synchronisation" x="-221" y="-204">right[id]!</label>
 			<label kind="assignment" x="-331" y="-229">grid[x][y]:=false,
 grid[x+length][y]:=true,
 x:=x+1</label>
@@ -102,7 +104,7 @@ x:=x+1</label>
 			<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">left[id]!</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,
 y:=y-1</label>
@@ -113,7 +115,7 @@ y:=y-1</label>
 			<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">right[id]!</label>
+			<label kind="synchronisation" x="-127" y="-195">up[id]!</label>
 			<label kind="assignment" x="-263" y="-161">grid[x][y+length]:=true,
 grid[x][y]:=false,
 y:=y+1</label>
@@ -161,26 +163,56 @@ bool done = 0;</declaration>
     grid[x][3] = true;
     grid[x+1][3] = true;
 }</declaration>
-		<location id="id9" x="493" y="-51">
+		<location id="id9" x="238" y="34">
+			<urgent/>
+		</location>
+		<location id="id10" x="221" y="-153">
+			<urgent/>
 		</location>
-		<location id="id10" x="51" y="-59">
+		<location id="id11" x="493" y="-51">
 		</location>
-		<location id="id11" x="-93" y="-68">
+		<location id="id12" x="51" y="-59">
 		</location>
-		<location id="id12" x="-204" y="-68">
+		<location id="id13" x="-93" y="-68">
+		</location>
+		<location id="id14" x="-204" y="-68">
 			<urgent/>
 		</location>
-		<init ref="id12"/>
+		<branchpoint id="id15" x="187" y="-85">
+		</branchpoint>
+		<init ref="id14"/>
 		<transition>
 			<source ref="id10"/>
+			<target ref="id12"/>
+		</transition>
+		<transition>
+			<source ref="id9"/>
+			<target ref="id12"/>
+		</transition>
+		<transition>
+			<source ref="id15"/>
 			<target ref="id9"/>
+			<label kind="probability" x="212" y="-25">1</label>
+		</transition>
+		<transition>
+			<source ref="id15"/>
+			<target ref="id10"/>
+			<label kind="probability" x="204" y="-119">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="id10"/>
-			<target ref="id10"/>
-			<label kind="guard" x="0" y="161">x &gt; 0 &amp;&amp; grid[x-1][3]</label>
+			<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,
@@ -189,31 +221,40 @@ x:=x-1</label>
 			<nail x="178" y="51"/>
 		</transition>
 		<transition>
-			<source ref="id10"/>
-			<target ref="id10"/>
-			<label kind="guard" x="-17" y="-255">x+2 &lt; 6 &amp;&amp; grid[x+2][3]</label>
+			<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-1][3]:=false,
+			<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="id11"/>
-			<target ref="id10"/>
+			<source ref="id13"/>
+			<target ref="id12"/>
 			<label kind="synchronisation" x="-75" y="-80">start?</label>
 		</transition>
 		<transition>
-			<source ref="id12"/>
-			<target ref="id11"/>
+			<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);
@@ -221,13 +262,14 @@ 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 = RedCar(7, 2); //RED
+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);
-system H1, H2, V3, V4, V5, V6, H7, H8, V9, HA, VB, HC, HD, Player;
+system H1, H2, V3, V4, V5, V6, H7, RED, V9, HA, VB, HC, HD, Player;
+*/
 
 // Advanced puzzle
 /*
@@ -240,9 +282,6 @@ H6 = HorzCar(3, 5, 1, 2);
 H7 = HorzCar(3, 6, 3, 0);
 system H1, V2, V3, V4, H5, H6, H7
 */
-
-// List one or more processes to be composed into a system.
-
     </system>
 	<queries>
 		<query>