uppaal/2.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 const int N = 13;
   7 typedef int[0,N-1] id_c;
   8
   9 chan up[N], down[N], left[N], right[N];</declaration>
  10         <template>
  11                 <name x="5" y="5">VertCar</name>
  12                 <parameter>int[2,3] length, const id_c id, int[0,5] x, const int[0,4] y</parameter>
  13                 <declaration>// Place local declarations here.</declaration>
  14                 <location id="id0" x="-212" y="-76">
  15                 </location>
  16                 <init ref="id0"/>
  17                 <transition>
  18                         <source ref="id0"/>
  19                         <target ref="id0"/>
  20                         <label kind="guard" x="-288" y="-68">x&gt;0</label>
  21                         <label kind="synchronisation" x="-288" y="-51">down[id]!</label>
  22                         <label kind="assignment" x="-288" y="-34">x:=x-1</label>
  23                         <nail x="-306" y="8"/>
  24                         <nail x="-136" y="0"/>
  25                 </transition>
  26                 <transition>
  27                         <source ref="id0"/>
  28                         <target ref="id0"/>
  29                         <label kind="guard" x="-306" y="-204">x+length &lt; 6</label>
  30                         <label kind="synchronisation" x="-314" y="-153">up[id]!</label>
  31                         <label kind="assignment" x="-306" y="-178">x:=x+1</label>
  32                         <nail x="-323" y="-102"/>
  33                         <nail x="-195" y="-178"/>
  34                         <nail x="-110" y="-102"/>
  35                 </transition>
  36         </template>
  37         <template>
  38                 <name>HorzCar</name>
  39                 <parameter>int[2,3] length, const id_c id, const int[0,4] x, int[0,5] y</parameter>
  40                 <location id="id1" x="-102" y="-34">
  41                 </location>
  42                 <init ref="id1"/>
  43                 <transition>
  44                         <source ref="id1"/>
  45                         <target ref="id1"/>
  46                         <label kind="guard" x="-135" y="8">y&gt;0</label>
  47                         <label kind="synchronisation" x="-135" y="25">left[id]!</label>
  48                         <label kind="assignment" x="-135" y="42">y:=y-1</label>
  49                         <nail x="-153" y="42"/>
  50                         <nail x="-34" y="42"/>
  51                 </transition>
  52                 <transition>
  53                         <source ref="id1"/>
  54                         <target ref="id1"/>
  55                         <label kind="guard" x="-160" y="-102">y+length &lt; 6</label>
  56                         <label kind="synchronisation" x="-160" y="-85">right[id]!</label>
  57                         <label kind="assignment" x="-160" y="-68">y:=y+1</label>
  58                         <nail x="-178" y="-102"/>
  59                         <nail x="-34" y="-102"/>
  60                 </transition>
  61         </template>
  62         <template>
  63                 <name>Player</name>
  64                 <location id="id2" x="-476" y="-178">
  65                 </location>
  66                 <init ref="id2"/>
  67         </template>
  68         <system>// Place template instantiations here.
  69 H1 = HorzCar(2, 0, 0, 5);
  70 H2 = HorzCar(2, 1, 2, 5);
  71 V3 = VertCar(2, 2, 4, 4);
  72 V4 = VertCar(2, 3, 2, 3);
  73 V5 = VertCar(3, 4, 5, 2);
  74 V6 = VertCar(2, 5, 1, 3);
  75 H7 = HorzCar(2, 6, 3, 4);
  76 H8 = HorzCar(2, 7, 3, 2);
  77 V9 = VertCar(3, 8, 0, 0);
  78 HA = HorzCar(2, 9, 1, 0);
  79 VB = VertCar(2, 10, 3, 0);
  80 HC = HorzCar(2, 11, 4, 1);
  81 HD = HorzCar(2, 12, 4, 0);
  82 // List one or more processes to be composed into a system.
  83 system H1, H2, V3, V4, V5, V6, H7, H8, V9, HA, VB, HC, HD;
  84     </system>
  85         <queries>
  86         </queries>
  87 </nta>