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

*From*: Hillel Wayne <hwayne@xxxxxxxxx>*Date*: Mon, 19 Jul 2021 16:51:00 -0500*References*: <b919c7af-ddf1-4960-bb38-9759a0a9b477n@googlegroups.com> <CAFRUCtZ0tKDvDCSBxYTXM-zB+Bt2Qiyti-AuD=18q0skxVFHTw@mail.gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101 Thunderbird/78.12.0

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

On 7/19/2021 2:27 PM, A. Jesse Jiryu
Davis wrote:

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

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.

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/7cee7e43-c257-e612-2f75-ae6dad4d999a%40gmail.com.

**References**:**Re: [tlaplus] Difference between action and temporal formula?***From:*A. Jesse Jiryu Davis

- Prev by Date:
**Re: [tlaplus] Difference between action and temporal formula?** - Next by Date:
**[tlaplus] Model checking a mutually recursive definition of a tree** - Previous by thread:
**Re: [tlaplus] Difference between action and temporal formula?** - Next by thread:
**[tlaplus] Model checking a mutually recursive definition of a tree** - Index(es):