<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>\r
<nta>\r
<declaration>// Place global declarations here.
-broadcast chan cool, inr[2], outr[2];
-</declaration>\r
+
+clock r1, r2;
+clock t;</declaration>\r
<template>\r
- <name x="5" y="5">Tank</name>\r
- <declaration>// Place local declarations here.
-clock temp = 102.0;</declaration>\r
- <location id="id0" x="-535" y="42">\r
- <name x="-612" y="8">overheating</name>\r
- <label kind="invariant" x="-620" y="59">temp' == 1.0</label>\r
+ <name x="5" y="5">Vessel</name>\r
+ <declaration>// Place local declarations here.</declaration>\r
+ <location id="id0" x="-374" y="-153">\r
+ <name x="-384" y="-187">Start</name>\r
+ <label kind="invariant" x="-459" y="-161">t <= 102</label>\r
+ <urgent/>\r
</location>\r
- <location id="id1" x="-119" y="0">\r
- <name x="-93" y="-8">cooling2</name>\r
- <label kind="invariant" x="-93" y="17">temp' == 0.1*temp - 12.0
-&& temp > 102</label>\r
+ <location id="id1" x="-467" y="8">\r
+ <name x="-552" y="-25">overheating</name>\r
+ <label kind="invariant" x="-501" y="25">t' == 0.1*t - 10.0
+&& r1' == 1
+&& r2' == 1</label>\r
</location>\r
- <location id="id2" x="-127" y="-127">\r
- <name x="-93" y="-136">cooling1</name>\r
- <label kind="invariant" x="-137" y="-110">temp' == 0.1*temp - 11.2
-&& temp > 102</label>\r
+ <location id="id2" x="-42" y="85">\r
+ <name x="-52" y="51">rod2</name>\r
+ <label kind="invariant" x="-8" y="68">t' == 0.1*t - 11.2
+&& r1' == 1
+&& r2' == 1
+&& t >= 102</label>\r
</location>\r
- <location id="id3" x="-238" y="-76">\r
- <label kind="invariant" x="-365" y="-59">temp' == 0.1*temp - 10.0</label>\r
- <urgent/>\r
+ <location id="id3" x="-42" y="-68">\r
+ <name x="-52" y="-102">rod1</name>\r
+ <label kind="invariant" x="-17" y="-102">t' == 0.1*t - 11.2
+&& r1' == 1
+&& r2' == 1
+&& t >= 102</label>\r
</location>\r
- <location id="id4" x="-416" y="-76">\r
- <name x="-492" y="-110">inRange</name>\r
- <label kind="invariant" x="-731" y="-85">temp' == 0.1*temp - 10.0 && temp < 110</label>\r
- <urgent/>\r
+ <location id="id4" x="-178" y="8">\r
+ <name x="-238" y="-59">inRange</name>\r
+ <label kind="invariant" x="-314" y="17">t' == 0.1*t - 10.0
+&& r1' == 1
+&& r2' == 1
+&& t >= 102
+&& t <= 110</label>\r
</location>\r
- <init ref="id4"/>\r
+ <init ref="id0"/>\r
<transition>\r
- <source ref="id4"/>\r
+ <source ref="id0"/>\r
<target ref="id0"/>\r
- <label kind="synchronisation" x="-517" y="-34">temp >= 110</label>\r
+ <label kind="guard" x="-408" y="-221">t < 102</label>\r
+ <label kind="assignment" x="-493" y="-221">t = 102,
+r1 = 25,
+r2 = 25</label>\r
+ <nail x="-433" y="-195"/>\r
+ <nail x="-331" y="-204"/>\r
</transition>\r
<transition>\r
- <source ref="id1"/>\r
+ <source ref="id0"/>\r
<target ref="id4"/>\r
- <label kind="guard" x="-390" y="38">temp >= 102 && temp <= 105</label>\r
- <label kind="synchronisation" x="-390" y="55">outr[1]!</label>\r
- <nail x="-119" y="76"/>\r
- <nail x="-408" y="68"/>\r
+ <label kind="guard" x="-561" y="-127">t >= 102 && r1 > 20 && r2 > 20</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id4"/>\r
+ <target ref="id1"/>\r
+ <label kind="guard" x="-408" y="-51">t >= 110 &&
+r1 <= 20
+&& r2 <= 20</label>\r
+ <nail x="-195" y="8"/>\r
</transition>\r
<transition>\r
<source ref="id2"/>\r
<target ref="id4"/>\r
- <label kind="guard" x="-398" y="-246">temp >= 102 && temp <= 105</label>\r
- <label kind="synchronisation" x="-398" y="-229">outr[0]!</label>\r
- <nail x="-127" y="-212"/>\r
- <nail x="-416" y="-212"/>\r
+ <label kind="guard" x="-187" y="178">t >= 102 && t <= 105</label>\r
+ <label kind="assignment" x="-160" y="161">r2 = 0</label>\r
+ <nail x="-42" y="161"/>\r
+ <nail x="-178" y="161"/>\r
</transition>\r
<transition>\r
- <source ref="id3"/>\r
- <target ref="id1"/>\r
- <label kind="synchronisation" x="-204" y="-25">inr[1]?</label>\r
+ <source ref="id4"/>\r
+ <target ref="id2"/>\r
+ <label kind="guard" x="-136" y="8">t >= 110 && r2 > 20</label>\r
</transition>\r
<transition>\r
<source ref="id3"/>\r
- <target ref="id2"/>\r
- <label kind="synchronisation" x="-220" y="-118">inr[0]?</label>\r
+ <target ref="id4"/>\r
+ <label kind="guard" x="-160" y="-178">t >= 102 && t <= 105</label>\r
+ <label kind="assignment" x="-153" y="-161">r1 = 0</label>\r
+ <nail x="-42" y="-144"/>\r
+ <nail x="-178" y="-144"/>\r
</transition>\r
<transition>\r
<source ref="id4"/>\r
<target ref="id3"/>\r
- <label kind="guard" x="-357" y="-110">temp >= 110</label>\r
- <label kind="synchronisation" x="-340" y="-93">cool!</label>\r
- </transition>\r
- </template>\r
- <template>\r
- <name>Rod</name>\r
- <parameter>int[0,1] id</parameter>\r
- <declaration>clock t;</declaration>\r
- <location id="id5" x="-221" y="-144">\r
- <name x="-246" y="-127">cooling</name>\r
- <urgent/>\r
- </location>\r
- <location id="id6" x="-323" y="-144">\r
- <name x="-357" y="-127">inVessel</name>\r
- </location>\r
- <location id="id7" x="-391" y="-144">\r
- <urgent/>\r
- </location>\r
- <location id="id8" x="-459" y="-144">\r
- <name x="-493" y="-127">available</name>\r
- </location>\r
- <init ref="id8"/>\r
- <transition>\r
- <source ref="id5"/>\r
- <target ref="id8"/>\r
- <label kind="guard" x="-449" y="-272">t >= 20</label>\r
- <nail x="-221" y="-238"/>\r
- <nail x="-467" y="-238"/>\r
- </transition>\r
- <transition>\r
- <source ref="id6"/>\r
- <target ref="id5"/>\r
- <label kind="synchronisation" x="-305" y="-161">outr[id]?</label>\r
- <label kind="assignment" x="-305" y="-144">t=0</label>\r
- </transition>\r
- <transition>\r
- <source ref="id7"/>\r
- <target ref="id6"/>\r
- <label kind="synchronisation" x="-374" y="-170">inr[id]!</label>\r
- </transition>\r
- <transition>\r
- <source ref="id8"/>\r
- <target ref="id7"/>\r
- <label kind="synchronisation" x="-441" y="-161">cool?</label>\r
+ <label kind="guard" x="-136" y="-17">t >= 110 && r1 > 20</label>\r
</transition>\r
</template>\r
<system>// Place template instantiations here.
// List one or more processes to be composed into a system.
-r1 = Rod(0);
-r2 = Rod(1);
-system Tank, r1, r2;
+v = Vessel();
+system v;
</system>\r
<queries>\r
<query>\r
- <formula>Pr [<=100] (<> Tank.overheating)\r
+ <formula>Pr [<=100] (<> v.overheating)\r
+ </formula>\r
+ <comment>\r
+ </comment>\r
+ </query>\r
+ <query>\r
+ <formula>simulate 5 [<=100] { t }\r
</formula>\r
<comment>\r
</comment>\r