From: pimjager <pim@pimjager.nl>
Date: Thu, 16 Jun 2016 12:52:58 +0000 (+0200)
Subject: Working on 3, f-ing uppaal is giving absurd errors
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=861c69dba9b4bc8944c1eb09101351503ab2a9bb;p=mc1516the.git

Working on 3, f-ing uppaal is giving absurd errors
---

diff --git a/uppaal/3.xml b/uppaal/3.xml
new file mode 100644
index 0000000..5861b32
--- /dev/null
+++ b/uppaal/3.xml
@@ -0,0 +1,121 @@
+<?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.
+chan cool, inr[2], outr[2];
+</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>
+		</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>
+		<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>
+		<location id="id3" x="-238" y="-76">
+			<label kind="invariant" x="-365" y="-59">temp' == 0.1*temp - 10.0</label>
+			<urgent/>
+		</location>
+		<location id="id4" x="-408" y="-76">
+			<name x="-484" y="-110">inRange</name>
+			<label kind="invariant" x="-595" y="-85">temp' == 0.1*temp - 10.0</label>
+		</location>
+		<init ref="id4"/>
+		<transition>
+			<source ref="id4"/>
+			<target ref="id0"/>
+		</transition>
+		<transition>
+			<source ref="id1"/>
+			<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"/>
+		</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"/>
+		</transition>
+		<transition>
+			<source ref="id3"/>
+			<target ref="id1"/>
+			<label kind="synchronisation" x="-204" y="-25">inr[1]?</label>
+		</transition>
+		<transition>
+			<source ref="id3"/>
+			<target ref="id2"/>
+			<label kind="synchronisation" x="-220" y="-118">inr[0]?</label>
+		</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>
+		</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;
+    </system>
+	<queries>
+	</queries>
+</nta>