Visualizing States

This page was moved to https://docs.tlapl.us/using:vscode:visualizing_states

---

TLC model checker can dump generated states to a file in DOT notation. Such .dot files can be visualized as graphs right in VS Code with the help of additional extensions. Here're the most popular of them:

• Graphviz Interactive Preview,
• Graphviz Preview,
• Graphviz (dot) language support for Visual Studio Code.

To generate .dot files while running model checking, add -dump dot file_name.dot TLC option in the extension settings. Setting variables usually come handy here — one can provide -dump dot ${modelName}.dot as a TLC option to automatically generate the resulting .dot file name based on the model being checked.