\subseteq vs \in SUBSET

[Lorin Hochstein]

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

[Andrew Helwer]

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

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

[lor...@gmail.com]

Thanks for the quick response, Andrew. I've subscribed to that github issue. (I tried to search this GG initially about this but I couldn't find a mention of it. Didn't think to search Github issues).

As an aside, OpenAI Codex was no help whatsoever in diagnosing this issue: it kept insisting that TLC was running against a stale file, and that's why I was seeing an error. And even when I figured out what was causing the problem and asked it to explain why, it gave an incorrect answer!

Me:

The problem was: roots \subseteq Obj 

If I do this: roots \in SUBSET Obj
It works. Why?

OpenAI Cdoex:

Given that the same expression works everywhere else in the module, the “roots undefined” at the roots ⊆ Obj line almost certainly means the token on that line wasn’t the same identifier as the one you declared. The most common way that happens is a stray non‑ASCII/whitespace character in the name (e.g., roots spelled with a non‑breaking space or some other invisible character). TLC then sees a brand‑new identifier with no declaration and flags it as undefined. When you retyped the line as roots \in SUBSET Obj, you replaced the bad token with the real roots, so the error went away. If you ever see this again, inspect the line for non‑ASCII/odd spacing (e.g., cat -vet or hexdump -C) and retype it in plain ASCII.

Take care,

Lorin

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/rZ6sfxMrgAM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUXN9fp5m2rHgoRBzcBaXK_sMxgm04uFHAALf-%3DR0AOV%3DA%40mail.gmail.com.

[Andrew Helwer]

Just for fun I hacked together an implementation of this by combining the logic of the SUBSET and \in operators. You can download the jar to try it out from this PR: https://github.com/ahelwer/tlaplus/pull/5

Doubt it will get upstreamed but anyway. Not too difficult to implement!

Andrew

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAErnbRb2dB5fRX%3D-jhcY9Hh2P%2B6ddVAw9c5y_kOMoB2o9ExcJQ%40mail.gmail.com.