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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Tue, 28 Nov 2017 20:31:45 -0800 (PST)*References*: <0beeba20-4b93-456a-ac9f-063026f8e944@googlegroups.com>

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.

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.

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_ ), but I have 2 problemswindows.html

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.

**Follow-Ups**:**Re: Visualize state graphs in TLA toolbox***From:*gajera . . .

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

- Prev by Date:
**Re: Visualize state graphs in TLA toolbox** - Next by Date:
**Re: [tlaplus] Visualize state graphs in TLA toolbox** - Previous by thread:
**Re: Visualize state graphs in TLA toolbox** - Next by thread:
**Re: Visualize state graphs in TLA toolbox** - Index(es):