# Difference between action and temporal formula?

20 views

### je...@emptysquare.net

Jul 16, 2021, 6:45:12 PM (9 days ago) Jul 16
to tlaplus
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

Jul 17, 2021, 4:21:53 AM (8 days ago) Jul 17
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.

### A. Jesse Jiryu Davis

Jul 19, 2021, 3:27:51 PM (6 days ago) Jul 19
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 <>.

--