add unicode version of model

Makefile

 PROBCLI=probcli
 all:
-	$(PROBCLI) Button/button.mch -animate 15 -visb Button/button.json traces/html/button.html
-	$(PROBCLI) Lift/Lift.mch -property 'groundf=-1 & topf=2' -animate 20 -visb Lift/lift_groups.json traces/html/lift_groups.html
-	$(PROBCLI) N-Queens/QueensWithEvents.mch -property 'n=8' -animate 15 -visb N-Queens/queens_8.json traces/html/queens8.html
-	$(PROBCLI) Physics/MovingParticles3.mch -animate 500 -visb Physics/three_bodies.json traces/html/three_bodies.html
-	$(PROBCLI) Train/SimpleTrainTrack.mch -trace_replay json traces/SimpleTrainTrack.prob2trace -visb Train/Track.json traces/html/Track.html
+	$(PROBCLI) Button/button.mch -animate 15 -visb_with_vars Button/button.json traces/html/button.html
+	$(PROBCLI) Lift/Lift.mch -property 'groundf=-1 & topf=2' -animate 20 -visb_with_vars Lift/lift_groups.json traces/html/lift_groups.html
+	$(PROBCLI) N-Queens/QueensWithEvents.mch -property 'n=8' -animate 15 -visb_with_vars N-Queens/queens_8.json traces/html/queens8.html
+	$(PROBCLI) Physics/MovingParticles3.mch -animate 500 -visb_with_vars Physics/three_bodies.json traces/html/three_bodies.html
+	$(PROBCLI) Train/SimpleTrainTrack.mch -trace_replay json traces/SimpleTrainTrack.prob2trace -visb_with_vars Train/Track.json traces/html/Track.html
 
 track:
-		$(PROBCLI) Train/SimpleTrainTrack.mch -trace_replay json traces/SimpleTrainTrack.prob2trace -visb Train/Track.json traces/html/Track.html
+		$(PROBCLI) Train/SimpleTrainTrack.mch -trace_replay json traces/SimpleTrainTrack.prob2trace -visb_with_vars Train/Track.json traces/html/Track.html
\ No newline at end of file
+two:
+		$(PROBCLI) Train/TwoTrainsMA.mch -trace_replay json traces/TwoTrainsMA.prob2trace -visb_with_vars Train/TwoTrainsMA.json traces/html/TwoTrainsMA.html
\ No newline at end of file

Train/TwoTrainsMA.mch

@@ -68,7 +68,7 @@ DEFINITIONS
   train_occ_all == UNION(train).(train:TRAINS|train_occ(train));
   train_ma_all == UNION(train).(train:dom(train_ma)|(1+train_front_end(train))..train_ma(train));
   train_length(train) == 1+train_front_end(train)-train_rear_end(train);
-  VISB_JSON_FILE == "TwoTrains.json"
+  VISB_JSON_FILE == "TwoTrainsMA.json"
 END
 
 

Train/TwoTrainsMA_Unicode.mch

