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

*From*: 杨永 <stephen...@xxxxxxxxx>*Date*: Thu, 25 Jan 2018 18:53:30 -0800 (PST)

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

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

- Prev by Date:
**Re: [tlaplus] TLAPS and primitive-recursive functions** - Next by Date:
**Re: [tlaplus] What is a TLA formula and a Temporal formula?** - Previous by thread:
**Re: TLA+ parser (Haskell library)** - Next by thread:
**Re: [tlaplus] What is a TLA formula and a Temporal formula?** - Index(es):