[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

dot/graphviz visualization for TLC


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]).


[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