+MACHINE TwoTrainsMA
+// A small example to show how one can use LibrarySVG to flexibliy visualise
+// train track zones and MAs; 
+// unicode and corrected version of model that contains some errors on purpose to show how visualisation can help spot them
+SETS
+  TTDS = {ttd1,ttd2,ttd3,ttd4};
+  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..4 , ttd2 ↦ 5..10 , ttd3 ↦ 11..25, ttd4 ↦ 26..30}
+∧ ∀(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" */,
+  train_front_end /*@desc "the maximal (aka right) position of a train" */,
+  train_ma /*@desc "the Movement Authority given to a train" */
+INVARIANT
+  occ ⊆ TTDS ∧
+  train_rear_end ∈ TRAINS → TRACK ∧
+  train_front_end ∈ TRAINS → TRACK ∧
+  train_ma ∈ TRAINS ⇸ TRACK ∧
+  ∀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 image ¬ empty" */ ∧
+  ∀(t1,t2).(t1∈TRAINS ∧ t2 ≠ t1 ⇒ train_occ(t1) ∩ train_occ(t2) = ∅) /*@desc "no collision" */ ∧
+  ∀(t1,t2).(t1∈TRAINS ∧ t2 ≠ t1 ⇒ train_reserved(t1) ∩ train_reserved(t2) = ∅) /*@desc "reserved areas disjoint" */ ASSERTIONS
+  ∀(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 := ∅
+OPERATIONS
+  
+  
+  TrainAcceptsFirstMA(tr,newMA) = PRE tr∉dom(train_ma) ∧ newMA∈TRACK ∧ newMA > train_front_end(tr) ∧
+      ∀(t2).(t2 ≠ tr ⇒ train_rear_end(tr)..newMA ∩ train_reserved(t2) = ∅) /*@desc "MA is safe" */ THEN
+     train_ma(tr) := newMA
+  END;
+  
+  TrainAcceptsNewMA(tr,newMA) = PRE tr∈dom(train_ma) ∧ newMA∈TRACK ∧ newMA > train_ma(tr) ∧
+      ∀(t2).(t2 ≠ tr ⇒ train_ma(tr)..newMA ∩ train_reserved(t2) = ∅) /*@desc "MA extension is safe" */ 
+     // TODO∈ use TTD info ∀(ttd).(ttd∈occ ⇒ train_ma(tr)..newMA
+      THEN
+     train_ma(tr) := newMA
+  END;
+  
+  TrainMoveForward(tr,new_front) = PRE tr∈dom(train_ma) ∧ 
+                                      // new_front = train_rear_end(tr) + train_length(tr) + 1 ∧ //buggy
+                                       new_front = train_front_end(tr) + 1 ∧ //correct
+                                       new_front∈TRACK ∧  new_front <= train_ma(tr) // correct: ≤
+                                       THEN
+    BEGIN train_rear_end(tr) := train_rear_end(tr) + 1 ||
+          train_front_end(tr) := new_front 
+    END;
+    occ := {ttd | ttd∈TTDS ∧ TTD_TrackElements(ttd) ∩ train_occ_all ≠ ∅} /* correct: ; use seq. composition instead of || */
+  END
+DEFINITIONS
+ "LibrarySVG.def"; // enable to use the external functions in the VisB json file
+  train_occ(train) ==
+         train_rear_end(train)..(train_rear_end(train)+train_length(train)-1);
+  train_reserved(train) == 
+         train_rear_end(train)..IF train∈dom(train_ma) THEN train_ma(train) ELSE train_front_end(train) END;
+  train_occ_all == UNION(train).(train∈TRAINS|train_occ(train));
+  train_ma_all == UNION(train).(train∈dom(train_ma)|(1+train_front_end(train))..train_ma(train));
+  train_length(train) == 1+train_front_end(train)-train_rear_end(train);
+  VISB_JSON_FILE == "TwoTrainsMA.json"
+END
+
+
+/*
+Demo
+ 1. Find deadlock, fix TrainMoveForward
+ 2. add disjunct ∨ 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

@@ -442,13 +442,31 @@
       ],
       "simulation": null,
       "visBVisualisation": "Train/TwoTrainsMA.json"
+    },
+    {
+      "name": "TwoTrainsMA_Unicode",
+      "description": "",
+      "location": "Train/TwoTrainsMA_Unicode.mch",
+      "lastUsedPreferenceName": "default",
+      "ltlFormulas": [],
+      "ltlPatterns": [],
+      "symbolicCheckingFormulas": [],
+      "symbolicAnimationFormulas": [],
+      "simulationItems": [],
+      "testCases": [],
+      "traces": [
+        "traces/TwoTrainsMA.prob2trace"
+      ],
+      "modelcheckingItems": [],
+      "simulation": null,
+      "visBVisualisation": "Train/TwoTrainsMA.json"
     }
   ],
   "preferences": [],
   "metadata": {
     "fileType": "Project",
     "formatVersion": 12,
-    "savedAt": "2021-05-05T10:13:41.024463Z",
+    "savedAt": "2021-05-06T12:36:10.371287Z",
     "creator": "User",
     "proB2KernelVersion": "4.0.0-SNAPSHOT",
     "proBCliVersion": null,