What is a TLA formula and a Temporal formula?

[杨永 <stephen...@xxxxxxxxx>]

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