uppaal/3.xml

   1 <?xml version="1.0" encoding="utf-8"?>
   2 <!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>
   3 <nta>
   4         <declaration>// Place global declarations here.
   5
   6 clock r1, r2;
   7 clock t;</declaration>
   8         <template>
   9                 <name x="5" y="5">Vessel</name>
  10                 <declaration>// Place local declarations here.</declaration>
  11                 <location id="id0" x="-374" y="-153">
  12                         <name x="-384" y="-187">Start</name>
  13                         <label kind="invariant" x="-459" y="-161">t &lt;= 102</label>
  14                         <urgent/>
  15                 </location>
  16                 <location id="id1" x="-467" y="8">
  17                         <name x="-552" y="-25">overheating</name>
  18                         <label kind="invariant" x="-501" y="25">t' == 0.1*t - 10.0
  19 &amp;&amp; r1' == 1
  20 &amp;&amp; r2' == 1</label>
  21                 </location>
  22                 <location id="id2" x="-42" y="85">
  23                         <name x="-52" y="51">rod2</name>
  24                         <label kind="invariant" x="-8" y="68">t' == 0.1*t - 11.2
  25 &amp;&amp; r1' == 1
  26 &amp;&amp; r2' == 1
  27 &amp;&amp; t &gt;= 102</label>
  28                 </location>
  29                 <location id="id3" x="-42" y="-68">
  30                         <name x="-52" y="-102">rod1</name>
  31                         <label kind="invariant" x="-17" y="-102">t' == 0.1*t - 11.2
  32 &amp;&amp; r1' == 1
  33 &amp;&amp; r2' == 1
  34 &amp;&amp; t &gt;= 102</label>
  35                 </location>
  36                 <location id="id4" x="-178" y="8">
  37                         <name x="-238" y="-59">inRange</name>
  38                         <label kind="invariant" x="-314" y="17">t' == 0.1*t - 10.0
  39 &amp;&amp; r1' == 1
  40 &amp;&amp; r2' == 1
  41 &amp;&amp; t &gt;= 102
  42 &amp;&amp; t &lt;= 110</label>
  43                 </location>
  44                 <init ref="id0"/>
  45                 <transition>
  46                         <source ref="id0"/>
  47                         <target ref="id0"/>
  48                         <label kind="guard" x="-408" y="-221">t &lt; 102</label>
  49                         <label kind="assignment" x="-493" y="-221">t = 102,
  50 r1 = 25,
  51 r2 = 25</label>
  52                         <nail x="-433" y="-195"/>
  53                         <nail x="-331" y="-204"/>
  54                 </transition>
  55                 <transition>
  56                         <source ref="id0"/>
  57                         <target ref="id4"/>
  58                         <label kind="guard" x="-561" y="-127">t &gt;= 102 &amp;&amp; r1 &gt; 20 &amp;&amp; r2 &gt; 20</label>
  59                 </transition>
  60                 <transition>
  61                         <source ref="id4"/>
  62                         <target ref="id1"/>
  63                         <label kind="guard" x="-408" y="-51">t &gt;= 110 &amp;&amp;
  64 r1 &lt;= 20
  65 &amp;&amp; r2 &lt;= 20</label>
  66                         <nail x="-195" y="8"/>
  67                 </transition>
  68                 <transition>
  69                         <source ref="id2"/>
  70                         <target ref="id4"/>
  71                         <label kind="guard" x="-187" y="178">t &gt;= 102 &amp;&amp; t &lt;= 105</label>
  72                         <label kind="assignment" x="-160" y="161">r2 = 0</label>
  73                         <nail x="-42" y="161"/>
  74                         <nail x="-178" y="161"/>
  75                 </transition>
  76                 <transition>
  77                         <source ref="id4"/>
  78                         <target ref="id2"/>
  79                         <label kind="guard" x="-136" y="8">t &gt;= 110 &amp;&amp; r2 &gt; 20</label>
  80                 </transition>
  81                 <transition>
  82                         <source ref="id3"/>
  83                         <target ref="id4"/>
  84                         <label kind="guard" x="-160" y="-178">t &gt;= 102 &amp;&amp; t &lt;= 105</label>
  85                         <label kind="assignment" x="-153" y="-161">r1 = 0</label>
  86                         <nail x="-42" y="-144"/>
  87                         <nail x="-178" y="-144"/>
  88                 </transition>
  89                 <transition>
  90                         <source ref="id4"/>
  91                         <target ref="id3"/>
  92                         <label kind="guard" x="-136" y="-17">t &gt;= 110 &amp;&amp; r1 &gt; 20</label>
  93                 </transition>
  94         </template>
  95         <system>// Place template instantiations here.
  96 // List one or more processes to be composed into a system.
  97 v = Vessel();
  98 system v;
  99     </system>
 100         <queries>
 101                 <query>
 102                         <formula>Pr [&lt;=100] (&lt;&gt; v.overheating)
 103                         </formula>
 104                         <comment>
 105                         </comment>
 106                 </query>
 107                 <query>
 108                         <formula>simulate 5 [&lt;=100] { t }
 109                         </formula>
 110                         <comment>
 111                         </comment>
 112                 </query>
 113         </queries>
 114 </nta>