hoi

diff --git a/a.pdf b/a.pdf
index 9ee5c69..baac29d 100644 (file)
Binary files a/a.pdf and b/a.pdf differ

diff --git a/uppaal/3.xml b/uppaal/3.xml
index 5861b32..6824ba4 100644 (file)
--- a/uppaal/3.xml
+++ b/uppaal/3.xml
@@ -2,7 +2,7 @@
 <!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.
-chan cool, inr[2], outr[2];
+broadcast chan cool, inr[2], outr[2];
 </declaration>\r
        <template>\r
                <name x="5" y="5">Tank</name>\r
@@ -26,14 +26,16 @@ clock temp = 102.0;</declaration>
                        <label kind="invariant" x="-365" y="-59">temp' == 0.1*temp - 10.0</label>\r
                        <urgent/>\r
                </location>\r
-               <location id="id4" x="-408" y="-76">\r
-                       <name x="-484" y="-110">inRange</name>\r
-                       <label kind="invariant" x="-595" y="-85">temp' == 0.1*temp - 10.0</label>\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 &amp;&amp; temp &lt; 110</label>\r
+                       <urgent/>\r
                </location>\r
                <init ref="id4"/>\r
                <transition>\r
                        <source ref="id4"/>\r
                        <target ref="id0"/>\r
+                       <label kind="synchronisation" x="-517" y="-34">temp &gt;= 110</label>\r
                </transition>\r
                <transition>\r
                        <source ref="id1"/>\r
@@ -117,5 +119,11 @@ r2 = Rod(1);
 system Tank, r1, r2;
     </system>\r
        <queries>\r
+               <query>\r
+                       <formula>Pr [&lt;=100]  (&lt;&gt; Tank.overheating)\r
+                       </formula>\r
+                       <comment>\r
+                       </comment>\r
+               </query>\r
        </queries>\r
 </nta>\r