Precedence Chain Property Pattern


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.


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.