Property Specification Language: Difference between revisions

Content deleted Content added
Line 18:
=== SERE-style operators===
 
The most commonly used PSL operator is the "suffix-implication" operator (a.k.a. the "triggers" operator), which is denoted by <math> \texttt{{mono|{{!}}{{=>} </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{{mono|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]]
[[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 (<math> \texttt{{mono|;} </math>}), Kleene-closure (<math> \texttt{{mono|*} </math>}), and union (<math> \texttt{{mono|{{!}}}}</math>), as well as operator for fusion (<math> \texttt{{mono|:}</math>}), intersection (<math> \texttt{{mono|\&\&}</math>}) and a weaker version (<math> \texttt{{mono|\&}</math>}), and many variations for consecutive counting <math> \texttt{{mono|[*n]} </math>} and in-consecutive counting e.g. <math> \texttt{{mono|[{{=}}n]} </math>} and <math> \texttt{{mono|[->n]} </math>}.
 
The trigger operator comes in several variations, shown in the table below.