TLA+ How to visualize the state graph

Question

I a new TLA+ user. I read that the TLA toolbox allows us to visualize the state graph after completion of model-checking.

In order to do so dot needs to be installed which I did. But I didn't figure out how to launch the visualization. Can I do it buy using the GUI or do I need to use a dedicated command line?

Thanks

Answer 1

To visualize the state graph, you'll need to:

1. Install Graphviz on your machine (which you've already done).
2. Configure the TLA+ Toolbox to point to the location of the dot executable on your local machine: Preferences → TLA+ Preferences → PDF Viewer → Specify dot command. (On my machine, I installed graphviz with homebrew, and my command is /usr/local/bin/dot).
3. In your TLC model: Additional TLC Options → TLC Options → Visualize state graph after completion of model checking (check this box)

When you run your model, there will be a State Graph tab with a Graphviz visualization of the state graph.