TLA+ 如何可视化状态图

Question

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

为此，需要安装 dot，我就是这样做的。但我没有弄清楚如何启动可视化。我可以使用 GUI 购买还是需要使用专用命令行？

谢谢

Answer 1

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

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

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