Differences

This shows you the differences between two versions of the page.

--- using:generating_state_graphs [2024/09/28 15:58] – created - external edit 127.0.0.1
+++ using:generating_state_graphs [2025/02/18 13:01] (current) – fponzi
@@ Line 1: / Line 1: @@
-====== Generating stage graphs ======
+====== Generating state graphs to visualize the state space ======
 TLC support the generation of a dot file that can be used to visualize the state space.
@@ Line 9: / Line 9: @@
 </code>
-then visualize the graph: * http://www.webgraphviz.com/ * From CLI: ''%%dot -Tps filename.dot -o outfile.ps%%''
+then visualize the graph:
+  * http://www.webgraphviz.com/
+  * From CLI: ''%%dot -Tps filename.dot -o outfile.ps%%''
 If the state graph is large, you can try to visualize it using:
-  * https:%%//%%cytoscape.org/index.html
+  * https://cytoscape.org/index.html
-  * https:%%//%%gephi.org/
+  * https://gephi.org/
 If you use intellij, there is a plugin to visualize/edit .dot files in the ide.
-From the TLA+ Toolbox:
+===== From the TLA+ Toolbox: =====
 if dot is not installed in the standard path, please adjust the dot path in the Toolbox’s preferences (File > Preferences > TLA+ Preferences > PDF Viewer > Specify dot command). Afterwards check “Visualize state graph after completion of model checking” before you run model-checking on the “Advanced Options” page of the model editor (see attached screenshot). The Toolbox will then add a tab to the model editor showing the state graph once model checking has completed.