Editing Property Specification Language (section)

=== Abort operators ===

PSL has several operators to deal with truncated paths (finite paths that may correspond to a prefix of the computation). Truncated paths occur in bounded-model checking, due to resets and in many other scenarios. The abort operators, specify how eventualities should be dealt with when a path has been truncated. They rely on the truncated semantics proposed in [1].

Here {{mono|p}} is any PSL formula and {{mono|b}} is any PSL Boolean expression. 
{| class="wikitable"
| <code> p async_abort b </code> 
| either p holds or p does not fail up until b holds; 

* b recognized asynchronously
|-
| <code> p sync_abort b </code> 
| either p holds or p does not fail up until b holds; 

* b recognized synchronously
|-
| <code> p abort b </code> 
| equivalent to p async_abort b
|-
|}