Existence Property Pattern
To describe a portion of a system's execution that contains an instance of certain events or states. Also known as Eventually.
Examples and Known Uses
The classic example of existence is specifying termination, e.g., on all executions do we eventually reach a terminal state.
We may wish to specify that a state/event occur at most some bounded number of times. The Bounded Existence pattern handles that case.
If one wishes to require the existence of a state characterized by multiple propositions or multiple events one can do this by defining P appropriately. One common use is to fill the role of P in the above mappings with disjunctions of propositions or event symbols. For other parameterizations of patterns consult the pattern notes.
This is an Occurrence pattern.