Implement mutual exclusion of train identified 1

ds/trains0.xml

@@ -128,42 +128,82 @@ id_tAB tail()
 {
    return list[len - 1];
 }</declaration>
-		<location id="id8" x="246" y="127">
-			<name x="229" y="85">Free</name>
+		<location id="id8" x="-42" y="59">
+			<name x="-93" y="51">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>
+		</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>
 		</location>
 		<init ref="id8"/>
+		<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"/>
+		</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>
+			<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"/>
+		</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>
+			<nail x="212" y="17"/>
+		</transition>
 	</template>
 	<system>system TrainAB, TrainBA, CTRL;
 </system>
 	<queries>
 		<query>
-			<formula>E&lt;&gt; TrainBA(1).BA
+			<formula>E&lt;&gt; TrainBA(1).BA</formula>
+			<comment></comment>
+		</query>
+		<query>
+			<formula>E&lt;&gt; TrainBA(2).BA
 			</formula>
-			<comment>
+			<comment>
 			</comment>
 		</query>
 		<query>
-			<formula>A[] forall (i : id_tBA) forall (j : id_tAB) TrainBA(i).BA &amp;&amp; TrainAB(j).AB imply i == j
+			<formula>A[] forall (i : id_tBA) forall (j : id_tAB) TrainBA(i).BA &amp;&amp; TrainAB(j).AB imply i == j
 			</formula>
-			<comment>
+			<comment>
 			</comment>
 		</query>
 		<query>
-			<formula>TrainBA(1).B --&gt; TrainBA(1).BA
+			<formula>TrainBA(1).B --&gt; TrainBA(1).BA
 			</formula>
-			<comment>
+			<comment>
 			</comment>
 		</query>
 		<query>
-			<formula>A&lt;&gt; TrainBA(1).BA
+			<formula>A&lt;&gt; TrainBA(1).BA
 			</formula>
-			<comment>
+			<comment>
 			</comment>
 		</query>
 		<query>
-			<formula>E&lt;&gt; TrainBA(1).BA &amp; TrainBA(2).BA
+			<formula>E&lt;&gt; TrainBA(1).BA &amp; TrainBA(2).BA
 			</formula>
-			<comment>
+			<comment>
 			</comment>
 		</query>
 	</queries>