From 5fc0b06755815a91d40492926390b0798964d2c6 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Mon, 22 Mar 2021 16:58:07 +0100
Subject: [PATCH] =?UTF-8?q?improve=20readme=20of=20Einstein=E2=80=99s=20pu?=
 =?UTF-8?q?zzle?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Einstein/Readme.md | 36 +++++++++++++++++++++---------------
 1 file changed, 21 insertions(+), 15 deletions(-)

diff --git a/Einstein/Readme.md b/Einstein/Readme.md
index 408c253..9e6544a 100644
--- a/Einstein/Readme.md
+++ b/Einstein/Readme.md
@@ -1,36 +1,42 @@
 # Einstein's Puzzle for VisB
 
-## What is VisB?
+## ProB2-UI and 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.
+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):
 ```
 probcli einsteins_puzzle.als -cbc-sequence run0 -visb_with_vars einstein_puzzle_als.json out.html
 ```
  
-## 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)).
+## 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 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"
+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"
  
+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
 ```
\ No newline at end of file
-- 
GitLab