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