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

[Branen Salmon <bugs@xxxxxxxxxx>]

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

Advance(next, this) ==
    next' = ~this

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

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

Next == ThisDeadlocks
==========================================================================

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.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.