1 <?xml version=
"1.0" encoding=
"utf-8"?>
2 <!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System
1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-
1_2.dtd'
>
4 <declaration>// Place global declarations here.
14 typedef int[
0, N-
1] id_c;
16 broadcast chan up[N], down[N], left[N], right[N], start, leftRed, rightRed;
20 bool grid[
6][
6];
</declaration>
22 <name x=
"5" y=
"5">HorzCar
</name>
23 <parameter>int[
2,
3] length, const id_c id, int[
0,
4] x, const int[
0,
5] y
</parameter>
24 <declaration>// Place local declarations here.
28 for (i=
0; i
<length; i++) {
32 <location id=
"id0" x=
"-425" y=
"-51">
34 <location id=
"id1" x=
"-535" y=
"-136">
37 <location id=
"id2" x=
"-212" y=
"-76">
43 <label kind=
"synchronisation" x=
"-407" y=
"-80">start?
</label>
48 <label kind=
"synchronisation" x=
"-517" y=
"-110">reg!
</label>
49 <label kind=
"assignment" x=
"-517" y=
"-93">register()
</label>
54 <label kind=
"guard" x=
"-280" y=
"8">x
>0 && !grid[x-
1][y]
</label>
55 <label kind=
"synchronisation" x=
"-246" y=
"102">left[id]!
</label>
56 <label kind=
"assignment" x=
"-340" y=
"34">grid[x+length-
1][y]:=false,
59 <nail x=
"-306" y=
"8"/>
60 <nail x=
"-136" y=
"0"/>
65 <label kind=
"guard" x=
"-306" y=
"-263">x+length
< 6 && !grid[x+length][y]
</label>
66 <label kind=
"synchronisation" x=
"-221" y=
"-204">right[id]!
</label>
67 <label kind=
"assignment" x=
"-331" y=
"-229">grid[x][y]:=false,
68 grid[x+length][y]:=true,
70 <nail x=
"-323" y=
"-102"/>
71 <nail x=
"-195" y=
"-178"/>
72 <nail x=
"-110" y=
"-102"/>
77 <parameter>int[
2,
3] length, const id_c id, const int[
0,
5] x, int[
0,
4] y
</parameter>
78 <declaration>void register() {
80 for(i=
0; i
<length; i++){
85 <location id=
"id3" x=
"-314" y=
"-34">
87 <location id=
"id4" x=
"-416" y=
"-76">
90 <location id=
"id5" x=
"-102" y=
"-34">
96 <label kind=
"synchronisation" x=
"-228" y=
"-72">start?
</label>
101 <label kind=
"synchronisation" x=
"-374" y=
"-110">reg!
</label>
102 <label kind=
"assignment" x=
"-374" y=
"-76">register()
</label>
103 <nail x=
"-255" y=
"-85"/>
108 <label kind=
"guard" x=
"-170" y=
"153">y
>0 && !grid[x][y-
1]
</label>
109 <label kind=
"synchronisation" x=
"-119" y=
"119">down[id]!
</label>
110 <label kind=
"assignment" x=
"-221" y=
"51">grid[x][y-
1]:=true,
111 grid[x][y+length-
1]:=false,
113 <nail x=
"-153" y=
"42"/>
114 <nail x=
"-34" y=
"42"/>
119 <label kind=
"guard" x=
"-204" y=
"-221">y+length
< 6 && !grid[x][y+length]
</label>
120 <label kind=
"synchronisation" x=
"-127" y=
"-195">up[id]!
</label>
121 <label kind=
"assignment" x=
"-263" y=
"-161">grid[x][y+length]:=true,
124 <nail x=
"-178" y=
"-102"/>
125 <nail x=
"-34" y=
"-102"/>
130 <declaration>int[
0,N] registered;
131 bool done =
0;
</declaration>
132 <location id=
"id6" x=
"-493" y=
"-255">
134 <location id=
"id7" x=
"-680" y=
"-246">
136 <location id=
"id8" x=
"-799" y=
"-246">
142 <label kind=
"synchronisation" x=
"-629" y=
"-272">finish?
</label>
143 <label kind=
"assignment" x=
"-662" y=
"-250">done :=
1</label>
148 <label kind=
"guard" x=
"-781" y=
"-280">registered == N
</label>
149 <label kind=
"synchronisation" x=
"-781" y=
"-263">start!
</label>
154 <label kind=
"synchronisation" x=
"-875" y=
"-365">reg?
</label>
155 <label kind=
"assignment" x=
"-926" y=
"-382">registered := registered+
1</label>
156 <nail x=
"-892" y=
"-263"/>
157 <nail x=
"-833" y=
"-331"/>
158 <nail x=
"-765" y=
"-314"/>
163 <parameter>const id_c id, int[
0,
5] x
</parameter>
164 <declaration>void register() {
168 <location id=
"id9" x=
"42" y=
"136">
171 <location id=
"id10" x=
"59" y=
"-238">
174 <location id=
"id11" x=
"493" y=
"-51">
176 <location id=
"id12" x=
"51" y=
"-59">
178 <location id=
"id13" x=
"-93" y=
"-68">
180 <location id=
"id14" x=
"-204" y=
"-68">
183 <branchpoint id=
"id15" x=
"187" y=
"-85">
189 <label kind=
"guard" x=
"67" y=
"38">x
<=
0 || grid[x-
1][
3]
</label>
195 <label kind=
"guard" x=
"93" y=
"-187">x+
2 >=
6 || grid[x+
2][
3]
</label>
196 <nail x=
"102" y=
"-127"/>
201 <label kind=
"guard" x=
"-136" y=
"-161">x+
2 < 6 && !grid[x+
2][
3]
</label>
202 <label kind=
"synchronisation" x=
"-68" y=
"-144">rightRed!
</label>
203 <label kind=
"assignment" x=
"-85" y=
"-212">grid[x][
3]:=false,
210 <label kind=
"guard" x=
"-144" y=
"-25">x
> 0 && !grid[x-
1][
3]
</label>
211 <label kind=
"synchronisation" x=
"-93" y=
"0">leftRed!
</label>
212 <label kind=
"assignment" x=
"-144" y=
"25">grid[x+
1][
3]:=false,
219 <label kind=
"probability" x=
"127" y=
"34">1</label>
224 <label kind=
"probability" x=
"178" y=
"-127">3</label>
233 <label kind=
"guard" x=
"416" y=
"-93">x ==
4</label>
234 <label kind=
"synchronisation" x=
"416" y=
"-76">finish!
</label>
239 <label kind=
"synchronisation" x=
"-75" y=
"-80">start?
</label>
244 <label kind=
"synchronisation" x=
"-186" y=
"-85">reg!
</label>
245 <label kind=
"assignment" x=
"-186" y=
"-68">register()
</label>
248 <system>// Place template instantiations here.
255 V1 = VertCar(
2,
1,
4,
3);
256 V2 = VertCar(
3,
2,
5,
2);
257 system RED, V1, V2, Player;
260 // Intermediate puzzle
262 H1 = HorzCar(
2,
0,
0,
5);
263 H2 = HorzCar(
2,
1,
2,
5);
264 V3 = VertCar(
2,
2,
4,
4);
265 V4 = VertCar(
2,
3,
2,
3);
266 V5 = VertCar(
3,
4,
5,
2);
267 V6 = VertCar(
2,
5,
1,
3);
268 H7 = HorzCar(
2,
6,
3,
4);
269 RED = RedCar(
7,
2); //RED
270 V9 = VertCar(
3,
8,
0,
0);
271 HA = HorzCar(
2,
9,
1,
0);
272 VB = VertCar(
2,
10,
3,
0);
273 HC = HorzCar(
2,
11,
4,
1);
274 HD = HorzCar(
2,
12,
4,
0);
275 system H1, H2, V3, V4, V5, V6, H7, RED, V9, HA, VB, HC, HD, Player;
280 H1 = HorzCar(
2,
0,
0,
5);
281 V2 = VertCar(
2,
1,
2,
4);
282 V3 = VertCar(
3,
2,
3,
3);
283 V4 = VertCar(
3,
3,
0,
2);
285 H6 = HorzCar(
3,
5,
1,
2);
286 H7 = HorzCar(
3,
6,
3,
0);
287 system H1, V2, V3, V4, RED, H6, H7, Player;
290 //Hard from website
1
293 V1 = VertCar(
2,
0,
0,
3);
294 V2 = VertCar(
2,
1,
1,
0);
295 V3 = VertCar(
2,
2,
2,
1);
296 V4 = VertCar(
2,
3,
3,
4);
297 V5 = VertCar(
3,
4,
4,
3);
298 V6 = VertCar(
3,
5,
5,
3);
299 H7 = HorzCar(
2,
6,
0,
2);
300 H8 = HorzCar(
3,
7,
0,
5);
301 H85= HorzCar(
3,
12,
1,
4);
302 H9 = HorzCar(
2,
8,
2,
0);
304 HB = HorzCar(
2,
10,
4,
0);
305 HC = HorzCar(
2,
11,
4,
1);
306 system V1, V2, V3, V4, V5, V6, H7, H8, H85, H9, RED, HB, HC, Player;
309 //Hard from website
2
311 V1 = VertCar(
2,
0,
0,
0);
312 V2 = VertCar(
3,
1,
2,
3);
313 V3 = VertCar(
3,
2,
3,
0);
314 V4 = VertCar(
3,
3,
5,
3);
315 H5 = HorzCar(
2,
4,
1,
1);
317 H7 = HorzCar(
2,
6,
3,
5);
318 H8 = HorzCar(
2,
7,
4,
0);
319 H9 = HorzCar(
2,
8,
4,
2);
320 system V1, V2, V3, V4, H5, RED, H7, H8, H9, Player;
324 <formula>E
<> Player.done ==
1