问题标签 [tla+]

几天来，在各种情况下，我一直在 TLA+ 工具箱中遇到以下错误：

以下是我想出的最简单的模块，它将重现该问题。我已经看到一些提到被覆盖的值，但是我看不出我是如何在规范中做一些事情来导致这个问题的。

有没有人看到错误，或者可以解释我错过了什么？

将 TypeOK 设置为不变量时，出现完整错误

我正在为一个工作项目尝试 TLA+。我想证明尽管数据内部发生了一些变化，但使用相同的键获取数据将返回相同的数据。为此，我想将外部系统建模为一个黑匣子，其响应具有某些属性。例如：

然后我想编写自己的系统，TLA+ 将根据指定的假设推断行为。那可能吗？

我有一个规范，我试图定义一个 LRU 缓存系统，我遇到的一个问题是如何从结构键/值对（基本上是字典或哈希映射）中删除值其他语言）。

到目前为止，这是规范本身（不完整）：

我在 Learn TLA Plus 网站上引用了此文档，但似乎没有从列表中删除键值对。到目前为止，我唯一能想到的就是过滤掉与键匹配的值并创建一个新的字典对象，但我更喜欢一种更直接访问的方法。

我正在从这个很棒的“学习 TLA+”页面学习 TLA+。

我无法得到和之间的实际区别。我从“真值表”的角度得到它，但我无法真正掌握它。=><=>

有人可以提供一个实用的 TLA+ 示例来突出这两者之间的区别吗？

有关的：

• https://math.stackexchange.com/questions/68293/what-is-the-difference-between-only-if-and-iff

变量state代表系统的状态，例如state \in {"ready", "prepare", "do", "cleanup", "done"}。如何表达state最终应该通过所有五个状态（以任何顺序）的条件？

工作示例（接受的答案）：

程序可以从 START 分支到 LEFT 或 RIGHT 分支。如何检查是否存在 LEFT 分支的执行路径和 RIGHT 分支的其他执行路径？

我有两套：

我想生成以下一组对：

在每个集合中，第一个元素来自 X，第二个元素来自 Y。X 可以重复，Y 不能。怎么做？

我现在正在检查指定系统，我对如何对以下模块进行模型检查感到有些困惑：

我看到Init和BNext公式都是运算符，由q. 我如何将它提供给模型检查器？

给定一个序列 S = <<1,2,3,4>> 和一个集合 S' = {1,2,3,4,5,6}。我们如何检查它们是否在 TLA+ 中包含相同的值？

我有两个规格：System 和 SystemMC。系统规范是我指定的系统的“好”规范，对文档很有用。它定义了一个 CONSTANT MessyAction(_) （在我正在编写的实际规范中，一个散列函数），以一种有效的模型可检查方式指定它是混乱的，因此会降低规范的可读性。我在 SystemMC 规范中实现了 MessyAction(_)，所以我可以对系统规范进行模型检查。但是，解析器在 SystemMC 规范中给出了以下错误：

实例化模块“System”中的级别错误：替换“MessyAction”的表达式或运算符的级别最多只能为 0。

这个错误是什么意思，我怎样才能在不添加一堆针对 TLC 优化的东西的情况下实现模型检查系统规范的目标？这是系统规格：

这是 SystemMC 规范：