Select Git revision
TwoTrains.prob2trace
-
Michael Leuschel authoredMichael Leuschel authored
Code owners
Assign users and groups as approvers for specific file changes. Learn more.
TwoTrains.prob2trace 14.36 KiB
{
"description": "",
"transitionList": [
{
"name": "$setup_constants",
"params": {},
"results": {},
"destState": {
"TTD_TrackElements": "{(ttd1↦{0,1,2,3,4,5,6,7,8,9,10}),(ttd2↦{11,12,13,14,15,16,17,18,19,20,21,22,23,24,25}),(ttd3↦{26,27,28,29,30})}",
"TrackElementNumber": "30",
"train_length": "{(tr1↦3),(tr2↦2)}",
"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↦4)}",
"occ": "∅"
},
"destStateNotChanged": [],
"preds": []
},
{
"name": "TTD_Occupied_By_Train",
"params": {
"ttd": "ttd1",
"tr": "tr1"
},
"results": {},
"destState": {
"occ": "{ttd1}"
},
"destStateNotChanged": [
"train_rear_end"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr1"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦1),(tr2↦4)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦1),(tr2↦5)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
}, {
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦1),(tr2↦6)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦1),(tr2↦7)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦1),(tr2↦8)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦1),(tr2↦9)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦1),(tr2↦10)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
}, {
"name": "TTD_Occupied_By_Train",
"params": {
"ttd": "ttd2",
"tr": "tr2"
},
"results": {},
"destState": {
"occ": "{ttd1,ttd2}"
},
"destStateNotChanged": [
"train_rear_end"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦1),(tr2↦11)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦1),(tr2↦12)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr1"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦2),(tr2↦12)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr1"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦3),(tr2↦12)}"
},
"destStateNotChanged": [
"occ"
],
"preds": [] },
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦3),(tr2↦13)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦3),(tr2↦14)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦3),(tr2↦15)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦3),(tr2↦16)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦3),(tr2↦17)}"
},
"destStateNotChanged": [
"occ"
],
"preds": [] },
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦3),(tr2↦18)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦3),(tr2↦19)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦3),(tr2↦20)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦3),(tr2↦21)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦3),(tr2↦22)}"
},
"destStateNotChanged": [
"occ"
],
"preds": [] },
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦3),(tr2↦23)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦3),(tr2↦24)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦3),(tr2↦25)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TTD_Occupied_By_Train",
"params": {
"ttd": "ttd3",
"tr": "tr2"
},
"results": {},
"destState": {
"occ": "{ttd1,ttd2,ttd3}"
},
"destStateNotChanged": [
"train_rear_end"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦3),(tr2↦26)}"
},
"destStateNotChanged": [
"occ"
], "preds": []
},
{
"name": "TTD_Free",
"params": {
"ttd": "ttd2"
},
"results": {},
"destState": {
"occ": "{ttd1,ttd3}"
},
"destStateNotChanged": [
"train_rear_end"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr1"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦4),(tr2↦26)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr1"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦5),(tr2↦26)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr1"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦6),(tr2↦26)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr1"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦7),(tr2↦26)}"
},
"destStateNotChanged": [
"occ"
], "preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr1"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦8),(tr2↦26)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr1"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦9),(tr2↦26)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TTD_Occupied_By_Train",
"params": {
"ttd": "ttd2",
"tr": "tr1"
},
"results": {},
"destState": {
"occ": "{ttd1,ttd2,ttd3}"
},
"destStateNotChanged": [
"train_rear_end"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr1"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦10),(tr2↦26)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦10),(tr2↦27)}"
},
"destStateNotChanged": [
"occ" ],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr2"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦10),(tr2↦28)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr1"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦11),(tr2↦28)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TTD_Free",
"params": {
"ttd": "ttd1"
},
"results": {},
"destState": {
"occ": "{ttd2,ttd3}"
},
"destStateNotChanged": [
"train_rear_end"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr1"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦12),(tr2↦28)}"
},
"destStateNotChanged": [
"occ"
],
"preds": []
},
{
"name": "TrainMoveForward",
"params": {
"tr": "tr1"
},
"results": {},
"destState": {
"train_rear_end": "{(tr1↦13),(tr2↦28)}"
},
"destStateNotChanged": [
"occ" ],
"preds": []
}
],
"variableNames": [
"occ",
"train_rear_end"
],
"constantNames": [
"TrackElementNumber",
"TRACK",
"TTD_TrackElements",
"train_length"
],
"setNames": [
"TTDS",
"TRAINS"
],
"machineOperationInfos": {
"TrainMoveForward": {
"operationName": "TrainMoveForward",
"parameterNames": [
"tr"
],
"outputParameterNames": [],
"topLevel": true,
"type": "CLASSICAL_B",
"readVariables": [
"TRACK",
"train_rear_end"
],
"writtenVariables": [
"train_rear_end"
],
"nonDetWrittenVariables": [],
"typeMap": {
"tr": "global('TRAINS')",
"'TRACK'": "set(integer)"
}
},
"TTD_Free": {
"operationName": "TTD_Free",
"parameterNames": [
"ttd"
],
"outputParameterNames": [],
"topLevel": true,
"type": "CLASSICAL_B",
"readVariables": [
"TTD_TrackElements",
"occ",
"train_length",
"train_rear_end"
],
"writtenVariables": [
"occ"
],
"nonDetWrittenVariables": [],
"typeMap": {
"'TTD_TrackElements'": "set(couple(global('TTDS'),set(integer)))",
"ttd": "global('TTDS')"
}
},
"TTD_Occupied_By_Train": {
"operationName": "TTD_Occupied_By_Train",
"parameterNames": [
"ttd",
"tr"
],
"outputParameterNames": [], "topLevel": true,
"type": "CLASSICAL_B",
"readVariables": [
"TTD_TrackElements",
"occ",
"train_length",
"train_rear_end"
],
"writtenVariables": [
"occ"
],
"nonDetWrittenVariables": [],
"typeMap": {
"'TTD_TrackElements'": "set(couple(global('TTDS'),set(integer)))",
"ttd": "global('TTDS')",
"tr": "global('TRAINS')"
}
}
},
"globalIdentifierTypes": {
"train_length": "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-04T16:44:16.543509Z",
"creator": "traceReplay",
"proB2KernelVersion": "4.0.0-SNAPSHOT",
"proBCliVersion": "1.11.0-nightly",
"modelName": "TwoTrains"
}
}