If I have a property of the form
[][A => (p /\ [] (q => r))]_vars (1)
where A is an action and p,q,r are state predicates, I get two complaints:
Level error in applying operator $SquareAct:
The level of argument 1 exceeds the maximum level allowed by the operator.
and
=> has both temporal formula and action as arguments.
If I remove the nested [] then both complaints go away (and TLC is fine with too)
[][A => (p /\ (q => r))]_vars (2)
However, even if I replace the A with another state predicate the second complaint still remains.
Could someone tell me where I'm going wrong. I don't recall seeing any restriction on nesting of temporal operators in the Specifying Systems book but I could have quite easily missed it. Regarding why TLC accepts the second formula (2), I assume its "nice" because its considered a Box-Action formula?
thanks