graphvisualizationtla+tlc

TLA+ How to visualize the state graph

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

Solution

  • 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.