uppaal/traingate.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 clock x, y, z;
   6
   7 chan approach, in, out, ex, lower, raise, down, up;</declaration>
   8         <template>
   9                 <name x="5" y="5">Train</name>
  10                 <declaration>// Place local declarations here.</declaration>
  11                 <location id="id0" x="-119" y="17">
  12                         <name x="-187" y="-17">safe</name>
  13                         <label kind="invariant" x="-187" y="17">x&lt;=5</label>
  14                 </location>
  15                 <location id="id1" x="8" y="17">
  16                         <name x="-2" y="-17">unsafe</name>
  17                         <label kind="invariant" x="-2" y="34">x&lt;=5</label>
  18                 </location>
  19                 <location id="id2" x="0" y="-110">
  20                         <name x="-10" y="-144">aproaching</name>
  21                         <label kind="invariant" x="25" y="-136">x&lt;=5</label>
  22                 </location>
  23                 <location id="id3" x="-127" y="-102">
  24                         <name x="-137" y="-136">initial</name>
  25                 </location>
  26                 <init ref="id3"/>
  27                 <transition>
  28                         <source ref="id0"/>
  29                         <target ref="id3"/>
  30                         <label kind="synchronisation" x="-119" y="-59">ex!</label>
  31                 </transition>
  32                 <transition>
  33                         <source ref="id1"/>
  34                         <target ref="id0"/>
  35                         <label kind="synchronisation" x="-101" y="0">out!</label>
  36                 </transition>
  37                 <transition>
  38                         <source ref="id2"/>
  39                         <target ref="id1"/>
  40                         <label kind="guard" x="4" y="-80">x&gt;2</label>
  41                         <label kind="synchronisation" x="4" y="-63">in!</label>
  42                 </transition>
  43                 <transition>
  44                         <source ref="id3"/>
  45                         <target ref="id2"/>
  46                         <label kind="synchronisation" x="-102" y="-127">approach!</label>
  47                         <label kind="assignment" x="-93" y="-102">x:=0</label>
  48                 </transition>
  49         </template>
  50         <template>
  51                 <name>Stupid</name>
  52                 <location id="id4" x="0" y="0">
  53                 </location>
  54                 <init ref="id4"/>
  55                 <transition>
  56                         <source ref="id4"/>
  57                         <target ref="id4"/>
  58                         <label kind="synchronisation" x="-119" y="-59">in?</label>
  59                         <nail x="-68" y="-85"/>
  60                         <nail x="-85" y="-8"/>
  61                 </transition>
  62                 <transition>
  63                         <source ref="id4"/>
  64                         <target ref="id4"/>
  65                         <label kind="synchronisation" x="93" y="-17">out?</label>
  66                         <nail x="93" y="-59"/>
  67                         <nail x="85" y="42"/>
  68                 </transition>
  69                 <transition>
  70                         <source ref="id4"/>
  71                         <target ref="id4"/>
  72                         <label kind="synchronisation" x="-67" y="4">down?</label>
  73                         <nail x="-85" y="42"/>
  74                         <nail x="25" y="68"/>
  75                 </transition>
  76                 <transition>
  77                         <source ref="id4"/>
  78                         <target ref="id4"/>
  79                         <label kind="synchronisation" x="1" y="-85">up?</label>
  80                         <nail x="-17" y="-68"/>
  81                         <nail x="68" y="-68"/>
  82                 </transition>
  83         </template>
  84         <template>
  85                 <name>Gate</name>
  86                 <location id="id5" x="-204" y="-25">
  87                         <name x="-246" y="0">raising</name>
  88                         <label kind="invariant" x="-274" y="-33">y&lt;=2</label>
  89                 </location>
  90                 <location id="id6" x="-42" y="-25">
  91                         <name x="-34" y="8">lowered</name>
  92                 </location>
  93                 <location id="id7" x="-42" y="-161">
  94                         <name x="-52" y="-195">lowering</name>
  95                         <label kind="invariant" x="-25" y="-161">y&lt;=1</label>
  96                 </location>
  97                 <location id="id8" x="-204" y="-161">
  98                         <name x="-214" y="-195">raised</name>
  99                 </location>
 100                 <init ref="id8"/>
 101                 <transition>
 102                         <source ref="id5"/>
 103                         <target ref="id8"/>
 104                         <label kind="guard" x="-191" y="-127">y&gt;=1</label>
 105                         <label kind="synchronisation" x="-178" y="-110">up!</label>
 106                 </transition>
 107                 <transition>
 108                         <source ref="id6"/>
 109                         <target ref="id5"/>
 110                         <label kind="synchronisation" x="-160" y="-42">raise?</label>
 111                         <label kind="assignment" x="-160" y="-25">y:=0</label>
 112                 </transition>
 113                 <transition>
 114                         <source ref="id7"/>
 115                         <target ref="id6"/>
 116                         <label kind="synchronisation" x="-42" y="-110">down!</label>
 117                 </transition>
 118                 <transition>
 119                         <source ref="id8"/>
 120                         <target ref="id7"/>
 121                         <label kind="synchronisation" x="-160" y="-178">lower?</label>
 122                         <label kind="assignment" x="-160" y="-161">y:=0</label>
 123                 </transition>
 124         </template>
 125         <template>
 126                 <name>Controller</name>
 127                 <location id="id9" x="187" y="-68">
 128                         <name x="177" y="-102">trainComing</name>
 129                         <label kind="invariant" x="229" y="-76">z&lt;=1</label>
 130                 </location>
 131                 <location id="id10" x="-153" y="-76">
 132                         <name x="-229" y="-51">trainLeaving</name>
 133                         <label kind="invariant" x="-221" y="-85">z &lt;= 1</label>
 134                 </location>
 135                 <location id="id11" x="-8" y="-76">
 136                 </location>
 137                 <init ref="id11"/>
 138                 <transition>
 139                         <source ref="id10"/>
 140                         <target ref="id11"/>
 141                         <label kind="synchronisation" x="-143" y="-178">raise!</label>
 142                         <nail x="-161" y="-161"/>
 143                         <nail x="-17" y="-161"/>
 144                 </transition>
 145                 <transition>
 146                         <source ref="id11"/>
 147                         <target ref="id10"/>
 148                         <label kind="synchronisation" x="-135" y="-93">ex?</label>
 149                         <label kind="assignment" x="-135" y="-76">z:=0</label>
 150                 </transition>
 151                 <transition>
 152                         <source ref="id9"/>
 153                         <target ref="id11"/>
 154                         <label kind="guard" x="10" y="-22">z==1</label>
 155                         <label kind="synchronisation" x="10" y="-5">lower!</label>
 156                         <nail x="187" y="17"/>
 157                         <nail x="-8" y="8"/>
 158                 </transition>
 159                 <transition>
 160                         <source ref="id11"/>
 161                         <target ref="id9"/>
 162                         <label kind="synchronisation" x="10" y="-89">approach?</label>
 163                         <label kind="assignment" x="10" y="-72">z:=0</label>
 164                 </transition>
 165         </template>
 166         <system>// Place template instantiations here.
 167 T = Train();
 168 G = Gate();
 169 C = Controller();
 170 Gezeik = Stupid();
 171 // List one or more processes to be composed into a system.
 172 system T, G, C, Gezeik;
 173     </system>
 174         <queries>
 175         </queries>
 176 </nta>