Content deleted Content added
fixed math symbols |
m WP:CHECKWIKI error fix. Section heading problem. Violates WP:MOSHEAD. |
||
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]}}.
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.
[[File:The trigger operator - slide 2.jpg|thumb|path satisfying ''r triggers p'' in two non-overlapping ways]]
Line 129 ⟶ 130:
|}
Below is a sample of some LTL-style operators of PSL.
Line 193 ⟶ 195:
|}
Sometimes it is desirable to change the definition of the ''next time-point'', for instance in multiply-clocked designs, or when a higher lever of abstraction is desired. The ''sampling operator'' (a.k.a ''the clock operator''), denoted {{color|red|@}}, is used for this purpose. The formula {{color|orange| p @ c }} where {{color|orange| p}} is a PSL formula and {{color|orange|c}} a PSL Boolean expressions holds on a given path if {{color|orange| p}} on that path projected on the cycles in which {{color|orange| c}} holds, as exemplified in the figures to the right.
[[File:Need for multiple clocks.jpg|thumb|path and formula showing need for a sampling operator]]
Line 206 ⟶ 209:
The semantics of formulas with nested @ is a little subtle. The interested reader is referred to [2].
PSL has several operators to deal with truncated paths (finite paths that may correspond to a prefix of the computation). Truncated paths occur in bounded-model checking, due to resets and in many other scenarios. The abort operators, specify how eventualities should be dealt with when a path has been truncated. They rely on the truncated semantics proposed in [1].
| |||