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