Re: [tlaplus] \subseteq vs \in SUBSET

You are correct that the two expressions are semantically equivalent. However, TLC currently does not support evaluating \subseteq in this way. The feature request is tracked in this issue: https://github.com/tlaplus/tlaplus/issues/336

This issue was also profiled in the March 2025 developer update: https://foundation.tlapl.us/blog/2025-03-dev-update/index.html#newbie-corner

Likely the least-invasive way to add this feature (and many other similar ones) to TLC would be addition of an AST rewriting pass, for which the main difficulty would be accurate error message translation across the rewrite boundary.

Andrew

On Thu, Jan 1, 2026 at 2:48 PM Lorin Hochstein <lorinh@xxxxxxxxx> wrote:

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.