From 9f18adf227103e67af7347b25c4325104f194e67 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Mon, 22 Mar 2021 08:26:26 +0100
Subject: [PATCH] add readme for Einstein

---
 Einstein/Readme.md | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 Einstein/Readme.md

diff --git a/Einstein/Readme.md b/Einstein/Readme.md
new file mode 100644
index 0000000..969156b
--- /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
-- 
GitLab