问题标签 [tla+]

是否可以检查模型中的每个合法状态是否已达到？如果可能的话，该属性应该如何写？

考虑下面调制 24 小时时钟的模块。我可以检查它hour是否处于非法状态，即它在 0 到 23 之间。但是如果我写了一个错误的Next谓词，例如hour' = (hour + 1) % 23，不是所有状态都达到了，但属性不会捕获这个错误。

我最近正在阅读“指定系统”一书。在第 5 章中，Leslie 定义了常量运算符 Send( , , , )。

我对如何为这个常量表达式赋值（真/假）感到困惑？我们是否需要为 TLC 模型检查器中的每个 (p, v, m, m') 分配真/假？

我有一个类似于以下的 TLA+ 规范：

而且我想Items是对称的，并从中选择一个元素Items并将其存储到item.

我一直在使用item = CHOOSE x \in Items: TRUE，但我了解到这会破坏项目的对称性：TLC 将始终从集合中选择第一个项目。

我想以保持对称的方式选择一个项目，以允许 TLC 探索所有状态。我不在乎我们选择了哪个项目——只要它是一个，并且它来自Items. （以后，我item需要\in Items.

虽然我更喜欢item成为单个元素，但item作为一组基数 1 也可以，所以稍后我可以检查\subseteq Items.

建议我替换CHOOSE为{x \in Items: TRUE}以保持对称性并使结果为\subseteq Items，但这不会将结果集限制为基数 1。

有没有办法让 TLA+ 从一组对称的值中给我一个项目或一组基数 1？

浏览此处主要显示了操作规范的简单示例，您可以在其中使用 引用下一个状态'，如下所示：

例如，/\ nCrashed' = nCrashed是一个逻辑语句“...AND next(nCrashed) == this(nCrashed)`。所以基本上，上述函数将一些变量设置为“处于下一个状态”。但这一切基本上都是一步完成的（至少在逻辑上）。

我想知道的是如何定义在多个步骤中发生的事情。说 10 步。

所以“在第三个状态之前，baz 会被设置为 bar 在第二个状态加一”。类似的东西。但这没有任何意义。在命令式语言中，您只需执行以下操作：

但这是有道理的，因为每个函数调用都发生在前一个函数调用之后。但我不知道如何在 TLA+ 中表示这一点。

想知道你应该如何完成在动作的时间逻辑+中需要不止一步的事情。另一个例子是while循环。

我有这个玩具示例，出于某种原因，从未断言过任何时间属性。即使是荒谬的，[](h = 123456)也不会失败 TLC。我不明白什么？

介绍.tla

介绍.cfg

tlc介绍

我使用 PlusCal 来模拟一个接受与正则表达式匹配的字符串的普通状态机(X*)(Y)。

即使我已经标记了 algorithm fair，以下时间条件由于口吃而失败......模型检查器允许状态机吸收 anX然后简单地停止Loop而不再做任何其他事情的情况。

在这样一个简单过程的背景下，公平实际上意味着什么？有没有办法告诉模型检查器状态机永远不会用完输入，因此总是会终止？

我正在对 TLA+ 中的主备份协议进行建模，并将复制配置放在一个元组中。一些设置 TLA+：

然后，在 Pluscal 算法中：

我有一个进程将 health 中的值设置为FALSE，并且想要另一个进程根据health是否为 FALSE从config中删除条目，同时保留config中剩余条目的顺序。

如果config是一个集合，删除不健康的条目将是微不足道的，但我正在寻找一种用元组来做到这一点的好方法。我可以在循环中使用Append，但这会导致 TLC 处理许多额外的状态。TLA+ 或 Pluscal 有什么更好的方法吗？

理想情况下，该解决方案不会假设 config 中的条目以排序顺序开始，但我可以解决这个限制。

我正在尝试 TLA+ 的定理证明工具来证明算法的安全性。但我发现 TLAPS 无法计算出非常“简单”的数学事实。

我的第一个问题是：

TLAPS 不能单独使用任何后端证明者来完成。我还尝试使用特定的后端证明者和其他策略：

但也失败了。类似地，不能检查其他类型的简单事实，例如：

我过去使用过一些后端定理证明器，例如 Z Solver 或 Isabelle，据我所知，它们非常强大。我想我在这里遗漏了一些东西......或者我不理解 TLAPS 证明组织者，或者我仍然需要加载一些带有公理的其他模块？

假设以下内容不正确

也就是有一些不满足Spec的行为表现出来[]P。我如何在 TLA+ 中表达这一点？

如果我使用简单的否定，我最终得到

然而，这个定理也有可能是不正确的！特别是，即使有一些行为不满足Spec，[]P也可能有一些行为满足，并且这种行为会反驳这个新定理。

是否有某种方式来表达“这个定理对于某些行为是不正确的”的想法，即对行为进行量化？

编辑：在考虑了我所要求的确切性质之后，我真的在问是否有一种[]P独立于注释的方法Spec？

我在证明涉及记录的细化映射时遇到了一些困难。下面是TLA 规范@github 的简化说明（请注意，这篇文章也在tlaplus-googlegroup 中，还没有回复。）：

SimpleVoting.tla:

它为每个参与者维护maxBal一个自然数。在IncreaseMaxBal(p, b)，maxBal[p]被增加到一个更大的值b。

Record.tla:

它维护一个二维“数组” state，其中state[p][q]是q从视图的状态，p而状态是记录： State == [maxBal : Nat, maxVBal : Nat]。

在Prepare(p, b)，state[p][p].maxBal被增加到一个更大的值b。

直观地，Record维持as 。因此，我想在以下细化映射下显示细化：maxBal[p]SimpleVotingstate[p][p].maxBalRecordSimpleVoting

但是，<3>2以下证明中的步骤失败。

义务<3>2如下。假设中的不state' = [state EXCEPT ![p] = ...]与结论相同[p_1 \in Participant |-> state[p_1][p_1].maxBal]' ...吗？什么不见​​了？我的证明有什么问题？