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

[Stephan Merz <stepha...@xxxxxxxxx>]

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.

Your formula

  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.