Select Git revision
train_4_POR_mch.prob2trace
Code owners
Assign users and groups as approvers for specific file changes. Learn more.
train_4_POR_mch.prob2trace 16.45 KiB
{
"description": "File created by ProB Tcl/Tk",
"transitionList": [
{
"name": "$setup_constants",
"destState": {
"rtbl": "{(A|->R1),(A|->R2),(A|->R3),(A|->R6),(A|->R7),(A|->R8),(B|->R1),(B|->R2),(B|->R3),(B|->R6),(B|->R7),(B|->R8),(C|->R1),(C|->R6),(D|->R2),(D|->R3),(D|->R7),(D|->R8),(E|->R2),(E|->R7),(F|->R2),(F|->R4),(F|->R7),(F|->R9),(G|->R2),(G|->R4),(G|->R7),(G|->R9),(H|->R4),(H|->R5),(H|->R9),(H|->R10),(I|->R4),(I|->R5),(I|->R9),(I|->R10),(J|->R3),(J|->R5),(J|->R8),(J|->R10),(K|->R3),(K|->R4),(K|->R8),(K|->R9),(L|->R1),(L|->R2),(L|->R3),(L|->R6),(L|->R7),(L|->R8),(M|->R4),(M|->R5),(M|->R9),(M|->R10),(N|->R3),(N|->R5),(N|->R8),(N|->R10)}",
"lst": "{(R1|->C),(R2|->G),(R3|->N),(R4|->G),(R5|->N),(R6|->L),(R7|->L),(R8|->L),(R9|->M),(R10|->M)}",
"nxt": "{(R1|->{(A|->B),(B|->C),(L|->A)}),(R2|->{(A|->B),(B|->D),(D|->E),(E|->F),(F|->G),(L|->A)}),(R3|->{(A|->B),(B|->D),(D|->K),(J|->N),(K|->J),(L|->A)}),(R4|->{(F|->G),(H|->I),(I|->K),(K|->F),(M|->H)}),(R5|->{(H|->I),(I|->J),(J|->N),(M|->H)}),(R6|->{(A|->L),(B|->A),(C|->B)}),(R7|->{(A|->L),(B|->A),(D|->B),(E|->D),(F|->E),(G|->F)}),(R8|->{(A|->L),(B|->A),(D|->B),(J|->K),(K|->D),(N|->J)}),(R9|->{(F|->K),(G|->F),(H|->M),(I|->H),(K|->I)}),(R10|->{(H|->M),(I|->H),(J|->I),(N|->J)})}",
"fst": "{(R1|->L),(R2|->L),(R3|->L),(R4|->M),(R5|->M),(R6|->C),(R7|->G),(R8|->N),(R9|->G),(R10|->N)}",
"SIG": "{(C|->S4),(G|->S5),(L|->S1),(M|->S2),(N|->S3)}",
"rht": "{(B|->A),(D|->A),(F|->A),(I|->A),(J|->A)}",
"lft": "{(B|->B),(D|->B),(F|->B),(I|->B),(J|->B)}",
"blpt": "{B,D,F,I,J}"
},
"destStateNotChanged": [
]
},
{
"name": "$initialise_machine",
"destState": {
"GRN": "{}",
"LBT": "{}",
"OCC": "{}",
"TRK": "{}",
"frm": "{}",
"rdy": "{}",
"resbl": "{}",
"resrt": "{}",
"rsrtbl": "{}"
},
"destStateNotChanged": [
]
},
{
"name": "route_reservation",
"params": {
"r": "R9"
},
"destState": {
"resbl": "{F,G,H,I,K,M}",
"resrt": "{R9}",
"rsrtbl": "{(F|->R9),(G|->R9),(H|->R9),(I|->R9),(K|->R9),(M|->R9)}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"TRK",
"frm",
"rdy"
]
},
{
"name": "point_positionning",
"params": {
"r": "R9"
},
"destState": {
"TRK": "{(F|->K),(G|->F),(H|->M),(I|->H),(K|->I)}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl" ]
},
{
"name": "route_reservation",
"params": {
"r": "R1"
},
"destState": {
"resbl": "{A,B,C,F,G,H,I,K,L,M}",
"resrt": "{R1,R9}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(F|->R9),(G|->R9),(H|->R9),(I|->R9),(K|->R9),(L|->R1),(M|->R9)}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"TRK",
"frm",
"rdy"
]
},
{
"name": "route_formation",
"params": {
"r": "R9"
},
"destState": {
"GRN": "{S5}",
"frm": "{R9}",
"rdy": "{R9}"
},
"destStateNotChanged": [
"LBT",
"OCC",
"TRK",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_1",
"params": {
"b": "G"
},
"destState": {
"GRN": "{}",
"LBT": "{G}",
"OCC": "{G}",
"rdy": "{}"
},
"destStateNotChanged": [
"TRK",
"frm",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "G"
},
"destState": {
"OCC": "{F,G}"
},
"destStateNotChanged": [
"GRN",
"LBT", "TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "G"
},
"destState": {
"LBT": "{F}",
"OCC": "{F}",
"resbl": "{A,B,C,F,H,I,K,L,M}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(F|->R9),(H|->R9),(I|->R9),(K|->R9),(L|->R1),(M|->R9)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "F"
},
"destState": {
"OCC": "{F,K}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "F"
},
"destState": {
"LBT": "{K}",
"OCC": "{K}",
"resbl": "{A,B,C,H,I,K,L,M}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(H|->R9),(I|->R9),(K|->R9),(L|->R1),(M|->R9)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "point_positionning",
"params": {
"r": "R1"
}, "destState": {
"TRK": "{(A|->B),(B|->C),(F|->K),(G|->F),(H|->M),(I|->H),(K|->I),(L|->A)}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "K"
},
"destState": {
"OCC": "{I,K}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "K"
},
"destState": {
"LBT": "{I}",
"OCC": "{I}",
"resbl": "{A,B,C,H,I,L,M}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(H|->R9),(I|->R9),(L|->R1),(M|->R9)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "I"
},
"destState": {
"OCC": "{H,I}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
] },
{
"name": "BACK_MOVE_2",
"params": {
"b": "I"
},
"destState": {
"LBT": "{H}",
"OCC": "{H}",
"resbl": "{A,B,C,H,L,M}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(H|->R9),(L|->R1),(M|->R9)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "H"
},
"destState": {
"OCC": "{H,M}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "H"
},
"destState": {
"LBT": "{M}",
"OCC": "{M}",
"resbl": "{A,B,C,L,M}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(L|->R1),(M|->R9)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "BACK_MOVE_1",
"params": {
"b": "M"
},
"destState": {
"LBT": "{}",
"OCC": "{}",
"resbl": "{A,B,C,L}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(L|->R1)}"
},
"destStateNotChanged": [ "GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "route_freeing",
"params": {
"r": "R9"
},
"destState": {
"frm": "{}",
"resrt": "{R1}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"TRK",
"rdy",
"resbl",
"rsrtbl"
]
},
{
"name": "route_reservation",
"params": {
"r": "R4"
},
"destState": {
"resbl": "{A,B,C,F,G,H,I,K,L,M}",
"resrt": "{R1,R4}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(F|->R4),(G|->R4),(H|->R4),(I|->R4),(K|->R4),(L|->R1),(M|->R4)}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"TRK",
"frm",
"rdy"
]
},
{
"name": "route_formation",
"params": {
"r": "R1"
},
"destState": {
"GRN": "{S1}",
"frm": "{R1}",
"rdy": "{R1}"
},
"destStateNotChanged": [
"LBT",
"OCC",
"TRK",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_1",
"params": {
"b": "L"
},
"destState": { "GRN": "{}",
"LBT": "{L}",
"OCC": "{L}",
"rdy": "{}"
},
"destStateNotChanged": [
"TRK",
"frm",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "L"
},
"destState": {
"OCC": "{A,L}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "point_positionning",
"params": {
"r": "R4"
},
"destState": {
"TRK": "{(A|->B),(B|->C),(F|->G),(H|->I),(I|->K),(K|->F),(L|->A),(M|->H)}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "A"
},
"destState": {
"OCC": "{A,B,L}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
}, {
"name": "FRONT_MOVE_2",
"params": {
"b": "B"
},
"destState": {
"OCC": "{A,B,C,L}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "L"
},
"destState": {
"LBT": "{A}",
"OCC": "{A,B,C}",
"resbl": "{A,B,C,F,G,H,I,K,M}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(F|->R4),(G|->R4),(H|->R4),(I|->R4),(K|->R4),(M|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "A"
},
"destState": {
"LBT": "{B}",
"OCC": "{B,C}",
"resbl": "{B,C,F,G,H,I,K,M}",
"rsrtbl": "{(B|->R1),(C|->R1),(F|->R4),(G|->R4),(H|->R4),(I|->R4),(K|->R4),(M|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "route_formation",
"params": {
"r": "R4"
},
"destState": {
"GRN": "{S2}",
"frm": "{R1,R4}",
"rdy": "{R4}"
},
"destStateNotChanged": [
"LBT",
"OCC", "TRK",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_1",
"params": {
"b": "M"
},
"destState": {
"GRN": "{}",
"LBT": "{B,M}",
"OCC": "{B,C,M}",
"rdy": "{}"
},
"destStateNotChanged": [
"TRK",
"frm",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "M"
},
"destState": {
"OCC": "{B,C,H,M}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "B"
},
"destState": {
"LBT": "{C,M}",
"OCC": "{C,H,M}",
"resbl": "{C,F,G,H,I,K,M}",
"rsrtbl": "{(C|->R1),(F|->R4),(G|->R4),(H|->R4),(I|->R4),(K|->R4),(M|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "BACK_MOVE_1",
"params": {
"b": "C"
},
"destState": {
"LBT": "{M}", "OCC": "{H,M}",
"resbl": "{F,G,H,I,K,M}",
"rsrtbl": "{(F|->R4),(G|->R4),(H|->R4),(I|->R4),(K|->R4),(M|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "route_freeing",
"params": {
"r": "R1"
},
"destState": {
"frm": "{R4}",
"resrt": "{R4}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"TRK",
"rdy",
"resbl",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "H"
},
"destState": {
"OCC": "{H,I,M}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "M"
},
"destState": {
"LBT": "{H}",
"OCC": "{H,I}",
"resbl": "{F,G,H,I,K}",
"rsrtbl": "{(F|->R4),(G|->R4),(H|->R4),(I|->R4),(K|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{ "name": "BACK_MOVE_2",
"params": {
"b": "H"
},
"destState": {
"LBT": "{I}",
"OCC": "{I}",
"resbl": "{F,G,I,K}",
"rsrtbl": "{(F|->R4),(G|->R4),(I|->R4),(K|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "I"
},
"destState": {
"OCC": "{I,K}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "I"
},
"destState": {
"LBT": "{K}",
"OCC": "{K}",
"resbl": "{F,G,K}",
"rsrtbl": "{(F|->R4),(G|->R4),(K|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "K"
},
"destState": {
"OCC": "{F,K}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy", "resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "K"
},
"destState": {
"LBT": "{F}",
"OCC": "{F}",
"resbl": "{F,G}",
"rsrtbl": "{(F|->R4),(G|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "F"
},
"destState": {
"OCC": "{F,G}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "F"
},
"destState": {
"LBT": "{G}",
"OCC": "{G}",
"resbl": "{G}",
"rsrtbl": "{(G|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "BACK_MOVE_1",
"params": {
"b": "G"
},
"destState": {
"LBT": "{}",
"OCC": "{}", "resbl": "{}",
"rsrtbl": "{}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "route_freeing",
"params": {
"r": "R4"
},
"destState": {
"frm": "{}",
"resrt": "{}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"TRK",
"rdy",
"resbl",
"rsrtbl"
]
}
],
"metadata": {
"fileType": "Trace",
"formatVersion": 1,
"savedAt": "2022-05-25T17:18:52Z",
"creator": "tcltk (leuschel)",
"proBCliVersion": "1.12.0-nightly",
"proBCliRevision": "94b13de9d6fba932404838299859bea55586e8aa",
"modelName": "train_4_POR",
"modelFile": "/Users/leuschel/git_root/JAVAPROB/visb-visualisation-examples/Train_B_Book/train_4_POR_mch.eventb"
}
}