Select Git revision
VisB-Examples.prob2project
Code owners
Assign users and groups as approvers for specific file changes. Learn more.
VisB-Examples.prob2project 17.14 KiB
{
"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
}
}