PTCaRet Plugin2.0 Input Syntax

From FSL
Jump to: navigation, search

PTCaRet formulae use the following syntax, which is defined in BNF:

(extended with the common {p} for zero or more and [p] for zero or one repetitions of p, respectively)

// BNF below is extended with {p} for zero or more and [p] for zero or one repetitions of p
<PTCaRet Plugin Input> ::= {"event" <Event Name>} "ptcaret:" <PTCaRet>
<PTCaRet> ::= "true" | "false" | <Event Name> | <PTCaRet> "and" <PTCaRet>
| <PTCaRet> "or" <PTCaRet> | "not" <PTCaRet> | <PTCaRet> "implies" <PTCaRet>
<!-- Normal boolean constants and operators>
| "(*)" <PTCaRet> | <PTCaRet> "S" <PTCaRet>
| "<*>" <PTCaRet> | "[*]" <PTCaRet>
<!-- Standard temporal operators>
| "(*a)" <PTCaRet> | <PTCaRet> "Sa" <PTCaRet>
| "<*a>" <PTCaRet> | "[*a]" <PTCaRet>
<!-- abstract temporal operators>
| "@b" <PTCaRet> | "@c" <PTCaRet>
<!-- derived temporal operators: at begin and at call>
| <PTCaRet> "Ss@b" <PTCaRet> | "<*s@b>" <PTCaRet>
| "[*s@b]" <PTCaRet>
<!-- derived begin stack operators>
| <PTCaRet> "Ss@c" <PTCaRet> | "<*s@c>" <PTCaRet>
| "[*s@c]" <PTCaRet>
<!-- derived call stack operators>
| <PTCaRet> "Ss@bc" <PTCaRet> | "<*s@bc>" <PTCaRet>
| "[*s@bc]" <PTCaRet>
<!-- derived begin-or-call stack operators>
<PTCaRet State> ::= "violation" | "validation"

Unary operators have higher precedence than binary operators. The binary operators in decreasing order of precedence are and > or > implies > S*; here S* includes all the variants of the since operator. Please refer to the corresponding technical report for formal definitions of these operators.

The definition of events is particular to the language instance of MOP used. For this plugin page itself, the event definitions are blank, as this is only a demonstration of the logic itself.


 event a
 event b
 event c
 ptcaret: a implies (not c Sa b)
Personal tools