Content deleted Content added
cap, bold, simplify heaidng |
m →SERE-style Operators: cap |
||
Line 16:
PSL's temporal operators can be roughly classified into ''LTL-style'' operators and ''regular-expression-style'' operators. Many PSL operators come in two versions, a strong version, indicated by an exclamation mark suffix ( {{color|red|!}} ), and a weak version. The ''strong version'' makes eventuality requirements (i.e. require that something will hold in the future), while the ''weak version'' does not. An ''underscore suffix'' ( {{color|red|_}} ) is used to differentiate ''inclusive'' vs. ''non-inclusive'' requirements. An {{color|red|a_}} and {{color|red|e_}} suffixes are used to denote ''universal'' vs. ''existential'' requirements. Exact time windows are denoted by {{color|red|[n]}} and flexible by {{color|red|[m..n]}}.
=== SERE-style
The most commonly used PSL operator is the "suffix-implication" operator (a.k.a the "triggers" operator), which is denoted by <math> \texttt{|=>} </math>. Its left operand is a PSL regular expression and its right operand is any PSL formula (be it in LTL style or regular expression style). The semantics of <math>\texttt{r |=>p}</math> is that on every time point i such that the sequence of time points up to i constitute a match to the regular expression r, the path from i+1 should satisfy the property p. This is exemplified in the figures on the right.
| |||