20 views

Skip to first unread message

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 <>.

Jul 17, 2021, 4:21:53 AM (8 days ago) Jul 17

to tla...@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+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.

Jul 19, 2021, 3:27:51 PM (6 days ago) Jul 19

to tla...@googlegroups.com

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.

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 <>.

--

Jul 19, 2021, 5:51:04 PM (6 days ago) Jul 19

to tla...@googlegroups.com

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.

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu