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.