Property Specification Language: Difference between revisions

Revision as of 23:16, 29 June 2019

Revision as of 23:17, 29 June 2019

Line 5:

== Syntax and semantics ==

PSL can express that if some scenario happens now, then another scenario should happen some time later. For instance, the property "a {{mono|request}} should always eventually be {{mono|grant}} ed" can be expressed by the PSL formula:

<source lang="text"> always (request -> eventually! grant)

</source>

The property "every {{mono|request}} which is immediately followed by an {{mono|ack}} signal, should be followed by a complete {{mono|data transfer}}, where a complete data transfer is a sequence starting with signal {{mono|start}}, ending with signal {{mono|end}} in which {{mono|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.