Property Specification Language: Difference between revisions

Revision as of 05:36, 17 August 2016

Revision as of 10:39, 24 August 2016

Line 9:

</source>

The property "every {{color|orange|request}} which is immediately followed by an {{color|orange|ack}} signal, should be followed by a competecomplete {{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.