问题标签 [tla+]

我想写一个这样的（a）公式：

但每次我尝试运行模型时，我都会收到错误消息，«在评估中，标识符 x 要么未定义，要么不是运算符。»

到底是怎么回事？这样的公式真的不能写吗？为什么？我该如何解决这个问题？

谢谢。

我想运行Raft 的 TLA+ 实现，所以我构建了一个新模块，并设置如下：

但是，TLC 会产生很多状态，而且似乎永远不会停止。

根据Lamport 的 Lecture 09，我想到也许我应该限制 和其他一些变量的长度。messages

所以我将以下代码添加到“状态约束”

但是，它现在会引发以下错误

我对此感到困惑。我的问题是如何在 Raft 的 TLA Spec 上正确运行 TLC？

---更新--- 我在问题 1中找到了一个配置

但是，我不知道如何使用它，因为我没有诸如此类的定义TermConstraint。

我一直在学习这门课程https://learntla.com/introduction/example/但是我在运行模型时遇到了困难。它根本不产生任何状态

版本 TLA+ = 1.8

这是控制台输出

这是模型

我不明白为什么选择“无行为规范”。选项列表中没有任何其他内容。然而，该课程选择“时间公式”。我在哪里可以找到该选项？

TLA+ 工具箱创建了大量文件和目录。使用规范和模型并将它们保持在 git 中的版本以及使用工具箱的好方法是什么？正常的工作流程是什么样的？

假设我们在tools.tla文件中有这些运算符：

我们想传递值（如python等编程语言中的参数）并在另一个文件中使用它们，调用它use.tla，只使用Max和Min而不重新实现它们；这怎么可能？