diff --git a/Einstein/Einstein.cfg b/Einstein/Einstein.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..f4aff4ea2ac193bbcc1f693552b3a514a595ffcb
--- /dev/null
+++ b/Einstein/Einstein.cfg
@@ -0,0 +1,5 @@
+INVARIANT
+ FindSolution
+
+SPECIFICATION
+ Spec
diff --git a/Einstein/Einstein.tla b/Einstein/Einstein.tla
new file mode 100644
index 0000000000000000000000000000000000000000..a523a4e6ec240f2e9cc18089a621b4d519c63931
--- /dev/null
+++ b/Einstein/Einstein.tla
@@ -0,0 +1,161 @@
+------------------- MODULE Einstein ------------------------
+(*
+
+Source: https://github.com/Isaac-DeFrain/TLAplusFun/tree/main/EinsteinRiddle
+and https://github.com/tlaplus/Examples/pull/31
+
+ To solve it ProB2-UI use the following command
+ in the Symbolic Pane of the Verifications View (middle-right)
+ Choose "Invariant" and click on "Add and Check"
+ To see the visualisation Choose "Open VisB"
+ in the visualisation menu, click on the "Open" icon
+ in the top-right of the VisB menu bar and select the
+ file "Einstein_tla.json"
+*)
+(*********************************************************************)
+(* Literature/Source: *)
+(* https://udel.edu/~os/riddle.html *)
+(* *)
+(* Situation: *)
+(* - There are 5 houses in five different colors. *)
+(* - In each house lives a person with a different nationality. *)
+(* - These five owners drink a certain type of beverage, smoke a *)
+(* certain brand of cigar and keep a certain pet. *)
+(* - No owners have the same pet, smoke the same brand of cigar, or *)
+(* drink the same beverage. *)
+(* *)
+(* Rules: *)
+(* 1 the Brit lives in the red house *)
+(* 2 the Swede keeps dogs as pets *)
+(* 3 the Dane drinks tea *)
+(* 4 the green house is on the left of the white house *)
+(* 5 the green house's owner drinks coffee *)
+(* 6 the person who smokes Pall Mall rears birds *)
+(* 7 the owner of the yellow house smokes Dunhill *)
+(* 8 the man living in the center house drinks mylk *)
+(* 9 the Norwegian lives in the first house *)
+(* 10 the man who smokes blends lives next to the one who keeps cats *)
+(* 11 the man who keeps horses lives next to man who smokes Dunhill *)
+(* 12 the owner who smokes BlueMaster drinks beer *)
+(* 13 the German smokes Prince *)
+(* 14 the Norwegian lives next to the blue house *)
+(* 15 the man who smokes blend has a neighbor who drinks water *)
+(* *)
+(* Question: *)
+(* Who owns the fish? *)
+(*********************************************************************)
+
+EXTENDS Naturals, FiniteSets
+
+\* Note that TLC!Permutations has a Java module override and, thus,
+\* would be evaluated faster. However, TLC!Permutations equals a
+\* set of records whereas Permutation below equals a set of tuples/
+\* sequences. Also, Permutation expects Cardinality(S) = 5.
+Permutation(S) ==
+ { p \in [ 1..5 -> S ] :
+ /\ p[2] \in S \ {p[1]}
+ /\ p[3] \in S \ {p[1], p[2]}
+ /\ p[4] \in S \ {p[1], p[2], p[3]}
+ /\ p[5] \in S \ {p[1], p[2], p[3], p[4]} }
+
+\* In most specs, the following parameterization would be defined as
+\* constants. Given that Einstein's riddle has only this
+\* parameterization, the constants are replaced with constant-level
+\* operators. As a side-effect, TLC evaluates them eagerly at startup,
+\* and Apalache successfully determines their types.
+NATIONALITIES == Permutation({ "brit", "swede", "dane", "norwegian", "german" })
+DRINKS == Permutation({ "beer", "coffee", "mylk", "tea", "water" })
+COLORS == Permutation({ "red", "white", "blue", "green", "yellow" })
+PETS == Permutation({ "bird", "cat", "dog", "fish", "horse" })
+CIGARS == Permutation({ "blend", "bm", "dh", "pm", "prince" })
+
+VARIABLES
+ nationality, \* tuple of nationalities
+ colors, \* tuple of house colors
+ pets, \* tuple of pets
+ cigars, \* tuple of cigars
+ drinks \* tuple of drinks
+
+------------------------------------------------------------
+
+(*********)
+(* Rules *)
+(*********)
+
+BritLivesInTheRedHouse == \E i \in 2..5 : nationality[i] = "brit" /\ colors[i] = "red"
+
+SwedeKeepsDogs == \E i \in 2..5 : nationality[i] = "swede" /\ pets[i] = "dog"
+
+DaneDrinksTea == \E i \in 2..5 : nationality[i] = "dane" /\ drinks[i] = "tea"
+
+GreenLeftOfWhite == \E i \in 1..4 : colors[i] = "green" /\ colors[i + 1] = "white"
+
+GreenOwnerDrinksCoffee == \E i \in 1..5 \ {3} : colors[i] = "green" /\ drinks[i] = "coffee"
+
+SmokesPallmallRearsBirds == \E i \in 1..5 : cigars[i] = "pm" /\ pets[i] = "bird"
+
+YellowOwnerSmokesDunhill == \E i \in 1..5 : colors[i] = "yellow" /\ cigars[i] = "dh"
+
+CenterDrinksMylk == drinks[3] = "mylk"
+
+NorwegianFirstHouse == nationality[1] = "norwegian"
+
+BlendSmokerLivesNextToCatOwner ==
+ \E i \in 1..4 :
+ \/ cigars[i] = "blend" /\ pets[i + 1] = "cat"
+ \/ pets[i] = "cat" /\ cigars[i + 1] = "blend"
+
+HorseKeeperLivesNextToDunhillSmoker ==
+ \E i \in 1..4 :
+ \/ cigars[i] = "dh" /\ pets[i + 1] = "horse"
+ \/ pets[i] = "horse" /\ cigars[i + 1] = "dh"
+
+BluemasterSmokerDrinksBeer == \E i \in 1..5 : cigars[i] = "bm" /\ drinks[i] = "beer"
+
+GermanSmokesPrince == \E i \in 2..5 : nationality[i] = "german" /\ cigars[i] = "prince"
+
+NorwegianLivesNextToBlueHouse == colors[2] = "blue" \* since the norwegian lives in the first house
+
+BlendSmokerHasWaterDrinkingNeighbor ==
+ \E i \in 1..4 :
+ \/ cigars[i] = "blend" /\ drinks[i + 1] = "water"
+ \/ drinks[i] = "water" /\ cigars[i + 1] = "blend"
+
+------------------------------------------------------------
+
+(************)
+(* Solution *)
+(************)
+
+Init ==
+ /\ drinks \in { p \in DRINKS : p[3] = "mylk" }
+ /\ nationality \in { p \in NATIONALITIES : p[1] = "norwegian" }
+ /\ colors \in { p \in COLORS : p[2] = "blue" }
+ /\ pets \in PETS
+ /\ cigars \in CIGARS
+
+Next ==
+ UNCHANGED <<nationality, colors, cigars, pets, drinks>>
+
+Spec == Init /\ [][Next]_<<nationality, colors, cigars, pets, drinks>>
+
+Solution ==
+ /\ BritLivesInTheRedHouse
+ /\ SwedeKeepsDogs
+ /\ DaneDrinksTea
+ /\ GreenLeftOfWhite
+ /\ GreenOwnerDrinksCoffee
+ /\ SmokesPallmallRearsBirds
+ /\ YellowOwnerSmokesDunhill
+ /\ CenterDrinksMylk
+ /\ NorwegianFirstHouse
+ /\ BlendSmokerLivesNextToCatOwner
+ /\ HorseKeeperLivesNextToDunhillSmoker
+ /\ BluemasterSmokerDrinksBeer
+ /\ GermanSmokesPrince
+ /\ NorwegianLivesNextToBlueHouse
+ /\ BlendSmokerHasWaterDrinkingNeighbor
+
+FindSolution == ~Solution
+
+============================================================
diff --git a/Einstein/Einstein_tla.json b/Einstein/Einstein_tla.json
new file mode 100644
index 0000000000000000000000000000000000000000..91fb2081c449915a7ee43607923967cabae29678
--- /dev/null
+++ b/Einstein/Einstein_tla.json
@@ -0,0 +1,35 @@
+{
+ "svg": "Houses.svg",
+ "items": [
+ {
+ "for": {"from":1, "to":5},
+ "id": "house%0",
+ "attr": "fill",
+ "value" :"colors(%0)"
+ },
+ {
+ "for": {"from":1, "to":5},
+ "id": "pet%0",
+ "attr": "text",
+ "value" :"pets(%0)"
+ },
+ {
+ "for": {"from":1, "to":5},
+ "id": "cigar%0",
+ "attr": "text",
+ "value" :"cigars(%0)"
+ },
+ {
+ "for": {"from":1, "to":5},
+ "id": "drink%0",
+ "attr": "text",
+ "value" :"drinks(%0)"
+ },
+ {
+ "for": {"from":1, "to":5},
+ "id": "nationality%0",
+ "attr": "text",
+ "value" :"nationality(%0)"
+ }
+ ]
+}
\ No newline at end of file
diff --git a/Einstein/einsteins_puzzle.als b/Einstein/einsteins_puzzle.als
index b2f77e3d9e0d76e545508f86b9ccc92a6297dcda..066f50d2019c8817994cac83957232542161d48a 100644
--- a/Einstein/einsteins_puzzle.als
+++ b/Einstein/einsteins_puzzle.als
@@ -1,4 +1,9 @@
+//
// Alloy Encoding of the Einstein Puzzle
+//
+// Model taken from:
+// https://stackoverflow.com/questions/47969967/alloy-model-of-the-einstein-puzzle
+//
// To solve it ProB2-UI use the following command
// in the Symbolic Pane of the Animation View (bottom-left)
// Type run0 and click on "Add and Check"
diff --git a/VisB-Examples.prob2project b/VisB-Examples.prob2project
index 33884e545b09c5fa2391bbad63403f73e1aca6c5..7652ea1d3527ad26a74c5d7590545821ce00cc75 100644
--- a/VisB-Examples.prob2project
+++ b/VisB-Examples.prob2project
@@ -26,9 +26,11 @@
}
],
"symbolicAnimationFormulas": [],
+ "simulationItems": [],
"testCases": [],
"traces": [],
"modelcheckingItems": [],
+ "simulation": null,
"visBVisualisation": "Button/button.json"
},
{
@@ -62,11 +64,13 @@
}
],
"symbolicAnimationFormulas": [],
+ "simulationItems": [],
"testCases": [],
"traces": [
"traces/QueensWithEvents.prob2trace"
],
"modelcheckingItems": [],
+ "simulation": null,
"visBVisualisation": "N-Queens/queens_8.json"
},
{
@@ -78,9 +82,11 @@
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
"symbolicAnimationFormulas": [],
+ "simulationItems": [],
"testCases": [],
"traces": [],
"modelcheckingItems": [],
+ "simulation": null,
"visBVisualisation": "Reals/Grapher.json"
},
{
@@ -92,12 +98,14 @@
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
"symbolicAnimationFormulas": [],
+ "simulationItems": [],
"testCases": [],
"traces": [
"traces/MovingParticles3.prob2trace",
"traces/MovingParticles.prob2trace"
],
"modelcheckingItems": [],
+ "simulation": null,
"visBVisualisation": "Physics/three_bodies.json"
},
{
@@ -109,10 +117,12 @@
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
"symbolicAnimationFormulas": [],
+ "simulationItems": [],
"testCases": [],
"traces": [],
"modelcheckingItems": [],
- "visBVisualisation": null
+ "simulation": null,
+ "visBVisualisation": "Physics/four_bodies.json"
},
{
"name": "WasserkocherEinfach_mch",
@@ -123,17 +133,226 @@
"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"
}
],
"preferences": [],
"metadata": {
"fileType": "Project",
- "formatVersion": 9,
- "savedAt": "2020-11-20T09:34:16.941580Z",
+ "formatVersion": 12,
+ "savedAt": "2021-03-21T21:16:32.522884Z",
"creator": "User",
"proB2KernelVersion": "4.0.0-SNAPSHOT",
"proBCliVersion": null,