0

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

CONSTANT Items
VARIABLE item

而且我想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？

4

1 回答 1

0

自从发布问题以来，我对 TLA+/TLC 有了更多了解，这是我的答案：

要简单地从初始谓词中的对称集中选择一个元素：

item \in Items

或在一个动作中：

item' \in Items

如果您想选择一个与谓词匹配的项目，如您可以使用 CHOOSE 指定的那样，那么这是替代方法：

item \in {x \in Items: P(x)}

这将形成与谓词匹配的项目子集，然后选择其中的一个元素。

这里有一些数据显示了这种语法和 CHOOSE 之间的区别。考虑这个模块：

----------------------------- MODULE ChooseDemo -----------------------------
CONSTANT Items
VARIABLE item

TypeInvariant == item \in Items

Init == item = CHOOSE x \in Items: TRUE

Next == item' \in {x \in Items: x /= item}
=============================================================================

当Items有三个项目：

  • 不是对称集：TLC 找到 1 个初始状态和总共 7 个（3 个不同的）状态。
  • 对称集：TLC 找到 1 个初始状态和总共 3 个（1 个不同的）状态。

现在考虑这个模块：

--------------------------- MODULE SetFormingDemo ---------------------------
CONSTANT Items
VARIABLE item

TypeInvariant == item \in Items

Init == item \in {x \in Items: TRUE}

Next == item' \in {x \in Items: x /= item}
=============================================================================

当Items有三个项目：

  • 不是对称集：TLC 找到 3 个（3 个不同的）初始状态和总共 9 个（3 个不同的）状态。
  • 对称集：TLC 找到 3（1 个不同）初始状态和总共 5（1 个不同）状态。

因此，通过使用集合形成语法，TLC 比使用 CHOOSE 找到更多的状态。

于 2019-02-18T23:38:52.847 回答