Skip to content
Snippets Groups Projects
Commit 83235f11 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add TLA Einstein model and visualisation

parent 81d0f42c
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Einstein/Einstein.cfg 0 → 100644
+ 5
− 0
View file @ 83235f11
INVARIANT
FindSolution
SPECIFICATION
Spec
Einstein/Einstein.tla 0 → 100644
+ 161
− 0
View file @ 83235f11
------------------- 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
============================================================
Einstein/Einstein_tla.json 0 → 100644
+ 35
− 0
View file @ 83235f11
{
"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
Einstein/einsteins_puzzle.als
+ 5
− 0
View file @ 83235f11
//
// Alloy Encoding of the Einstein Puzzle // 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 // To solve it ProB2-UI use the following command
// in the Symbolic Pane of the Animation View (bottom-left) // in the Symbolic Pane of the Animation View (bottom-left)
// Type run0 and click on "Add and Check" // Type run0 and click on "Add and Check"
......
VisB-Examples.prob2project
+ 222
− 3
View file @ 83235f11
...@@ -26,9 +26,11 @@ ...@@ -26,9 +26,11 @@
} }
], ],
"symbolicAnimationFormulas": [], "symbolicAnimationFormulas": [],
"simulationItems": [],
"testCases": [], "testCases": [],
"traces": [], "traces": [],
"modelcheckingItems": [], "modelcheckingItems": [],
"simulation": null,
"visBVisualisation": "Button/button.json" "visBVisualisation": "Button/button.json"
}, },
{ {
...@@ -62,11 +64,13 @@ ...@@ -62,11 +64,13 @@
} }
], ],
"symbolicAnimationFormulas": [], "symbolicAnimationFormulas": [],
"simulationItems": [],
"testCases": [], "testCases": [],
"traces": [ "traces": [
"traces/QueensWithEvents.prob2trace" "traces/QueensWithEvents.prob2trace"
], ],
"modelcheckingItems": [], "modelcheckingItems": [],
"simulation": null,
"visBVisualisation": "N-Queens/queens_8.json" "visBVisualisation": "N-Queens/queens_8.json"
}, },
{ {
...@@ -78,9 +82,11 @@ ...@@ -78,9 +82,11 @@
"ltlPatterns": [], "ltlPatterns": [],
"symbolicCheckingFormulas": [], "symbolicCheckingFormulas": [],
"symbolicAnimationFormulas": [], "symbolicAnimationFormulas": [],
"simulationItems": [],
"testCases": [], "testCases": [],
"traces": [], "traces": [],
"modelcheckingItems": [], "modelcheckingItems": [],
"simulation": null,
"visBVisualisation": "Reals/Grapher.json" "visBVisualisation": "Reals/Grapher.json"
}, },
{ {
...@@ -92,12 +98,14 @@ ...@@ -92,12 +98,14 @@
"ltlPatterns": [], "ltlPatterns": [],
"symbolicCheckingFormulas": [], "symbolicCheckingFormulas": [],
"symbolicAnimationFormulas": [], "symbolicAnimationFormulas": [],
"simulationItems": [],
"testCases": [], "testCases": [],
"traces": [ "traces": [
"traces/MovingParticles3.prob2trace", "traces/MovingParticles3.prob2trace",
"traces/MovingParticles.prob2trace" "traces/MovingParticles.prob2trace"
], ],
"modelcheckingItems": [], "modelcheckingItems": [],
"simulation": null,
"visBVisualisation": "Physics/three_bodies.json" "visBVisualisation": "Physics/three_bodies.json"
}, },
{ {
...@@ -109,10 +117,12 @@ ...@@ -109,10 +117,12 @@
"ltlPatterns": [], "ltlPatterns": [],
"symbolicCheckingFormulas": [], "symbolicCheckingFormulas": [],
"symbolicAnimationFormulas": [], "symbolicAnimationFormulas": [],
"simulationItems": [],
"testCases": [], "testCases": [],
"traces": [], "traces": [],
"modelcheckingItems": [], "modelcheckingItems": [],
"visBVisualisation": null "simulation": null,
"visBVisualisation": "Physics/four_bodies.json"
}, },
{ {
"name": "WasserkocherEinfach_mch", "name": "WasserkocherEinfach_mch",
...@@ -123,17 +133,226 @@ ...@@ -123,17 +133,226 @@
"ltlPatterns": [], "ltlPatterns": [],
"symbolicCheckingFormulas": [], "symbolicCheckingFormulas": [],
"symbolicAnimationFormulas": [], "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": [], "testCases": [],
"traces": [], "traces": [],
"modelcheckingItems": [], "modelcheckingItems": [],
"simulation": null,
"visBVisualisation": "Waterboiler/visb_wasserkocher.json" "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": [], "preferences": [],
"metadata": { "metadata": {
"fileType": "Project", "fileType": "Project",
"formatVersion": 9, "formatVersion": 12,
"savedAt": "2020-11-20T09:34:16.941580Z", "savedAt": "2021-03-21T21:16:32.522884Z",
"creator": "User", "creator": "User",
"proB2KernelVersion": "4.0.0-SNAPSHOT", "proB2KernelVersion": "4.0.0-SNAPSHOT",
"proBCliVersion": null, "proBCliVersion": null,
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment