# Re: [tlaplus] \in works, while \subseteq gives a “identifier undefined” error

Hello,

both \in and \subseteq are valid TLA+ operators. However, when TLC evaluates the initial condition of a specification, it interprets the first formula (in left-to-right order) of the form

x = e    or    x \in S

(where x is a variable and e is a state-level expression) as a deterministic, respectively non-deterministic assignment to the variable x. In other words, it generates an initial state in which x is set to the value of e, respectively one initial state per element of the set S. An analogous convention applies to interpreting formulas x' = e and x' \in S that appear in the next-state relation.

members \subseteq People

is interpreted as a regular state predicate, and its evaluation fails because the variable "members" has not yet been assigned a value, as stated by the TLC error message. You want to write

members \in SUBSET People

which is semantically equivalent to your formula but follows the syntactic shape of a non-deterministic assignment.

Hope this helps,
Stephan

> On 22 Nov 2018, at 09:11, Philip White <phi...@xxxxxxxxxxxxx> wrote:
>
> 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
>
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.



• Follow-Ups: