dot/graphviz visualization for TLC

[Markus Alexander Kuppe]

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

[fl]

Once we developed a feeling for how useful this feature really is,

Can you give us the algorithm you use. Tlaplus+ comments
is good choice (Reading the code is not a goog one).

Having the algorithm will give us the ability to make sense of
all that and to develop the feeling required above.

--
FL

[Markus Alexander Kuppe]

On 06.01.2016 19:59, fl wrote:
> Can you give us the algorithm you use. Tlaplus+ comments
> is good choice (Reading the code is not a goog one).
>
> Having the algorithm will give us the ability to make sense of
> all that and to develop the feeling required above.

Hi Frederic,

there is no algorithm to study. The feature simply extends TLC's "-dump"
command and makes it output states in dot format [1] (instead of the
default TLA+ format). The dot output can then be fed into GraphViz [2]
which renders it to a graph.

Cheers
Markus

[1] https://en.wikipedia.org/wiki/DOT_(graph_description_language)
[2] http://www.graphviz.org/

[jarjuk]

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