diff --git a/Train/TwoTrains.svg b/Train/TwoTrains.svg
index 988efb4b1f4fdd42dbefc245cf1c926eeffc1c62..ce510a0a8cc90f2c95088f9d2b3109e6e1b49cbc 100644
--- a/Train/TwoTrains.svg
+++ b/Train/TwoTrains.svg
@@ -2,8 +2,8 @@
<svg
xmlns="http://www.w3.org/2000/svg"
width="900"
- height="400"
- viewBox="5 15 150 30"
+ height="200"
+ viewBox="5 15 150 20"
version="1.1"
id="svg5154">
@@ -25,8 +25,8 @@
fill : lightgray
}
.train-hover {
- fill : red;
- stroke-width: 0.5;
+ fill : rosybrown;
+ stroke-width: 0.35;
stroke : black;
}
.train-back {
@@ -40,13 +40,18 @@
fill : green
}
.green-ma {
- fill : lightgreen;
+ fill : khaki;
stroke : none;
stroke-width: 0.1;
opacity: 1.0
}
</style>
+ <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.25)" />
+
<polygon id = "train_polygon_tr1"
points="0,0 100,0"
class="train-normal"
@@ -88,10 +93,6 @@
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
index 508fe86a41d921fe4a556d523efbc5e0b95e058a..610b0ef50ed09edb09cf9fafd10e680c210ced1f 100644
--- a/Train/TwoTrainsMA.json
+++ b/Train/TwoTrainsMA.json
@@ -28,7 +28,7 @@
"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"
+ "comment":"colour train back polygon"
},
{
"repeat": ["tr1","tr2"],
@@ -41,7 +41,7 @@
"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))",
+ "value":"\"Train %0 is at \" ^ TO_STRING(train_rear_end(%0)) ^ \"..\" ^ TO_STRING(train_front_end(%0)) ^ IF %0:dom(train_ma) THEN \" with MA until \" ^ TO_STRING(train_ma(%0)) ELSE \" and has no MA\" END",
"comment":"adapt info field of train"
},
@@ -72,21 +72,21 @@
{
"id":"ma_polygon",
"attr":"points",
- "value":"svg_set_polygon(train_ma_all,100.0/real(TrackElementNumber+1),100.0,0.5)",
+ "value":"svg_set_polygon(train_ma_all,100.0/real(TrackElementNumber+1),100.0,0.75)",
"comment":"show MA reserved zones"
}
],
"events":[
{
"id":"occupied_ttd_polygon",
- "event":"TTD_Free",
+ "event":"TrainAcceptsFirstMA",
"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",
+ "event":"TrainAcceptsNewMA",
"optional" : true,
"hovers": [{ "attr":"stroke", "enter":"black", "leave":"none"},
{ "attr":"opacity", "enter":"0.5", "leave":"1.0"}]
diff --git a/Train/TwoTrainsMA.mch b/Train/TwoTrainsMA.mch
index 5348d5afa1aaa6234c2f62e6013b4f8703fac8bb..1e3d418f2a11babe2ea17e7fb143a359aebdb340 100644
--- a/Train/TwoTrainsMA.mch
+++ b/Train/TwoTrainsMA.mch
@@ -45,17 +45,19 @@ OPERATIONS
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
+ // 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:TRACK & new_front < train_ma(tr) THEN
+ // 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) // buggy : <=
+ 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*/
+ train_front_end(tr) := new_front ;
+ occ := {ttd | ttd:TTDS & TTD_TrackElements(ttd) /\ train_occ_all /= {}} /* buggy ; use seq. composition instead of || */
END
DEFINITIONS
"LibrarySVG.def"; // enable to use the external functions in the VisB json file
diff --git a/VisB-Examples.prob2project b/VisB-Examples.prob2project
index daa043b9cb905150544ccfcb2b0a3a62ee35c49f..4856c72980d37be8deea04143e4840088c3dd08f 100644
--- a/VisB-Examples.prob2project
+++ b/VisB-Examples.prob2project
@@ -422,17 +422,33 @@
"symbolicAnimationFormulas": [],
"simulationItems": [],
"testCases": [],
- "traces": [],
- "modelcheckingItems": [],
+ "traces": [
+ "traces/TwoTrainsMA.prob2trace"
+ ],
+ "modelcheckingItems": [
+ {
+ "nodesLimit": "-",
+ "timeLimit": "-",
+ "options": {
+ "options": [
+ "FIND_DEADLOCKS",
+ "FIND_INVARIANT_VIOLATIONS",
+ "INSPECT_EXISTING_NODES"
+ ]
+ },
+ "goal": "-",
+ "shouldExecute": true
+ }
+ ],
"simulation": null,
- "visBVisualisation": null
+ "visBVisualisation": "Train/TwoTrainsMA.json"
}
],
"preferences": [],
"metadata": {
"fileType": "Project",
"formatVersion": 12,
- "savedAt": "2021-05-05T07:39:51.437871Z",
+ "savedAt": "2021-05-05T10:13:41.024463Z",
"creator": "User",
"proB2KernelVersion": "4.0.0-SNAPSHOT",
"proBCliVersion": null,
diff --git a/traces/TwoTrainsMA.prob2trace b/traces/TwoTrainsMA.prob2trace
new file mode 100644
index 0000000000000000000000000000000000000000..17809f564c09f821204fb8efc90994d8fa83c67d
--- /dev/null
+++ b/traces/TwoTrainsMA.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