Editing Property Specification Language (section)

=== SERE-style operators===

The most commonly used PSL operator is the "suffix-implication" operator (also known as the "triggers" operator), which is denoted by {{mono|{{!}}{{=}}>}}. 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 {{mono|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 figures 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 regular expressions of PSL have the common operators for concatenation ({{mono|;}}), Kleene-closure ({{mono|*}}), and union ({{mono|{{!}}}}), as well as operator for fusion ({{mono|:}}), intersection ({{mono|&&}}) and a weaker version ({{mono|&}}), and many variations for consecutive counting {{mono|[*n]}} and in-consecutive counting e.g. {{mono|[{{=}}n]}} and {{mono|[->n]}}.

The trigger operator comes in several variations, shown in the table below.

Here {{mono|s}} and {{mono|t}} are PSL-regular expressions, and {{mono|p}} is a PSL formula.
 {| class="wikitable"
| <syntaxhighlight lang="text"> s |=> t! </syntaxhighlight> 
| 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
|-
| <syntaxhighlight lang="text"> s |-> t! </syntaxhighlight> 
| 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
|-
| <syntaxhighlight lang="text"> s |=> t </syntaxhighlight> 
| 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
|-
| <syntaxhighlight lang="text"> s |-> t </syntaxhighlight> 
| 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 may "get stuck" in the middle
|-
|}

Operators for concatenation, fusion, union, intersection and their variations are shown in the table below.

Here {{mono|s}} and {{mono|t}} are PSL regular expressions.
{| class="wikitable"
| <code> s ; t </code> 
| match of s followed by a match of t, t starts the cycle after s ends
|-
| <code>s : t </code> 
| match of s followed by a match of t, t starts the same cycle that s ends
|-
| <syntaxhighlight lang="text" inline>s | t </syntaxhighlight> 
| match of s or match of t 
|-
| <code>s && t </code> 
| match of s and match of t, duration of both is of same length 
|-
| <code>s & t </code> 
| match of s and match of t, duration matches maybe different
|-
| <code> s within t </code> 
| match of s within a match of t, abbreviation of ([*]; s; [*]) && t
|-
|}

Operators for consecutive repetitions are shown in the table below.

Here {{mono|s}} is a PSL regular expression. 
{| class="wikitable"
| <code> s[*i]  </code> 
| i consecutive repetitions of s
|-
| <code> s[*i..j] </code> 
| between i to j consecutive repetitions of s
|-
| <code> s[*i..] </code> 
| at least i to consecutive repetitions of s
|-
| <code> s[*] </code> 
| zero or more consecutive repetitions of s
|-
| <code> s[+] </code> 
| one or more consecutive repetitions of s
|-
|}

Operators for non-consecutive repetitions are shown in the table below.

Here {{mono|b}} is any PSL Boolean expression. 
{| class="wikitable"
| <code> b[=i] </code> 
| i not necessarily consecutive repetitions of b, 
*equivalent to (!b[*];b)[*i]; !b[*]
|-
| <syntaxhighlight lang="text" inline> b[=i..j] </syntaxhighlight> 
| at least i  and no more than j not necessarily consecutive repetitions of b, 
*equivalent to (!b[*];b)[*i..j]; !b[*]
|-
| <code> b[=i..] </code> 
| at least i not necessarily consecutive repetitions of b, 
*equivalent to (!b[*];b)[*i..]; !b[*]
|-
| <syntaxhighlight lang="text" inline> b[->m] </syntaxhighlight> 
| m not necessarily consecutive repetitions of b ending with b, 
*equivalent to (!b[*];b)[*m]
|-
| <code> b[->m:n] </code> 
| at least m and no more than n not necessarily consecutive repetitions of b ending with b, 
*equivalent to (!b[*];b)[*m..n]
|-
| <code> b[->m..] </code> 
| at least m not necessarily consecutive repetitions of b ending with b, 
*equivalent to (!b[*];b)[*m..]; !b[*]
|-
| <code> b[->] </code> 
| shortcut for b[->1], 
*equivalent to (!b[*];b)
|-
|}