[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Branen Salmon <bugs@xxxxxxxxxx>*Date*: Wed, 10 Apr 2019 14:22:54 -0700 (PDT)*References*: <2cffcbe8-ade6-4f43-bd5a-bd90896dbd66@googlegroups.com> <9E9E2778-E313-4A55-B3F1-C9E447FBAF00@gmail.com>

Ah, that makes perfect sense. Thanks!

Branen

On Wednesday, April 10, 2019 at 8:59:16 AM UTC-4, Stephan Merz wrote:

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' = ~ ywhich 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 = ~ ywhich evaluates to FALSE, hence no new state satisfying this formula can be constructed.StephanOn 10 Apr 2019, at 03:55, Branen Salmon <bu...@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 tla...@googlegroups.com .

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

**References**:**[tlaplus] Priming variables from "exists in" expressions?***From:*Branen Salmon

**Re: [tlaplus] Priming variables from "exists in" expressions?***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Priming variables from "exists in" expressions?** - Next by Date:
**Re: [tlaplus] Re: [noob] Liveness property not violated as expected** - Previous by thread:
**Re: [tlaplus] Priming variables from "exists in" expressions?** - Next by thread:
**[tlaplus] TLA+ for introduction to software engineering?** - Index(es):