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 chan approach, in, out, ex, lower, raise, down, up;
</declaration>
9 <name x=
"5" y=
"5">Train
</name>
10 <declaration>// Place local declarations here.
</declaration>
11 <location id=
"id0" x=
"-119" y=
"17">
12 <name x=
"-187" y=
"-17">safe
</name>
13 <label kind=
"invariant" x=
"-187" y=
"17">x
<=
5</label>
15 <location id=
"id1" x=
"8" y=
"17">
16 <name x=
"-2" y=
"-17">unsafe
</name>
17 <label kind=
"invariant" x=
"-2" y=
"34">x
<=
5</label>
19 <location id=
"id2" x=
"0" y=
"-110">
20 <name x=
"-10" y=
"-144">aproaching
</name>
21 <label kind=
"invariant" x=
"25" y=
"-136">x
<=
5</label>
23 <location id=
"id3" x=
"-127" y=
"-102">
24 <name x=
"-137" y=
"-136">initial
</name>
30 <label kind=
"synchronisation" x=
"-119" y=
"-59">ex!
</label>
35 <label kind=
"synchronisation" x=
"-101" y=
"0">out!
</label>
40 <label kind=
"guard" x=
"4" y=
"-80">x
>2</label>
41 <label kind=
"synchronisation" x=
"4" y=
"-63">in!
</label>
46 <label kind=
"synchronisation" x=
"-102" y=
"-127">approach!
</label>
47 <label kind=
"assignment" x=
"-93" y=
"-102">x:=
0</label>
52 <location id=
"id4" x=
"0" y=
"0">
58 <label kind=
"synchronisation" x=
"-119" y=
"-59">in?
</label>
59 <nail x=
"-68" y=
"-85"/>
60 <nail x=
"-85" y=
"-8"/>
65 <label kind=
"synchronisation" x=
"93" y=
"-17">out?
</label>
66 <nail x=
"93" y=
"-59"/>
72 <label kind=
"synchronisation" x=
"-67" y=
"4">down?
</label>
73 <nail x=
"-85" y=
"42"/>
79 <label kind=
"synchronisation" x=
"1" y=
"-85">up?
</label>
80 <nail x=
"-17" y=
"-68"/>
81 <nail x=
"68" y=
"-68"/>
86 <location id=
"id5" x=
"-204" y=
"-25">
87 <name x=
"-246" y=
"0">raising
</name>
88 <label kind=
"invariant" x=
"-274" y=
"-33">y
<=
2</label>
90 <location id=
"id6" x=
"-42" y=
"-25">
91 <name x=
"-34" y=
"8">lowered
</name>
93 <location id=
"id7" x=
"-42" y=
"-161">
94 <name x=
"-52" y=
"-195">lowering
</name>
95 <label kind=
"invariant" x=
"-25" y=
"-161">y
<=
1</label>
97 <location id=
"id8" x=
"-204" y=
"-161">
98 <name x=
"-214" y=
"-195">raised
</name>
104 <label kind=
"guard" x=
"-191" y=
"-127">y
>=
1</label>
105 <label kind=
"synchronisation" x=
"-178" y=
"-110">up!
</label>
110 <label kind=
"synchronisation" x=
"-160" y=
"-42">raise?
</label>
111 <label kind=
"assignment" x=
"-160" y=
"-25">y:=
0</label>
116 <label kind=
"synchronisation" x=
"-42" y=
"-110">down!
</label>
121 <label kind=
"synchronisation" x=
"-160" y=
"-178">lower?
</label>
122 <label kind=
"assignment" x=
"-160" y=
"-161">y:=
0</label>
126 <name>Controller
</name>
127 <location id=
"id9" x=
"187" y=
"-68">
128 <name x=
"177" y=
"-102">trainComing
</name>
129 <label kind=
"invariant" x=
"229" y=
"-76">z
<=
1</label>
131 <location id=
"id10" x=
"-153" y=
"-76">
132 <name x=
"-229" y=
"-51">trainLeaving
</name>
133 <label kind=
"invariant" x=
"-221" y=
"-85">z
<=
1</label>
135 <location id=
"id11" x=
"-8" y=
"-76">
141 <label kind=
"synchronisation" x=
"-143" y=
"-178">raise!
</label>
142 <nail x=
"-161" y=
"-161"/>
143 <nail x=
"-17" y=
"-161"/>
148 <label kind=
"synchronisation" x=
"-135" y=
"-93">ex?
</label>
149 <label kind=
"assignment" x=
"-135" y=
"-76">z:=
0</label>
154 <label kind=
"guard" x=
"10" y=
"-22">z==
1</label>
155 <label kind=
"synchronisation" x=
"10" y=
"-5">lower!
</label>
156 <nail x=
"187" y=
"17"/>
162 <label kind=
"synchronisation" x=
"10" y=
"-89">approach?
</label>
163 <label kind=
"assignment" x=
"10" y=
"-72">z:=
0</label>
166 <system>// Place template instantiations here.
171 // List one or more processes to be composed into a system.
172 system T, G, C, Gezeik;