<nta>\r
<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;
-chan up[N], down[N], left[N], right[N];</declaration>\r
+broadcast chan up[N], down[N], left[N], right[N], start, leftRed, rightRed;
+
+chan reg, finish;
+
+bool grid[6][6];</declaration>\r
<template>\r
- <name x="5" y="5">VertCar</name>\r
- <parameter>int[2,3] length, const id_c id, int[0,5] x, const int[0,4] y</parameter>\r
- <declaration>// Place local declarations here.</declaration>\r
- <location id="id0" x="-212" y="-76">\r
+ <name x="5" y="5">HorzCar</name>\r
+ <parameter>int[2,3] length, const id_c id, int[0,4] x, const int[0,5] y</parameter>\r
+ <declaration>// Place local declarations here.
+
+void register() {
+ int i;
+ for (i=0; i<length; i++) {
+ grid[x+i][y] = true;
+ }
+}</declaration>\r
+ <location id="id0" x="-425" y="-51">\r
+ </location>\r
+ <location id="id1" x="-535" y="-136">\r
+ <urgent/>\r
+ </location>\r
+ <location id="id2" x="-212" y="-76">\r
</location>\r
- <init ref="id0"/>\r
+ <init ref="id1"/>\r
<transition>\r
<source ref="id0"/>\r
+ <target ref="id2"/>\r
+ <label kind="synchronisation" x="-407" y="-80">start?</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id1"/>\r
<target ref="id0"/>\r
- <label kind="guard" x="-288" y="-68">x>0</label>\r
- <label kind="synchronisation" x="-288" y="-51">down[id]!</label>\r
- <label kind="assignment" x="-288" y="-34">x:=x-1</label>\r
+ <label kind="synchronisation" x="-517" y="-110">reg!</label>\r
+ <label kind="assignment" x="-517" y="-93">register()</label>\r
+ </transition>\r
+ <transition>\r
+ <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="assignment" x="-340" y="34">grid[x+length-1][y]:=false,
+grid[x-1][y]:=true,
+x:=x-1</label>\r
<nail x="-306" y="8"/>\r
<nail x="-136" y="0"/>\r
</transition>\r
<transition>\r
- <source ref="id0"/>\r
- <target ref="id0"/>\r
- <label kind="guard" x="-306" y="-204">x+length < 6</label>\r
- <label kind="synchronisation" x="-314" y="-153">up[id]!</label>\r
- <label kind="assignment" x="-306" y="-178">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="assignment" x="-331" y="-229">grid[x][y]:=false,
+grid[x+length][y]:=true,
+x:=x+1</label>\r
<nail x="-323" y="-102"/>\r
<nail x="-195" y="-178"/>\r
<nail x="-110" y="-102"/>\r
</transition>\r
</template>\r
<template>\r
- <name>HorzCar</name>\r
- <parameter>int[2,3] length, const id_c id, const int[0,4] x, int[0,5] y</parameter>\r
- <location id="id1" x="-102" y="-34">\r
+ <name>VertCar</name>\r
+ <parameter>int[2,3] length, const id_c id, const int[0,5] x, int[0,4] y</parameter>\r
+ <declaration>void register() {
+ int i;
+ for(i=0; i<length; i++){
+ grid[x][y+i] = true;
+ }
+}
+</declaration>\r
+ <location id="id3" x="-314" y="-34">\r
</location>\r
- <init ref="id1"/>\r
+ <location id="id4" x="-416" y="-76">\r
+ <urgent/>\r
+ </location>\r
+ <location id="id5" x="-102" y="-34">\r
+ </location>\r
+ <init ref="id4"/>\r
<transition>\r
- <source ref="id1"/>\r
- <target ref="id1"/>\r
- <label kind="guard" x="-135" y="8">y>0</label>\r
- <label kind="synchronisation" x="-135" y="25">left[id]!</label>\r
- <label kind="assignment" x="-135" y="42">y:=y-1</label>\r
+ <source ref="id3"/>\r
+ <target ref="id5"/>\r
+ <label kind="synchronisation" x="-228" y="-72">start?</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id4"/>\r
+ <target ref="id3"/>\r
+ <label kind="synchronisation" x="-374" y="-110">reg!</label>\r
+ <label kind="assignment" x="-374" y="-76">register()</label>\r
+ <nail x="-255" y="-85"/>\r
+ </transition>\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,
+grid[x][y+length-1]:=false,
+y:=y-1</label>\r
<nail x="-153" y="42"/>\r
<nail x="-34" y="42"/>\r
</transition>\r
<transition>\r
- <source ref="id1"/>\r
- <target ref="id1"/>\r
- <label kind="guard" x="-160" y="-102">y+length < 6</label>\r
- <label kind="synchronisation" x="-160" y="-85">right[id]!</label>\r
- <label kind="assignment" x="-160" y="-68">y:=y+1</label>\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,
+grid[x][y]:=false,
+y:=y+1</label>\r
<nail x="-178" y="-102"/>\r
<nail x="-34" y="-102"/>\r
</transition>\r
</template>\r
<template>\r
<name>Player</name>\r
- <location id="id2" x="-476" y="-178">\r
+ <declaration>int[0,N] registered;
+bool done = 0;</declaration>\r
+ <location id="id6" x="-493" y="-255">\r
+ </location>\r
+ <location id="id7" x="-680" y="-246">\r
</location>\r
- <init ref="id2"/>\r
+ <location id="id8" x="-799" y="-246">\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
+ </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
+ </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
+ </transition>\r
+ </template>\r
+ <template>\r
+ <name>RedCar</name>\r
+ <parameter>const id_c id, int[0,5] x</parameter>\r
+ <declaration>void register() {
+ grid[x][3] = true;
+ grid[x+1][3] = true;
+}</declaration>\r
+ <location id="id9" x="42" y="136">\r
+ <urgent/>\r
+ </location>\r
+ <location id="id10" x="59" y="-238">\r
+ <urgent/>\r
+ </location>\r
+ <location id="id11" x="493" y="-51">\r
+ </location>\r
+ <location id="id12" x="51" y="-59">\r
+ </location>\r
+ <location id="id13" x="-93" y="-68">\r
+ </location>\r
+ <location id="id14" x="-204" y="-68">\r
+ <urgent/>\r
+ </location>\r
+ <branchpoint id="id15" x="187" y="-85">\r
+ </branchpoint>\r
+ <init ref="id14"/>\r
+ <transition>\r
+ <source ref="id9"/>\r
+ <target ref="id12"/>\r
+ <label kind="guard" x="67" y="38">x <= 0 || grid[x-1][3]</label>\r
+ <nail x="93" y="8"/>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id10"/>\r
+ <target ref="id12"/>\r
+ <label kind="guard" x="93" y="-187">x+2 >= 6 || grid[x+2][3]</label>\r
+ <nail x="102" y="-127"/>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id10"/>\r
+ <target ref="id12"/>\r
+ <label kind="guard" x="-136" y="-161">x+2 < 6 && !grid[x+2][3]</label>\r
+ <label kind="synchronisation" x="-68" y="-144">rightRed!</label>\r
+ <label kind="assignment" x="-85" y="-212">grid[x][3]:=false,
+grid[x+2][3]:=true,
+x:=x+1</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id9"/>\r
+ <target ref="id12"/>\r
+ <label kind="guard" x="-144" y="-25">x > 0 && !grid[x-1][3]</label>\r
+ <label kind="synchronisation" x="-93" y="0">leftRed!</label>\r
+ <label kind="assignment" x="-144" y="25">grid[x+1][3]:=false,
+grid[x-1][3]:=true,
+x:=x-1</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id15"/>\r
+ <target ref="id9"/>\r
+ <label kind="probability" x="127" y="34">1</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id15"/>\r
+ <target ref="id10"/>\r
+ <label kind="probability" x="178" y="-127">3</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id12"/>\r
+ <target ref="id15"/>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id12"/>\r
+ <target ref="id11"/>\r
+ <label kind="guard" x="416" y="-93">x == 4</label>\r
+ <label kind="synchronisation" x="416" y="-76">finish!</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id13"/>\r
+ <target ref="id12"/>\r
+ <label kind="synchronisation" x="-75" y="-80">start?</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id14"/>\r
+ <target ref="id13"/>\r
+ <label kind="synchronisation" x="-186" y="-85">reg!</label>\r
+ <label kind="assignment" x="-186" y="-68">register()</label>\r
+ </transition>\r
</template>\r
<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);
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);
-system H1, H2, V3, V4, V5, V6, H7, H8, V9, HA, VB, HC, HD;
+system H1, H2, V3, V4, V5, V6, H7, RED, V9, HA, VB, HC, HD, Player;
+*/
// Advanced puzzle
/*
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>\r
<queries>\r
+ <query>\r
+ <formula>E<> Player.done == 1\r
+ </formula>\r
+ <comment>\r
+ </comment>\r
+ </query>\r
</queries>\r
</nta>\r
repositories / mc1516the.git / blobdiff