[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Karolis Petrauskas <k.petrauskas@xxxxxxxxx>*Date*: Sat, 17 Jul 2021 11:21:40 +0300*References*: <b919c7af-ddf1-4960-bb38-9759a0a9b477n@googlegroups.com>

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

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.

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/CAFteovJ8CX52barLpZQaSnzep0%2BMMDVz9bw%2BMiA%2BRMSO__RAQA%40mail.gmail.com.

- Prev by Date:
**Re: [tlaplus] TLC and parameterized INSTANCE** - Next by Date:
**Re: [tlaplus] Difference between action and temporal formula?** - Previous by thread:
**Re: [tlaplus] TLC and parameterized INSTANCE** - Next by thread:
**Re: [tlaplus] Difference between action and temporal formula?** - Index(es):