-
Notifications
You must be signed in to change notification settings - Fork 30
Visualizing States
Andrew Lygin edited this page Feb 13, 2021
·
2 revisions
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.