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

Re: [tlaplus] What is a TLA formula and a Temporal formula?



Within temporal formulas, action formulas must be "protected", i.e. occur in the form [][A]_v or dually <><<A>>_v.

In particular, <>(<<A>>_v \/ <<B>>_v) does not obey this restriction: the action formulas appear in the immediate scope of \/. Of course, if it were accepted as a formula, it would be equivalent to <><<A>>_v \/ <><<B>>_v, and the latter is a well-formed formula.

Stephan


On 26 Jan 2018, at 03:53, 杨永 <stephen...@xxxxxxxxx> wrote:

Hi, guys

I am reading the Tla+ Specifying Systems confused by TLA formula. For example, on page 95, the first sentence "...because []<>(<<A>>_v \/ <<B>>_v ) isn't a TLA formula." where <<A >>_v and <<B>>_v are actions, however, []<><<A \/ B>>_v is a TLA formula."

I don't know why. Can somebody explain the reason?

I appreciate,

Yong

--
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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.