【发布时间】：2019-02-02 23:02:39
【问题描述】：
我是一个新的TLA+ 用户。
我读到TLA 工具箱允许我们在模型检查完成后可视化状态图。
为此，我需要安装 dot。 但我不知道如何启动可视化。 我可以使用 GUI 购买还是需要使用专用命令行？
谢谢
【问题讨论】：
标签： graph visualization tla+ tlc
【发布时间】：2019-02-02 23:02:39
【问题描述】：
要可视化状态图，您需要：
- 在您的机器上安装Graphviz（您已经完成了）。
- 将
TLA+ Toolbox配置为指向本地计算机上的dot可执行文件的位置：首选项 → TLA+ 首选项 → PDF 查看器 → 指定点命令。 （在我的机器上，我用自制软件安装了graphviz，我的命令是/usr/local/bin/dot）。 - 在您的 TLC 模型中：附加 TLC 选项 → TLC 选项 → 模型检查完成后可视化状态图（选中此框）
当您运行模型时，将出现一个 State Graph 选项卡，其中包含状态图的 Graphviz 可视化。
【讨论】：