Content deleted Content added
m WP:CHECKWIKI error fix. Section heading problem. Violates WP:MOSHEAD. |
m →Syntax and Semantics: <source lang="text"> |
||
Line 6:
PSL can express that if some scenario happens now, then another scenario should happen some time later. For instance, the property "a {{color|orange|request}} should always eventually be {{color|orange|grant}} ed can be expressed by the PSL formula:
<source lang="text"> always (request -> eventually! grant)
</source>
The property "every {{color|orange|request}} which is immediately followed by an {{color|orange|ack}} signal, should be followed by a compete {{color|orange|data transfer}}, where a complete data transfer is a sequence starting with signal {{color|orange|start}}, ending with signal {{color|orange|end}} in which {{color|orange|busy}} holds at the meantime can be expressed by the PSL formula:
<source lang="text"> (true[*]; req; ack) |=> (start; busy[*]; end) </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 lang="text">(true[*]; req; ack) |=> (start; busy[*]; end)</source>]]
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]}}.
Line 29:
Here {{color|orange|s}} and {{color|orange|t}} are PSL-regular expressions, and {{color|orange|p}} is a PSL formula.
{| class="wikitable"
| <source lang="text"> s |=> t! </source>
| if there is a match of s, then there is a match of t on the suffix of the trace,
*t starts the cycle after s ends,
*the match of t must reach to its end
|-
| <source lang="text"> s |-> t </source>
| if there is a match of s, then there is a match of t on the suffix of the trace,
*t starts the same cycle that s ends,
*the match of t must reach to its end
|-
| <source lang="text"> s |=> t! </source>
| if there is a match of s, then there is a match of t on the suffix of the trace,
*t starts the cycle after s ends,
*the match of t may "get stuck" in the middle
|-
| <source lang="text"> s |-> t </source>
| if there is a match of s, then there is a match of t on the suffix of the trace,
*t starts the same cycle that s ends,
Line 61:
| match of s followed by a match of t, t starts the same cycle that s ends
|-
| <source lang="text">s | t </source>
| match of s or match of t
|-
Line 104:
*equivalent to (!b[*];b)[*i]; !b[*]
|-
| <source lang="text"> b[=i..j] </source>
| at least i and mo more than j not necessarily consecutive repetitions of b,
*equivalent to (!b[*];b)[*i..j]; !b[*]
Line 112:
*equivalent to (!b[*];b)[*i..]; !b[*]
|-
| <source lang="text"> b[->m] </source>
| m not necessarily consecutive repetitions of b ending with b,
*equivalent to (!b[*];b)[*m]
Line 201:
The first property states that "every {{color|orange|request}} which is immediately followed by an {{color|orange|ack}} signal, should be followed by a compete {{color|orange|data transfer}}, where a complete data transfer is a sequence starting with signal {{color|orange|start}}, ending with signal {{color|orange|end}} in which {{color|orange|data}} should hold at least 8 times:
<source lang="text"> ((true[*]; req; ack) |=> (start; data[=8]; end) </source>
But sometimes it is desired to consider only the cases where the above signals occur on a cycle where {{color|orange|clk}} is high.
This is depicted in the second figure in which although the formula
<source lang="text"> ((true[*]; req; ack) |=> (start; data[*3]; end) @ clk </source>
uses {{color|orange|data[*3]}} and {{color|orange|[*n]}} is consecutive repetition, the matching trace has 3 non-consecutive time points where {{color|orange|data}} holds, but when considering only the time points where {{color|orange|clk}} holds, the time points where {{color|orange|data}} hold become consecutive.
[[File:Multiple clocks.jpg|thumb|path and formula showing effect of the sampling operator @]]
| |||