Content deleted Content added
No edit summary |
Added description of the clock operator, and figures explaining both the trigger operator and the clock operator Tag: possible conflict of interest |
||
Line 8:
</source>
The property "
<source> ((
A trace satisfying this formula is given in the figure on the right.
[[File:The trigger operator - slide 1.jpg|thumb|a simple trace satisfying <source>(true[*]; req; ack) |=> (start; data[=8]; end)</source>]]
===Operators===
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 Operators====
The most commonly used PSL operator is the "suffix-implication" operator (a.k.a the "triggers" operator), which is denoted by {{code|{{!}}=>}}. 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 {{code|r{{!}}=>p}} 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 pictures on the right.
[[File:The trigger operator - slide 2.jpg|thumb|path satisfying ''r triggers p'' in two non-overlapping ways]]
[[File:The trigger operator - slide 3.jpg|thumb|path satisfying ''r triggers p'' in two overlapping ways]]
[[File:The trigger operator - slide 4.jpg|thumb|path satisfying ''r triggers p' in three ways]]
The trigger operator comes in several variations, shown in the table below.
Line 186 ⟶ 131:
|}
==== LTL-style Operators====
Below is a sample of some LTL-style operators of PSL.
Here {{color|orange|p}} and {{color|orange|q}} are any PSL formulas.
{| class="wikitable"
| always p
| property p holds on every time point
|-
| never p
| property p does not holds on any time point
|-
| eventually! p
| there exists a future time point where p holds
|-
| next! p
| there exists a next time point, and p holds on this point
|-
| next p
| if there exists a next time point, then p holds on this point
|-
| next![n] p
| there exists an n-th time point, and p holds on this point
|-
| next[n] p
| if there exists an n-th time point, then p holds on this point
|-
| next_e![m..n] p
| there exists a time point, within m-th to n-th from the current where p holds.
|-
| next_e[m..n] p
| if there exists at least n-th time points, then p holds on one of the m-th to n-th points.
|-
| next_a![m..n] p
| there exists at least n more time points and p holds in all the time points between the m-th to the n-th, inclusive.
|-
| next_a[m..n] p
| p holds on all the next m-th through n-th time points, however many exist
|-
| p until! q
| there exists a time point where q holds, and p hold up until that time point
|-
| p until q
| p holds up until a time point where q hold, if such exists
|-
| p until!_ q
| there exists a time point where q holds, and p hold up until that time point and in that time point
|-
| p until q
| p holds up until a time point where q hold, and in that time point, if such exists
|-
| p before! q
| p holds strictly before the time point where q holds, and p eventually holds
|-
| p before q
| p holds strictly before the time point where q holds, if p never holds, then neither does q
|-
| p before!_ q
| p holds before or at the same time point where q holds, and p eventually holds
|-
| p before_ q
| p holds before or at the same time point where q holds, if p never holds, then neither does q
|-
|}
==== The Sampling Operators====
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]]
[[File:Multiple clocks.jpg|thumb|path and formula showing effect of the sampling operator @]]
The semantics of formulas with nested @ is a little subtle. The interested reader is referred to [2].
==== The Abort Operators ====
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].
Line 203 ⟶ 219:
|-
|}
Line 232 ⟶ 246:
*{{cite doi|10.1109/IEEESTD.2010.5446004}}
**IEC 62531:2012 {{cite doi|10.1109/IEEESTD.2012.6228486}}
*''Reasoning with Temporal Logic on Truncated Paths'', Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac, David Van Campenhout
[http://www.research.ibm.com/people/e/eisner/papers/cav49.pdf] {{cite doi|10.1007/978-3-540-45069-6_3}}
*''The Definition of a Temporal Clock Operator'', Cindy Eisner, Dana Fisman, John Havlicek, Anthony McIsaac, David Van Campenhout
[http://www.cis.upenn.edu/~fisman/documents/EFHMV_ICALP03_full.pdf] {{cite doi|10.1007/3-540-45061-0_67}}
==External links==
| |||