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 broadcast chan cool, inr[2], outr[2];
   6 </declaration>
   7         <template>
   8                 <name x="5" y="5">Tank</name>
   9                 <declaration>// Place local declarations here.
  10 clock temp = 102.0;</declaration>
  11                 <location id="id0" x="-535" y="42">
  12                         <name x="-612" y="8">overheating</name>
  13                         <label kind="invariant" x="-620" y="59">temp' == 1.0</label>
  14                 </location>
  15                 <location id="id1" x="-119" y="0">
  16                         <name x="-93" y="-8">cooling2</name>
  17                         <label kind="invariant" x="-93" y="17">temp' == 0.1*temp - 12.0
  18 &amp;&amp; temp &gt; 102</label>
  19                 </location>
  20                 <location id="id2" x="-127" y="-127">
  21                         <name x="-93" y="-136">cooling1</name>
  22                         <label kind="invariant" x="-137" y="-110">temp' == 0.1*temp - 11.2
  23 &amp;&amp; temp &gt; 102</label>
  24                 </location>
  25                 <location id="id3" x="-238" y="-76">
  26                         <label kind="invariant" x="-365" y="-59">temp' == 0.1*temp - 10.0</label>
  27                         <urgent/>
  28                 </location>
  29                 <location id="id4" x="-416" y="-76">
  30                         <name x="-492" y="-110">inRange</name>
  31                         <label kind="invariant" x="-731" y="-85">temp' == 0.1*temp - 10.0 &amp;&amp; temp &lt; 110</label>
  32                         <urgent/>
  33                 </location>
  34                 <init ref="id4"/>
  35                 <transition>
  36                         <source ref="id4"/>
  37                         <target ref="id0"/>
  38                         <label kind="synchronisation" x="-517" y="-34">temp &gt;= 110</label>
  39                 </transition>
  40                 <transition>
  41                         <source ref="id1"/>
  42                         <target ref="id4"/>
  43                         <label kind="guard" x="-390" y="38">temp &gt;= 102 &amp;&amp; temp &lt;= 105</label>
  44                         <label kind="synchronisation" x="-390" y="55">outr[1]!</label>
  45                         <nail x="-119" y="76"/>
  46                         <nail x="-408" y="68"/>
  47                 </transition>
  48                 <transition>
  49                         <source ref="id2"/>
  50                         <target ref="id4"/>
  51                         <label kind="guard" x="-398" y="-246">temp &gt;= 102 &amp;&amp; temp &lt;= 105</label>
  52                         <label kind="synchronisation" x="-398" y="-229">outr[0]!</label>
  53                         <nail x="-127" y="-212"/>
  54                         <nail x="-416" y="-212"/>
  55                 </transition>
  56                 <transition>
  57                         <source ref="id3"/>
  58                         <target ref="id1"/>
  59                         <label kind="synchronisation" x="-204" y="-25">inr[1]?</label>
  60                 </transition>
  61                 <transition>
  62                         <source ref="id3"/>
  63                         <target ref="id2"/>
  64                         <label kind="synchronisation" x="-220" y="-118">inr[0]?</label>
  65                 </transition>
  66                 <transition>
  67                         <source ref="id4"/>
  68                         <target ref="id3"/>
  69                         <label kind="guard" x="-357" y="-110">temp &gt;= 110</label>
  70                         <label kind="synchronisation" x="-340" y="-93">cool!</label>
  71                 </transition>
  72         </template>
  73         <template>
  74                 <name>Rod</name>
  75                 <parameter>int[0,1] id</parameter>
  76                 <declaration>clock t;</declaration>
  77                 <location id="id5" x="-221" y="-144">
  78                         <name x="-246" y="-127">cooling</name>
  79                         <urgent/>
  80                 </location>
  81                 <location id="id6" x="-323" y="-144">
  82                         <name x="-357" y="-127">inVessel</name>
  83                 </location>
  84                 <location id="id7" x="-391" y="-144">
  85                         <urgent/>
  86                 </location>
  87                 <location id="id8" x="-459" y="-144">
  88                         <name x="-493" y="-127">available</name>
  89                 </location>
  90                 <init ref="id8"/>
  91                 <transition>
  92                         <source ref="id5"/>
  93                         <target ref="id8"/>
  94                         <label kind="guard" x="-449" y="-272">t &gt;= 20</label>
  95                         <nail x="-221" y="-238"/>
  96                         <nail x="-467" y="-238"/>
  97                 </transition>
  98                 <transition>
  99                         <source ref="id6"/>
 100                         <target ref="id5"/>
 101                         <label kind="synchronisation" x="-305" y="-161">outr[id]?</label>
 102                         <label kind="assignment" x="-305" y="-144">t=0</label>
 103                 </transition>
 104                 <transition>
 105                         <source ref="id7"/>
 106                         <target ref="id6"/>
 107                         <label kind="synchronisation" x="-374" y="-170">inr[id]!</label>
 108                 </transition>
 109                 <transition>
 110                         <source ref="id8"/>
 111                         <target ref="id7"/>
 112                         <label kind="synchronisation" x="-441" y="-161">cool?</label>
 113                 </transition>
 114         </template>
 115         <system>// Place template instantiations here.
 116 // List one or more processes to be composed into a system.
 117 r1 = Rod(0);
 118 r2 = Rod(1);
 119 system Tank, r1, r2;
 120     </system>
 121         <queries>
 122                 <query>
 123                         <formula>Pr [&lt;=100]  (&lt;&gt; Tank.overheating)
 124                         </formula>
 125                         <comment>
 126                         </comment>
 127                 </query>
 128         </queries>
 129 </nta>