Hi, by popular demand and inspired by Jarjuk's patch, the newest CI builds [1] comes with support to write the dump file in dot format [2]. Attached is an SVG that shows the state space for the OneBit protocol taken from section 7.7 of the Hyperbook. To make TLC write the .dot file (from which PNGs, SVGs, ... can be manually generated), add "-dump dot /path/where/dotfile/should/be/created" to the "TLC command line parameters" on the Advanced Options page of the Toolbox. Afterwards, run dot [3] on the resulting .dot file. Once we developed a feeling for how useful this feature really is, the next step would be to integrate direct visualization support into the Toolbox (based on EclipseGraphviz [4]). Cheers Markus [1] http://tla.msr-inria.inria.fr/tlatoolbox/ci/products/ [2] https://en.wikipedia.org/wiki/DOT_(graph_description_language) [3] http://www.graphviz.org/Download.php [4] https://github.com/abstratt/eclipsegraphviz
Attachment:
obm.svg
Description: image/svg