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

[Philip White]

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

[Stephan Merz]

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

> --
> 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...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Philip White]

Stephan, thank you for the reply.

It sounds like you're saying that TLA+/TLC interprets "\in" as an assignment, while it interprets "\subseteq" as a regular state predicate (non-assignment).

So to make my initial condition work, I need to find an expression in the form of "=" or "\in", hence what you suggested with "\in SUBSET".

Do I have it right?

Is this distinction documented anywhere?

Thanks.

[Leslie Lamport]

Chapter 14 of Specifying Systems explains how TLC works and what kind of specifications it can handle.  (It does not document the approximately infinite number of ways of writing specifications that TLC can't handle.)

Leslie

On Thursday, November 22, 2018 at 12:32:36 PM UTC-8, Philip White wrote:

 ...