Visualize state graphs in TLA toolbox

[gajera...@gmail.com]

Hi there,

I want to see the graph of distinct state basically when I click on column header after running the model checking. So, I was going through this document
https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/advanced-page.html
"In order to visualize a state graph, the path to the dot executable of the GraphViz project has to be set on the State Graph preference page on the File/Preferences menu".

I download GraphViz (https://graphviz.gitlab.io/_pages/Download/Download_windows.html), but I have 2 problems
1) I don't know what this means "dot executable of the GraphViz project"
2) I don't see any State Graph preference page in File/Preferences menu in my toolbox.

[Jared Summers]

On Tuesday, November 28, 2017 at 8:08:38 PM UTC-5, gajera...@gmail.com wrote:

Hi there,

I want to see the graph of distinct state basically when I click on column header after running the model checking. So, I was going through this document
https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/advanced-page.html
"In order to visualize a state graph, the path to the dot executable of the GraphViz project has to be set on the State Graph preference page on the File/Preferences menu".

I download GraphViz (https://graphviz.gitlab.io/_pages/Download/Download_windows.html), but I have 2 problems
1) I don't know what this means "dot executable of the GraphViz project"

The GraphViz installation will include an exe called "dot.exe". I don't have Windows to test this on, but I'd expect it to be located somewhere like "C:\Program Files\GraphViz\bin".

 

2) I don't see any State Graph preference page in File/Preferences menu in my toolbox.

I'm not sure about this one. I can find a "Specify dot command" option: Go into File/Preferences. Expand "TLA+ Preferences"  and then select "PDF Viewer". It's located here. This may be what you need. Put the path to the executable here, your field will contain something like:

  C:\Program Files\GraphViz\bin\dot.exe

Though no mention of "State Graph".

If you add the GraphViz\bin directory to your system's path variable, then you should just need to put in "dot.exe" or perhaps just "dot".

[gajera...@gmail.com]

Thanks Jared.
Did everything you told, restarted toolbox, ran model and when I click on Distinct State or States found header column, still not showing anything.

[Leslie Lamport]

You seem to be confusing two different things:

   (a) the state graph, which is displayed after model checking is complete if you checked
       the appropriate box in the TLC options section of the Advanced Model page before
       running the model checker.

   (b) The graph of the number of states found versus time which is displayed, and continually
       updated while the model checker is running, if you click on the appropriate column
       header in the Statistics section of the Model Checking Results page.  It is the graphical
       representation of the data in the chosen statistics column, and it will be invisible unless
       there are at least two items in that column.     

If either of those two is not properly displayed, explain what you did, what you expected to see, and what you did see.

[Markus Alexander Kuppe]

On 29.11.2017 01:54, gajera...@gmail.com wrote:
> 2) I don't see any State Graph preference page in File/Preferences menu in my toolbox.

Hi Shirish,

the current documentation is indeed incorrect. There used to be a "State
Graph" preference page but it was eventually merged into the "PDF
Viewer" page.

The corrected documentation can be found on-line [1] and will be part of
the next Toolbox release.

Thanks

Markus

[1]
https://tla.msr-inria.inria.fr/tlatoolbox/ci/doc/model/advanced-page.html   

[sglaser.com]

1) I don't know what this means "dot executable of the GraphViz project”

“dot" is one of the executables supplied by graphviz. It will be located in the bin directory of the installation.

• dot - makes ``hierarchical’’ or layered drawings of directed graphs. The layout algorithm aims edges in the same direction (top to bottom, or left to right) and then attempts to avoid edge crossings and reduce edge length.

---

Steve Glaser
sgl...@sglaser.com

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

[gajera...@gmail.com]

Yes, you are right I was confusing 1 and 2 as you mentioned when I checked "Visualize state graph after completing of model checking" in Advance option I start getting graph for all States. Thanks.

[gajera...@gmail.com]

Thanks Markus