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

*From*: gajera...@xxxxxxxxx*Date*: Wed, 29 Nov 2017 12:00:00 -0800 (PST)*References*: <0beeba20-4b93-456a-ac9f-063026f8e944@googlegroups.com> <9f416e0a-7394-41d6-8df2-9b993b945bc5@googlegroups.com>

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.

**References**:**Visualize state graphs in TLA toolbox***From:*gajera . . .

**Re: Visualize state graphs in TLA toolbox***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] Visualize state graphs in TLA toolbox** - Next by Date:
**Check that both branches are executed** - Previous by thread:
**Re: Visualize state graphs in TLA toolbox** - Next by thread:
**Re: [tlaplus] Visualize state graphs in TLA toolbox** - Index(es):