Skip to content
Snippets Groups Projects
Commit 9bdb9b6e authored by Michael Leuschel's avatar Michael Leuschel
Browse files

update generated html for Alloy Einstein solution

parent 7c11f72e
No related branches found
No related tags found
No related merge requests found
...@@ -24,8 +24,8 @@ Note: you can re-create the [standalone HTML export in the repo](html/einsteins_ ...@@ -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 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).
![VisB Wrong Solution visualized](screenshots/VisB-Alloy-Wrong.png "ProB2-UI ViSb Alloy Wrong Solution of Einstein's Puzzle") <!-- ![VisB Wrong Solution visualized](screenshots/VisB-Alloy-Wrong.png "ProB2-UI ViSb Alloy Wrong Solution of Einstein's Puzzle") -->
## TLA+ Encoding of the Einstein Puzzle ## 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)). 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)).
......
...@@ -130,7 +130,7 @@ ...@@ -130,7 +130,7 @@
setAttr("nationality3","text","Englishman"); setAttr("nationality3","text","Englishman");
setAttr("cigarette3","text","Pall_Mall"); setAttr("cigarette3","text","Pall_Mall");
setAttr("drink3","text","milk"); setAttr("drink3","text","milk");
setAttr("pet4","text","dog"); setAttr("pet4","text","fish");
setAttr("nationality4","text","German"); setAttr("nationality4","text","German");
setAttr("cigarette4","text","Prince"); setAttr("cigarette4","text","Prince");
setAttr("drink4","text","coffee"); setAttr("drink4","text","coffee");
...@@ -265,7 +265,7 @@ version="1.1" id="svg2"> ...@@ -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|-&gt;Dunhills),(1|-&gt;Blend),(2|-&gt;Pall_Mall),(3|-&gt;Prince),(4|-&gt;Blue_Masters)}</td></tr> <tr id="var_rowcigarette_House"> <td>5</td> <td>cigarette_House</td> <td id="bVar_cigarette_House">{(0|-&gt;Dunhills),(1|-&gt;Blend),(2|-&gt;Pall_Mall),(3|-&gt;Prince),(4|-&gt;Blue_Masters)}</td></tr>
<tr id="var_rowpet_House"> <td>6</td> <td>pet_House</td> <td id="bVar_pet_House">{(0|-&gt;cat),(1|-&gt;horse),(2|-&gt;bird),(3|-&gt;dog),(4|-&gt;dog)}</td></tr> <tr id="var_rowpet_House"> <td>6</td> <td>pet_House</td> <td id="bVar_pet_House">{(0|-&gt;cat),(1|-&gt;horse),(2|-&gt;bird),(3|-&gt;fish),(4|-&gt;dog)}</td></tr>
</table> </table>
</div> </div>
<button type="button" class="collapsible collapsible-style">Sets (5/5)</button> <button type="button" class="collapsible collapsible-style">Sets (5/5)</button>
...@@ -296,7 +296,7 @@ version="1.1" id="svg2"> ...@@ -296,7 +296,7 @@ version="1.1" id="svg2">
</div> </div>
<button type="button" class="collapsible-style">Info</button> <button type="button" class="collapsible-style">Info</button>
<div class="coll-content-vis"> <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 <br>Main specification file: einsteins_puzzle.als
</table> </table>
</div> </div>
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment