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 threw an unexpected exception. This was probably caused by an error in the spec or model. See the User Output or TLC Console for clues to what happened. The exception was a java.lang.RuntimeException : TLC cannot handle this conjunct of the spec: line X, col Y to line Z, col T of module Group

...指向Next的全部内容。

我相信我的 Next 写得很好，因为这里有一个与我的 Next 非常相似的示例模型：https://github.com/tlaplus/Examples/blob/master/specifications/aba-asyn-byz/aba_asyn_byz.tla#L110

此外，Leslie Lamport's Specifying Systems 的第 14.2.2 节说：

TLC can evaluate a set-valued expression only if that expression equals a finite set[...]. TLC will evaluate expressions of the following forms only if it can enumerate the set S:

并提供了"there exists x in S such that p"的例子。

如何解决这个错误？

Answer 1

问题出在我在 Init 中使用 \subseteq，如这里的回答：

TLC 无法处理规范的这种结合

TLC cannot handle this conjunct of the spec

tla+

tlc