From 11dbd96e1d4a57cb2cb636604f7b18b9f094a5e1 Mon Sep 17 00:00:00 2001 From: Michael Leuschel <leuschel@uni-duesseldorf.de> Date: Mon, 22 Mar 2021 10:26:31 +0100 Subject: [PATCH] add comment on how to generate html export --- Einstein/Readme.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/Einstein/Readme.md b/Einstein/Readme.md index 7541a3e..408c253 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 -- GitLab