====== Visualizing States ======

TLC model checker can dump generated states to a file in [[https://www.graphviz.org/doc/info/lang.html|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:
 - [[https://marketplace.visualstudio.com/items?itemName=tintinweb.graphviz-interactive-preview|Graphviz Interactive Preview]],
 - [[https://marketplace.visualstudio.com/items?itemName=EFanZh.graphviz-preview|Graphviz Preview]],
 - [[https://marketplace.visualstudio.com/items?itemName=joaompinto.vscode-graphviz|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 [[alygin/vscode-tlaplus/wiki/Settings|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.