Hello Markus,
Thank You for the enhancement!
I am certain that this feature is useful for sw-engineers, such as I, who are
not that familiar with the concept of "non-determinism" :)
BR,
Jukka
On Tuesday, January 5, 2016 at 12:43:35 PM UTC+2, Markus Alexander Kuppe wrote:
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