问题标签 [tla+]

我知道决策树和不变量是什么（如果这是正确的术语）。使用的所有其他定义（UsingTor,UsingProxy等可以是任何东西）。如何使用 TLA+ 检查决策树的每个叶子是否满足不变量？

如果决策树是一系列状态，我会知道如何做到这一点：我会检查它是否总是以满足这个不变量的状态结束。不知道如何做到这一点。

假设我有一组简单的顺序操作（我将首先强制定义）：

也就是说，我们有一个棋子a并在 position 开始1。然后我们依次将它移动到 3，然后到 5，然后是 4，然后是 2。每一步一次。

您如何使用 TLA+ 来定义它？试图围绕如何在 TLA+中指定复杂的命令式动作序列。

我有以下队列规范：

当我使用以下常量值运行 TLC 时：

还有这些限制：

它报告这些错误：

但是规范允许 中的值(0 .. L)，那么为什么 TLC 报告q=1, q=2, q=3,q=4作为无效状态？

错误跟踪输出如下：

一个人应该如何识别那些被认为是错误的和那些不是来自这个跟踪的？界面不显示红灯q=0。

考虑一下我有一组节点的情况，我想对它们声明一些排序。最简单的方法是将节点集及其排名声明为常量：

现在是时候为这些常量分配模型值了。Node很简单，我只是将它定义为工具箱中的一组模型值：

NodeRank我尝试用普通作业做类似的事情：

但是，当我运行 TLC 时，这些ASSUME语句被违反了。进一步检查表明这是因为在普通赋值中NodeRank,n1和n2被视为字符串而不是模型值。这是有道理的，因为这是定义记录的常用方法（使用字符串作为域）。我如何定义NodeRank它以使用n1和n2模型值作为其域？

在我的模块中，我试图代表外部 API 的行为（它可能以 200 HTTP 状态或 4XX/5XX HTTP 状态响应；这意味着它有 2 种可能的状态相对于我的系统 => 成功或失败）。

简而言之，我应该如何描述我的系统使用的外部 API，以及它应该根据 API 的响应（成功或失败）做出可预测的反应？（我多久收到一次成功/失败的响应；我不知道，这是“随机的”）

我正在尝试在 TLA+ 中模拟David Gries 的咖啡罐问题，但我被困在这一部分：

“你能说最后剩下的豆子的颜色与最初在罐头里的黑豆和白豆的数量有关吗？”

我不知道如何处理这个问题。您能否提供一些建议或提示？（也欢迎提供方法）

这是我在 TLA+ 中的代码：

在我的规范中，我试图检查序列中的变化是 -1、0 还是 1。

我将这个不变量描述如下：

TLC 模型检查器输出以下内容：

实际上，我想{"1", "2", "3", ..., "N"}从集合中构建一个1..N集合。如何将数字转换为字符串？

给定集合，例如 {1, 2, 4, 10, 6} 我怎样才能将元素 4 获取到变量 var。我想要的是从集合中获取元素“4”到变量 var: var = 4 并从集合中删除元素 4：set = {1, 2, 10, 6}

语言 TLA+ 使用范围作为其运算符优先级（参见指定系统[ PDF ]一书中第 271 页的表格）。引用：

如果两个运算符的范围重叠，则它们的相对优先级是未指定的。

例如，$运算符（优先级 9-13）与+运算符（优先级 10-10）冲突，但与<运算符（优先级 5-5）不冲突。

运算符优先级范围是正式语言中常用的甚至是预先存在的概念吗？我通过一些搜索在网上找不到任何关于此的信息。是否有用于解析这种优先方案或将该方案转换为标准单值优先方案的算法？是否有任何解析器生成器处理运算符优先级范围？与单值优先级相比，通过这种方法可以获得什么？