This page describe mappings for property patterns in quantified regular expressions (QREs). For other information about the patterns click on the pattern links.
Information about the entire pattern system is available at the Specification Patterns Home Page.
Let "." be the set of all events symbols,
let [- P,Q,R] denote the expression that matches any symbol
except P Q and R and let e? denote
zero or one instance of expression e, and let e^k
denote k instances of e.
P is false :
| Globally | [- P]* |
| Before R | [- R]* | [-P,R]*; R; .* |
| After Q | [- Q]*; (Q; [- P]*)? |
| Between Q and R | ([- Q]*; Q; [- P,R]*; R)*; [- Q]*; (Q; [- R]*)? |
| After Q until R | ([- Q]*; Q; [- P,R]*; R)*; [-Q]*; (Q; [- P,R]*)? |
Event P occurs:
| Globally | [- P]*; P; .* |
| Before R | [- R]* | [-P,R]*; P; .* |
| After Q | [- Q]*; (Q; [- P]*; P; .*)? |
| Between Q and R | ([- Q]*; Q; [- P,R]*; P; [-R]*; R)*; [- Q]*; (Q; [- R ]*)? |
| After Q until R | ([- Q]*; Q; [- P,R]*; P; [-R]*; R)*; [-Q]*; (Q; [- P, R]*; P; [-R]*)? |
QREs allow us to formulate mappings for the general case (as opposed to a specific instance as with some other formalisms, e.g., LTL and CTL).
Event P occurs at most k times:
| Globally | (([- P]*;P)?)^k; [- P]* |
| Before R | [- R]* | (([- P,R]*;P)?)^k; [- P,R]*; R; .* |
| After Q | [- Q]*; (Q; (([- P]*;P)?)^k; [- P]* )? |
| Between Q and R | ([- Q]*; Q; (([- P,R]*;P)?)^k; [- P,R]*; R)*; [- Q]*; (Q; [- R]*)? |
| After Q until R | ([- Q]*; Q; (([- P,R]*;P)?)^k; [- P,R]*; R)*; [-Q]*; (Q; (([- P,R]*;P)?)^k; [- P,R]*)? |
Specifying universality in an event-based formalism requires the identification of complementary events. The positive event, P, is defined such that after an occurrence of P states have the property. The negative event, N, is defined such that after an ocurrence of N states fail to have the property. Then we define universality throughout a scope as having seen a P prior to the beginning of the scope with no N until after the close of the scope.
Our assumption is that the initial state has the desired property.
| Globally | [- N]* |
| Before R | [- R]* | [- N,R]*; R; .* |
| After Q | [- Q]* | ([- Q]*;P)? ; [- N,Q]* ; Q ; [- N]* |
| Between Q and R | ( ([- Q]*;P)? ; [- N,Q]*; Q; [- N,R]*; R )* ; [- Q]*; (Q; [- R]*)? |
| After Q until R | ( ([- Q]*;P)? ; [- N,Q]*; Q; [- N,R]*; R )* ; ( [- Q]* | ([- Q]*;P)? ; [- N,Q]*; Q; [- N,R]* ) |
S precedes P:
| Globally | [-P]* | ([-S,P]*; S; .*) |
| Before R | [-R]* | ([-P,R]*; R; .*) | ([-S,P,R]*; S; .*) |
| After Q | [-Q]*; (Q; ([-P]* | ([-S,P]*; S; .*)) )? |
| Between Q and R | [-Q]*; (Q; [-P,R]* | ([-S,P,R]*; S; [-R]*) R; [-Q]*)*; (Q; [-R]*)? |
| After Q until R | [-Q]*; (Q; [-P,R]* | ([-S,P,R]*; S; [-R]*) R; [-Q]*)*; (Q; ([-P,R]* | ([-S,P,R]*; S; [-R]*)) )? |
S responds to P :
| Globally | [-P]*; (P; [-S]*; S; [-P]*)* |
| Before R | [-R]* | [-P,R]*; (P; [-S,R]*; S; [-P,R]*)*; R; .* |
| After Q | [-Q]*; (Q; [-P]*; (P; [-S]*; S; [-P]*)* )? |
| Between Q and R | [-Q]*; (Q; [-P,R]*; (P; [-S,R]*; S; [-P,R]*)*; R; [-Q]*)*; (Q; [-R]*)? |
| After Q until R | [-Q]*; (Q; [-P,R]*; (P; [-S,R]*; S; [-P,R]*)*; R; [-Q]*)*; (Q; [-P,R]*; (P; [-S,R]*; S; [-P,R]*)*)? |
This is the 2 cause-1 effect mapping.
S, T precedes P:
| Globally | [-P]* | ([-P,S]*; S; [-P,T]*; T; .*) |
| Before R | [-R]* | ([-P,R]*; R; .*) | ([-P,R,S]*; S; [-P,R,T]*; T; .*) |
| After Q | [-Q]*; (Q; ([-P]* | ([-P,S]*; S; [-P,T]*; T; .*)))? |
| Between Q and R | [-Q]*; (Q; ([-P,R]* | ([-P,R,S]*; S; [-P,R,T]*; T; [-R]*)); R; [-Q]*)*; (Q; [-R]*)? |
| After Q until R | [-Q]*; (Q; ([-P,R]* | ([-S,P,R]*; S; [-P,R,T]*; T; [-R]*)); R; [-Q]*)*; (Q; ([-P,R]* | ([-P,R,S]*; S; [-P,R,T]*; T; [-R]*)))? |
This is the 1 cause-2 effect mapping.
P precedes (S, T):
| Globally | [-P,S]*;((P; .*) | (S; [-T]*))? |
| Before R | ([-R]*) | ([-P,S,R]*; ((P; [-R]*) | (S; [-T,R]*))?; R; .*) |
| After Q | [-Q]*; (Q; ([-P,S]*; ((P; .*) | (S; [-T]*))?))? |
| Between Q and R | [-Q]*; (Q; [-P,S,R]*;((P; [-R]*) | (S;[-T,R]*))?; R; [-Q]*)*; (Q; [-R]*)? |
| After Q until R | [-Q]*; (Q; [-P,S,R]*; ((P; [-R]*) | (S; [-T,R]*))?; R; [-Q]*)*; (Q; ([-P,S,R]*; ((P; [-R]*) | (S; [-T,R]*))?))? |
This is the 2 stimulus-1 response mapping.
P responds to S,T:
| Globally | ([- S]*; S; [- T]*; T; [- P]*; P)*; [- S]*; (S; [- T]*)? |
| Before R | [- R]* | ([- S,R]*; S; [- T,R]*; T; [- P,R]*; P)*; [- S,R]*; (S; [- T,R]*)?; R; .* |
| After Q | [- Q]*; (Q; ([- S]*; S; [- T]*; T; [- P]*; P)*; [- S]*; (S; [- T]*)?)? |
| Between Q and R | ([- Q]*; Q; ([- S,R]*; S; [- T,R]*; T; [- P,R]*; P)*; [- S,R]*; (S; [-T,R]*)?; R)*; [- Q]*; (Q; [- R]*)? |
| After Q until R | ([- Q]*; Q; ([- S,R]*; S; [- T,R]*; T; [- P,R]*; P)*; [- S,R]*; (S; [-T,R]*)?; R)*; [- Q]*; (Q; ([- S,R]*; S; [- T,R]*; T; [- P,R]*; P)* )? |
This is the 1 stimulus-2 response mapping.
S,T responds to P:
| Globally | ([- P]*; P; [- S]*; S; [- T]*; T)*; [- P]* |
| Before R | [- R]* | ([- P,R]*; P; [- S,R]*; S; [- T,R]*; T)*; [- P,R]*; R; .* |
| After Q | [- Q]*; (Q; ([- P]*; P; [- S]*; S; [- T]*; T)*; [- P]*)? |
| Between Q and R | ([- Q]*; Q; ([- P,R]*; P; [- S,R]*; S; [- T,R]*; T)*; [- P,R]*; R)*; [- Q]*; (Q; [- R]*)? |
| After Q until R | ([- Q]*; Q; ([- P,R]*; P; [- S,R]*; S; [- T,R]*; T)*; [- P,R]*; R)*; [- Q]*; (Q; ([- P,R]*; P; [- S,R]*; S; [- T,R]*; T)* )? |
This is the 2-1 response chain constrained with a single event.
S,T without Z responds to P:
| Globally | ([- P]*; P; [- S]*; S; [- T,Z]*; T)*; [- P]* |
| Before R | [- R]* | ([- P,R]*; P; [- S,R]*; S; [- T,R,Z]*; T)*; [- P,R]*; R; .* |
| After Q | [- Q]*; (Q; ([- P]*; P; [- S]*; S; [- T,Z]*; T)*; [- P]*)? |
| Between Q and R | ([- Q]*; Q; ([- P,R]*; P; [- S,R]*; S; [- T,R,Z]*; T)*; [- P,R]*; R)*; [- Q]*; (Q; [- R]*)? |
| After Q until R | ([- Q]*; Q; ([- P,R]*; P; [- S,R]*; S; [- T,R,Z]*; T)*; [- P,R]*; R)*; [- Q]*; (Q; ([- P,R]*; P; [- S,R]*; S; [- T,R,Z]*; T)* )? |