Absence Property Pattern
To describe a portion of a system's execution that is free of certain events or states. Also known as Never.
Examples and Known Uses
The most common example is mutual exclusion. In a state-based model, the scope would be global and P would be a state formula that is true if more than one process is in its critical section. For an event-based model, the scope would be a segment of the execution in which some process is in its critical section (i.e., between an enter section event and a leave section event), and P would be the event that some other process enters its critical section.
This pattern is the dual of the Existence pattern. In fact, in many specification formalisms negation and explicit queries for existence will be used to formulate an instance of the Absence pattern, as seen in the examples above.
Note that Between scopes in this pattern (with a false proposition or empty event symbol) appear to be able to specify the same thing as a Response pattern with global scope. This is not the case, however, since the cause-effect relationship is required for the Response whereas the scope for this pattern is optional.
If one wishes to exclude states 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.