Difference between action and temporal formula?

[je...@emptysquare.net]

Chapter 8 of “Specifying Systems” often makes a distinction between an action and a temporal formula, but I’m having trouble finding any definitions earlier the book that tell me what the difference is. Is it this?: actions are ordinary formulas with primed variables and/or ENABLED, and temporal formulas also permit [] and <>.

[Karolis Petrauskas]

At least in my understanding the distinction is that a temporal formula defines a behaviour, and the action only a relation between two states.

I find the TLA paper very useful and complementary to the book as well: https://lamport.azurewebsites.net/pubs/lamport-actions.pdf.

In sections 3 and 4 the actions are considered as elementary temporal formulas.

Karolis

On Sat, Jul 17, 2021 at 1:45 AM je...@emptysquare.net <je...@emptysquare.net> wrote:

Chapter 8 of “Specifying Systems” often makes a distinction between an action and a temporal formula, but I’m having trouble finding any definitions earlier the book that tell me what the difference is. Is it this?: actions are ordinary formulas with primed variables and/or ENABLED, and temporal formulas also permit [] and <>.

--
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/b919c7af-ddf1-4960-bb38-9759a0a9b477n%40googlegroups.com.

[A. Jesse Jiryu Davis]

Reviewing, I find that a temporal formula is an assertion about behaviors. So a temporal formula maps from behaviors (i.e. infinite sequences of steps, including stuttering steps) to bools.

An action, on the other hand, is an ordinary formula with primed and unprimed variables. I suppose it maps from steps to bools.

In Specifying Systems 8.3, the book discusses what happens when substituting actions for temporal formulas in TLA tautologies, and it says that the resulting formulas might not be TLA formulas. For example, if A and B are actions:

"[]<>(<<A>>_v \/ <<B>>_v) isn't a TLA formula."

Why isn't it? And why does the book go on to imply that "substituting <<A \/ B>>_v for <<A>>_v \/ <<B>>_v" turns it into a TLA formula?

Thanks.

On Fri, Jul 16, 2021 at 6:45 PM je...@emptysquare.net <je...@emptysquare.net> wrote:

Chapter 8 of “Specifying Systems” often makes a distinction between an action and a temporal formula, but I’m having trouble finding any definitions earlier the book that tell me what the difference is. Is it this?: actions are ordinary formulas with primed variables and/or ENABLED, and temporal formulas also permit [] and <>.

--

[Hillel Wayne]

Section 16.2.4 gives a syntactic definition of a valid TLA formula, which is defined inductively from a few base rules. Since []<>(<<A>>_v \/ <<B>>_v) cannot be built from those rules, it's not a valid TLA formula, even though it's a temporal formula. But you can construct []<><<A \/ B>>_v, which is logically equivalent.

H

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFRUCtZ0tKDvDCSBxYTXM-zB%2BBt2Qiyti-AuD%3D18q0skxVFHTw%40mail.gmail.com.