\in works, while \subseteq gives a “identifier undefined” error

[Philip White <phi...@xxxxxxxxxxxxx>]

Hello,

I wrote about my problem on Stack Overflow[1], but I’m not sure how well that’s used by TLA+ enthusiasts, so I want to reproduce my question here.

I have the following simplified spec:

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

Init == members \subseteq People

Next == members' = members

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

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

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?

Thank you.

1: https://stackoverflow.com/questions/53426052/in-works-while-subseteq-gives-a-identifier-undefined-error

— 
Philip