Property Specification Language: Difference between revisions

Revision as of 23:17, 29 June 2019

Revision as of 17:47, 29 August 2019

Line 14:

[[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 ( {{mono|!}} ), 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'' ( {{mono|_}} ) is used to differentiate ''inclusive'' vs. ''non-inclusive'' requirements. An {{mono|a__a}} and {{mono|e__e}} suffixes are used to denote ''universal'' (all) vs. ''existential'' (exists) requirements. Exact time windows are denoted by {{mono|[n]}} and flexible by {{mono|[m..n]}}.

=== SERE-style operators===