{
  "name": "VisB-Examples",
  "description": "",
  "machines": [
    {
      "name": "button",
      "description": "",
      "location": "Button/button.mch",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [
        {
          "type": "INVARIANT",
          "name": "",
          "description": "Invariant",
          "code": "",
          "selected": true
        },
        {
          "type": "SYMBOLIC_MODEL_CHECK",
          "name": "BMC",
          "description": "Symbolic model checking",
          "code": "BMC",
          "selected": true
        }
      ],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Button/button.json"
    },
    {
      "name": "QueensWithEvents",
      "description": "",
      "location": "N-Queens/QueensWithEvents.mch",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [
        {
          "type": "SYMBOLIC_MODEL_CHECK",
          "name": "BMC",
          "description": "Symbolic model checking",
          "code": "BMC",
          "selected": true
        },
        {
          "type": "INVARIANT",
          "name": "",
          "description": "Invariant",
          "code": "",
          "selected": true
        },
        {
          "type": "INVARIANT",
          "name": "SetQueen",
          "description": "Invariant",
          "code": "SetQueen",
          "selected": true
        }
      ],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [
        "traces/QueensWithEvents.prob2trace"
      ],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "N-Queens/queens_8.json"
    },
    {
      "name": "Grapher",
      "description": "",
      "location": "Reals/Grapher.mch",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Reals/Grapher.json"
    },
    {
      "name": "MovingParticles3",
      "description": "",
      "location": "Physics/MovingParticles3.mch",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [
        "traces/MovingParticles3.prob2trace",
        "traces/MovingParticles.prob2trace"
      ],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Physics/three_bodies.json"
    },
    {
      "name": "MovingParticles4",
      "description": "",
      "location": "Physics/MovingParticles4.mch",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Physics/four_bodies.json"
    },
    {
      "name": "WasserkocherEinfach_mch",
      "description": "",
      "location": "Waterboiler/WasserkocherEinfach_mch.eventb",
      "lastUsedPreferenceName": "default",
      "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"
    },
    {
      "name": "WasserKocherFalsch1_mch",
      "description": "",
      "location": "Waterboiler/WasserKocherFalsch1_mch.eventb",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Waterboiler/visb_wasserkocher.json"
    },
    {
      "name": "WasserkocherFalsch2_mch",
      "description": "",
      "location": "Waterboiler/WasserkocherFalsch2_mch.eventb",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Waterboiler/visb_wasserkocher.json"
    },
    {
      "name": "m0_island_bridge_3cars_mch",
      "description": "",
      "location": "Bridge/m0_island_bridge_3cars_mch.eventb",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Bridge/visb_m0.json"
    },
    {
      "name": "m1_bridge_mch",
      "description": "",
      "location": "Bridge/m1_bridge_mch.eventb",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Bridge/visb_m1.json"
    },
    {
      "name": "Lift",
      "description": "",
      "location": "Lift/Lift.mch",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Lift/lift_groups.json"
    },
    {
      "name": "SimpleTrainTrack",
      "description": "",
      "location": "Train/SimpleTrainTrack.mch",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [
        "traces/SimpleTrainTrack.prob2trace"
      ],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Train/Track.json"
    },
    {
      "name": "TrafficLight",
      "description": "",
      "location": "TrafficLight/TrafficLight.mch",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "TrafficLight/traffic_light.json"
    },
    {
      "name": "button (1)",
      "description": "",
      "location": "Button/Z/button.tex",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Button/Z/button.json"
    },
    {
      "name": "button (2)",
      "description": "",
      "location": "Button/TLA/button.tla",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Button/TLA/button.json"
    },
    {
      "name": "einsteins_puzzle",
      "description": "",
      "location": "Einstein/einsteins_puzzle.als",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [
        {
          "type": "SEQUENCE",
          "name": "run0",
          "description": "Sequence",
          "code": "run0",
          "selected": true
        }
      ],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Einstein/einstein_puzzle_als.json"
    },
    {
      "name": "Einstein",
      "description": "",
      "location": "Einstein/Einstein.tla",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [
        {
          "type": "INVARIANT",
          "name": "",
          "description": "Invariant",
          "code": "",
          "selected": true
        }
      ],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Einstein/Einstein_tla.json"
    },
    {
      "name": "einsteins_enum",
      "description": "",
      "location": "Einstein/einsteins_enum.als",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": null
    },
    {
      "name": "TwoTrains",
      "description": "",
      "location": "Train/TwoTrains.mch",
      "lastUsedPreferenceName": "default",
      "ltlFormulas": [],
      "ltlPatterns": [],
      "symbolicCheckingFormulas": [],
      "symbolicAnimationFormulas": [],
      "simulationItems": [],
      "testCases": [],
      "traces": [
        "traces/TwoTrains.prob2trace"
      ],
      "modelcheckingItems": [],
      "simulation": null,
      "visBVisualisation": "Train/TwoTrains.json"
    }
  ],
  "preferences": [],
  "metadata": {
    "fileType": "Project",
    "formatVersion": 12,
    "savedAt": "2021-05-04T16:44:31.663852Z",
    "creator": "User",
    "proB2KernelVersion": "4.0.0-SNAPSHOT",
    "proBCliVersion": null,
    "modelName": null
  }
}