Skip to content

Commit

Permalink
Merged changes from master
Browse files Browse the repository at this point in the history 
Signed-off-by: Andrew Helwer <[email protected]>
  • Loading branch information
@ahelwer
ahelwer committed Jan 31, 2024
2 parents a124725 + 666625d commit 8aad761
Show file tree
Hide file tree
Showing 3 changed files with 63 additions and 40 deletions.
5 changes: 3 additions & 2 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 | ✔ | ✔ | ✔ | ✔ | |
Expand Down Expand Up @@ -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 | | | | ✔ | |
Expand Down
3 changes: 2 additions & 1 deletion manifest.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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": [
Expand Down
95 changes: 58 additions & 37 deletions specifications/EinsteinRiddle/Einstein.tla
View file
Original file line number Diff line number Diff line change
@@ -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]}
Expand All @@ -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

------------------------------------------------------------
Expand Down Expand Up @@ -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 == <<nationality, colors, cigars, pets, drinks>>

Next ==
UNCHANGED <<nationality, colors, cigars, pets, drinks>>
UNCHANGED vars

Spec == Init /\ [][Next]_<<nationality, colors, cigars, pets, drinks>>
Spec == Init /\ [][Next]_vars

Solution ==
/\ BritLivesInTheRedHouse
Expand All @@ -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^'.

============================================================

0 comments on commit 8aad761

Please sign in to comment.