From ae985ad1161d3642d03f2c2ed62529190240a143 Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Tue, 30 Jan 2024 18:58:36 -0800 Subject: [PATCH] Add Apalache checkmark for EinstinRiddle + comment Signed-off-by: Giuliano Losa --- README.md | 2 +- specifications/EinsteinRiddle/Einstein.tla | 71 ++++++++++++---------- 2 files changed, 39 insertions(+), 34 deletions(-) diff --git a/README.md b/README.md index 359f9dce..c0490e3b 100644 --- a/README.md +++ b/README.md @@ -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 | | | | ✔ | | diff --git a/specifications/EinsteinRiddle/Einstein.tla b/specifications/EinsteinRiddle/Einstein.tla index e9ff0f68..eb67a5d3 100644 --- a/specifications/EinsteinRiddle/Einstein.tla +++ b/specifications/EinsteinRiddle/Einstein.tla @@ -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 @@ -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^'. -============================================================ +============================================================ \ No newline at end of file