X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=uppaal%2F3.xml;h=3351546e6175bf36e2ac93e03d73ac46d5c9b123;hb=ab82a74fde0ebab959eacf4f8c5c8f0da8ff2a40;hp=6824ba4dbd5d59fce12d61d20ae72fa7c6ce051f;hpb=8439966f2bc1fe022435fa8fa314d5354952a9fe;p=mc1516the.git

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