diff --git a/README.md b/README.md index 5042f473..9b066c90 100644 --- a/README.md +++ b/README.md @@ -16,6 +16,7 @@ All specs in this repository are subject to CI validation to ensure quality. ## Examples Included Here Here is a list of specs included in this repository, with links to the relevant directory and flags for various features: +<<<<<<< HEAD | Name | Author(s) | Beginner | TLAPS Proof | PlusCal | TLC Model | Apalache | | --------------------------------------------------------------------------------------------------- | --------------------------------------------------- | :------: | :---------: | :-----: | :-------: | :------: | | [Teaching Concurrency](specifications/TeachingConcurrency) | Leslie Lamport | ✔ | ✔ | ✔ | ✔ | | @@ -68,8 +69,8 @@ Here is a list of specs included in this repository, with links to the relevant | [Finitizing Monotonic Systems](specifications/FiniteMonotonic) | Andrew Helwer | | | | ✔ | | | [Multi-Car Elevator System](specifications/MultiCarElevator) | Andrew Helwer | | | | ✔ | | | [Nano Blockchain Protocol](specifications/NanoBlockchain) | Andrew Helwer | | | | ✔ | | -| [The Readers-Writers Problem](specifications/ReadersWriters) | Isaac DeFrain | | | | ✔ | | -| [Einstein's Riddle](specifications/EinsteinRiddle) | Isaac DeFrain | | | | ✔ | | +| [The Readers-Writers Problem](specifications/ReadersWriters) | Isaac DeFrain, Giuliano Losa | | | | ✔ | | +| [Einstein's Riddle](specifications/EinsteinRiddle) | Isaac DeFrain | | | | ✔ | ✔ | | [Asynchronous Byzantine Consensus](specifications/aba-asyn-byz) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | | [Folklore Reliable Broadcast](specifications/bcastFolklore) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | | [The Bosco Byzantine Consensus Algorithm](specifications/bosco) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | diff --git a/manifest.json b/manifest.json index a99866b4..e953ce0d 100644 --- a/manifest.json +++ b/manifest.json @@ -420,7 +420,8 @@ "description": "Five houses, five people, various facts, who lives in what house?", "sources": [], "authors": [ - "Isaac DeFrain" + "Isaac DeFrain", + "Giuliano Losa" ], "tags": [], "modules": [ diff --git a/specifications/EinsteinRiddle/Einstein.tla b/specifications/EinsteinRiddle/Einstein.tla index 0797ec70..eb67a5d3 100644 --- a/specifications/EinsteinRiddle/Einstein.tla +++ b/specifications/EinsteinRiddle/Einstein.tla @@ -1,46 +1,53 @@ ------------------- MODULE Einstein ------------------------ -(*********************************************************************) -(* 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? *) -(*********************************************************************) +(*********************************************************************************) +(* 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? *) +(* *) +(* Note that `^TLC^' takes a very long time to find the solution because it *) +(* blindly enumerates all possible combinations of assignments to the variables; *) +(* in contrast, `^Apalache^' finds the solution easily using an `^SMT^' solver. *) +(* Instructions to run `^Apalache^' appear at the end of the file. *) +(*********************************************************************************) EXTENDS Naturals, FiniteSets +House == 1..5 + \* 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 ] : +Permutation(S) == + { p \in [ House -> 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]} @@ -58,10 +65,15 @@ PETS == Permutation({ "bird", "cat", "dog", "fish", "horse" }) CIGARS == Permutation({ "blend", "bm", "dh", "pm", "prince" }) VARIABLES + \* @type: Int -> Str; nationality, \* tuple of nationalities + \* @type: Int -> Str; colors, \* tuple of house colors + \* @type: Int -> Str; pets, \* tuple of pets + \* @type: Int -> Str; cigars, \* tuple of cigars + \* @type: Int -> Str; drinks \* tuple of drinks ------------------------------------------------------------ @@ -122,10 +134,15 @@ Init == /\ pets \in PETS /\ cigars \in CIGARS +\* Apalache cannot infer the type of `vars' because it could be a sequence or a tuple. +\* So we explicitely tell Apalache that it is a sequence by adding the following annotation: +\* @type: Seq(Int -> Str); +vars == <> + Next == - UNCHANGED <> + UNCHANGED vars -Spec == Init /\ [][Next]_<> +Spec == Init /\ [][Next]_vars Solution == /\ BritLivesInTheRedHouse @@ -146,4 +163,8 @@ Solution == FindSolution == ~Solution -============================================================ +\* To find the solution with the `^Apalache^' model-checker, run: +\* `^apalache-mc check --init=Init --inv=FindSolution --length=0 --run-dir=./outout Einstein.tla^' +\* You will then find the solution in `^./output/violation.tla^'. + +============================================================ \ No newline at end of file