tla+ - \in 有效，而 \subseteq 给出“标识符未定义”错误

Question

我有以下规格：

------------------------------ MODULE Group ------------------------------
CONSTANTS People
VARIABLES members

Init == members \subseteq People

Next == members' = members

Group == Init /\ [][Next]_members

=============================================================================

（我将这个规范简化到它没有做任何有用的事情的地步。）

当我尝试通过 TLC 运行它时，我收到以下错误：

在评估中，标识符成员要么未定义，要么不是运算符。

错误指向该Init行。

当我将Init行更改为：

Init == members \in People

它验证得很好。

我想要前一个功能，因为我的意思是members成为一个人的集合，而不是一个人。

根据Leslie Lamport's Specifying Systems的第 16.1.6 节，“TLA+ 在集合上提供了以下运算符：”并列出了\in和\subseteq。

为什么 TLA+ 不让我使用\subseteq？

Answer 1

虽然这是一个有效的 TLA+ 表达式，但 TLC 只能x通过语句x' = e或将下一个状态值分配给变量x' \in S。有关详细信息，请参阅第 14.2.6 节。这也适用于初始分配。在你的情况下，你可能想要members \in SUBSET People.