From ea652ee621ce4ff6d32b157ae13e88e4bac99415 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Wed, 5 May 2021 10:35:56 +0200
Subject: [PATCH] add new more sophisticated example
---
Train/TwoTrains.json | 6 ++
Train/TwoTrains.svg | 15 +++++
Train/TwoTrainsMA.json | 111 +++++++++++++++++++++++++++++++++++++
Train/TwoTrainsMA.mch | 79 ++++++++++++++++++++++++++
VisB-Examples.prob2project | 18 +++++-
5 files changed, 228 insertions(+), 1 deletion(-)
create mode 100644 Train/TwoTrainsMA.json
create mode 100644 Train/TwoTrainsMA.mch
diff --git a/Train/TwoTrains.json b/Train/TwoTrains.json
index 334f5c0..ee5409b 100644
--- a/Train/TwoTrains.json
+++ b/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":[
diff --git a/Train/TwoTrains.svg b/Train/TwoTrains.svg
index c066b51..988efb4 100644
--- a/Train/TwoTrains.svg
+++ b/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"
diff --git a/Train/TwoTrainsMA.json b/Train/TwoTrainsMA.json
new file mode 100644
index 0000000..508fe86
--- /dev/null
+++ b/Train/TwoTrainsMA.json
@@ -0,0 +1,111 @@
+{
+ "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
diff --git a/Train/TwoTrainsMA.mch b/Train/TwoTrainsMA.mch
new file mode 100644
index 0000000..5348d5a
--- /dev/null
+++ b/Train/TwoTrainsMA.mch
@@ -0,0 +1,79 @@
+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
diff --git a/VisB-Examples.prob2project b/VisB-Examples.prob2project
index cfd613e..daa043b 100644
--- a/VisB-Examples.prob2project
+++ b/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,
--
GitLab