Skip to content

Commit

Permalink
Add Apalache checkmark for EinstinRiddle + comment (#117)
Browse files Browse the repository at this point in the history 
Signed-off-by: Giuliano Losa <[email protected]>
  • Loading branch information
@nano-o
nano-o authored Jan 31, 2024
1 parent 7db81cd commit 666625d
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 34 deletions.
2 changes: 1 addition & 1 deletion README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ Here is a list of specs included in this repository, with links to the relevant
| [Checkpoint Coordination](specifications/CheckpointCoordination) | Andrew Helwer | | | | ✔ | |
| [Finitizing Monotonic Systems](specifications/FiniteMonotonic) | Andrew Helwer | | | | ✔ | |
| [The Readers-Writers Problem](specifications/ReadersWriters) | Isaac DeFrain | | | | ✔ | |
| [Einstein's Riddle](specifications/EinsteinRiddle) | Isaac DeFrain | | | | ✔ | |
| [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
71 changes: 38 additions & 33 deletions specifications/EinsteinRiddle/Einstein.tla
View file
Original file line number Diff line number Diff line change
@@ -1,37 +1,42 @@
------------------- 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

Expand Down Expand Up @@ -162,4 +167,4 @@ FindSolution == ~Solution
\* `^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 666625d

Please sign in to comment.