我是一个新的 TLA+ 用户。 我看到 TLA 工具箱可以在模型检查完成后可视化状态图。 为了实现这一点，需要安装 dot，我已经安装好了。 但我没有弄清楚如何启动可视化。 我可以使用 GUI 进行吗，还是需要使用专用的命令行？ 谢谢

我正在使用VS Code和vscode-tlaplus插件来学习TLA+，而不是TLA+工具箱。现在我有一个TLA文件，在其中定义了一些常量：---- MODULE test ---- EXTENDS TLC, Integers, Sequences CONSTANTS Capacity, ...

我想翻译一些在TLA中指定的动作，这些动作与Erlang有关。您是否能想到任何直接在Erlang中完成此操作或可用于此类操作的框架的自然方法？简而言之（非常简洁），TLA操作是变量的条件，其中一些是带撇号的，表示它们代表下一个状态中变量的值。例如： Action(x,y,z) -> ...

我正在撰写我的硕士论文，需要在时间逻辑中说明和验证我的方法。 在我的情况下，哪种时间逻辑最好使用？我真的希望能得到关于我的方法和如何继续的反馈。 我的模型由参与者组成，将同时执行。对于每个参与者，可以注册规则。它们看起来像这样： conditions -> action 例如。...