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

*From*: 钱晨 <allenhandora@xxxxxxxxx>*Date*: Tue, 27 Aug 2024 00:14:44 -0700 (PDT)

Hi,

I‘m reading chapter 8.1 of the Specify System. It says on page 91:

"although technically it’s not because <A> v(angle A sub v) isn’t a temporal formula."

During my first reading of the sentence, I understood it is not invariant under stuttering, so it is not a legal TLA formula.

While after reading the Chapter 8.4, it says on page 96:

"The obvious way to write this assertion is []<>HCnxt, but that’s not a legal TLA formula because HCnxt is an action, not a temporal formula. However, an HCnxt step advances the value hr of the clock, so it changes hr. Therefore, an HCnxt step is also an HCnxt step that changes hr—that is, it’s an <HCnxt>hr step. We can thus write the liveness property that the clock never stops as []<><HCnxt>hr."

It seems the <A> v(angle A sub v) isn't a legal temporal formula. So I can't understand whether <A> v(angle A sub v) is a legal temporal formula.

Thanks.

-- "The obvious way to write this assertion is []<>HCnxt, but that’s not a legal TLA formula because HCnxt is an action, not a temporal formula. However, an HCnxt step advances the value hr of the clock, so it changes hr. Therefore, an HCnxt step is also an HCnxt step that changes hr—that is, it’s an <HCnxt>hr step. We can thus write the liveness property that the clock never stops as []<><HCnxt>hr."

It seems the <A> v(angle A sub v) isn't a legal temporal formula. So I can't understand whether <A> v(angle A sub v) is a legal temporal formula.

Thanks.

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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b561a9d2-5a7b-4438-b03f-d1d44f605f96n%40googlegroups.com.

**Follow-Ups**:

- Prev by Date:
**Re: [tlaplus] Asynchronous Composition with Parameterized Submodules** - Next by Date:
**[tlaplus] The Future of TLA+** - Previous by thread:
**[tlaplus] Sub-action of Next in vscode plugin** - Next by thread:
**Re: [tlaplus] Question about temporal formulas definition in book Specify System(version 21-07-04)** - Index(es):