{
  "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"
  }
}