graph - TLA+ 如何可视化状态图

Question

我是新TLA+用户。我读到该TLA工具箱允许我们在模型检查完成后可视化状态图。

为此，我需要安装 dot 。但我不知道如何启动可视化。我可以使用 GUI 购买还是需要使用专用命令行？

谢谢

标签： graphvisualizationtla+tlc

Answer 1

要可视化状态图，您需要：

1. 在您的机器上安装Graphviz（您已经完成了）。
2. 将 配置TLA+ Toolbox为指向dot本地计算机上可执行文件的位置：首选项 → TLA+ 首选项 → PDF 查看器 → 指定点命令。（在我的机器上，我用自制软件安装了graphviz，我的命令是/usr/local/bin/dot）。
3. 在您的 TLC 模型中：附加 TLC 选项 → TLC 选项 → 模型检查完成后可视化状态图（选中此框）

当你运行你的模型时，会有一个State Graph带有状态图的 Graphviz 可视化的选项卡。