{
  "description": "File created by ProB Tcl/Tk",
  "transitionList": [
    {
      "name": "$partial_setup_constants",
      "destState": {
        "A": "2.0",
        "b": "1.0",
        "e": "2.0",
        "sl": "5.0"
      }
    },
    {
      "name": "$initialise_machine",
      "destState": {
        "a": "2.0",
        "a2": "0.0",
        "m": "0.0",
        "phase": "1",
        "phase2": "1",
        "v": "0.0",
        "v2": "0.0",
        "z": "0.0",
        "z2": "0.0"
      }
    },
    {
      "name": "get_limit",
      "params": {
        "x": "30"
      },
      "destState": {
        "m": "30.0"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "phase",
        "phase2",
        "v",
        "v2",
        "z",
        "z2"
      ]
    },
    {
      "name": "decide_2",
      "destState": {
        "phase": "2"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase2",
        "v",
        "v2",
        "z",
        "z2"
      ]
    },
    {
      "name": "drive_2",
      "destState": {
        "phase": "1",
        "v": "4.0",
        "z": "4.0"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase2",
        "v2",
        "z2"
      ]
    },
    {
      "name": "decide_1",
      "destState": {
        "a": "-1.0",
        "phase": "2"
      },
      "destStateNotChanged": [
        "a2",
        "m",
        "phase2",
        "v",
        "v2",
        "z",
        "z2"
      ]
    },
    {
      "name": "drive_2",
      "destState": {
        "phase": "1",
        "v": "2.0",
        "z": "10.0"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase2",
        "v2",
        "z2"
      ]
    },
    {
      "name": "decide_1",
      "destState": {
        "phase": "2"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase2",
        "v",
        "v2",
        "z",
        "z2"
      ]
    },
    {
      "name": "drive_1",
      "destState": {
        "phase": "1",
        "v": "0.0",
        "z": "12.0"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase2",
        "v2",
        "z2"
      ]
    },
    {
      "name": "decide_2_2",
      "destState": {
        "a2": "2.0",
        "phase2": "2"
      },
      "destStateNotChanged": [
        "a",
        "m",
        "phase",
        "v",
        "v2",
        "z",
        "z2"
      ]
    },
    {
      "name": "drive_2_2",
      "destState": {
        "phase2": "1",
        "v2": "4.0",
        "z2": "4.0"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase",
        "v",
        "z"
      ]
    },
    {
      "name": "decide_2",
      "destState": {
        "a": "2.0",
        "phase": "2"
      },
      "destStateNotChanged": [
        "a2",
        "m",
        "phase2",
        "v",
        "v2",
        "z",
        "z2"
      ]
    },
    {
      "name": "drive_2",
      "destState": {
        "phase": "1",
        "v": "4.0",
        "z": "16.0"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase2",
        "v2",
        "z2"
      ]
    },
    {
      "name": "decide_1_2",
      "destState": {
        "a2": "-1.0",
        "phase2": "2"
      },
      "destStateNotChanged": [
        "a",
        "m",
        "phase",
        "v",
        "v2",
        "z",
        "z2"
      ]
    },
    {
      "name": "drive_2_2",
      "destState": {
        "phase2": "1",
        "v2": "2.0",
        "z2": "10.0"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase",
        "v",
        "z"
      ]
    },
    {
      "name": "decide_1",
      "destState": {
        "a": "-1.0",
        "phase": "2"
      },
      "destStateNotChanged": [
        "a2",
        "m",
        "phase2",
        "v",
        "v2",
        "z",
        "z2"
      ]
    },
    {
      "name": "decide_1_2",
      "destState": {
        "phase2": "2"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase",
        "v",
        "v2",
        "z",
        "z2"
      ]
    },
    {
      "name": "drive_1_2",
      "destState": {
        "phase2": "1",
        "v2": "0.0",
        "z2": "12.0"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase",
        "v",
        "z"
      ]
    },
    {
      "name": "drive_2",
      "destState": {
        "phase": "1",
        "v": "2.0",
        "z": "22.0"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase2",
        "v2",
        "z2"
      ]
    },
    {
      "name": "decide_1",
      "destState": {
        "phase": "2"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase2",
        "v",
        "v2",
        "z",
        "z2"
      ]
    },
    {
      "name": "drive_1",
      "destState": {
        "phase": "1",
        "v": "0.0",
        "z": "24.0"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase2",
        "v2",
        "z2"
      ]
    },
    {
      "name": "decide_2_2",
      "destState": {
        "a2": "2.0",
        "phase2": "2"
      },
      "destStateNotChanged": [
        "a",
        "m",
        "phase",
        "v",
        "v2",
        "z",
        "z2"
      ]
    },
    {
      "name": "drive_2_2",
      "destState": {
        "phase2": "1",
        "v2": "4.0",
        "z2": "16.0"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase",
        "v",
        "z"
      ]
    },
    {
      "name": "decide_1_2",
      "destState": {
        "a2": "-1.0",
        "phase2": "2"
      },
      "destStateNotChanged": [
        "a",
        "m",
        "phase",
        "v",
        "v2",
        "z",
        "z2"
      ]
    },
    {
      "name": "drive_2_2",
      "destState": {
        "phase2": "1",
        "v2": "2.0",
        "z2": "22.0"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase",
        "v",
        "z"
      ]
    },
    {
      "name": "decide_1_2",
      "destState": {
        "phase2": "2"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase",
        "v",
        "v2",
        "z",
        "z2"
      ]
    },
    {
      "name": "drive_1_2",
      "destState": {
        "phase2": "1",
        "v2": "0.0",
        "z2": "24.0"
      },
      "destStateNotChanged": [
        "a",
        "a2",
        "m",
        "phase",
        "v",
        "z"
      ]
    }
  ],
  "metadata": {
    "fileType": "Trace",
    "formatVersion": 1,
    "savedAt": "2026-06-25T12:37:45Z",
    "creator": "tcltk (leuschel)",
    "proBCliVersion": "1.16.0-nightly",
    "proBCliRevision": "f5e3035df36490b9e95d76c5145f34f0b4ff78e1",
    "modelName": "T_m1_prob_real",
    "modelFile": "/Users/leuschel/git_root/prob_examples/public_examples/EventBPrologPackages/Abrial_Hybrid/hybrid_train/T_m1_prob_real.mch"
  }
}