TLC不能处理规范的这种连接。

Question

我有一个TLA+模块，概括起来如下：

--- MODULE Group ---

CONSTANTS People
VARIABLES members

Join(person) == ...
Leave(person) == ...

Init == members \subseteq People

Next == \E p \in People :
            \/ Join(p)
            \/ Leave(p)

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

当我尝试用TLC进行模型检查时，我会得到以下错误：

TLC抛出了一个意想不到的异常。这可能是由规范或模型中的错误引起的。请参阅用户输出或TLC控制台，以了解发生了什么。例外情况是，java.lang.RuntimeException : TLC无法处理规范的连接: X行，col到模块组的Z，col行。

...pointing到Next的整个内容。

我相信我的Next写得很好，因为这里有一个与我的Next非常相似的示例模型：byz.tla#L110

此外，Leslie Lamport's 第14.2.2节指出：

只有当集合值表达式等于有限集时，TLC才能计算该表达式.只有当TLC能够枚举集合S时，TLC才会计算下列表单的表达式：

并给出了“S中存在x，使得p”的例子。

如何解决这个错误？

Answer 1

问题在于我在Init中使用了Init，如下所示：\in works, while \subseteq gives a "identifier undefined" error