//const int N=13;
// Advanced
//const int N = 7;
-//easy test puzzle
-const int N=3;
+//hard from website 1
+const int N=13;
+//hard from website 2
+//const int N=9;
typedef int[0, N-1] id_c;
<source ref="id2"/>\r
<target ref="id2"/>\r
<label kind="guard" x="-280" y="8">x>0 && !grid[x-1][y]</label>\r
- <label kind="synchronisation" x="-246" y="102">left[id]!</label>\r
+ <label kind="synchronisation" x="-153" y="-42">left[id]!</label>\r
<label kind="assignment" x="-340" y="34">grid[x+length-1][y]:=false,
grid[x-1][y]:=true,
x:=x-1</label>\r
<source ref="id2"/>\r
<target ref="id2"/>\r
<label kind="guard" x="-306" y="-263">x+length < 6 && !grid[x+length][y]</label>\r
- <label kind="synchronisation" x="-221" y="-204">right[id]!</label>\r
+ <label kind="synchronisation" x="-170" y="-170">right[id]!</label>\r
<label kind="assignment" x="-331" y="-229">grid[x][y]:=false,
grid[x+length][y]:=true,
x:=x+1</label>\r
<transition>\r
<source ref="id3"/>\r
<target ref="id5"/>\r
- <label kind="synchronisation" x="-228" y="-72">start?</label>\r
+ <label kind="synchronisation" x="-246" y="-59">start?</label>\r
</transition>\r
<transition>\r
<source ref="id4"/>\r
<transition>\r
<source ref="id5"/>\r
<target ref="id5"/>\r
- <label kind="guard" x="-170" y="153">y>0 && !grid[x][y-1]</label>\r
- <label kind="synchronisation" x="-119" y="119">down[id]!</label>\r
- <label kind="assignment" x="-221" y="51">grid[x][y-1]:=true,
+ <label kind="guard" x="-153" y="153">y>0 && !grid[x][y-1]</label>\r
+ <label kind="synchronisation" x="-153" y="119">down[id]!</label>\r
+ <label kind="assignment" x="-153" y="51">grid[x][y-1]:=true,
grid[x][y+length-1]:=false,
y:=y-1</label>\r
<nail x="-153" y="42"/>\r
<transition>\r
<source ref="id5"/>\r
<target ref="id5"/>\r
- <label kind="guard" x="-204" y="-221">y+length < 6 && !grid[x][y+length]</label>\r
- <label kind="synchronisation" x="-127" y="-195">up[id]!</label>\r
- <label kind="assignment" x="-263" y="-161">grid[x][y+length]:=true,
+ <label kind="guard" x="-161" y="-204">y+length < 6 && !grid[x][y+length]</label>\r
+ <label kind="synchronisation" x="-161" y="-178">up[id]!</label>\r
+ <label kind="assignment" x="-161" y="-153">grid[x][y+length]:=true,
grid[x][y]:=false,
y:=y+1</label>\r
<nail x="-178" y="-102"/>\r
<name>Player</name>\r
<declaration>int[0,N] registered;
bool done = 0;</declaration>\r
- <location id="id6" x="-493" y="-255">\r
+ <location id="id6" x="-476" y="-459">\r
</location>\r
- <location id="id7" x="-680" y="-246">\r
+ <location id="id7" x="-663" y="-450">\r
</location>\r
- <location id="id8" x="-799" y="-246">\r
+ <location id="id8" x="-782" y="-450">\r
</location>\r
<init ref="id8"/>\r
<transition>\r
<source ref="id7"/>\r
<target ref="id6"/>\r
- <label kind="synchronisation" x="-629" y="-272">finish?</label>\r
- <label kind="assignment" x="-662" y="-250">done := 1</label>\r
+ <label kind="synchronisation" x="-612" y="-476">finish?</label>\r
+ <label kind="assignment" x="-645" y="-454">done := 1</label>\r
</transition>\r
<transition>\r
<source ref="id8"/>\r
<target ref="id7"/>\r
- <label kind="guard" x="-781" y="-280">registered == N</label>\r
- <label kind="synchronisation" x="-781" y="-263">start!</label>\r
+ <label kind="guard" x="-764" y="-484">registered == N</label>\r
+ <label kind="synchronisation" x="-764" y="-467">start!</label>\r
</transition>\r
<transition>\r
<source ref="id8"/>\r
<target ref="id8"/>\r
- <label kind="synchronisation" x="-875" y="-365">reg?</label>\r
- <label kind="assignment" x="-926" y="-382">registered := registered+1</label>\r
- <nail x="-892" y="-263"/>\r
- <nail x="-833" y="-331"/>\r
- <nail x="-765" y="-314"/>\r
+ <label kind="synchronisation" x="-833" y="-561">reg?</label>\r
+ <label kind="assignment" x="-909" y="-578">registered := registered+1</label>\r
+ <nail x="-875" y="-467"/>\r
+ <nail x="-816" y="-535"/>\r
+ <nail x="-748" y="-518"/>\r
</transition>\r
</template>\r
<template>\r
<transition>\r
<source ref="id15"/>\r
<target ref="id9"/>\r
- <label kind="probability" x="127" y="34">1</label>\r
+ <label kind="probability" x="161" y="-34">1</label>\r
</transition>\r
<transition>\r
<source ref="id15"/>\r
//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);
HC = HorzCar(2, 11, 4, 1);
HD = HorzCar(2, 12, 4, 0);
system H1, H2, V3, V4, V5, V6, H7, RED, V9, HA, VB, HC, HD, Player;
-*/
+
// Advanced puzzle
/*
V2 = VertCar(2, 1, 2, 4);
V3 = VertCar(3, 2, 3, 3);
V4 = VertCar(3, 3, 0, 2);
-H5 = HorzCar(2, 4, 1, 3);
+RED = RedCar(4, 1);
H6 = HorzCar(3, 5, 1, 2);
H7 = HorzCar(3, 6, 3, 0);
-system H1, V2, V3, V4, H5, H6, H7
+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;
*/
- </system>\r
+
+//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>\r
<queries>\r
<query>\r
<formula>E<> Player.done == 1\r