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.
5 broadcast chan cool, inr[
2], outr[
2];
8 <name x=
"5" y=
"5">Tank
</name>
9 <declaration>// Place local declarations here.
10 clock temp =
102.0;
</declaration>
11 <location id=
"id0" x=
"-535" y=
"42">
12 <name x=
"-612" y=
"8">overheating
</name>
13 <label kind=
"invariant" x=
"-620" y=
"59">temp' ==
1.0</label>
15 <location id=
"id1" x=
"-119" y=
"0">
16 <name x=
"-93" y=
"-8">cooling2
</name>
17 <label kind=
"invariant" x=
"-93" y=
"17">temp' ==
0.1*temp -
12.0
18 && temp
> 102</label>
20 <location id=
"id2" x=
"-127" y=
"-127">
21 <name x=
"-93" y=
"-136">cooling1
</name>
22 <label kind=
"invariant" x=
"-137" y=
"-110">temp' ==
0.1*temp -
11.2
23 && temp
> 102</label>
25 <location id=
"id3" x=
"-238" y=
"-76">
26 <label kind=
"invariant" x=
"-365" y=
"-59">temp' ==
0.1*temp -
10.0</label>
29 <location id=
"id4" x=
"-416" y=
"-76">
30 <name x=
"-492" y=
"-110">inRange
</name>
31 <label kind=
"invariant" x=
"-731" y=
"-85">temp' ==
0.1*temp -
10.0 && temp
< 110</label>
38 <label kind=
"synchronisation" x=
"-517" y=
"-34">temp
>=
110</label>
43 <label kind=
"guard" x=
"-390" y=
"38">temp
>=
102 && temp
<=
105</label>
44 <label kind=
"synchronisation" x=
"-390" y=
"55">outr[
1]!
</label>
45 <nail x=
"-119" y=
"76"/>
46 <nail x=
"-408" y=
"68"/>
51 <label kind=
"guard" x=
"-398" y=
"-246">temp
>=
102 && temp
<=
105</label>
52 <label kind=
"synchronisation" x=
"-398" y=
"-229">outr[
0]!
</label>
53 <nail x=
"-127" y=
"-212"/>
54 <nail x=
"-416" y=
"-212"/>
59 <label kind=
"synchronisation" x=
"-204" y=
"-25">inr[
1]?
</label>
64 <label kind=
"synchronisation" x=
"-220" y=
"-118">inr[
0]?
</label>
69 <label kind=
"guard" x=
"-357" y=
"-110">temp
>=
110</label>
70 <label kind=
"synchronisation" x=
"-340" y=
"-93">cool!
</label>
75 <parameter>int[
0,
1] id
</parameter>
76 <declaration>clock t;
</declaration>
77 <location id=
"id5" x=
"-221" y=
"-144">
78 <name x=
"-246" y=
"-127">cooling
</name>
81 <location id=
"id6" x=
"-323" y=
"-144">
82 <name x=
"-357" y=
"-127">inVessel
</name>
84 <location id=
"id7" x=
"-391" y=
"-144">
87 <location id=
"id8" x=
"-459" y=
"-144">
88 <name x=
"-493" y=
"-127">available
</name>
94 <label kind=
"guard" x=
"-449" y=
"-272">t
>=
20</label>
95 <nail x=
"-221" y=
"-238"/>
96 <nail x=
"-467" y=
"-238"/>
101 <label kind=
"synchronisation" x=
"-305" y=
"-161">outr[id]?
</label>
102 <label kind=
"assignment" x=
"-305" y=
"-144">t=
0</label>
107 <label kind=
"synchronisation" x=
"-374" y=
"-170">inr[id]!
</label>
112 <label kind=
"synchronisation" x=
"-441" y=
"-161">cool?
</label>
115 <system>// Place template instantiations here.
116 // List one or more processes to be composed into a system.
123 <formula>Pr [
<=
100] (
<> Tank.overheating)