Skip to content
Snippets Groups Projects
Commit c143df5b authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add descriptions to model

parent a1b2fe56
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Train/TwoTrainsMA.mch
+ 19
− 11
View file @ c143df5b
...@@ -2,34 +2,40 @@ MACHINE TwoTrainsMA ...@@ -2,34 +2,40 @@ MACHINE TwoTrainsMA
// A small example to show how one can use LibrarySVG to flexibliy visualise // 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 // train track zones and MAs; model contains some errors on purpose to show how visualisation can help spot them
SETS SETS
TTDS = {ttd1,ttd2,ttd3,ttd4}; TTDS = {ttd1,ttd2,ttd3,ttd4} /*@desc "Trackside Track Detection zones" */;
TRAINS = {tr1,tr2} TRAINS = {tr1,tr2} /*@desc "The set of trains" */
CONSTANTS 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 PROPERTIES
TrackElementNumber : NATURAL1 TrackElementNumber : NATURAL1
& TRACK = 0..TrackElementNumber & TRACK = 0..TrackElementNumber
& TTD_TrackElements : TTDS --> FIN1(TRACK) & TTD_TrackElements : TTDS --> FIN1(TRACK)
& TrackElementNumber = 30 & TrackElementNumber = 25
& TTD_TrackElements = {ttd1 |-> 0..4 , ttd2 |-> 5..10 , ttd3 |-> 11..25, ttd4 |-> 26..30} & 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" */ & !(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" */ & union(ran(TTD_TrackElements)) = TRACK /*desc "TTDs cover the entire track" */
VARIABLES VARIABLES
occ /*@desc "the occupied TTDs" */, occ /*@desc "the occupied TTDs" */,
train_rear_end /*@desc "the minimal (aka left) position of a train" */, 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_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 INVARIANT
occ <: TTDS & occ <: TTDS /*@desc "occ is a set of TTDs" */ &
train_rear_end : TRAINS --> TRACK & train_rear_end : TRAINS --> TRACK &
train_front_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: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" */ & !tr.(tr:TRAINS => train_front_end(tr) >= train_rear_end(tr)) /*@desc "train positions on track not empty" */ &
!(t1,t2).(t1:TRAINS & t2 /= t1 => train_occ(t1) /\ train_occ(t2) = {}) /*@desc "no collision" */ & /*@label "SAF-1" */ !(t1,t2).(t1:TRAINS & t2 /= t1
!(t1,t2).(t1:TRAINS & t2 /= t1 => train_reserved(t1) /\ train_reserved(t2) = {}) /*@desc "reserved areas disjoint" */ ASSERTIONS => 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 !(ttd,tr).(ttd /: occ & tr:TRAINS
=> train_occ(tr) /\ TTD_TrackElements(ttd) = {}) /*@desc "TTDs marked as free are really free" */ => train_occ(tr) /\ TTD_TrackElements(ttd) = {}) /*@desc "TTDs marked as free are really free" */
INITIALISATION INITIALISATION
...@@ -39,11 +45,13 @@ OPERATIONS ...@@ -39,11 +45,13 @@ OPERATIONS
TrainAcceptsFirstMA(tr,newMA) = PRE tr/:dom(train_ma) & newMA:TRACK & newMA > train_front_end(tr) & 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 !(t2).(t2 /= tr => train_rear_end(tr)..newMA /\ train_reserved(t2) = {}) /*@desc "MA is safe" */ THEN
train_ma(tr) := newMA train_ma(tr) := newMA
END; END;
TrainAcceptsNewMA(tr,newMA) = PRE tr:dom(train_ma) & newMA:TRACK & newMA > train_ma(tr) & 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" */ !(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 // TODO: use TTD info !(ttd).(ttd:occ => train_ma(tr)..newMA
THEN THEN
......
Train/TwoTrainsMA_Unicode.mch
+ 8
− 15
View file @ c143df5b
MACHINE TwoTrainsMA MACHINE TwoTrainsMA_Unicode
// A small example to show how one can use LibrarySVG to flexibliy visualise // A small example to show how one can use LibrarySVG to flexibliy visualise
// train track zones and MAs; // 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 // unicode and corrected version of model that contains some errors on purpose to show how visualisation can help spot them
SETS SETS
TTDS = {ttd1,ttd2,ttd3,ttd4}; TTDS = {ttd1,ttd2,ttd3,ttd4} /*@desc "Trackside Track Detection zones" */;
TRAINS = {tr1,tr2} TRAINS = {tr1,tr2} /*@desc "The set of trains" */
CONSTANTS 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 PROPERTIES
TrackElementNumber ∈ NATURAL1 TrackElementNumber ∈ NATURAL1
∧ TRACK = 0..TrackElementNumber ∧ TRACK = 0..TrackElementNumber
...@@ -23,7 +25,7 @@ VARIABLES ...@@ -23,7 +25,7 @@ VARIABLES
train_front_end /*@desc "the maximal (aka right) 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 train" */
INVARIANT INVARIANT
occ ⊆ TTDS ∧ occ ⊆ TTDS /*@desc "occ is a set of TTDs" */ ∧
train_rear_end ∈ TRAINS → TRACK ∧ train_rear_end ∈ TRAINS → TRACK ∧
train_front_end ∈ TRAINS → TRACK ∧ train_front_end ∈ TRAINS → TRACK ∧
train_ma ∈ TRAINS ⇸ TRACK ∧ train_ma ∈ TRAINS ⇸ TRACK ∧
...@@ -72,12 +74,3 @@ DEFINITIONS ...@@ -72,12 +74,3 @@ DEFINITIONS
train_length(train) == 1+train_front_end(train)-train_rear_end(train); train_length(train) == 1+train_front_end(train)-train_rear_end(train);
VISB_JSON_FILE == "TwoTrainsMA.json" VISB_JSON_FILE == "TwoTrainsMA.json"
END END
\ No newline at end of file
/*
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
VisB-Examples.prob2project
+ 13
− 1
View file @ c143df5b
...@@ -438,6 +438,18 @@ ...@@ -438,6 +438,18 @@
}, },
"goal": "-", "goal": "-",
"shouldExecute": true "shouldExecute": true
},
{
"nodesLimit": "-",
"timeLimit": "-",
"options": {
"options": [
"FIND_INVARIANT_VIOLATIONS",
"INSPECT_EXISTING_NODES"
]
},
"goal": "-",
"shouldExecute": true
} }
], ],
"simulation": null, "simulation": null,
...@@ -466,7 +478,7 @@ ...@@ -466,7 +478,7 @@
"metadata": { "metadata": {
"fileType": "Project", "fileType": "Project",
"formatVersion": 12, "formatVersion": 12,
"savedAt": "2021-05-06T12:36:10.371287Z", "savedAt": "2021-05-06T13:17:55.964399Z",
"creator": "User", "creator": "User",
"proB2KernelVersion": "4.0.0-SNAPSHOT", "proB2KernelVersion": "4.0.0-SNAPSHOT",
"proBCliVersion": null, "proBCliVersion": null,
......
traces/TwoTrainsMA.prob2trace
+ 7
− 31
View file @ c143df5b
...@@ -6,9 +6,6 @@ ...@@ -6,9 +6,6 @@
"params": {}, "params": {},
"results": {}, "results": {},
"destState": { "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": [], "destStateNotChanged": [],
"preds": [] "preds": []
...@@ -18,10 +15,6 @@ ...@@ -18,10 +15,6 @@
"params": {}, "params": {},
"results": {}, "results": {},
"destState": { "destState": {
"train_rear_end": "{(tr1↦0),(tr2↦5)}",
"train_front_end": "{(tr1↦2),(tr2↦6)}",
"train_ma": "∅",
"occ": "{ttd1,ttd2}"
}, },
"destStateNotChanged": [], "destStateNotChanged": [],
"preds": [] "preds": []
...@@ -29,12 +22,12 @@ ...@@ -29,12 +22,12 @@
{ {
"name": "TrainAcceptsFirstMA", "name": "TrainAcceptsFirstMA",
"params": { "params": {
"newMA": "14", "newMA": "15",
"tr": "tr2" "tr": "tr2"
}, },
"results": {}, "results": {},
"destState": { "destState": {
"train_ma": "{(tr2↦14)}" "train_ma": "{(tr2↦15)}"
}, },
"destStateNotChanged": [ "destStateNotChanged": [
"train_front_end", "train_front_end",
...@@ -80,12 +73,12 @@ ...@@ -80,12 +73,12 @@
{ {
"name": "TrainAcceptsFirstMA", "name": "TrainAcceptsFirstMA",
"params": { "params": {
"newMA": "4", "newMA": "5",
"tr": "tr1" "tr": "tr1"
}, },
"results": {}, "results": {},
"destState": { "destState": {
"train_ma": "{(tr1↦4),(tr2↦14)}" "train_ma": "{(tr1↦5),(tr2↦15)}"
}, },
"destStateNotChanged": [ "destStateNotChanged": [
"train_front_end", "train_front_end",
...@@ -204,7 +197,7 @@ ...@@ -204,7 +197,7 @@
}, },
"results": {}, "results": {},
"destState": { "destState": {
"train_ma": "{(tr1↦10),(tr2↦14)}" "train_ma": "{(tr1↦10),(tr2↦15)}"
}, },
"destStateNotChanged": [ "destStateNotChanged": [
"train_front_end", "train_front_end",
...@@ -250,12 +243,12 @@ ...@@ -250,12 +243,12 @@
{ {
"name": "TrainAcceptsNewMA", "name": "TrainAcceptsNewMA",
"params": { "params": {
"newMA": "23", "newMA": "25",
"tr": "tr2" "tr": "tr2"
}, },
"results": {}, "results": {},
"destState": { "destState": {
"train_ma": "{(tr1↦10),(tr2↦23)}" "train_ma": "{(tr1↦10),(tr2↦25)}"
}, },
"destStateNotChanged": [ "destStateNotChanged": [
"train_front_end", "train_front_end",
...@@ -400,23 +393,6 @@ ...@@ -400,23 +393,6 @@
], ],
"preds": [] "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", "name": "TrainMoveForward",
"params": { "params": {
......
traces/TwoTrainsMA_30.prob2trace 0 → 100644
+ 651
− 0
View file @ c143df5b
{
"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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment