Priming variables from "exists in" expressions?

[Branen Salmon]

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

[Stephan Merz]

Expanding the operator definition for the two actions produces

(1)  \E y \in {x} : x' = ~ y   \* for "ThisAdvances"

and

(2)  \E y \in {x} : y' = ~ y  \* for "ThisDeadlocks"

Evaluating (1) in the initial state where x = TRUE yields

(1')  \E y \in {TRUE} : x' = ~ y

which is true for the successor state in which x = FALSE, so this will be the new state constructed by TLC.

In contrast, when evaluating (2), observe that the quantifiers \A and \E bind values ("constants" in TLA+ jargon), therefore y' reduces to y (just as 42' reduces to 42) and therefore we get

(2')  \E y \in {TRUE} : y = ~ y

which evaluates to FALSE, hence no new state satisfying this formula can be constructed.

Stephan

--
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 post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Branen Salmon]

Ah, that makes perfect sense.  Thanks!

Branen

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.