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

["A. Jesse Jiryu Davis" <jesse@xxxxxxxxxxxxxxx>]

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

-- 
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/CAFRUCtZ0tKDvDCSBxYTXM-zB%2BBt2Qiyti-AuD%3D18q0skxVFHTw%40mail.gmail.com.