Re: Visualize state graphs in TLA toolbox

[gajera...@xxxxxxxxx]

On Tuesday, November 28, 2017 at 5:54:27 PM UTC-8, Jared Summers wrote:
> On Tuesday, November 28, 2017 at 8:08:38 PM UTC-5, gaje...@xxxxxxxxx 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".

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.