@@ -14,9 +14,13 @@ To solve it ProB2-UI use the following command in the Symbolic Pane of the Anima
...
@@ -14,9 +14,13 @@ To solve it ProB2-UI use the following command in the Symbolic Pane of the Anima
Type run0 and click on "Add and Check"
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"
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"
![ProB2-UI Alloy Version of Einstein's Puzzle](screenshots/ProB2UI-Alloy-Einstein.png"ProB2-UI Alloy Version of Einstein's Puzzle")
## TLA+ Encoding
## TLA+ Encoding
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)).
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)).
To solve it ProB2-UI use the the Symbolic Pane of the Verifications View (middle-right)
To solve it ProB2-UI use the the Symbolic Pane of the Verifications View (middle-right)
Choose "Invariant" and click on "Add and Check"
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"
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"
![ProB2-UI TLA Version of Einstein's Puzzle](screenshots/ProB2UI-TLA-Einstein.png"ProB2-UI TLA Version of Einstein's Puzzle")
