diff --git a/Einstein/Readme.md b/Einstein/Readme.md index 14dc0da6cb76edb683cd611420d37a1466b56f69..fc46534fc3887bd24c46381b29c8b37f78fd26fa 100644 --- a/Einstein/Readme.md +++ b/Einstein/Readme.md @@ -8,7 +8,7 @@ It will contain the [VisB](https://www3.hhu.de/stups/prob/index.php/VisB) view t ## Alloy Encoding of the Einstein Puzzle -The Alloy model of the puzzle is taken from [Stackoverflow](https://stackoverflow.com/questions/47969967/alloy-model-of-the-einstein-puzzle) +The Alloy model of the puzzle is a corrected version adapted from [Stackoverflow](https://stackoverflow.com/questions/47969967/alloy-model-of-the-einstein-puzzle). To solve it in [ProB2-UI](https://www3.hhu.de/stups/prob/index.php/Download#ProB2_UI_using_Java_FX) - select the "Symbolic" pane of the "Animation" view (bottom-left of the main window) @@ -23,7 +23,10 @@ Note: you can re-create the [standalone HTML export in the repo](html/einsteins_ ``` probcli einsteins_puzzle.als -cbc-sequence run0 -visb_with_vars einstein_puzzle_als.json out.html ``` - + +Note that the initial solution from [Stackoverflow](https://stackoverflow.com/questions/47969967/alloy-model-of-the-einstein-puzzle) was missing constraints. +  + ## TLA+ Encoding of the Einstein Puzzle The TLA+ model is taken from the [TlaPlus Examples Repo](https://github.com/tlaplus/Examples/pull/31) (the model initially came from [DeFrain](https://github.com/Isaac-DeFrain/TLAplusFun/tree/main/EinsteinRiddle)). diff --git a/Einstein/einsteins_puzzle.als b/Einstein/einsteins_puzzle.als index 066f50d2019c8817994cac83957232542161d48a..e12a5b6bcdec03ce4d097598a86d99e990ef6261 100644 --- a/Einstein/einsteins_puzzle.als +++ b/Einstein/einsteins_puzzle.als @@ -86,5 +86,11 @@ fact constraints { some disjoint h,h': House | (h.nationality = Norwegian) and (h'.color= blue) and (h.next = h') // 15. The Blend smoker has a neighbor who drinks water. some disj h,h': House | (h.cigarette = Blend) and (h'.drink = water) and ((h.next = h') or (h.prev = h')) + + // Missing constraints (not in Stackoverflow solution): + // No owners have the same pet, smoke the same brand of cigar or drink the same beverage. + no disj h,h': House | h.pet = h'.pet // otherwise there are solutions with green and white house having both dog as pet + no disj h,h': House | h.cigarette = h'.cigarette // not really required + no disj h,h': House | h.drink = h'.drink // not really required } -run {} for 5 \ No newline at end of file +run {} for 5 diff --git a/Einstein/screenshots/Alloy-Wrong.png b/Einstein/screenshots/Alloy-Wrong.png new file mode 100644 index 0000000000000000000000000000000000000000..f921c51d94ca2cce694b938e8abf026b0d6432f9 Binary files /dev/null and b/Einstein/screenshots/Alloy-Wrong.png differ diff --git a/Einstein/screenshots/ProB2UI-Alloy-Einstein-Wrong.png b/Einstein/screenshots/ProB2UI-Alloy-Einstein-Wrong.png new file mode 100644 index 0000000000000000000000000000000000000000..82be34be6ece91cbe99cff65f306a761550cb9c0 Binary files /dev/null and b/Einstein/screenshots/ProB2UI-Alloy-Einstein-Wrong.png differ diff --git a/Einstein/screenshots/ProB2UI-Alloy-Einstein.png b/Einstein/screenshots/ProB2UI-Alloy-Einstein.png index 82be34be6ece91cbe99cff65f306a761550cb9c0..f10e0f4a26903ee0471dd0294517c5de37d6fb51 100644 Binary files a/Einstein/screenshots/ProB2UI-Alloy-Einstein.png and b/Einstein/screenshots/ProB2UI-Alloy-Einstein.png differ diff --git a/Einstein/screenshots/VisB-Alloy-Wrong.png b/Einstein/screenshots/VisB-Alloy-Wrong.png new file mode 100644 index 0000000000000000000000000000000000000000..976fd12ee99c5daa8f335d1ead4a802180ac110c Binary files /dev/null and b/Einstein/screenshots/VisB-Alloy-Wrong.png differ