Re: Visualize state graphs in TLA toolbox

[gajera...@xxxxxxxxx]

On Tuesday, November 28, 2017 at 8:31:45 PM UTC-8, Leslie Lamport wrote:
> 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.
> 
> 
> On Tuesday, November 28, 2017 at 5:08:38 PM UTC-8, gajerashirish 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"
> 
> 2) I don't see any State Graph preference page in File/Preferences menu in my toolbox.

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.