Atomic proposition | ap ::= | r | ff | tt | meth |
Box label | l ::= | tau | meth call meth | meth ret meth |
Property | phi ::= | ap | not ap | (phi) | phi /\ phi | phi \/ phi | [l]phi | prop_var | nu prop_var . phi |
where meth is a string starting with a lower case, while prop_var is a string starting with an upper case.
Interfaces are given as a list of method names, separated by spaces only.
Example:
Property: nu X. ([a call b] ff) /\ ([tau] X) /\ ([a call a] X) /\ ([a ret a] X)
Interface: a b