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

*From*: Stephen <stephen...@xxxxxxxxx>*Date*: Sat, 27 Jan 2018 16:55:23 -0800 (PST)*References*: <ba9a50d4-c57c-4a29-9fc8-d6758441ee11@googlegroups.com> <7F55C3AD-64FD-4FBE-B5ED-6C65B34AD883@gmail.com>

Hi Stephan,

Thanks for your reply.

Regards,

Yong

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

在 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.StephanOn 26 Jan 2018, at 03:53, 杨永 <steph...@xxxxxxxxx> wrote:Hi, guysI 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 .

**References**:**What is a TLA formula and a Temporal formula?***From:*杨永

**Re: [tlaplus] What is a TLA formula and a Temporal formula?***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Modelling thread preemption** - Next by Date:
**MIT license?** - Previous by thread:
**Re: [tlaplus] What is a TLA formula and a Temporal formula?** - Next by thread:
**MIT license?** - Index(es):