From: pimjager <pim@pimjager.nl>
Date: Thu, 16 Jun 2016 14:54:46 +0000 (+0200)
Subject: Kut UPPAAL stik er in
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=9246e172503063182077123de3815100ed20de73;p=mc1516the.git

Kut UPPAAL stik er in
---

diff --git a/uppaal/3_v2.xml b/uppaal/3_v2.xml
new file mode 100644
index 0000000..8f30c8a
--- /dev/null
+++ b/uppaal/3_v2.xml
@@ -0,0 +1,110 @@
+<?xml version="1.0" encoding="utf-8"?>
+<!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.
+
+clock r1, r2;
+clock t;
+clock time;</declaration>
+	<template>
+		<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="-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="-42" y="85">
+			<name x="-52" y="51">rod2</name>
+			<label kind="invariant" x="-34" y="102">t' == 0.1*t - 12.0
+&amp;&amp; r1' == 1 
+&amp;&amp; r2' == 1</label>
+			<urgent/>
+		</location>
+		<location id="id3" x="-42" y="-68">
+			<name x="-52" y="-102">rod1</name>
+			<label kind="invariant" x="-25" y="-76">t' == 0.1*t - 11.2
+&amp;&amp; r1' == 1 
+&amp;&amp; r2' == 1</label>
+			<urgent/>
+		</location>
+		<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>
+			<urgent/>
+		</location>
+		<init ref="id0"/>
+		<transition>
+			<source ref="id0"/>
+			<target ref="id0"/>
+			<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="id0"/>
+			<target ref="id4"/>
+			<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="-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="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="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="-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.
+v = Vessel();
+system v;
+    </system>
+	<queries>
+		<query>
+			<formula>simulate 5 [&lt;=50] { t }
+			</formula>
+			<comment>
+			</comment>
+		</query>
+	</queries>
+</nta>