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 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="-408" y="-76">
  30                         <name x="-484" y="-110">inRange</name>
  31                         <label kind="invariant" x="-595" y="-85">temp' == 0.1*temp - 10.0</label>
  32                 </location>
  33                 <init ref="id4"/>
  34                 <transition>
  35                         <source ref="id4"/>
  36                         <target ref="id0"/>
  37                 </transition>
  38                 <transition>
  39                         <source ref="id1"/>
  40                         <target ref="id4"/>
  41                         <label kind="guard" x="-390" y="38">temp &gt;= 102 &amp;&amp; temp &lt;= 105</label>
  42                         <label kind="synchronisation" x="-390" y="55">outr[1]!</label>
  43                         <nail x="-119" y="76"/>
  44                         <nail x="-408" y="68"/>
  45                 </transition>
  46                 <transition>
  47                         <source ref="id2"/>
  48                         <target ref="id4"/>
  49                         <label kind="guard" x="-398" y="-246">temp &gt;= 102 &amp;&amp; temp &lt;= 105</label>
  50                         <label kind="synchronisation" x="-398" y="-229">outr[0]!</label>
  51                         <nail x="-127" y="-212"/>
  52                         <nail x="-416" y="-212"/>
  53                 </transition>
  54                 <transition>
  55                         <source ref="id3"/>
  56                         <target ref="id1"/>
  57                         <label kind="synchronisation" x="-204" y="-25">inr[1]?</label>
  58                 </transition>
  59                 <transition>
  60                         <source ref="id3"/>
  61                         <target ref="id2"/>
  62                         <label kind="synchronisation" x="-220" y="-118">inr[0]?</label>
  63                 </transition>
  64                 <transition>
  65                         <source ref="id4"/>
  66                         <target ref="id3"/>
  67                         <label kind="guard" x="-357" y="-110">temp &gt;= 110</label>
  68                         <label kind="synchronisation" x="-340" y="-93">cool!</label>
  69                 </transition>
  70         </template>
  71         <template>
  72                 <name>Rod</name>
  73                 <parameter>int[0,1] id</parameter>
  74                 <declaration>clock t;</declaration>
  75                 <location id="id5" x="-221" y="-144">
  76                         <name x="-246" y="-127">cooling</name>
  77                         <urgent/>
  78                 </location>
  79                 <location id="id6" x="-323" y="-144">
  80                         <name x="-357" y="-127">inVessel</name>
  81                 </location>
  82                 <location id="id7" x="-391" y="-144">
  83                         <urgent/>
  84                 </location>
  85                 <location id="id8" x="-459" y="-144">
  86                         <name x="-493" y="-127">available</name>
  87                 </location>
  88                 <init ref="id8"/>
  89                 <transition>
  90                         <source ref="id5"/>
  91                         <target ref="id8"/>
  92                         <label kind="guard" x="-449" y="-272">t &gt;= 20</label>
  93                         <nail x="-221" y="-238"/>
  94                         <nail x="-467" y="-238"/>
  95                 </transition>
  96                 <transition>
  97                         <source ref="id6"/>
  98                         <target ref="id5"/>
  99                         <label kind="synchronisation" x="-305" y="-161">outr[id]?</label>
 100                         <label kind="assignment" x="-305" y="-144">t=0</label>
 101                 </transition>
 102                 <transition>
 103                         <source ref="id7"/>
 104                         <target ref="id6"/>
 105                         <label kind="synchronisation" x="-374" y="-170">inr[id]!</label>
 106                 </transition>
 107                 <transition>
 108                         <source ref="id8"/>
 109                         <target ref="id7"/>
 110                         <label kind="synchronisation" x="-441" y="-161">cool?</label>
 111                 </transition>
 112         </template>
 113         <system>// Place template instantiations here.
 114 // List one or more processes to be composed into a system.
 115 r1 = Rod(0);
 116 r2 = Rod(1);
 117 system Tank, r1, r2;
 118     </system>
 119         <queries>
 120         </queries>
 121 </nta>