Precedence Chain Property Pattern
Precedence Chain Property Pattern
Intent
This is a scalable pattern. We describe the 1 cause - 2 effect
version here.
To describe a relationship between an event/state P and a
sequence of events/states (S, T) in which the occurrence of
S followed by T within the scope must be preceded by
an occurrence of the the sequence P within the same scope.
In state-based formalisms, the beginning of the enabled sequence
(S, T) may be satisfied by the same state as the enabling
condition (i.e., P and S may be true in the same
state).
Example Mappings
Examples and Known Uses
An example of this pattern, assuming reliable communication
between client and server, is that
"If a client makes a request and there is no response, then
the server must have crashed."
This would be expressed by parameterizing the
constrained variant of the
1-2 precedence chain pattern
as:
ServerCrash precedes ClientRequest, []!Response
without Response
in LTL.
Relationships
Note that this pattern does not require that each occurrence of
the enabled sequence will have its own occurrence of the enabling
condition.
This is an Order pattern.