From c143df5bfefddb7c0090d24657a4a39c8e523967 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Thu, 6 May 2021 15:28:33 +0200
Subject: [PATCH] add descriptions to model
---
Train/TwoTrainsMA.mch | 30 +-
Train/TwoTrainsMA_Unicode.mch | 23 +-
VisB-Examples.prob2project | 14 +-
traces/TwoTrainsMA.prob2trace | 38 +-
traces/TwoTrainsMA_30.prob2trace | 651 +++++++++++++++++++++++++++++++
5 files changed, 698 insertions(+), 58 deletions(-)
create mode 100644 traces/TwoTrainsMA_30.prob2trace
diff --git a/Train/TwoTrainsMA.mch b/Train/TwoTrainsMA.mch
index 3dd1d2e..95b51af 100644
--- a/Train/TwoTrainsMA.mch
+++ b/Train/TwoTrainsMA.mch
@@ -2,34 +2,40 @@ 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}
+ TTDS = {ttd1,ttd2,ttd3,ttd4} /*@desc "Trackside Track Detection zones" */;
+ TRAINS = {tr1,tr2} /*@desc "The set of trains" */
CONSTANTS
- TrackElementNumber, TRACK, TTD_TrackElements
+ TrackElementNumber /*@desc "The maximum nr of a track element" */,
+ TRACK /*desc "The set of positions comprising the track" */,
+ TTD_TrackElements /*@desc "Mapping from TTDs to sets of positions" */
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}
+& TrackElementNumber = 25
+& TTD_TrackElements = {ttd1 |-> 0..4 , ttd2 |-> 5..10 , ttd3 |-> 11..20, ttd4 |-> 21..25}
& !(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" */
+ train_ma /*@desc "the Movement Authority given to a registered train" */
INVARIANT
- occ <: TTDS &
+ occ <: TTDS /*@desc "occ is a set of TTDs" */ &
train_rear_end : TRAINS --> TRACK &
train_front_end : TRAINS --> TRACK &
- train_ma : TRAINS +-> TRACK &
+ train_ma : TRAINS +-> TRACK /*@desc "partial function associating trains with farthest point it is allowed to move" */ &
!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
+ !tr.(tr:TRAINS => train_front_end(tr) >= train_rear_end(tr)) /*@desc "train positions on track not empty" */ &
+ /*@label "SAF-1" */ !(t1,t2).(t1:TRAINS & t2 /= t1
+ => train_occ(t1) /\ train_occ(t2) = {}) /*@desc "no collision" */ &
+ /*@label "SAF-2" */ !(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
@@ -39,11 +45,13 @@ OPERATIONS
TrainAcceptsFirstMA(tr,newMA) = PRE tr/:dom(train_ma) & newMA:TRACK & newMA > train_front_end(tr) &
+ newMA mod 5 = 0 /*@desc "Restriction to restrict state space for MC" */ &
!(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) &
+ newMA mod 5 = 0 /*@desc "Restriction to restrict state space for MC" */ &
!(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
diff --git a/Train/TwoTrainsMA_Unicode.mch b/Train/TwoTrainsMA_Unicode.mch
index 4f6c1c6..927fa3d 100644
--- a/Train/TwoTrainsMA_Unicode.mch
+++ b/Train/TwoTrainsMA_Unicode.mch
@@ -1,12 +1,14 @@
-MACHINE TwoTrainsMA
+MACHINE TwoTrainsMA_Unicode
// 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}
+ TTDS = {ttd1,ttd2,ttd3,ttd4} /*@desc "Trackside Track Detection zones" */;
+ TRAINS = {tr1,tr2} /*@desc "The set of trains" */
CONSTANTS
- TrackElementNumber, TRACK, TTD_TrackElements
+ TrackElementNumber /*@desc "The maximum nr of a track element" */,
+ TRACK /*desc "The set of positions comprising the track" */,
+ TTD_TrackElements /*@desc "Mapping from TTDs to sets of positions" */
PROPERTIES
TrackElementNumber ∈ NATURAL1
∧ TRACK = 0..TrackElementNumber
@@ -23,7 +25,7 @@ VARIABLES
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 ∧
+ occ ⊆ TTDS /*@desc "occ is a set of TTDs" */ ∧
train_rear_end ∈ TRAINS → TRACK ∧
train_front_end ∈ TRAINS → TRACK ∧
train_ma ∈ TRAINS ⇸ TRACK ∧
@@ -71,13 +73,4 @@ DEFINITIONS
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
+END
\ No newline at end of file
diff --git a/VisB-Examples.prob2project b/VisB-Examples.prob2project
index 0efbf3d..6c61fa0 100644
--- a/VisB-Examples.prob2project
+++ b/VisB-Examples.prob2project
@@ -438,6 +438,18 @@
},
"goal": "-",
"shouldExecute": true
+ },
+ {
+ "nodesLimit": "-",
+ "timeLimit": "-",
+ "options": {
+ "options": [
+ "FIND_INVARIANT_VIOLATIONS",
+ "INSPECT_EXISTING_NODES"
+ ]
+ },
+ "goal": "-",
+ "shouldExecute": true
}
],
"simulation": null,
@@ -466,7 +478,7 @@
"metadata": {
"fileType": "Project",
"formatVersion": 12,
- "savedAt": "2021-05-06T12:36:10.371287Z",
+ "savedAt": "2021-05-06T13:17:55.964399Z",
"creator": "User",
"proB2KernelVersion": "4.0.0-SNAPSHOT",
"proBCliVersion": null,
diff --git a/traces/TwoTrainsMA.prob2trace b/traces/TwoTrainsMA.prob2trace
index 17809f5..ec1f193 100644
--- a/traces/TwoTrainsMA.prob2trace
+++ b/traces/TwoTrainsMA.prob2trace
@@ -6,9 +6,6 @@
"params": {},
"results": {},
"destState": {
- "TTD_TrackElements": "{(ttd1↦{0,1,2,3,4}),(ttd2↦{5,6,7,8,9,10}),(ttd3↦{11,12,13,14,15,16,17,18,19,20,21,22,23,24,25}),(ttd4↦{26,27,28,29,30})}",
- "TrackElementNumber": "30",
- "TRACK": "{0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30}"
},
"destStateNotChanged": [],
"preds": []
@@ -18,10 +15,6 @@
"params": {},
"results": {},
"destState": {
- "train_rear_end": "{(tr1↦0),(tr2↦5)}",
- "train_front_end": "{(tr1↦2),(tr2↦6)}",
- "train_ma": "∅",
- "occ": "{ttd1,ttd2}"
},
"destStateNotChanged": [],
"preds": []
@@ -29,12 +22,12 @@
{
"name": "TrainAcceptsFirstMA",
"params": {
- "newMA": "14",
+ "newMA": "15",
"tr": "tr2"
},
"results": {},
"destState": {
- "train_ma": "{(tr2↦14)}"
+ "train_ma": "{(tr2↦15)}"
},
"destStateNotChanged": [
"train_front_end",
@@ -80,12 +73,12 @@
{
"name": "TrainAcceptsFirstMA",
"params": {
- "newMA": "4",
+ "newMA": "5",
"tr": "tr1"
},
"results": {},
"destState": {
- "train_ma": "{(tr1↦4),(tr2↦14)}"
+ "train_ma": "{(tr1↦5),(tr2↦15)}"
},
"destStateNotChanged": [
"train_front_end",
@@ -204,7 +197,7 @@
},
"results": {},
"destState": {
- "train_ma": "{(tr1↦10),(tr2↦14)}"
+ "train_ma": "{(tr1↦10),(tr2↦15)}"
},
"destStateNotChanged": [
"train_front_end",
@@ -250,12 +243,12 @@
{
"name": "TrainAcceptsNewMA",
"params": {
- "newMA": "23",
+ "newMA": "25",
"tr": "tr2"
},
"results": {},
"destState": {
- "train_ma": "{(tr1↦10),(tr2↦23)}"
+ "train_ma": "{(tr1↦10),(tr2↦25)}"
},
"destStateNotChanged": [
"train_front_end",
@@ -400,23 +393,6 @@
],
"preds": []
},
- {
- "name": "TrainAcceptsNewMA",
- "params": {
- "newMA": "25",
- "tr": "tr2"
- },
- "results": {},
- "destState": {
- "train_ma": "{(tr1↦10),(tr2↦25)}"
- },
- "destStateNotChanged": [
- "train_front_end",
- "train_rear_end",
- "occ"
- ],
- "preds": []
- },
{
"name": "TrainMoveForward",
"params": {
diff --git a/traces/TwoTrainsMA_30.prob2trace b/traces/TwoTrainsMA_30.prob2trace
new file mode 100644
index 0000000..17809f5
--- /dev/null
+++ b/traces/TwoTrainsMA_30.prob2trace
@@ -0,0 +1,651 @@
+{
+ "description": "",
+ "transitionList": [
+ {
+ "name": "$setup_constants",
+ "params": {},
+ "results": {},
+ "destState": {
+ "TTD_TrackElements": "{(ttd1↦{0,1,2,3,4}),(ttd2↦{5,6,7,8,9,10}),(ttd3↦{11,12,13,14,15,16,17,18,19,20,21,22,23,24,25}),(ttd4↦{26,27,28,29,30})}",
+ "TrackElementNumber": "30",
+ "TRACK": "{0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30}"
+ },
+ "destStateNotChanged": [],
+ "preds": []
+ },
+ {
+ "name": "$initialise_machine",
+ "params": {},
+ "results": {},
+ "destState": {
+ "train_rear_end": "{(tr1↦0),(tr2↦5)}",
+ "train_front_end": "{(tr1↦2),(tr2↦6)}",
+ "train_ma": "∅",
+ "occ": "{ttd1,ttd2}"
+ },
+ "destStateNotChanged": [],
+ "preds": []
+ },
+ {
+ "name": "TrainAcceptsFirstMA",
+ "params": {
+ "newMA": "14",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_ma": "{(tr2↦14)}"
+ },
+ "destStateNotChanged": [
+ "train_front_end",
+ "train_rear_end",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "7",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦2),(tr2↦7)}",
+ "train_rear_end": "{(tr1↦0),(tr2↦6)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "8",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦2),(tr2↦8)}",
+ "train_rear_end": "{(tr1↦0),(tr2↦7)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainAcceptsFirstMA",
+ "params": {
+ "newMA": "4",
+ "tr": "tr1"
+ },
+ "results": {},
+ "destState": {
+ "train_ma": "{(tr1↦4),(tr2↦14)}"
+ },
+ "destStateNotChanged": [
+ "train_front_end",
+ "train_rear_end",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "9",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦2),(tr2↦9)}",
+ "train_rear_end": "{(tr1↦0),(tr2↦8)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "3",
+ "tr": "tr1"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦3),(tr2↦9)}",
+ "train_rear_end": "{(tr1↦1),(tr2↦8)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "10",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦3),(tr2↦10)}",
+ "train_rear_end": "{(tr1↦1),(tr2↦9)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "11",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_rear_end": "{(tr1↦1),(tr2↦10)}",
+ "train_front_end": "{(tr1↦3),(tr2↦11)}",
+ "occ": "{ttd1,ttd2,ttd3}"
+ },
+ "destStateNotChanged": [
+ "train_ma"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "12",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_rear_end": "{(tr1↦1),(tr2↦11)}",
+ "train_front_end": "{(tr1↦3),(tr2↦12)}",
+ "occ": "{ttd1,ttd3}"
+ },
+ "destStateNotChanged": [
+ "train_ma"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "13",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦3),(tr2↦13)}",
+ "train_rear_end": "{(tr1↦1),(tr2↦12)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainAcceptsNewMA",
+ "params": {
+ "newMA": "10",
+ "tr": "tr1"
+ },
+ "results": {},
+ "destState": {
+ "train_ma": "{(tr1↦10),(tr2↦14)}"
+ },
+ "destStateNotChanged": [
+ "train_front_end",
+ "train_rear_end",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "4",
+ "tr": "tr1"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦4),(tr2↦13)}",
+ "train_rear_end": "{(tr1↦2),(tr2↦12)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "5",
+ "tr": "tr1"
+ },
+ "results": {},
+ "destState": {
+ "train_rear_end": "{(tr1↦3),(tr2↦12)}",
+ "train_front_end": "{(tr1↦5),(tr2↦13)}",
+ "occ": "{ttd1,ttd2,ttd3}"
+ },
+ "destStateNotChanged": [
+ "train_ma"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainAcceptsNewMA",
+ "params": {
+ "newMA": "23",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_ma": "{(tr1↦10),(tr2↦23)}"
+ },
+ "destStateNotChanged": [
+ "train_front_end",
+ "train_rear_end",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "14",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦5),(tr2↦14)}",
+ "train_rear_end": "{(tr1↦3),(tr2↦13)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "6",
+ "tr": "tr1"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦6),(tr2↦14)}",
+ "train_rear_end": "{(tr1↦4),(tr2↦13)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "15",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦6),(tr2↦15)}",
+ "train_rear_end": "{(tr1↦4),(tr2↦14)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "7",
+ "tr": "tr1"
+ },
+ "results": {},
+ "destState": {
+ "train_rear_end": "{(tr1↦5),(tr2↦14)}",
+ "train_front_end": "{(tr1↦7),(tr2↦15)}",
+ "occ": "{ttd2,ttd3}"
+ },
+ "destStateNotChanged": [
+ "train_ma"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "16",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦7),(tr2↦16)}",
+ "train_rear_end": "{(tr1↦5),(tr2↦15)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "8",
+ "tr": "tr1"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦8),(tr2↦16)}",
+ "train_rear_end": "{(tr1↦6),(tr2↦15)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "17",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦8),(tr2↦17)}",
+ "train_rear_end": "{(tr1↦6),(tr2↦16)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "18",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦8),(tr2↦18)}",
+ "train_rear_end": "{(tr1↦6),(tr2↦17)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainAcceptsNewMA",
+ "params": {
+ "newMA": "25",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_ma": "{(tr1↦10),(tr2↦25)}"
+ },
+ "destStateNotChanged": [
+ "train_front_end",
+ "train_rear_end",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "19",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦8),(tr2↦19)}",
+ "train_rear_end": "{(tr1↦6),(tr2↦18)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "20",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦8),(tr2↦20)}",
+ "train_rear_end": "{(tr1↦6),(tr2↦19)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "21",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦8),(tr2↦21)}",
+ "train_rear_end": "{(tr1↦6),(tr2↦20)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "22",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦8),(tr2↦22)}",
+ "train_rear_end": "{(tr1↦6),(tr2↦21)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "9",
+ "tr": "tr1"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦9),(tr2↦22)}",
+ "train_rear_end": "{(tr1↦7),(tr2↦21)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "23",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦9),(tr2↦23)}",
+ "train_rear_end": "{(tr1↦7),(tr2↦22)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ },
+ {
+ "name": "TrainMoveForward",
+ "params": {
+ "new_front": "24",
+ "tr": "tr2"
+ },
+ "results": {},
+ "destState": {
+ "train_front_end": "{(tr1↦9),(tr2↦24)}",
+ "train_rear_end": "{(tr1↦7),(tr2↦23)}"
+ },
+ "destStateNotChanged": [
+ "train_ma",
+ "occ"
+ ],
+ "preds": []
+ }
+ ],
+ "variableNames": [
+ "occ",
+ "train_rear_end",
+ "train_front_end",
+ "train_ma"
+ ],
+ "constantNames": [
+ "TrackElementNumber",
+ "TRACK",
+ "TTD_TrackElements"
+ ],
+ "setNames": [
+ "TTDS",
+ "TRAINS"
+ ],
+ "machineOperationInfos": {
+ "TrainMoveForward": {
+ "operationName": "TrainMoveForward",
+ "parameterNames": [
+ "tr",
+ "new_front"
+ ],
+ "outputParameterNames": [],
+ "topLevel": true,
+ "type": "CLASSICAL_B",
+ "readVariables": [
+ "TRACK",
+ "TTD_TrackElements",
+ "train_front_end",
+ "train_ma",
+ "train_rear_end"
+ ],
+ "writtenVariables": [
+ "occ",
+ "train_front_end",
+ "train_rear_end"
+ ],
+ "nonDetWrittenVariables": [],
+ "typeMap": {
+ "'TTD_TrackElements'": "set(couple(global('TTDS'),set(integer)))",
+ "new_front": "integer",
+ "tr": "global('TRAINS')",
+ "'TRACK'": "set(integer)"
+ }
+ },
+ "TrainAcceptsFirstMA": {
+ "operationName": "TrainAcceptsFirstMA",
+ "parameterNames": [
+ "tr",
+ "newMA"
+ ],
+ "outputParameterNames": [],
+ "topLevel": true,
+ "type": "CLASSICAL_B",
+ "readVariables": [
+ "TRACK",
+ "train_front_end",
+ "train_ma",
+ "train_rear_end"
+ ],
+ "writtenVariables": [
+ "train_ma"
+ ],
+ "nonDetWrittenVariables": [],
+ "typeMap": {
+ "newMA": "integer",
+ "tr": "global('TRAINS')",
+ "'TRACK'": "set(integer)"
+ }
+ },
+ "TrainAcceptsNewMA": {
+ "operationName": "TrainAcceptsNewMA",
+ "parameterNames": [
+ "tr",
+ "newMA"
+ ],
+ "outputParameterNames": [],
+ "topLevel": true,
+ "type": "CLASSICAL_B",
+ "readVariables": [
+ "TRACK",
+ "train_front_end",
+ "train_ma",
+ "train_rear_end"
+ ],
+ "writtenVariables": [
+ "train_ma"
+ ],
+ "nonDetWrittenVariables": [],
+ "typeMap": {
+ "newMA": "integer",
+ "tr": "global('TRAINS')",
+ "'TRACK'": "set(integer)"
+ }
+ }
+ },
+ "globalIdentifierTypes": {
+ "train_ma": "set(couple(global('TRAINS'),integer))",
+ "train_front_end": "set(couple(global('TRAINS'),integer))",
+ "train_rear_end": "set(couple(global('TRAINS'),integer))",
+ "occ": "set(global('TTDS'))"
+ },
+ "metadata": {
+ "fileType": "Trace",
+ "formatVersion": 2,
+ "savedAt": "2021-05-05T08:42:50.789906Z",
+ "creator": "traceReplay",
+ "proB2KernelVersion": "4.0.0-SNAPSHOT",
+ "proBCliVersion": "1.11.0-nightly",
+ "modelName": "TwoTrainsMA"
+ }
+}
\ No newline at end of file
--
GitLab