diff --git a/Einstein/Readme.md b/Einstein/Readme.md index 969156ba59c594ed708164a878997e0ce86fd61f..7541a3e1cde12da2e5f67b67a8194a99ce929de2 100644 --- a/Einstein/Readme.md +++ b/Einstein/Readme.md @@ -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" 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 + 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 diff --git a/Einstein/screenshots/ProB2UI-Alloy-Einstein.png b/Einstein/screenshots/ProB2UI-Alloy-Einstein.png new file mode 100644 index 0000000000000000000000000000000000000000..82be34be6ece91cbe99cff65f306a761550cb9c0 Binary files /dev/null and b/Einstein/screenshots/ProB2UI-Alloy-Einstein.png differ diff --git a/Einstein/screenshots/ProB2UI-TLA-Einstein.png b/Einstein/screenshots/ProB2UI-TLA-Einstein.png new file mode 100644 index 0000000000000000000000000000000000000000..d080c772540ca9875a9b701b3ff30b0e7c7b4aaf Binary files /dev/null and b/Einstein/screenshots/ProB2UI-TLA-Einstein.png differ