[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


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 ------------------------------

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