From 584d9e8698c36bd146f40285d6300ea087c3a5b3 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Tue, 4 May 2021 22:51:05 +0200
Subject: [PATCH] add variation of two trains
---
Train/TwoTrains.mch | 2 +-
Train/TwoTrainsB.mch | 64 ++++++++++++++++++++++++++++++++++++++
VisB-Examples.prob2project | 32 ++++++++++++++++++-
3 files changed, 96 insertions(+), 2 deletions(-)
create mode 100644 Train/TwoTrainsB.mch
diff --git a/Train/TwoTrains.mch b/Train/TwoTrains.mch
index 763eec1..d00179d 100644
--- a/Train/TwoTrains.mch
+++ b/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
diff --git a/Train/TwoTrainsB.mch b/Train/TwoTrainsB.mch
new file mode 100644
index 0000000..2ccc56f
--- /dev/null
+++ b/Train/TwoTrainsB.mch
@@ -0,0 +1,64 @@
+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
diff --git a/VisB-Examples.prob2project b/VisB-Examples.prob2project
index 24b25b9..cfd613e 100644
--- a/VisB-Examples.prob2project
+++ b/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,
--
GitLab