-
Notifications
You must be signed in to change notification settings - Fork 36
Visualizing States
Andrew Lygin edited this page Feb 13, 2021
·
3 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:
- Graphviz Interactive Preview,
- Graphviz Preview,
- Graphviz (dot) language support for Visual Studio Code
to name a few.
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.