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

[Stephen <stephen...@xxxxxxxxx>]

Hi Stephan,

Thanks for your reply.

Regards,

Yong

在 2018年1月26日星期五 UTC+8下午4:10:07，Stephan Merz写道：

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, 杨永 <steph...@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...@googlegroups.com.
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.