我有一个 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 行，Y 行到 Z 行，模块组的 T 行
...指向Next.
我相信我Next的写得很好，因为这是一个与Next我的非常相似的示例模型：https ://github.com/tlaplus/Examples/blob/master/specifications/aba-asyn-byz/aba_asyn_byz.tla#L110
此外，Leslie Lamport指定系统的第 14.2.2 节说：
只有当表达式等于有限集[...]时，TLC 才能评估集值表达式。只有当 TLC 可以枚举集合S时，TLC 才会评估以下形式的表达式：
并提供“ S中存在x使得p ”的例子。
我该如何解决这个错误？