add new more sophisticated example

Train/TwoTrains.json

@@ -61,6 +61,12 @@
       "attr":"points",
       "value":"svg_set_polygon(FREE_TE,100.0/real(TrackElementNumber+1),100.0,2.0)",
       "comment":"show free TTD zones"
+    },
+    {
+      "id":"ma_polygon",
+      "attr":"visibility",
+      "value":"\"hidden\"",
+      "comment":"hide MA reserved zones"
     }
     ],
   "events":[ 

Train/TwoTrains.svg

@@ -30,10 +30,21 @@
             stroke : black;
         }
         .train-back {
+            stroke-width: 0.2;
+            stroke : black;
+            fill : gray80
+        }
+        .train-back-connected {
             stroke-width: 0.2;
             stroke : black;
             fill : green
         }
+        .green-ma {
+            fill : lightgreen;
+            stroke : none;
+            stroke-width: 0.1;
+            opacity: 1.0
+        }
    </style>
    
     <polygon id = "train_polygon_tr1"
@@ -77,6 +88,10 @@
        stroke="gray" fill="none"
        transform="translate(10,22.5)" />
        
+  <polygon id = "ma_polygon"
+       points="0,0 0,2 10,2 10,0 70,0 70,1 90,1 90,0"
+       class = "green-ma"
+       transform="translate(10,19.5)" />
        
   <rect id = "ttd_rect"
        style="stroke-width: 0.1"

Train/TwoTrainsMA.json

+{
+  "svg":"TwoTrains.svg",
+    "definitions":[
+    { "name":"OCC_TE",
+      "value" : "union(ran(%tt.(tt:occ|TTD_TrackElements(tt))))"
+    },
+    { "name":"FREE_TE",
+      "value" : "union(ran(%tt.(tt/:occ|TTD_TrackElements(tt))))"
+    }],
+  "items":[
+  
+    {
+	  "repeat": ["tr1","tr2"],
+      "id":"train_polygon_%0",
+      "attr":"points",
+      "value":"svg_train(train_rear_end(%0), train_length(%0) ,100.0/real(TrackElementNumber+1),1.0,3.0)",
+      "comment":"show train position using a slanted polygon"
+    },
+    {
+	  "repeat": ["tr1","tr2"],
+      "id":"train_back_%0",
+      "attr":"points",
+      "value":"svg_train(real(train_rear_end(%0)), 0.3 ,100.0/real(TrackElementNumber+1),0.0,3.0)",
+      "comment":"show train back polygon"
+    },
+    {
+	  "repeat": ["tr1","tr2"],
+      "id":"train_back_%0",
+      "attr":"class",
+      "value":"IF %0 : dom(train_ma) THEN \"train-back-connected\" ELSE \"train-back\" END",
+      "comment":"show train back polygon"
+    },
+    {
+	  "repeat": ["tr1","tr2"],
+      "id":"train_info_text_%0",
+      "attr":"x",
+      "value":"real(train_rear_end(%0))*100.0/real(TrackElementNumber+1)",
+      "comment":"move info field above train"
+    },
+    {
+	  "repeat": ["tr1","tr2"],
+      "id":"train_info_text_%0",
+      "attr":"text",
+      "value":"\"Train %0: \" ^ TO_STRING(train_rear_end(%0)) ^ \"..\" ^ TO_STRING(train_rear_end(%0)+train_length(%0))",
+      "comment":"adapt info field of train"
+    },
+    
+    {
+      "id":"track_polyline",
+      "attr":"points",
+      "value":"svg_axis({TrackElementNumber+1} \\/ TRACK ,100.0/real(TrackElementNumber+1),100.0,1.0)",
+      "comment":"show ticks for Track units"
+    },
+    {
+      "id":"ttd_polyline",
+      "attr":"points",
+      "value":"svg_axis({0} \\/ ran(%tt.(tt:TTDS|1+max(TTD_TrackElements(tt)))),100.0/real(TrackElementNumber+1),100.0,2.0)",
+      "comment":"show ticks for TTD Limits"
+    },
+    {
+      "id":"occupied_ttd_polygon",
+      "attr":"points",
+      "value":"svg_set_polygon(OCC_TE,100.0/real(TrackElementNumber+1),100.0,2.0)",
+      "comment":"show occupied TTD zones"
+    },
+    {
+      "id":"cleared_ttd_polygon",
+      "attr":"points",
+      "value":"svg_set_polygon(FREE_TE,100.0/real(TrackElementNumber+1),100.0,2.0)",
+      "comment":"show free TTD zones"
+    },
+    {
+      "id":"ma_polygon",
+      "attr":"points",
+      "value":"svg_set_polygon(train_ma_all,100.0/real(TrackElementNumber+1),100.0,0.5)",
+      "comment":"show MA reserved zones"
+    }
+    ],
+  "events":[ 
+    {
+      "id":"occupied_ttd_polygon",
+      "event":"TTD_Free",
+      "optional" : true,
+      "hovers": [{ "attr":"stroke", "enter":"black", "leave":"none"},
+                 { "attr":"opacity", "enter":"0.5", "leave":"1.0"}]
+    },
+    {
+      "id":"cleared_ttd_polygon",
+      "event":"TTD_Occupied_By_Train",
+      "optional" : true,
+      "hovers": [{ "attr":"stroke", "enter":"black", "leave":"none"},
+                 { "attr":"opacity", "enter":"0.5", "leave":"1.0"}]
+    },
+    {
+      "id":"train_polygon_tr1",
+      "event":"TrainMoveForward",
+      "predicates" : ["tr=tr1"],
+      "optional" : true,
+      "hovers": [{ "attr":"class", "enter":"train-hover", "leave":"train-normal"},
+                 { "id":"train_info_text_tr1", "attr":"visibility", "enter":"visible", "leave":"hidden"}]
+    },
+    {
+      "id":"train_polygon_tr2",
+      "event":"TrainMoveForward",
+      "predicates" : ["tr=tr2"],
+      "optional" : true,
+      "hovers": [{ "attr":"class", "enter":"train-hover", "leave":"train-normal"},
+                 { "id":"train_info_text_tr2", "attr":"visibility", "enter":"visible", "leave":"hidden"}]
+    }
+    ]
+}
\ No newline at end of file

