[tlaplus] \subseteq vs \in SUBSET

[Lorin Hochstein <lorinh@xxxxxxxxx>]

I was trying to use \subseteq in a clause in my Init definition. This led to a TLC error when model checking.

Here's a simple example to illustrate the issue:

---- MODULE simple ----
CONSTANT U
VARIABLE S

Init == S \subseteq U

Add == \E x \in U \ S: S' = S \cup {x}
Rem == \E x \in S: S' = S \ {x}

Next == Add \/ Rem
=======

Checking this with TLC yields the error:

In evaluation, the identifier S is either undefined or not an operator.

On the other hand, if I express Init like this instead:

Init == S \in SUBSET U

then TLC succeeds. 

What is the reason that \subseteq results in a TLC error but \in SUBSET succeeds? I thought they were semantically equivalent.

Thanks,
Lorin

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/c4ae2941-d7b9-4e97-91f7-be8a404d4257n%40googlegroups.com.