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