add more descriptions

Train/TwoTrainsMA.mch

@@ -11,13 +11,14 @@ CONSTANTS
 PROPERTIES
   TrackElementNumber : NATURAL1
 & TRACK = 0..TrackElementNumber
-
 & TTD_TrackElements : TTDS --> FIN1(TRACK)
+& !(ttd1,ttd2).(ttd1:TTDS & ttd2 /= ttd1
+      => TTD_TrackElements(ttd1) /\ TTD_TrackElements(ttd2) = {}) /*desc "TTDs are disjoint" */
+& union(ran(TTD_TrackElements)) = TRACK /*desc "TTDs cover the entire track" */
 
+// Configuration Data (normally as refines/extends):
 & TrackElementNumber = 25
 & TTD_TrackElements = {ttd1 |-> 0..4 , ttd2 |-> 5..10 , ttd3 |-> 11..20, ttd4 |-> 21..25}
-& !(ttd1,ttd2).(ttd1:TTDS & ttd2 /= ttd1 => TTD_TrackElements(ttd1) /\ TTD_TrackElements(ttd2) = {}) /*desc "TTDs are disjoint" */
-& union(ran(TTD_TrackElements)) = TRACK /*desc "TTDs cover the entire track" */
 VARIABLES
   occ /*@desc "the occupied TTDs" */,
   train_rear_end /*@desc "the minimal (aka left) position of a train" */,
@@ -28,25 +29,28 @@ INVARIANT
   train_rear_end : TRAINS --> TRACK &
   train_front_end : TRAINS --> TRACK &
   train_ma : TRAINS +-> TRACK /*@desc "partial function associating trains with farthest point it is allowed to move" */ &
-  !tr.(tr:dom(train_ma) => train_front_end(tr) <= train_ma(tr)) /*@desc "trains stay within their MA" */ &
-  !tr.(tr:TRAINS => train_front_end(tr) >= train_rear_end(tr)) /*@desc "train positions on track not empty" */ &
+  /*@label "ASSUME-1" */ !tr.(tr:dom(train_ma)
+                         => train_front_end(tr) <= train_ma(tr)) /*@desc "trains stay within their MA" */ &
+  /*@label "ASSUME-2" */ !tr.(tr:TRAINS
+                         => train_front_end(tr) >= train_rear_end(tr)) /*@desc "train position not empty" */ &
   /*@label "SAF-1" */ !(t1,t2).(t1:TRAINS & t2 /= t1
                          => train_occ(t1) /\ train_occ(t2) = {}) /*@desc "no collision" */ &
   /*@label "SAF-2" */ !(t1,t2).(t1:TRAINS & t2 /= t1
                          => train_reserved(t1) /\ train_reserved(t2) = {}) /*@desc "reserved areas disjoint" */
 
 ASSERTIONS
-  !(ttd,tr).(ttd /: occ & tr:TRAINS
+  /*@label "ASSUME-3" */ !(ttd,tr).(ttd /: occ & tr:TRAINS
               => train_occ(tr) /\ TTD_TrackElements(ttd) = {}) /*@desc "TTDs marked as free are really free" */
 INITIALISATION
    occ := {ttd1,ttd2} || 
-  train_rear_end := {tr1 |-> 0, tr2 |-> 5} || train_front_end := {tr1 |->2, tr2|->6} || train_ma := {}
+   train_rear_end := {tr1 |-> 0, tr2 |-> 5} || train_front_end := {tr1 |->2, tr2|->6} ||
+   train_ma := {}
 OPERATIONS
   
-  
   TrainAcceptsFirstMA(tr,newMA) = PRE tr/:dom(train_ma) & newMA:TRACK & newMA > train_front_end(tr) &
       newMA mod 5 = 0 /*@desc "Restriction to restrict state space for MC" */ &
-      !(t2).(t2 /= tr => train_rear_end(tr)..newMA /\ train_reserved(t2) = {}) /*@desc "MA is safe" */ THEN
+      !(t2).(t2:TRAINS & t2 /= tr
+               => train_rear_end(tr)..newMA /\ train_reserved(t2) = {}) /*@desc "MA is safe" */ THEN
      train_ma(tr) := newMA
   END;
   
@@ -86,4 +90,5 @@ Demo
  2. add disjunct or train_rear_end(tr) > train_front_end(t2) 
  3. animate and see that everything works
  4. show visualisation
+ 5. Fix train bug in TrainMoveForward: new_front = train_front_end(tr) + 1 & //correct
 */
\ No newline at end of file