You will need to download a recent version of [ProB2-UI](https://www3.hhu.de/stups/prob/index.php/Download#ProB2_UI_using_Java_FX).
After that, you can follow [these](https://www3.hhu.de/stups/prob/index.php/VisB) instructions.
You will need to download a recent version of [ProB2-UI](https://www3.hhu.de/stups/prob/index.php/Download#ProB2_UI_using_Java_FX) for the examples below.
It will contain the [VisB](https://www3.hhu.de/stups/prob/index.php/VisB) view to allow visualizing states using SVG graphics and simple JSON annotations.
## Alloy Encoding of the Einstein Puzzle
Model taken from [Stackoverflow](https://stackoverflow.com/questions/47969967/alloy-model-of-the-einstein-puzzle)
To solve it ProB2-UI use the following command in the Symbolic Pane of the Animation View (bottom-left)
Type run0 and click on "Add and Check"
To see the visualisation Choose "Open VisB" in the visualisation menu, click on the "Open" icon in the top-right of the VisB menu bar and select the file "einstein_puzzle_als.json"
The Alloy model of the puzzle is taken 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)
- select "Sequence" and type "run0" and click on "Add and Check" (run0 is a B operation which is a translation of an Alloy command to solve the puzzle)
- to see the visualisation Choose "Open VisB" in the visualisation menu, click on the "Open" icon in the top-right of the VisB menu bar and select the file "einstein_puzzle_als.json".
You should then see something like the following picture:
![ProB2-UI Alloy Version of Einstein's Puzzle](screenshots/ProB2UI-Alloy-Einstein.png"ProB2-UI Alloy Version of Einstein's Puzzle")
You can create [HTML export](html/einsteins_puzzle.als.html) by calling the [command-line version of ProB](https://prob.hhu.de/w/index.php?title=Using_the_Command-Line_Version_of_ProB):
Note: you can re-create the [standalone HTML export in the repo](html/einsteins_puzzle.als.html) by calling the [command-line version of ProB](https://prob.hhu.de/w/index.php?title=Using_the_Command-Line_Version_of_ProB):
Model taken from [TlaPlus Examples Repo](https://github.com/tlaplus/Examples/pull/31)(model initially from [DeFrain](https://github.com/Isaac-DeFrain/TLAplusFun/tree/main/EinsteinRiddle)).
## 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)).
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 "Verifications" view (middle-right)
- choose "Invariant" and click on "Add and Check". Note: the invariant contains the negated solutions predicate: finding a counter example corresponds to solving the puzzle.
- to see a visualisation of the solution (i.e., counter example): choose "Open VisB" in the visualisation menu, click on the "Open" icon in the top-right of the VisB menu bar and select the file "Einstein_tla.json"
To solve it ProB2-UI use the the Symbolic Pane of the Verifications View (middle-right)
Choose "Invariant" and click on "Add and Check"
To see the visualisation Choose "Open VisB" in the visualisation menu, click on the "Open" icon in the top-right of the VisB menu bar and select the file "Einstein_tla.json"
You should then see something like the following picture:
![ProB2-UI TLA Version of Einstein's Puzzle](screenshots/ProB2UI-TLA-Einstein.png"ProB2-UI TLA Version of Einstein's Puzzle")
You can create an [HTML export](html/Einstein_tla.html) by calling the [command-line version of ProB](https://prob.hhu.de/w/index.php?title=Using_the_Command-Line_Version_of_ProB)
Note: you can re-create the [standalone HTML export in the repo](html/Einstein_tla.html) by calling the [command-line version of ProB](https://prob.hhu.de/w/index.php?title=Using_the_Command-Line_Version_of_ProB)
```
probcli Einstein.tla -cbc all -visb_with_vars Einstein_tla.json out.html
