Implement mutual exclusion with several trains

ds/trains0.xml

@@ -22,23 +22,23 @@ chan        accesAB[NAB], accesBA[NBA], libAB[NAB], libBA[NBA];
 		<parameter>const id_tBA id</parameter>
 		<declaration>clock x;</declaration>
 		<location id="id0" x="-51" y="0">
-			<name x="-59" y="17">A</name>
+			<name x="-51" y="17">A</name>
 		</location>
-		<location id="id1" x="102" y="0">
-			<name x="102" y="17">BA</name>
-			<label kind="invariant" x="119" y="0">x&lt;=10</label>
+		<location id="id1" x="34" y="0">
+			<name x="25" y="17">BA</name>
+			<label kind="invariant" x="51" y="-8">x&lt;=10</label>
 		</location>
-		<location id="id2" x="102" y="-127">
-			<name x="92" y="-161">B</name>
+		<location id="id2" x="34" y="-127">
+			<name x="34" y="-161">B</name>
 		</location>
 		<location id="id3" x="-51" y="-127">
-			<name x="-61" y="-161">Safe</name>
+			<name x="-59" y="-161">Safe</name>
 		</location>
 		<init ref="id3"/>
 		<transition>
 			<source ref="id0"/>
 			<target ref="id3"/>
-			<label kind="synchronisation" x="-51" y="-80">libBA[id] !</label>
+			<label kind="synchronisation" x="-51" y="-68">libBA[id] !</label>
 		</transition>
 		<transition>
 			<source ref="id1"/>
@@ -47,8 +47,8 @@ chan        accesAB[NAB], accesBA[NBA], libAB[NAB], libBA[NBA];
 		<transition>
 			<source ref="id2"/>
 			<target ref="id1"/>
-			<label kind="synchronisation" x="102" y="-80">accesBA[id] ?</label>
-			<label kind="assignment" x="102" y="-63">x:=0</label>
+			<label kind="synchronisation" x="42" y="-85">accesBA[id] ?</label>
+			<label kind="assignment" x="42" y="-68">x:=0</label>
 		</transition>
 		<transition>
 			<source ref="id3"/>
@@ -59,24 +59,24 @@ chan        accesAB[NAB], accesBA[NBA], libAB[NAB], libBA[NBA];
 		<name x="40" y="16">TrainAB</name>
 		<parameter>const id_tAB id</parameter>
 		<declaration>clock x;</declaration>
-		<location id="id4" x="96" y="96">
-			<name x="48" y="80">Safe</name>
+		<location id="id4" x="127" y="93">
+			<name x="116" y="65">Safe</name>
 		</location>
-		<location id="id5" x="256" y="96">
-			<name x="272" y="80">A</name>
+		<location id="id5" x="212" y="93">
+			<name x="211" y="65">A</name>
 		</location>
-		<location id="id6" x="96" y="232">
-			<name x="32" y="216">B</name>
+		<location id="id6" x="127" y="229">
+			<name x="124" y="243">B</name>
 		</location>
-		<location id="id7" x="256" y="232">
-			<name x="272" y="216">AB</name>
-			<label kind="invariant" x="246" y="249">x&lt;=10</label>
+		<location id="id7" x="212" y="229">
+			<name x="202" y="243">AB</name>
+			<label kind="invariant" x="228" y="218">x&lt;=10</label>
 		</location>
 		<init ref="id4"/>
 		<transition>
 			<source ref="id6"/>
 			<target ref="id4"/>
-			<label kind="synchronisation" x="96" y="147">libAB[id] !</label>
+			<label kind="synchronisation" x="127" y="144">libAB[id] !</label>
 		</transition>
 		<transition>
 			<source ref="id7"/>
@@ -85,8 +85,8 @@ chan        accesAB[NAB], accesBA[NBA], libAB[NAB], libBA[NBA];
 		<transition>
 			<source ref="id5"/>
 			<target ref="id7"/>
-			<label kind="synchronisation" x="256" y="147">accesAB[id] ?</label>
-			<label kind="assignment" x="256" y="164">x:=0</label>
+			<label kind="synchronisation" x="212" y="144">accesAB[id] ?</label>
+			<label kind="assignment" x="212" y="161">x:=0</label>
 		</transition>
 		<transition>
 			<source ref="id4"/>
@@ -128,44 +128,86 @@ id_tAB tail()
 {
    return list[len - 1];
 }</declaration>
-		<location id="id8" x="-42" y="59">
-			<name x="-93" y="51">Free</name>
+		<location id="id8" x="-102" y="51">
+			<name x="-153" y="43">Free</name>
 		</location>
 		<location id="id9" x="212" y="-68">
-			<name x="202" y="-102">AB</name>
-			<label kind="comments" x="204" y="-127">At least one train is going from A to B</label>
+			<name x="178" y="-59">AB</name>
+			<label kind="comments" x="34" y="-59">At least one on AB</label>
 		</location>
 		<location id="id10" x="212" y="187">
-			<name x="204" y="204">BA</name>
-			<label kind="comments" x="204" y="229">At least one from B to A</label>
+			<name x="178" y="161">BA</name>
+			<label kind="comments" x="34" y="161">At least one on BA</label>
 		</location>
 		<init ref="id8"/>
 		<transition>
 			<source ref="id10"/>
+			<target ref="id10"/>
+			<label kind="select" x="221" y="263">e:id_tBA</label>
+			<label kind="synchronisation" x="221" y="280">libBA[e] ?</label>
+			<label kind="assignment" x="221" y="297">ba --</label>
+			<nail x="280" y="255"/>
+			<nail x="212" y="255"/>
+		</transition>
+		<transition>
+			<source ref="id10"/>
+			<target ref="id10"/>
+			<label kind="select" x="357" y="187">e:id_tBA</label>
+			<label kind="synchronisation" x="357" y="204">accesBA[e] !</label>
+			<label kind="assignment" x="357" y="221">ba ++</label>
+			<nail x="348" y="187"/>
+			<nail x="348" y="255"/>
+		</transition>
+		<transition>
+			<source ref="id9"/>
+			<target ref="id9"/>
+			<label kind="select" x="408" y="-153">e:id_tAB</label>
+			<label kind="synchronisation" x="408" y="-136">accesAB[e] !</label>
+			<label kind="assignment" x="408" y="-119">ab++</label>
+			<label kind="comments" x="408" y="-178">One more train on AB</label>
+			<nail x="399" y="-68"/>
+			<nail x="399" y="-178"/>
+		</transition>
+		<transition>
+			<source ref="id9"/>
+			<target ref="id9"/>
+			<label kind="select" x="136" y="-161">e:id_tAB</label>
+			<label kind="synchronisation" x="136" y="-144">libAB[e] ?</label>
+			<label kind="assignment" x="136" y="-127">ab--</label>
+			<label kind="comments" x="59" y="-187">One train leaves AB</label>
+			<nail x="289" y="-187"/>
+			<nail x="212" y="-187"/>
+		</transition>
+		<transition>
+			<source ref="id10"/>
 			<target ref="id8"/>
-			<label kind="synchronisation" x="-119" y="144">libBA[1] ?</label>
-			<label kind="comments" x="-255" y="170">Last train leaving BA section</label>
-			<nail x="-42" y="187"/>
+			<label kind="guard" x="-170" y="136">ba == 0</label>
+			<label kind="comments" x="-221" y="161">No train on BA</label>
+			<nail x="-102" y="187"/>
 		</transition>
 		<transition>
 			<source ref="id8"/>
 			<target ref="id10"/>
-			<label kind="synchronisation" x="238" y="102">accesBA[1] !</label>
-			<label kind="comments" x="238" y="127">First train from B to A</label>
+			<label kind="select" x="221" y="102">e:id_tBA</label>
+			<label kind="synchronisation" x="221" y="119">accesBA[e] !</label>
+			<label kind="assignment" x="221" y="136">ba++</label>
+			<label kind="comments" x="221" y="76">First train on BA</label>
 			<nail x="212" y="85"/>
 		</transition>
 		<transition>
 			<source ref="id9"/>
 			<target ref="id8"/>
-			<label kind="synchronisation" x="-119" y="-85">libAB[1] ?</label>
-			<label kind="comments" x="-255" y="-59">Last train leaving AB section</label>
-			<nail x="-42" y="-68"/>
+			<label kind="guard" x="-169" y="-85">ab == 0</label>
+			<label kind="comments" x="-221" y="-59">No train on AB</label>
+			<nail x="-101" y="-68"/>
 		</transition>
 		<transition>
 			<source ref="id8"/>
 			<target ref="id9"/>
-			<label kind="synchronisation" x="229" y="-34">accesAB[1] !</label>
-			<label kind="comments" x="229" y="-8">First train from A heading to B</label>
+			<label kind="select" x="221" y="0">e:id_tAB</label>
+			<label kind="synchronisation" x="221" y="17">accesAB[e] !</label>
+			<label kind="assignment" x="221" y="34">ab++</label>
+			<label kind="comments" x="221" y="-25">First train on AB</label>
 			<nail x="212" y="17"/>
 		</transition>
 	</template>