Intent
To describe a portion of a system's execution that contains an instance of certain events or states. Also known as Eventually.
Example Mappings
Examples and Known Uses
The classic example of existence is specifying termination, e.g., on all executions do we eventually reach a terminal state.
Relationships
This pattern is the dual of the Absence pattern. In fact, in many specification formalisms negation and explicit queries for existence will be used to formulate an instance of the Absence pattern.
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.