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