\in works, while \subseteq gives a "identifier undefined" error

Question

I have the following spec:

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

Init == members \subseteq People

Next == members' = members

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

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

(I simplified this spec to the point where it's not doing anything useful.)

When I try to run it through TLC, I get the following error:

In evaluation, the identifier members is either undefined or not an operator.

The error points to the Init line.

When I change the Init line to:

Init == members \in People

it validates fine.

I want the former functionality because I mean for members to be a collection of People, not a single person.

According to section 16.1.6 of Leslie Lamport's Specifying Systems, "TLA+ provides the following operators on sets:" and lists both \in and \subseteq.

Why is TLA+ not letting me use \subseteq?

Answer 1

While that is a valid TLA+ expression, TLC can only assign next-state values to a variable x by the statements x' = e or x' \in S. See section 14.2.6 for details. This holds for the initial assignment, too. In your case, you probably want members \in SUBSET People.