Select Git revision
sysBiolAlgClass.R
Code owners
Assign users and groups as approvers for specific file changes. Learn more.
TwoTrainsMA.prob2trace 14.10 KiB
{
"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"
}
}