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.
10 typedef int[
0,N-
1] id_c;
12 broadcast chan up[N], down[N], left[N], right[N], start, leftRed, rightRed;
16 bool grid[
6][
6];
</declaration>
18 <name x=
"5" y=
"5">HorzCar
</name>
19 <parameter>int[
2,
3] length, const id_c id, int[
0,
4] x, const int[
0,
5] y
</parameter>
20 <declaration>// Place local declarations here.
24 for (i=
0; i
<length; i++) {
28 <location id=
"id0" x=
"-425" y=
"-51">
30 <location id=
"id1" x=
"-535" y=
"-136">
33 <location id=
"id2" x=
"-212" y=
"-76">
39 <label kind=
"synchronisation" x=
"-407" y=
"-80">start?
</label>
44 <label kind=
"synchronisation" x=
"-517" y=
"-110">reg!
</label>
45 <label kind=
"assignment" x=
"-517" y=
"-93">register()
</label>
50 <label kind=
"guard" x=
"-288" y=
"-68">x
>0 && !grid[x-
1][y]
</label>
51 <label kind=
"synchronisation" x=
"-288" y=
"-51">down[id]!
</label>
52 <label kind=
"assignment" x=
"-288" y=
"-34">x:=x-
1</label>
53 <nail x=
"-306" y=
"8"/>
54 <nail x=
"-136" y=
"0"/>
59 <label kind=
"guard" x=
"-306" y=
"-204">x+length
< 6 && !grid[x+length][y]
</label>
60 <label kind=
"synchronisation" x=
"-314" y=
"-153">up[id]!
</label>
61 <label kind=
"assignment" x=
"-306" y=
"-178">x:=x+
1</label>
62 <nail x=
"-323" y=
"-102"/>
63 <nail x=
"-195" y=
"-178"/>
64 <nail x=
"-110" y=
"-102"/>
69 <parameter>int[
2,
3] length, const id_c id, const int[
0,
5] x, int[
0,
4] y
</parameter>
70 <declaration>void register() {
72 for(i=
0; i
<length; i++){
77 <location id=
"id3" x=
"-314" y=
"-34">
79 <location id=
"id4" x=
"-416" y=
"-76">
82 <location id=
"id5" x=
"-102" y=
"-34">
88 <label kind=
"synchronisation" x=
"-228" y=
"-72">start?
</label>
93 <label kind=
"synchronisation" x=
"-374" y=
"-110">reg!
</label>
94 <label kind=
"assignment" x=
"-374" y=
"-76">register()
</label>
95 <nail x=
"-255" y=
"-85"/>
100 <label kind=
"guard" x=
"-135" y=
"8">y
>0 && !grid[x][y-
1]
</label>
101 <label kind=
"synchronisation" x=
"-135" y=
"25">left[id]!
</label>
102 <label kind=
"assignment" x=
"-135" y=
"42">y:=y-
1</label>
103 <nail x=
"-153" y=
"42"/>
104 <nail x=
"-34" y=
"42"/>
109 <label kind=
"guard" x=
"-160" y=
"-102">y+length
< 6 && !grid[x][y+length]
</label>
110 <label kind=
"synchronisation" x=
"-160" y=
"-85">right[id]!
</label>
111 <label kind=
"assignment" x=
"-160" y=
"-68">y:=y+
1</label>
112 <nail x=
"-178" y=
"-102"/>
113 <nail x=
"-34" y=
"-102"/>
118 <declaration>int[
0,N] registered;
</declaration>
119 <location id=
"id6" x=
"-680" y=
"-246">
121 <location id=
"id7" x=
"-799" y=
"-246">
127 <label kind=
"guard" x=
"-781" y=
"-280">registered == N
</label>
128 <label kind=
"synchronisation" x=
"-781" y=
"-263">start!
</label>
133 <label kind=
"synchronisation" x=
"-875" y=
"-365">reg?
</label>
134 <label kind=
"assignment" x=
"-926" y=
"-382">registered := registered+
1</label>
135 <nail x=
"-892" y=
"-263"/>
136 <nail x=
"-833" y=
"-331"/>
137 <nail x=
"-765" y=
"-314"/>
142 <parameter>const id_c id, int[
0,
5] x
</parameter>
143 <declaration>void register() {
147 <location id=
"id8" x=
"51" y=
"-59">
149 <location id=
"id9" x=
"-93" y=
"-68">
151 <location id=
"id10" x=
"-204" y=
"-68">
158 <label kind=
"guard" x=
"-7" y=
"-42">x
> 0 && grid[x-
1][
3]
</label>
159 <label kind=
"synchronisation" x=
"-7" y=
"-25">leftRed!
</label>
160 <label kind=
"assignment" x=
"-7" y=
"-8">x := x-
1, grid[x+
1][
3] := false, grid[x-
1][
3] := true
</label>
161 <nail x=
"-25" y=
"42"/>
162 <nail x=
"178" y=
"51"/>
167 <label kind=
"guard" x=
"1" y=
"-135">x+
2 < 6 && grid[x+
2][
3]
</label>
168 <label kind=
"synchronisation" x=
"1" y=
"-118">rightRed!
</label>
169 <label kind=
"assignment" x=
"1" y=
"-101">x := x+
1, grid[x][
3] := false, grid[x+
2][
3] := true
</label>
170 <nail x=
"-17" y=
"-144"/>
171 <nail x=
"144" y=
"-136"/>
176 <label kind=
"synchronisation" x=
"-75" y=
"-80">start?
</label>
181 <label kind=
"synchronisation" x=
"-186" y=
"-85">reg!
</label>
182 <label kind=
"assignment" x=
"-186" y=
"-68">register()
</label>
185 <system>// Place template instantiations here.
187 // Intermediate puzzle
188 H1 = HorzCar(
2,
0,
0,
5);
189 H2 = HorzCar(
2,
1,
2,
5);
190 V3 = VertCar(
2,
2,
4,
4);
191 V4 = VertCar(
2,
3,
2,
3);
192 V5 = VertCar(
3,
4,
5,
2);
193 V6 = VertCar(
2,
5,
1,
3);
194 H7 = HorzCar(
2,
6,
3,
4);
195 H8 = HorzCar(
2,
7,
3,
2);
196 V9 = VertCar(
3,
8,
0,
0);
197 HA = HorzCar(
2,
9,
1,
0);
198 VB = VertCar(
2,
10,
3,
0);
199 HC = HorzCar(
2,
11,
4,
1);
200 HD = HorzCar(
2,
12,
4,
0);
201 system H1, H2, V3, V4, V5, V6, H7, H8, V9, HA, VB, HC, HD, Player;
205 H1 = HorzCar(
2,
0,
0,
5);
206 V2 = VertCar(
2,
1,
2,
4);
207 V3 = VertCar(
3,
2,
3,
3);
208 V4 = VertCar(
3,
3,
0,
2);
209 H5 = HorzCar(
2,
4,
1,
3);
210 H6 = HorzCar(
3,
5,
1,
2);
211 H7 = HorzCar(
3,
6,
3,
0);
212 system H1, V2, V3, V4, H5, H6, H7
215 // List one or more processes to be composed into a system.