diff --git a/Einstein/Readme.md b/Einstein/Readme.md index 7541a3e1cde12da2e5f67b67a8194a99ce929de2..408c253ca6c7469b390e1a3bb590bb9d70f4fe51 100644 --- a/Einstein/Readme.md +++ b/Einstein/Readme.md @@ -16,6 +16,11 @@ To see the visualisation Choose "Open VisB" in the visualisation menu, click on  +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): +``` +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)). @@ -23,4 +28,9 @@ Model taken from [TlaPlus Examples Repo](https://github.com/tlaplus/Examples/pul 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 +  + +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) +``` +probcli Einstein.tla -cbc all -visb_with_vars Einstein_tla.json out.html +``` \ No newline at end of file