[tlaplus] Priming variables from "exists in" expressions?

• From: Branen Salmon <bugs@xxxxxxxxxx>
• Date: Tue, 9 Apr 2019 18:55:43 -0700 (PDT)

Hello, all--

I've been writing toy modules in the course of learning TLA, and in the course of debugging one, I noticed that priming a variable defined in an "exists in" expression seems to result in a next-state expression that's always false.  I've flipped through [what I think are] the relevant sections of Specifying Systems and searched around online, but haven't been able to figure out whether this is due to a limitation in TLC or if there's some mathematical subtlety that I'm missing that makes my spec incorrect.

For example:

-------------------------- MODULE ExistsInPrime --------------------------
VARIABLES x

Init ==
x = TRUE

next' = ~this

\* This next-state progression works fine.
\E y \in {x}: Advance(x, y)

\* This next-state progression is never true.
\E y \in {x}: Advance(y, y)

==========================================================================

If anyone could help me understand why ThisDeadlocks and ThisAdvances produce different results in TLC, I'd appreciate it.

Thanks,
Branen

--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.