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 broadcast chan up[N], down[N], left[N], right[N], start, leftRed, rightRed;
  13
  14 chan reg;
  15
  16 bool grid[6][6];</declaration>
  17         <template>
  18                 <name x="5" y="5">HorzCar</name>
  19                 <parameter>int[2,3] length, const id_c id, int[0,4] x, const int[0,5] y</parameter>
  20                 <declaration>// Place local declarations here.
  21
  22 void register() {
  23     int i;
  24     for (i=0; i&lt;length; i++) {
  25         grid[x+i][y] = true;
  26     }
  27 }</declaration>
  28                 <location id="id0" x="-425" y="-51">
  29                 </location>
  30                 <location id="id1" x="-535" y="-136">
  31                         <urgent/>
  32                 </location>
  33                 <location id="id2" x="-212" y="-76">
  34                 </location>
  35                 <init ref="id1"/>
  36                 <transition>
  37                         <source ref="id0"/>
  38                         <target ref="id2"/>
  39                         <label kind="synchronisation" x="-407" y="-80">start?</label>
  40                 </transition>
  41                 <transition>
  42                         <source ref="id1"/>
  43                         <target ref="id0"/>
  44                         <label kind="synchronisation" x="-517" y="-110">reg!</label>
  45                         <label kind="assignment" x="-517" y="-93">register()</label>
  46                 </transition>
  47                 <transition>
  48                         <source ref="id2"/>
  49                         <target ref="id2"/>
  50                         <label kind="guard" x="-288" y="-68">x&gt;0 &amp;&amp; !grid[x-1][y]</label>
  51                         <label kind="synchronisation" x="-288" y="-51">down[id]!</label>
  52                         <label kind="assignment" x="-288" y="-34">x:=x-1</label>
  53                         <nail x="-306" y="8"/>
  54                         <nail x="-136" y="0"/>
  55                 </transition>
  56                 <transition>
  57                         <source ref="id2"/>
  58                         <target ref="id2"/>
  59                         <label kind="guard" x="-306" y="-204">x+length &lt; 6 &amp;&amp; !grid[x+length][y]</label>
  60                         <label kind="synchronisation" x="-314" y="-153">up[id]!</label>
  61                         <label kind="assignment" x="-306" y="-178">x:=x+1</label>
  62                         <nail x="-323" y="-102"/>
  63                         <nail x="-195" y="-178"/>
  64                         <nail x="-110" y="-102"/>
  65                 </transition>
  66         </template>
  67         <template>
  68                 <name>VertCar</name>
  69                 <parameter>int[2,3] length, const id_c id, const int[0,5] x, int[0,4] y</parameter>
  70                 <declaration>void register() {
  71     int i;
  72     for(i=0; i&lt;length; i++){
  73         grid[x][y+i] = true;
  74     }
  75 }
  76 </declaration>
  77                 <location id="id3" x="-314" y="-34">
  78                 </location>
  79                 <location id="id4" x="-416" y="-76">
  80                         <urgent/>
  81                 </location>
  82                 <location id="id5" x="-102" y="-34">
  83                 </location>
  84                 <init ref="id4"/>
  85                 <transition>
  86                         <source ref="id3"/>
  87                         <target ref="id5"/>
  88                         <label kind="synchronisation" x="-228" y="-72">start?</label>
  89                 </transition>
  90                 <transition>
  91                         <source ref="id4"/>
  92                         <target ref="id3"/>
  93                         <label kind="synchronisation" x="-374" y="-110">reg!</label>
  94                         <label kind="assignment" x="-374" y="-76">register()</label>
  95                         <nail x="-255" y="-85"/>
  96                 </transition>
  97                 <transition>
  98                         <source ref="id5"/>
  99                         <target ref="id5"/>
 100                         <label kind="guard" x="-135" y="8">y&gt;0 &amp;&amp; !grid[x][y-1]</label>
 101                         <label kind="synchronisation" x="-135" y="25">left[id]!</label>
 102                         <label kind="assignment" x="-135" y="42">y:=y-1</label>
 103                         <nail x="-153" y="42"/>
 104                         <nail x="-34" y="42"/>
 105                 </transition>
 106                 <transition>
 107                         <source ref="id5"/>
 108                         <target ref="id5"/>
 109                         <label kind="guard" x="-160" y="-102">y+length &lt; 6 &amp;&amp; !grid[x][y+length]</label>
 110                         <label kind="synchronisation" x="-160" y="-85">right[id]!</label>
 111                         <label kind="assignment" x="-160" y="-68">y:=y+1</label>
 112                         <nail x="-178" y="-102"/>
 113                         <nail x="-34" y="-102"/>
 114                 </transition>
 115         </template>
 116         <template>
 117                 <name>Player</name>
 118                 <declaration>int[0,N] registered;</declaration>
 119                 <location id="id6" x="-680" y="-246">
 120                 </location>
 121                 <location id="id7" x="-799" y="-246">
 122                 </location>
 123                 <init ref="id7"/>
 124                 <transition>
 125                         <source ref="id7"/>
 126                         <target ref="id6"/>
 127                         <label kind="guard" x="-781" y="-280">registered == N</label>
 128                         <label kind="synchronisation" x="-781" y="-263">start!</label>
 129                 </transition>
 130                 <transition>
 131                         <source ref="id7"/>
 132                         <target ref="id7"/>
 133                         <label kind="synchronisation" x="-875" y="-365">reg?</label>
 134                         <label kind="assignment" x="-926" y="-382">registered := registered+1</label>
 135                         <nail x="-892" y="-263"/>
 136                         <nail x="-833" y="-331"/>
 137                         <nail x="-765" y="-314"/>
 138                 </transition>
 139         </template>
 140         <template>
 141                 <name>RedCar</name>
 142                 <parameter>const id_c id, int[0,5] x</parameter>
 143                 <declaration>void register() {
 144     grid[x][3] = true;
 145     grid[x+1][3] = true;
 146 }</declaration>
 147                 <location id="id8" x="51" y="-59">
 148                 </location>
 149                 <location id="id9" x="-93" y="-68">
 150                 </location>
 151                 <location id="id10" x="-204" y="-68">
 152                         <urgent/>
 153                 </location>
 154                 <init ref="id10"/>
 155                 <transition>
 156                         <source ref="id8"/>
 157                         <target ref="id8"/>
 158                         <label kind="guard" x="-7" y="-42">x &gt; 0 &amp;&amp; grid[x-1][3]</label>
 159                         <label kind="synchronisation" x="-7" y="-25">leftRed!</label>
 160                         <label kind="assignment" x="-7" y="-8">x := x-1, grid[x+1][3] := false, grid[x-1][3] := true</label>
 161                         <nail x="-25" y="42"/>
 162                         <nail x="178" y="51"/>
 163                 </transition>
 164                 <transition>
 165                         <source ref="id8"/>
 166                         <target ref="id8"/>
 167                         <label kind="guard" x="1" y="-135">x+2 &lt; 6 &amp;&amp; grid[x+2][3]</label>
 168                         <label kind="synchronisation" x="1" y="-118">rightRed!</label>
 169                         <label kind="assignment" x="1" y="-101">x := x+1, grid[x][3] := false, grid[x+2][3] := true</label>
 170                         <nail x="-17" y="-144"/>
 171                         <nail x="144" y="-136"/>
 172                 </transition>
 173                 <transition>
 174                         <source ref="id9"/>
 175                         <target ref="id8"/>
 176                         <label kind="synchronisation" x="-75" y="-80">start?</label>
 177                 </transition>
 178                 <transition>
 179                         <source ref="id10"/>
 180                         <target ref="id9"/>
 181                         <label kind="synchronisation" x="-186" y="-85">reg!</label>
 182                         <label kind="assignment" x="-186" y="-68">register()</label>
 183                 </transition>
 184         </template>
 185         <system>// Place template instantiations here.
 186
 187 // Intermediate puzzle
 188 H1 = HorzCar(2, 0, 0, 5);
 189 H2 = HorzCar(2, 1, 2, 5);
 190 V3 = VertCar(2, 2, 4, 4);
 191 V4 = VertCar(2, 3, 2, 3);
 192 V5 = VertCar(3, 4, 5, 2);
 193 V6 = VertCar(2, 5, 1, 3);
 194 H7 = HorzCar(2, 6, 3, 4);
 195 H8 = HorzCar(2, 7, 3, 2);
 196 V9 = VertCar(3, 8, 0, 0);
 197 HA = HorzCar(2, 9, 1, 0);
 198 VB = VertCar(2, 10, 3, 0);
 199 HC = HorzCar(2, 11, 4, 1);
 200 HD = HorzCar(2, 12, 4, 0);
 201 system H1, H2, V3, V4, V5, V6, H7, H8, V9, HA, VB, HC, HD, Player;
 202
 203 // Advanced puzzle
 204 /*
 205 H1 = HorzCar(2, 0, 0, 5);
 206 V2 = VertCar(2, 1, 2, 4);
 207 V3 = VertCar(3, 2, 3, 3);
 208 V4 = VertCar(3, 3, 0, 2);
 209 H5 = HorzCar(2, 4, 1, 3);
 210 H6 = HorzCar(3, 5, 1, 2);
 211 H7 = HorzCar(3, 6, 3, 0);
 212 system H1, V2, V3, V4, H5, H6, H7
 213 */
 214
 215 // List one or more processes to be composed into a system.
 216
 217     </system>
 218         <queries>
 219         </queries>
 220 </nta>