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

[Michael Leuschel <leus...@xxxxxxxxxxxxxxxxxxxxx>]

Hi Frederic,

On 17 Dec 2015, at 17:48, fl <freder...@xxxxxxxxxxx> wrote:

 

This one is impressive.

 

http://www.hpcwire.com/2013/11/16/sc13-research-highlight-large-graph-processing-without-overhead/

 

The software used to render the graph is not provided but it shows at least that large graphs

are not out of reach. (Wen you think it is supposed to represent "A Protein Interaction Map of

Drosophila melanogaster" (a fly then) you are definitely convinced that "There are more things in

heaven and earth,  Horatio,  // Than are dreamt of in your philosophy."  Hamlet (1.5.167-8)

—

Yes, that looks very impressive indeed.

Thanks to your posts, I have also found this link which also mentions the sfdp tool:

 http://stackoverflow.com/questions/13417411/laying-out-a-large-graph-with-graphviz

sdfp accepts dot files as input; so it could be used for Mark’s TLC visualization.

I have just updated ProB so that there is now the option to use sfdp instead of dot for rendering the state space.

It renders much faster for larger state spaces; but I am not really sure that it will be that useful for users yet. Probably one would have to add some custom colouring of the nodes, depending on some user-specified _expression_/property, to help a human make sense of the visualization.

I can publish some of the state space visualizations for TLC models on a website if you are interested (the size of the generated PDFs get larger; so I am not inclined to post them here on the mailing list).

Greetings,

Michael