Question about temporal formulas definition in book Specify System(version 21-07-04)

[钱晨]

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.

[Hillel Wayne]

<<A>>_v isn't a temporal formula (it's an action), but by page 91, ◇<<A>>_v is a temporal formula. Page 89 proves that if F is a temporal formula, □F is also a temporal formula. So then □(◇<<A>>_v) is also a temporal formula, making the liveness property on page 96 a valid property.

H

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