+ <template>\r
+ <name>Player</name>\r
+ <declaration>int[0,N] registered;
+bool done = 0;</declaration>\r
+ <location id="id6" x="-493" y="-255">\r
+ </location>\r
+ <location id="id7" x="-680" y="-246">\r
+ </location>\r
+ <location id="id8" x="-799" y="-246">\r
+ </location>\r
+ <init ref="id8"/>\r
+ <transition>\r
+ <source ref="id7"/>\r
+ <target ref="id6"/>\r
+ <label kind="synchronisation" x="-629" y="-272">finish?</label>\r
+ <label kind="assignment" x="-662" y="-250">done := 1</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id8"/>\r
+ <target ref="id7"/>\r
+ <label kind="guard" x="-781" y="-280">registered == N</label>\r
+ <label kind="synchronisation" x="-781" y="-263">start!</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id8"/>\r
+ <target ref="id8"/>\r
+ <label kind="synchronisation" x="-875" y="-365">reg?</label>\r
+ <label kind="assignment" x="-926" y="-382">registered := registered+1</label>\r
+ <nail x="-892" y="-263"/>\r
+ <nail x="-833" y="-331"/>\r
+ <nail x="-765" y="-314"/>\r
+ </transition>\r
+ </template>\r
+ <template>\r
+ <name>RedCar</name>\r
+ <parameter>const id_c id, int[0,5] x</parameter>\r
+ <declaration>void register() {
+ grid[x][3] = true;
+ grid[x+1][3] = true;
+}</declaration>\r
+ <location id="id9" x="493" y="-51">\r
+ </location>\r
+ <location id="id10" x="51" y="-59">\r
+ </location>\r
+ <location id="id11" x="-93" y="-68">\r
+ </location>\r
+ <location id="id12" x="-204" y="-68">\r
+ <urgent/>\r
+ </location>\r
+ <init ref="id12"/>\r
+ <transition>\r
+ <source ref="id10"/>\r
+ <target ref="id9"/>\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="id10"/>\r
+ <target ref="id10"/>\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="id10"/>\r
+ <target ref="id10"/>\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-1][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="id11"/>\r
+ <target ref="id10"/>\r
+ <label kind="synchronisation" x="-75" y="-80">start?</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id12"/>\r
+ <target ref="id11"/>\r
+ <label kind="synchronisation" x="-186" y="-85">reg!</label>\r
+ <label kind="assignment" x="-186" y="-68">register()</label>\r
+ </transition>\r
+ </template>\r