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