<label kind="guard" x="-170" y="153">y>0 && !grid[x][y-1]</label>\r
<label kind="synchronisation" x="-119" y="119">down[id]!</label>\r
<label kind="assignment" x="-221" y="51">grid[x][y-1]:=true,
-grid[x][y+length-1]:=true,
+grid[x][y+length-1]:=false,
y:=y-1</label>\r
<nail x="-153" y="42"/>\r
<nail x="-34" y="42"/>\r
grid[x][3] = true;
grid[x+1][3] = true;
}</declaration>\r
- <location id="id9" x="238" y="34">\r
+ <location id="id9" x="42" y="136">\r
<urgent/>\r
</location>\r
- <location id="id10" x="221" y="-153">\r
+ <location id="id10" x="59" y="-238">\r
<urgent/>\r
</location>\r
<location id="id11" x="493" y="-51">\r
<branchpoint id="id15" x="187" y="-85">\r
</branchpoint>\r
<init ref="id14"/>\r
+ <transition>\r
+ <source ref="id9"/>\r
+ <target ref="id12"/>\r
+ <label kind="guard" x="67" y="38">x <= 0 || grid[x-1][3]</label>\r
+ <nail x="93" y="8"/>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id10"/>\r
+ <target ref="id12"/>\r
+ <label kind="guard" x="93" y="-187">x+2 >= 6 || grid[x+2][3]</label>\r
+ <nail x="102" y="-127"/>\r
+ </transition>\r
<transition>\r
<source ref="id10"/>\r
<target ref="id12"/>\r
+ <label kind="guard" x="-136" y="-161">x+2 < 6 && !grid[x+2][3]</label>\r
+ <label kind="synchronisation" x="-68" y="-144">rightRed!</label>\r
+ <label kind="assignment" x="-85" y="-212">grid[x][3]:=false,
+grid[x+2][3]:=true,
+x:=x+1</label>\r
</transition>\r
<transition>\r
<source ref="id9"/>\r
<target ref="id12"/>\r
+ <label kind="guard" x="-144" y="-25">x > 0 && !grid[x-1][3]</label>\r
+ <label kind="synchronisation" x="-93" y="0">leftRed!</label>\r
+ <label kind="assignment" x="-144" y="25">grid[x+1][3]:=false,
+grid[x-1][3]:=true,
+x:=x-1</label>\r
</transition>\r
<transition>\r
<source ref="id15"/>\r
<target ref="id9"/>\r
- <label kind="probability" x="212" y="-25">1</label>\r
+ <label kind="probability" x="127" y="34">1</label>\r
</transition>\r
<transition>\r
<source ref="id15"/>\r
<target ref="id10"/>\r
- <label kind="probability" x="204" y="-119">3</label>\r
+ <label kind="probability" x="178" y="-127">3</label>\r
</transition>\r
<transition>\r
<source ref="id12"/>\r
<label kind="guard" x="416" y="-93">x == 4</label>\r
<label kind="synchronisation" x="416" y="-76">finish!</label>\r
</transition>\r
- <transition>\r
- <source ref="id12"/>\r
- <target ref="id12"/>\r
- <label kind="guard" x="0" y="161">x > 0 && !grid[x-1][3]</label>\r
- <label kind="synchronisation" x="25" y="119">leftRed!</label>\r
- <label kind="assignment" x="-85" y="85">grid[x+1][3]:=false,
-grid[x-1][3]:=true,
-x:=x-1</label>\r
- <nail x="-25" y="42"/>\r
- <nail x="178" y="51"/>\r
- </transition>\r
- <transition>\r
- <source ref="id12"/>\r
- <target ref="id12"/>\r
- <label kind="guard" x="-17" y="-255">x+2 < 6 && !grid[x+2][3]</label>\r
- <label kind="synchronisation" x="25" y="-221">rightRed!</label>\r
- <label kind="assignment" x="-85" y="-187">grid[x][3]:=false,
-grid[x+2][3]:=true,
-x:=x+1</label>\r
- <nail x="-17" y="-144"/>\r
- <nail x="144" y="-136"/>\r
- </transition>\r
<transition>\r
<source ref="id13"/>\r
<target ref="id12"/>\r