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

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

On 10 Apr 2019, at 03:55, Branen Salmon <bugs@xxxxxxxxxx> wrote:

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.

--
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.