How to visualize the state graph?

[Rachel Delafon]

Hi, 

I a new TLA+ user. I read that the TLA toolbox allows us to visualize the state graph after completion of model-checking.

In order to do so dot needs to be installed which I did. But I didn't figure out how to launch the visualization. Can I do it buy using the GUI or do I need to use a dedicated command line?

Thanks

Rachel

[Markus Kuppe]

On 28.08.2018 05:54, Rachel Delafon wrote:

I a new TLA+ user. I read that the TLA toolbox allows us to visualize the state graph after completion of model-checking.

In order to do so dot needs to be installed which I did. But I didn't figure out how to launch the visualization. Can I do it buy using the GUI or do I need to use a dedicated command line?

Hi Rachel,

if dot is not installed in the standard path, please adjust the dot path in the Toolbox's preferences (File > Preferences > TLA+ Preferences > PDF Viewer > Specify dot command). Afterwards check "Visualize state graph after completion of model checking" before you run model-checking on the "Advanced Options" page of the model editor (see attached screenshot). The Toolbox will then add a tab to the model editor showing the state graph once model checking has completed.

Note that the visualization is only useful for small state spaces. For larger ones, the dot rendering will timeout. In this case you can try to render the dot output file manually on the command line with a different dot settings, i.e. layout. The dot file is found in the model subdirectory of your specification.

Thanks

Markus

[Rachel Delafon]

Hi Markus, 

Thank you very much for your answer. 

I feel embarrassed  for annoying you with such a silly question. I thought I've checked all the tabs/pages... Apparently not!

Even though my model state space is too big to be visualised (as you anticipated it), I've simplified it and now I have a nice graph to analyse.

Thanks 

    

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Markus Kuppe]

On 28.08.2018 11:31, Rachel Delafon wrote:
> Thank you very much for your answer. 
> I feel embarrassed  for annoying you with such a silly question. I
> thought I've checked all the tabs/pages... Apparently not!
> Even though my model state space is too big to be visualised (as you
> anticipated it), I've simplified it and now I have a nice graph to analyse.

Hi Rachel,

for larger state spaces you might want to experiment with Cytospace [1]
or Gephi [2]. For Cytospace you have to "massage" TLC's dot output first
though [3].

Thanks
Markus

[1] http://cytoscape.org/index.html
[2] https://gephi.org/
[3] https://github.com/idekerlab/dot-app/issues/16

[Rachel Delafon]

Hi Markus, 

that sounds really interesting! 

Thanks  for those valuable inputs.

Rachel

[Alen]

Hi Markus, 

I met some questions when using Gephi to open the dot output. It cannot recognize some edges in the file. So the graph it shows is totally different from toolbox graph. Here is the spec (from the hyperbook) and the dot output I used. Is it necessary to modify the file before I use it? 

Thanks

Alen

[Markus Kuppe]

On 07.11.18 00:05, Alen wrote:
> I met some questions when using Gephi to open the dot output. It cannot
> recognize some edges in the file. So the graph it shows is totally
> different from toolbox graph. Here is the spec (from the hyperbook) and
> the dot output I used. Is it necessary to modify the file before I use it? 

Hi Alen,

can you try with the most recent Toolbox build [1]? Commits [2][3]
addresses incompatibilities with external viewers. You might also want
to try Cytoscape's [4] dot import [5] which recently fixed an important
bug [6].

Thanks
Markus

[1] https://tla.msr-inria.inria.fr/tlatoolbox/ci/products/
[2]
https://github.com/tlaplus/tlaplus/commit/0487bcc992e7011d378c35c05ef947e69c8460e5
[3]
https://github.com/tlaplus/tlaplus/commit/50e83b357ff7251d42527fc2e2478bc4a179843c
[4] https://cytoscape.org/
[5] http://apps.cytoscape.org/apps/dotapp
[6] https://github.com/idekerlab/dot-app/issues/16