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.
7 typedef int[
0,N-
1] id_c;
9 chan up[N], down[N], left[N], right[N];
</declaration>
11 <name x=
"5" y=
"5">VertCar
</name>
12 <parameter>int[
2,
3] length, const id_c id, int[
0,
5] x, const int[
0,
4] y
</parameter>
13 <declaration>// Place local declarations here.
</declaration>
14 <location id=
"id0" x=
"-212" y=
"-76">
20 <label kind=
"guard" x=
"-288" y=
"-68">x
>0</label>
21 <label kind=
"synchronisation" x=
"-288" y=
"-51">down[id]!
</label>
22 <label kind=
"assignment" x=
"-288" y=
"-34">x:=x-
1</label>
23 <nail x=
"-306" y=
"8"/>
24 <nail x=
"-136" y=
"0"/>
29 <label kind=
"guard" x=
"-306" y=
"-204">x+length
< 6</label>
30 <label kind=
"synchronisation" x=
"-314" y=
"-153">up[id]!
</label>
31 <label kind=
"assignment" x=
"-306" y=
"-178">x:=x+
1</label>
32 <nail x=
"-323" y=
"-102"/>
33 <nail x=
"-195" y=
"-178"/>
34 <nail x=
"-110" y=
"-102"/>
39 <parameter>int[
2,
3] length, const id_c id, const int[
0,
4] x, int[
0,
5] y
</parameter>
40 <location id=
"id1" x=
"-102" y=
"-34">
46 <label kind=
"guard" x=
"-135" y=
"8">y
>0</label>
47 <label kind=
"synchronisation" x=
"-135" y=
"25">left[id]!
</label>
48 <label kind=
"assignment" x=
"-135" y=
"42">y:=y-
1</label>
49 <nail x=
"-153" y=
"42"/>
50 <nail x=
"-34" y=
"42"/>
55 <label kind=
"guard" x=
"-160" y=
"-102">y+length
< 6</label>
56 <label kind=
"synchronisation" x=
"-160" y=
"-85">right[id]!
</label>
57 <label kind=
"assignment" x=
"-160" y=
"-68">y:=y+
1</label>
58 <nail x=
"-178" y=
"-102"/>
59 <nail x=
"-34" y=
"-102"/>
64 <location id=
"id2" x=
"-476" y=
"-178">
68 <system>// Place template instantiations here.
69 H1 = HorzCar(
2,
0,
0,
5);
70 H2 = HorzCar(
2,
1,
2,
5);
71 V3 = VertCar(
2,
2,
4,
4);
72 V4 = VertCar(
2,
3,
2,
3);
73 V5 = VertCar(
3,
4,
5,
2);
74 V6 = VertCar(
2,
5,
1,
3);
75 H7 = HorzCar(
2,
6,
3,
4);
76 H8 = HorzCar(
2,
7,
3,
2);
77 V9 = VertCar(
3,
8,
0,
0);
78 HA = HorzCar(
2,
9,
1,
0);
79 VB = VertCar(
2,
10,
3,
0);
80 HC = HorzCar(
2,
11,
4,
1);
81 HD = HorzCar(
2,
12,
4,
0);
82 // List one or more processes to be composed into a system.
83 system H1, H2, V3, V4, V5, V6, H7, H8, V9, HA, VB, HC, HD;