diff --git a/Einstein/Readme.md b/Einstein/Readme.md index fc46534fc3887bd24c46381b29c8b37f78fd26fa..ed7cdd05c33d376486f20fb5ffa91e0e75acd399 100644 --- a/Einstein/Readme.md +++ b/Einstein/Readme.md @@ -24,8 +24,8 @@ 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. -  +Note that the initial solution from [Stackoverflow](https://stackoverflow.com/questions/47969967/alloy-model-of-the-einstein-puzzle) was missing constraints, which was apparent in the visualisation (dog appeared twice). +<!--  --> ## 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/html/einsteins_puzzle.als.html b/Einstein/html/einsteins_puzzle.als.html index 9b6484e58def9b0705ab72279c5cfb2cedf65f99..a5bdc183fa4277f739f47e999f70ba5ea0dcb3bf 100644 --- a/Einstein/html/einsteins_puzzle.als.html +++ b/Einstein/html/einsteins_puzzle.als.html @@ -130,7 +130,7 @@ setAttr("nationality3","text","Englishman"); setAttr("cigarette3","text","Pall_Mall"); setAttr("drink3","text","milk"); - setAttr("pet4","text","dog"); + setAttr("pet4","text","fish"); setAttr("nationality4","text","German"); setAttr("cigarette4","text","Prince"); setAttr("drink4","text","coffee"); @@ -265,7 +265,7 @@ version="1.1" id="svg2"> <tr id="var_rowcigarette_House"> <td>5</td> <td>cigarette_House</td> <td id="bVar_cigarette_House">{(0|->Dunhills),(1|->Blend),(2|->Pall_Mall),(3|->Prince),(4|->Blue_Masters)}</td></tr> - <tr id="var_rowpet_House"> <td>6</td> <td>pet_House</td> <td id="bVar_pet_House">{(0|->cat),(1|->horse),(2|->bird),(3|->dog),(4|->dog)}</td></tr> + <tr id="var_rowpet_House"> <td>6</td> <td>pet_House</td> <td id="bVar_pet_House">{(0|->cat),(1|->horse),(2|->bird),(3|->fish),(4|->dog)}</td></tr> </table> </div> <button type="button" class="collapsible collapsible-style">Sets (5/5)</button> @@ -296,7 +296,7 @@ version="1.1" id="svg2"> </div> <button type="button" class="collapsible-style">Info</button> <div class="coll-content-vis"> -Generated on 22/3/2021 at 8:20 using ProB version 1.11.0-nightly +Generated on 23/3/2021 at 9:51 using ProB version 1.11.0-nightly <br>Main specification file: einsteins_puzzle.als </table> </div>