{
  "name": "VisB-Examples",
  "description": "",
  "machines": [
    {
      "name": "button",
      "description": "",
      "location": "Button/button.mch",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [
        {
          "type": "INVARIANT",
          "code": "",
          "selected": true
        },
        {
          "type": "SYMBOLIC_MODEL_CHECK",
          "code": "BMC",
          "selected": true
        }
      ],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Button/button.json",
      "historyChartItems": []
    },
    {
      "name": "QueensWithEvents",
      "description": "",
      "location": "N-Queens/QueensWithEvents.mch",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [
        {
          "type": "SYMBOLIC_MODEL_CHECK",
          "code": "BMC",
          "selected": true
        },
        {
          "type": "INVARIANT",
          "code": "",
          "selected": true
        },
        {
          "type": "INVARIANT",
          "code": "SetQueen",
          "selected": true
        }
      ],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [
        "traces/QueensWithEvents.prob2trace"
      ],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "N-Queens/queens_8.json",
      "historyChartItems": []
    },
    {
      "name": "Grapher",
      "description": "",
      "location": "Reals/Grapher.mch",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Reals/Grapher.json",
      "historyChartItems": []
    },
    {
      "name": "MovingParticles3",
      "description": "",
      "location": "Physics/MovingParticles3.mch",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [
        "traces/MovingParticles3.prob2trace",
        "traces/MovingParticles.prob2trace"
      ],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Physics/three_bodies.json",
      "historyChartItems": []
    },
    {
      "name": "MovingParticles4",
      "description": "",
      "location": "Physics/MovingParticles4.mch",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Physics/n_bodies_visb.json",
      "historyChartItems": []
    },
    {
      "name": "WasserkocherEinfach_mch",
      "description": "",
      "location": "Waterboiler/WasserkocherEinfach_mch.eventb",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [
        {
          "nodesLimit": "-",
          "timeLimit": "-",
          "options": {
            "options": [
              "FIND_INVARIANT_VIOLATIONS",
              "INSPECT_EXISTING_NODES"
            ]
          },
          "goal": "-",
          "shouldExecute": true
        }
      ],
      "simulation": null,
      "visBVisualisation": "Waterboiler/visb_wasserkocher.json",
      "historyChartItems": []
    },
    {
      "name": "WasserKocherFalsch1_mch",
      "description": "",
      "location": "Waterboiler/WasserKocherFalsch1_mch.eventb",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Waterboiler/visb_wasserkocher.json",
      "historyChartItems": []
    },
    {
      "name": "WasserkocherFalsch2_mch",
      "description": "",
      "location": "Waterboiler/WasserkocherFalsch2_mch.eventb",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Waterboiler/visb_wasserkocher.json",
      "historyChartItems": []
    },
    {
      "name": "m0_island_bridge_3cars_mch",
      "description": "",
      "location": "Bridge/m0_island_bridge_3cars_mch.eventb",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Bridge/visb_m0.json",
      "historyChartItems": []
    },
    {
      "name": "m1_bridge_mch",
      "description": "",
      "location": "Bridge/m1_bridge_mch.eventb",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Bridge/visb_m1.json",
      "historyChartItems": []
    },
    {
      "name": "Lift",
      "description": "",
      "location": "Lift/Lift.mch",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Lift/lift_groups.json",
      "historyChartItems": []
    },
    {
      "name": "SimpleTrainTrack",
      "description": "",
      "location": "Train/SimpleTrainTrack.mch",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [
        "traces/SimpleTrainTrack.prob2trace"
      ],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Train/Track.json",
      "historyChartItems": []
    },
    {
      "name": "TrafficLight",
      "description": "",
      "location": "TrafficLight/TrafficLight.mch",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "TrafficLight/traffic_light.json",
      "historyChartItems": []
    },
    {
      "name": "button (1)",
      "description": "",
      "location": "Button/Z/button.tex",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Button/Z/button.json",
      "historyChartItems": []
    },
    {
      "name": "button (2)",
      "description": "",
      "location": "Button/TLA/button.tla",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Button/TLA/button.json",
      "historyChartItems": []
    },
    {
      "name": "einsteins_puzzle",
      "description": "",
      "location": "Einstein/einsteins_puzzle.als",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [
        {
          "type": "SEQUENCE",
          "code": "run0",
          "selected": true
        }
      ],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Einstein/einstein_puzzle_als.json",
      "historyChartItems": []
    },
    {
      "name": "Einstein",
      "description": "",
      "location": "Einstein/Einstein.tla",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [
        {
          "type": "INVARIANT",
          "code": "",
          "selected": true
        }
      ],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Einstein/Einstein_tla.json",
      "historyChartItems": []
    },
    {
      "name": "einsteins_enum",
      "description": "",
      "location": "Einstein/einsteins_enum.als",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": null,
      "historyChartItems": []
    },
    {
      "name": "TwoTrains",
      "description": "",
      "location": "Train/TwoTrains.mch",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [
        "traces/TwoTrains.prob2trace"
      ],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Train/TwoTrains.json",
      "historyChartItems": []
    },
    {
      "name": "TwoTrainsB",
      "description": "",
      "location": "Train/TwoTrainsB.mch",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [
        {
          "nodesLimit": "-",
          "timeLimit": "-",
          "options": {
            "options": [
              "FIND_DEADLOCKS",
              "FIND_INVARIANT_VIOLATIONS",
              "INSPECT_EXISTING_NODES"
            ]
          },
          "goal": "-",
          "shouldExecute": true
        }
      ],
      "simulation": null,
      "visBVisualisation": "Train/TwoTrains.json",
      "historyChartItems": []
    },
    {
      "name": "TwoTrainsMA",
      "description": "",
      "location": "Train/TwoTrainsMA.mch",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [
        "traces/TwoTrainsMA.prob2trace"
      ],
      "modelcheckingItems": [
        {
          "nodesLimit": "-",
          "timeLimit": "-",
          "options": {
            "options": [
              "FIND_DEADLOCKS",
              "FIND_INVARIANT_VIOLATIONS",
              "INSPECT_EXISTING_NODES"
            ]
          },
          "goal": "-",
          "shouldExecute": true
        },
        {
          "nodesLimit": "-",
          "timeLimit": "-",
          "options": {
            "options": [
              "FIND_INVARIANT_VIOLATIONS",
              "INSPECT_EXISTING_NODES"
            ]
          },
          "goal": "-",
          "shouldExecute": true
        }
      ],
      "simulation": null,
      "visBVisualisation": "Train/TwoTrainsMA.json",
      "historyChartItems": []
    },
    {
      "name": "TwoTrainsMA_Unicode",
      "description": "",
      "location": "Train/TwoTrainsMA_Unicode.mch",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [
        "traces/TwoTrainsMA.prob2trace"
      ],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Train/TwoTrainsMA.json",
      "historyChartItems": []
    },
    {
      "name": "R6GearsDoorsHandleValvesControllerSwitch",
      "description": "",
      "location": "LandingGear/model/R6GearsDoorsHandleValvesControllerSwitch.bum",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "LandingGear/LandingGear.json",
      "historyChartItems": []
    },
    {
      "name": "m913",
      "description": "",
      "location": "HD/m913.bum",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [
        "../HDMachine/model/m913.prob2trace",
        "../HDMachine/model/m913_2.prob2trace"
      ],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "HD/hd.json",
      "historyChartItems": []
    },
    {
      "name": "button2",
      "description": "",
      "location": "Button/button2.mch",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Button/button2.json",
      "historyChartItems": []
    },
    {
      "name": "SolarSystem",
      "description": "",
      "location": "Physics/SolarSystem.mch",
      "lastUsedPreferenceName": "default",
      "validationTasks": [],
      "validationObligations": [],
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": "Physics/MovingParticles_simulation.json",
      "visBVisualisation": null,
      "historyChartItems": []
    }
  ],
  "requirements": [],
  "preferences": [],
  "metadata": {
    "fileType": "Project",
    "formatVersion": 23,
    "savedAt": "2022-04-14T12:01:28.278060Z",
    "creator": "User",
    "proB2KernelVersion": "4.0.0-SNAPSHOT",
    "proBCliVersion": null,
    "modelName": null
  }
}