TLA+如何可视化状态图

Question

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

为了做到这一点，需要安装点，我这样做了。但我不知道如何启动可视化。我可以使用GUI购买它吗?或者我需要使用专用的命令行？

谢谢

Answer 1

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

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

当您运行模型时，将有一个State Graph选项卡，其中包含状态图的Graphviz可视化。