Re: [tlaplus] Re: How to read the graph generated by TLC? Is there a way to specify its location?

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 16.12.2015 16:16, fl wrote:
> There is a demand obviously and if you can give use a TLAPLUS specification
> of your algorithm we can try to implement it using other tools using
> graphviz or another
> tool.

Hi Frederic,

I recently used graphviz to visualize the technical representation of
TLC's liveness graph (i.e. see [1] where the labels are
fingerprints/tableau ids). For a directed graph, I found though that
graphviz either doesn't handle more than a few dozen states or creates
an incomprehensible entangled mess (with its fast layout algorithm).

As for my prototype, there is no TLA+ specification or even an
implementation of a layout algorithm. It rather uses Eclipse Zest [2]
which implements similar algorithms to those in graphviz.

Besides the deficiencies of the graphing libraries, you will also have
to make TLC keep the actual states rather than fingerprints or you won't
be able to print the variable assignments (my prototype effectively
explores the state graph twice).

That said, you find the prototype's source code at Codeplex [3].


Does anybody know the number of states ProB's visualization can
realistically handle?

Cheers
Markus

[1]
http://tlaplus.codeplex.com/Download/AttachmentDownload.ashx?ProjectName=tlaplus&WorkItemId=8&FileAttachmentId=1441621
[2] https://www.eclipse.org/gef/zest/
[3] http://tlaplus.codeplex.com/SourceControl/latest