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.