Re: [tlaplus] Difference between action and temporal formula?

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...@xxxxxxxxxxxxxxx <jesse@xxxxxxxxxxxxxxx> 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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b919c7af-ddf1-4960-bb38-9759a0a9b477n%40googlegroups.com.