diff --git a/Einstein/Readme.md b/Einstein/Readme.md new file mode 100644 index 0000000000000000000000000000000000000000..969156ba59c594ed708164a878997e0ce86fd61f --- /dev/null +++ b/Einstein/Readme.md @@ -0,0 +1,22 @@ +# Einstein's Puzzle for VisB + +## What is VisB? + +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. + + +## 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" + +## 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)). + + 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" \ No newline at end of file