add variation of two trains

Train/TwoTrains.mch

@@ -37,7 +37,7 @@ OPERATIONS
   END
 DEFINITIONS
  "LibrarySVG.def"; // enable to use the external functions in the VisB json file
-  train_occ(tr) == train_rear_end(tr)..(train_rear_end(tr)+train_length(tr));
+  train_occ(tr) == train_rear_end(tr)..(train_rear_end(tr)+train_length(tr)-1);
   train_occ_all == UNION(tr).(tr:TRAINS|train_occ(tr));
   VISB_JSON_FILE == "TwoTrains.json"
 ASSERTIONS

Train/TwoTrainsB.mch

+MACHINE TwoTrainsB
+// A small example to show how one can use LibrarySVG to flexibliy visualise
+// train track zones,...
+SETS
+  TTDS = {ttd1,ttd2,ttd3};
+  TRAINS = {tr1,tr2}
+CONSTANTS
+  TrackElementNumber, TRACK, TTD_TrackElements
+PROPERTIES
+  TrackElementNumber : NATURAL1
+& TRACK = 0..TrackElementNumber
+
+& TTD_TrackElements : TTDS --> FIN1(TRACK)
+
+& TrackElementNumber = 30
+& TTD_TrackElements = {ttd1 |-> 0..10 , ttd2 |-> 11..25 , ttd3 |-> 26..30}
+VARIABLES
+  occ /*@desc "the occupied TTDs" */,
+  train_rear_end /*@desc "the minimal (aka left) position of a train" */,
+  train_front_end /*@desc "the maximal (aka right) position of a train" */
+INVARIANT
+  occ <: TTDS &
+  train_rear_end : TRAINS --> TRACK &
+  train_front_end : TRAINS --> TRACK &
+  !tr.(tr:TRAINS => train_front_end(tr) >= train_rear_end(tr)) /*@desc "train image not empty" */ &
+  !(t1,t2).(t1:TRAINS & t2 /= t1 => train_occ(t1) /\ train_occ(t2) = {}) /*@desc "no collision" */
+INITIALISATION
+  occ := {ttd1} || train_rear_end := {tr1 |-> 0, tr2 |-> 5} || train_front_end := {tr1 |->2, tr2|->6}
+OPERATIONS
+  
+  TTD_Occupied_By_Train(ttd,tr) = PRE ttd:TTDS \ occ /*@desc "TTD is free */ &
+     train_occ(tr) /\ TTD_TrackElements(ttd) /= {} /*@desc "train occupies TTD */ THEN
+    occ := occ \/ {ttd}
+  END;
+  
+  TTD_Free(ttd) = PRE ttd:occ &
+     train_occ_all /\ TTD_TrackElements(ttd) = {} THEN
+    occ := occ \ {ttd}
+  END;
+  
+  TrainMoveForward(tr,new_front) = PRE tr:TRAINS & new_front = train_rear_end(tr) + train_length(tr) + 1 & //buggy
+                                      new_front:TRACK & 
+        !t2.(t2 /= tr => new_front < train_rear_end(t2) /*@desc not reaching train in front */
+                         // or train_rear_end(tr) > train_front_end(t2) /*@desc train behind */
+                         ) THEN
+    train_rear_end(tr) := train_rear_end(tr) + 1 ||
+    train_front_end(tr) := new_front
+  END
+DEFINITIONS
+ "LibrarySVG.def"; // enable to use the external functions in the VisB json file
+  train_occ(tr) == train_rear_end(tr)..(train_rear_end(tr)+train_length(tr)-1);
+  train_occ_all == UNION(tr).(tr:TRAINS|train_occ(tr));
+  train_length(tr) == 1+train_front_end(tr)-train_rear_end(tr);
+  VISB_JSON_FILE == "TwoTrains.json"
+END
+
+
+/*
+Demo
+ 1. Find deadlock, fix TrainMoveForward
+ 2. add disjunct or train_rear_end(tr) > train_front_end(t2) 
+ 3. animate and see that everything works
+ 4. show visualisation
+*/
\ No newline at end of file

VisB-Examples.prob2project

@@ -380,13 +380,43 @@
       "modelcheckingItems": [],
       "simulation": null,
       "visBVisualisation": "Train/TwoTrains.json"
+    },
+    {
+      "name": "TwoTrainsB",
+      "description": "",
+      "location": "Train/TwoTrainsB.mch",
+      "lastUsedPreferenceName": "default",
+      "ltlFormulas": [],
+      "ltlPatterns": [],
+      "symbolicCheckingFormulas": [],
+      "symbolicAnimationFormulas": [],
+      "simulationItems": [],
+      "testCases": [],
+      "traces": [],
+      "modelcheckingItems": [
+        {
+          "nodesLimit": "-",
+          "timeLimit": "-",
+          "options": {
+            "options": [
+              "FIND_DEADLOCKS",
+              "FIND_INVARIANT_VIOLATIONS",
+              "INSPECT_EXISTING_NODES"
+            ]
+          },
+          "goal": "-",
+          "shouldExecute": true
+        }
+      ],
+      "simulation": null,
+      "visBVisualisation": "Train/TwoTrains.json"
     }
   ],
   "preferences": [],
   "metadata": {
     "fileType": "Project",
     "formatVersion": 12,
-    "savedAt": "2021-05-04T16:44:31.663852Z",
+    "savedAt": "2021-05-04T20:43:11.650963Z",
     "creator": "User",
     "proB2KernelVersion": "4.0.0-SNAPSHOT",
     "proBCliVersion": null,