[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] How to visualize the state graph?

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? 



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].


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

Attachment: Diehard.tla
Description: Binary data

Attachment: Model_1.dot
Description: MS-Word document