From a1b2fe56bdab34020835d145e58d6a1cdc3fccf2 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Thu, 6 May 2021 14:37:38 +0200
Subject: [PATCH] add unicode version of model
---
Makefile | 14 +++---
Train/TwoTrainsMA.mch | 2 +-
Train/TwoTrainsMA_Unicode.mch | 83 +++++++++++++++++++++++++++++++++++
VisB-Examples.prob2project | 20 ++++++++-
4 files changed, 111 insertions(+), 8 deletions(-)
create mode 100644 Train/TwoTrainsMA_Unicode.mch
diff --git a/Makefile b/Makefile
index 35c47fa..fd22e5d 100644
--- a/Makefile
+++ b/Makefile
@@ -1,10 +1,12 @@
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
\ No newline at end of file
+ $(PROBCLI) Train/SimpleTrainTrack.mch -trace_replay json traces/SimpleTrainTrack.prob2trace -visb_with_vars Train/Track.json traces/html/Track.html
+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
diff --git a/Train/TwoTrainsMA.mch b/Train/TwoTrainsMA.mch
index 1e3d418..3dd1d2e 100644
--- a/Train/TwoTrainsMA.mch
+++ b/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
diff --git a/Train/TwoTrainsMA_Unicode.mch b/Train/TwoTrainsMA_Unicode.mch
new file mode 100644
index 0000000..4f6c1c6
--- /dev/null
+++ b/Train/TwoTrainsMA_Unicode.mch
@@ -0,0 +1,83 @@
+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
diff --git a/VisB-Examples.prob2project b/VisB-Examples.prob2project
index 4856c72..0efbf3d 100644
--- a/VisB-Examples.prob2project
+++ b/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,
--
GitLab