Skip to content
Snippets Groups Projects
Commit 11dbd96e authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add comment on how to generate html export

parent a2176f1e
No related branches found
No related tags found
No related merge requests found
......@@ -16,6 +16,11 @@ To see the visualisation Choose "Open VisB" in the visualisation menu, click on
![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):
```
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)).
......@@ -24,3 +29,8 @@ Model taken from [TlaPlus Examples Repo](https://github.com/tlaplus/Examples/pul
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"
![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)
```
probcli Einstein.tla -cbc all -visb_with_vars Einstein_tla.json out.html
```
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment