[SOLVED] TLC cannot handle this conjunct of the spec

TLC cannot handle this conjunct of the spec

I have a TLA+ module, which, summarized, looks like this:

--- MODULE Group ---

CONSTANTS People
VARIABLES members

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

Init == members \subseteq People

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

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

When I try to model-check this with TLC, I get the following error:

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

...pointing to the entire content of Next.

I believe my Next is well-written, because here's an example model that has a very similar Next to mine: https://github.com/tlaplus/Examples/blob/master/specifications/aba-asyn-byz/aba_asyn_byz.tla#L110

Also, section 14.2.2 of Leslie Lamport's Specifying Systems says:

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:

and provides the example of "there exists x in S such that p".

How can I solve this error?

Solution