Train/TwoTrainsMA.mch

+MACHINE TwoTrainsMA
+// A small example to show how one can use LibrarySVG to flexibliy visualise
+// train track zones and MAs; model 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 not 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" */ 
+     // !(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:TRACK &  new_front < train_ma(tr) THEN
+    train_rear_end(tr) := train_rear_end(tr) + 1 ||
+    train_front_end(tr) := new_front ||
+    occ := {ttd | ttd:TTDS & TTD_TrackElements(ttd) /\ train_occ_all /= {}} /* buggy ; use seq. composition*/
+  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 == "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

@@ -410,13 +410,29 @@
       ],
       "simulation": null,
       "visBVisualisation": "Train/TwoTrains.json"
+    },
+    {
+      "name": "TwoTrainsMA",
+      "description": "",
+      "location": "Train/TwoTrainsMA.mch",
+      "lastUsedPreferenceName": "default",
+      "ltlFormulas": [],
+      "ltlPatterns": [],
+      "symbolicCheckingFormulas": [],
+      "symbolicAnimationFormulas": [],
+      "simulationItems": [],
+      "testCases": [],
+      "traces": [],
+      "modelcheckingItems": [],
+      "simulation": null,
+      "visBVisualisation": null
     }
   ],
   "preferences": [],
   "metadata": {
     "fileType": "Project",
     "formatVersion": 12,
-    "savedAt": "2021-05-04T20:43:11.650963Z",
+    "savedAt": "2021-05-05T07:39:51.437871Z",
     "creator": "User",
     "proB2KernelVersion": "4.0.0-SNAPSHOT",
     "proBCliVersion": null,