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 //hard from website 1
  10 const int N=13;
  11 //hard from website 2
  12 //const int N=9;
  13
  14 typedef int[0, N-1] id_c;
  15
  16 broadcast chan up[N], down[N], left[N], right[N], start, leftRed, rightRed;
  17
  18 chan reg, finish;
  19
  20 bool grid[6][6];</declaration>
  21         <template>
  22                 <name x="5" y="5">HorzCar</name>
  23                 <parameter>int[2,3] length, const id_c id, int[0,4] x, const int[0,5] y</parameter>
  24                 <declaration>// Place local declarations here.
  25
  26 void register() {
  27     int i;
  28     for (i=0; i&lt;length; i++) {
  29         grid[x+i][y] = true;
  30     }
  31 }</declaration>
  32                 <location id="id0" x="-425" y="-51">
  33                 </location>
  34                 <location id="id1" x="-535" y="-136">
  35                         <urgent/>
  36                 </location>
  37                 <location id="id2" x="-212" y="-76">
  38                 </location>
  39                 <init ref="id1"/>
  40                 <transition>
  41                         <source ref="id0"/>
  42                         <target ref="id2"/>
  43                         <label kind="synchronisation" x="-407" y="-80">start?</label>
  44                 </transition>
  45                 <transition>
  46                         <source ref="id1"/>
  47                         <target ref="id0"/>
  48                         <label kind="synchronisation" x="-517" y="-110">reg!</label>
  49                         <label kind="assignment" x="-517" y="-93">register()</label>
  50                 </transition>
  51                 <transition>
  52                         <source ref="id2"/>
  53                         <target ref="id2"/>
  54                         <label kind="guard" x="-280" y="8">x&gt;0 &amp;&amp; !grid[x-1][y]</label>
  55                         <label kind="synchronisation" x="-153" y="-42">left[id]!</label>
  56                         <label kind="assignment" x="-340" y="34">grid[x+length-1][y]:=false,
  57 grid[x-1][y]:=true,
  58 x:=x-1</label>
  59                         <nail x="-306" y="8"/>
  60                         <nail x="-136" y="0"/>
  61                 </transition>
  62                 <transition>
  63                         <source ref="id2"/>
  64                         <target ref="id2"/>
  65                         <label kind="guard" x="-306" y="-263">x+length &lt; 6 &amp;&amp; !grid[x+length][y]</label>
  66                         <label kind="synchronisation" x="-170" y="-170">right[id]!</label>
  67                         <label kind="assignment" x="-331" y="-229">grid[x][y]:=false,
  68 grid[x+length][y]:=true,
  69 x:=x+1</label>
  70                         <nail x="-323" y="-102"/>
  71                         <nail x="-195" y="-178"/>
  72                         <nail x="-110" y="-102"/>
  73                 </transition>
  74         </template>
  75         <template>
  76                 <name>VertCar</name>
  77                 <parameter>int[2,3] length, const id_c id, const int[0,5] x, int[0,4] y</parameter>
  78                 <declaration>void register() {
  79     int i;
  80     for(i=0; i&lt;length; i++){
  81         grid[x][y+i] = true;
  82     }
  83 }
  84 </declaration>
  85                 <location id="id3" x="-314" y="-34">
  86                 </location>
  87                 <location id="id4" x="-416" y="-76">
  88                         <urgent/>
  89                 </location>
  90                 <location id="id5" x="-102" y="-34">
  91                 </location>
  92                 <init ref="id4"/>
  93                 <transition>
  94                         <source ref="id3"/>
  95                         <target ref="id5"/>
  96                         <label kind="synchronisation" x="-246" y="-59">start?</label>
  97                 </transition>
  98                 <transition>
  99                         <source ref="id4"/>
 100                         <target ref="id3"/>
 101                         <label kind="synchronisation" x="-374" y="-110">reg!</label>
 102                         <label kind="assignment" x="-374" y="-76">register()</label>
 103                         <nail x="-255" y="-85"/>
 104                 </transition>
 105                 <transition>
 106                         <source ref="id5"/>
 107                         <target ref="id5"/>
 108                         <label kind="guard" x="-153" y="153">y&gt;0 &amp;&amp; !grid[x][y-1]</label>
 109                         <label kind="synchronisation" x="-153" y="119">down[id]!</label>
 110                         <label kind="assignment" x="-153" y="51">grid[x][y-1]:=true,
 111 grid[x][y+length-1]:=false,
 112 y:=y-1</label>
 113                         <nail x="-153" y="42"/>
 114                         <nail x="-34" y="42"/>
 115                 </transition>
 116                 <transition>
 117                         <source ref="id5"/>
 118                         <target ref="id5"/>
 119                         <label kind="guard" x="-161" y="-204">y+length &lt; 6 &amp;&amp; !grid[x][y+length]</label>
 120                         <label kind="synchronisation" x="-161" y="-178">up[id]!</label>
 121                         <label kind="assignment" x="-161" y="-153">grid[x][y+length]:=true,
 122 grid[x][y]:=false,
 123 y:=y+1</label>
 124                         <nail x="-178" y="-102"/>
 125                         <nail x="-34" y="-102"/>
 126                 </transition>
 127         </template>
 128         <template>
 129                 <name>Player</name>
 130                 <declaration>int[0,N] registered;
 131 bool done = 0;</declaration>
 132                 <location id="id6" x="-476" y="-459">
 133                 </location>
 134                 <location id="id7" x="-663" y="-450">
 135                 </location>
 136                 <location id="id8" x="-782" y="-450">
 137                 </location>
 138                 <init ref="id8"/>
 139                 <transition>
 140                         <source ref="id7"/>
 141                         <target ref="id6"/>
 142                         <label kind="synchronisation" x="-612" y="-476">finish?</label>
 143                         <label kind="assignment" x="-645" y="-454">done := 1</label>
 144                 </transition>
 145                 <transition>
 146                         <source ref="id8"/>
 147                         <target ref="id7"/>
 148                         <label kind="guard" x="-764" y="-484">registered == N</label>
 149                         <label kind="synchronisation" x="-764" y="-467">start!</label>
 150                 </transition>
 151                 <transition>
 152                         <source ref="id8"/>
 153                         <target ref="id8"/>
 154                         <label kind="synchronisation" x="-833" y="-561">reg?</label>
 155                         <label kind="assignment" x="-909" y="-578">registered := registered+1</label>
 156                         <nail x="-875" y="-467"/>
 157                         <nail x="-816" y="-535"/>
 158                         <nail x="-748" y="-518"/>
 159                 </transition>
 160         </template>
 161         <template>
 162                 <name>RedCar</name>
 163                 <parameter>const id_c id, int[0,5] x</parameter>
 164                 <declaration>void register() {
 165     grid[x][3] = true;
 166     grid[x+1][3] = true;
 167 }</declaration>
 168                 <location id="id9" x="42" y="136">
 169                         <urgent/>
 170                 </location>
 171                 <location id="id10" x="59" y="-238">
 172                         <urgent/>
 173                 </location>
 174                 <location id="id11" x="493" y="-51">
 175                 </location>
 176                 <location id="id12" x="51" y="-59">
 177                 </location>
 178                 <location id="id13" x="-93" y="-68">
 179                 </location>
 180                 <location id="id14" x="-204" y="-68">
 181                         <urgent/>
 182                 </location>
 183                 <branchpoint id="id15" x="187" y="-85">
 184                 </branchpoint>
 185                 <init ref="id14"/>
 186                 <transition>
 187                         <source ref="id9"/>
 188                         <target ref="id12"/>
 189                         <label kind="guard" x="67" y="38">x &lt;= 0 || grid[x-1][3]</label>
 190                         <nail x="93" y="8"/>
 191                 </transition>
 192                 <transition>
 193                         <source ref="id10"/>
 194                         <target ref="id12"/>
 195                         <label kind="guard" x="93" y="-187">x+2 &gt;= 6 || grid[x+2][3]</label>
 196                         <nail x="102" y="-127"/>
 197                 </transition>
 198                 <transition>
 199                         <source ref="id10"/>
 200                         <target ref="id12"/>
 201                         <label kind="guard" x="-136" y="-161">x+2 &lt; 6 &amp;&amp; !grid[x+2][3]</label>
 202                         <label kind="synchronisation" x="-68" y="-144">rightRed!</label>
 203                         <label kind="assignment" x="-85" y="-212">grid[x][3]:=false,
 204 grid[x+2][3]:=true,
 205 x:=x+1</label>
 206                 </transition>
 207                 <transition>
 208                         <source ref="id9"/>
 209                         <target ref="id12"/>
 210                         <label kind="guard" x="-144" y="-25">x &gt; 0 &amp;&amp; !grid[x-1][3]</label>
 211                         <label kind="synchronisation" x="-93" y="0">leftRed!</label>
 212                         <label kind="assignment" x="-144" y="25">grid[x+1][3]:=false,
 213 grid[x-1][3]:=true,
 214 x:=x-1</label>
 215                 </transition>
 216                 <transition>
 217                         <source ref="id15"/>
 218                         <target ref="id9"/>
 219                         <label kind="probability" x="161" y="-34">1</label>
 220                 </transition>
 221                 <transition>
 222                         <source ref="id15"/>
 223                         <target ref="id10"/>
 224                         <label kind="probability" x="178" y="-127">3</label>
 225                 </transition>
 226                 <transition>
 227                         <source ref="id12"/>
 228                         <target ref="id15"/>
 229                 </transition>
 230                 <transition>
 231                         <source ref="id12"/>
 232                         <target ref="id11"/>
 233                         <label kind="guard" x="416" y="-93">x == 4</label>
 234                         <label kind="synchronisation" x="416" y="-76">finish!</label>
 235                 </transition>
 236                 <transition>
 237                         <source ref="id13"/>
 238                         <target ref="id12"/>
 239                         <label kind="synchronisation" x="-75" y="-80">start?</label>
 240                 </transition>
 241                 <transition>
 242                         <source ref="id14"/>
 243                         <target ref="id13"/>
 244                         <label kind="synchronisation" x="-186" y="-85">reg!</label>
 245                         <label kind="assignment" x="-186" y="-68">register()</label>
 246                 </transition>
 247         </template>
 248         <system>// Place template instantiations here.
 249
 250
 251
 252 //easy test puzzle
 253 /*
 254 RED = RedCar(0,2);
 255 V1 = VertCar(2, 1, 4, 3);
 256 V2 = VertCar(3, 2, 5, 2);
 257 system RED, V1, V2, Player;
 258 */
 259
 260 // Intermediate puzzle
 261
 262 H1 = HorzCar(2, 0, 0, 5);
 263 H2 = HorzCar(2, 1, 2, 5);
 264 V3 = VertCar(2, 2, 4, 4);
 265 V4 = VertCar(2, 3, 2, 3);
 266 V5 = VertCar(3, 4, 5, 2);
 267 V6 = VertCar(2, 5, 1, 3);
 268 H7 = HorzCar(2, 6, 3, 4);
 269 RED = RedCar(7, 2); //RED
 270 V9 = VertCar(3, 8, 0, 0);
 271 HA = HorzCar(2, 9, 1, 0);
 272 VB = VertCar(2, 10, 3, 0);
 273 HC = HorzCar(2, 11, 4, 1);
 274 HD = HorzCar(2, 12, 4, 0);
 275 system H1, H2, V3, V4, V5, V6, H7, RED, V9, HA, VB, HC, HD, Player;
 276
 277
 278 // Advanced puzzle
 279 /*
 280 H1 = HorzCar(2, 0, 0, 5);
 281 V2 = VertCar(2, 1, 2, 4);
 282 V3 = VertCar(3, 2, 3, 3);
 283 V4 = VertCar(3, 3, 0, 2);
 284 RED = RedCar(4, 1);
 285 H6 = HorzCar(3, 5, 1, 2);
 286 H7 = HorzCar(3, 6, 3, 0);
 287 system H1, V2, V3, V4, RED, H6, H7, Player;
 288 */
 289
 290 //Hard from website 1
 291 //Can not be solved
 292 /*
 293 V1 = VertCar(2, 0, 0, 3);
 294 V2 = VertCar(2, 1, 1, 0);
 295 V3 = VertCar(2, 2, 2, 1);
 296 V4 = VertCar(2, 3, 3, 4);
 297 V5 = VertCar(3, 4, 4, 3);
 298 V6 = VertCar(3, 5, 5, 3);
 299 H7 = HorzCar(2, 6, 0, 2);
 300 H8 = HorzCar(3, 7, 0, 5);
 301 H85= HorzCar(3,12, 1, 4);
 302 H9 = HorzCar(2, 8, 2, 0);
 303 RED = RedCar(9, 2);
 304 HB = HorzCar(2,10, 4, 0);
 305 HC = HorzCar(2,11, 4, 1);
 306 system V1, V2, V3, V4, V5, V6, H7, H8, H85, H9, RED, HB, HC, Player;
 307 */
 308
 309 //Hard from website 2
 310 /*
 311 V1 = VertCar(2, 0, 0, 0);
 312 V2 = VertCar(3, 1, 2, 3);
 313 V3 = VertCar(3, 2, 3, 0);
 314 V4 = VertCar(3, 3, 5, 3);
 315 H5 = HorzCar(2, 4, 1, 1);
 316 RED = RedCar(5, 3);
 317 H7 = HorzCar(2, 6, 3, 5);
 318 H8 = HorzCar(2, 7, 4, 0);
 319 H9 = HorzCar(2, 8, 4, 2);
 320 system V1, V2, V3, V4, H5, RED, H7, H8, H9, Player;
 321 */</system>
 322         <queries>
 323                 <query>
 324                         <formula>E&lt;&gt; Player.done == 1
 325                         </formula>
 326                         <comment>
 327                         </comment>
 328                 </query>
 329         </queries>
 330 </nta>