Safety-LTL is now provided for specifying local specifications
Tips for using *entry* atomic proposition in local specifications:
- *entry* atomic propositions should only be used for stating calls (in practice they are mainly used for stating self calls)
- we recommend to use them by one of the following patterns:
- X (!m || !entry), where m is a method name. States that next action is not a call to method m
- X (m && entry) -> phi, where m is a method name and phi is a safety-LTL formula.
States that if method m is called in this state, phi holds from the state after the call.
- Example: m -> G (X (!m || !entry)), means that method m does not contain any self call.
You are free to use *entry* atomic proposition with no restriction for global properties.