# PTCaRet Plugin3 Input Syntax

The MOP PTCaRet plugin syntax instantiates the generic <Logic Name>, <Logic Syntax>, and <Logic State> from the Logic Repository Syntax. It is used in conjunction with the <Logic Repository I/O> syntax, and defined using BNF

// BNF below is extended with {p} for zero or more and [p] for zero or one repetitions of p

// The mandatory MOP logic syntax

<PTCaRet Name> ::= "ptcaret"

<PTCaRet Syntax> ::= "true" | "false"

| <Event Name> // events are atomic propositions

| <Not> <PTCaRet Syntax> // negation

| <PTCaRet Syntax> <And> <PTCaRet Syntax> // conjunction

| <PTCaRet Syntax> <Or> <PTCaRet Syntax> // disjunction

| <PTCaRet Syntax> <Xor> <PTCaRet Syntax> // XOR: eXclusive OR

| <PTCaRet Syntax> <Implies> <PTCaRet Syntax> // implies

| <PTCaRet Syntax> "<->" <PTCaRet Syntax> // if and only if

| "[*]" <PTCaRet Syntax> // always in the past

| "<*>" <PTCaRet Syntax> // eventually in the past

| "(*)" <PTCaRet Syntax> // previously

| <PTCaRet Syntax> "S" <PTCaRet Syntax> // since

| "[*a]" <PTCaRet Syntax> // abstract always in the past

| "<*a>" <PTCaRet Syntax> // abstract eventually in the past

| "(*a)" <PTCaRet Syntax> // abstract previously

| <PTCaRet Syntax> "Sa" <PTCaRet Syntax> // abstract since

| "@b" <PTCaRet Syntax> // at begin

| "@c" <PTCaRet Syntax> // at call

| "<*s@b>" <PTCaRet Syntax> // eventually at begin in the stack

| "[*s@b]" <PTCaRet Syntax> // always at begin in the stack

| <PTCaRet Syntax> "Ss@b" <PTCaRet Syntax> // since at begin in the stack

| "<*s@c>" <PTCaRet Syntax> // eventually at call in the stack

| "[*s@c]" <PTCaRet Syntax> // always at call in the stack

| <PTCaRet Syntax> "Ss@c" <PTCaRet Syntax> // since at call in the stack

| "<*s@bc>" <PTCaRet Syntax> // eventually at begin or call

// in the stack

| "[*s@bc]" <PTCaRet Syntax> // always at begin or call

// in the stack

| <PTCaRet Syntax> "Ss@bc" <PTCaRet Syntax> // since at begin or call

// in the stack

<PTCaRet State> ::= "violation" | "validation"

// The auxiliary elements for the logic syntax

<Not> ::= "!" | "not"

<And> ::= "/\" | "and" | "&&"

<Or> ::= "\/" | "or" | "||"

<Xor> ::= "++" | "xor" | "^"

<Implies> ::= "->" | "=>" | "implies"

### <PTCaRet Name>

<PTCaRet Name> instantiates <Logic Name> from the MOP Syntax. It denotes the PTCaRet logic using the string "ptcaret".

### <PTCaRet Syntax>

<PTCaRet Syntax> instantiates <Logic Syntax> from the MOP Syntax.
<PTCaRet Syntax> is based on constants and atomic propositions with boolean operators and
temporal operators. The different operators in decreasing order of precedence are
[*]
`,` <*>
`,` (*)
`,` [*a]
`,` <*a>
`,` (*a)
`,` @b
`,` @c
`,` <*s@b>
`,` [*s@b]
`,` <*s@c>
`,` [*s@c]
`,` <*s@bc>
`,` [*s@bc]
`,` !
`,` not
`>` S
`>` Sa
`>` Ss@bc
`>` Ss@c
`>` Ss@b
`>` <And>
`>` <Xor>
`>` <Or>
`>` <Implies>
`>` <->.

The last nineteen operators from <PTCaRet Syntax> are called temporal and have the following interpretation:

- [*]
`X`holds if`X`holds in all past time points - <*>
`X`holds if`X`holds in some past time point - (*)
`X`holds if`X`holds at the previous time point -
`X`S`Y`holds if`Y`holds in some past time point, and since then`X`has held (strict since) - [*a]
`X`holds if`X`holds in all past time points except time points in the method which already returned - <*a>
`X`holds if`X`holds in some past time point except time points in the method which already returned - (*a)
`X`holds if`X`holds at the previous time point except time points in the method which already returned -
`X`Sa`Y`holds if`Y`holds in some past time point except time points in the method which already returned, and since then`X`has held (strict since) - @b
`X`holds if`X`holds at every begin of the methods in the current stack - @c
`X`holds if`X`holds at every call to the methods in the current stack - <*s@b>
`X`holds if`X`holds at every begin of the methods in the stacks of some past time points - [*s@b]
`X`holds if`X`holds at every begin of the methods in the stacks of all past time points -
`X`Ss@b`Y`holds if`Y`holds at begin in some past time points, and since then`X`has held at every begin of the methods in the stacks - <*s@c>
`X`holds if`X`holds at every call of the methods in the stacks of some past time points - [*s@c]
`X`holds if`X`holds at every call of the methods in the stacks of all past time points -
`X`Ss@c`Y`holds if`Y`holds at call in some past time points, and since then`X`has held at every call of the methods in the stacks - <*s@c>
`X`holds if`X`holds at every begin or call of the methods in the stacks of some past time points - [*s@c]
`X`holds if`X`holds at every begin or call of the methods in the stacks of all past time points -
`X`Ss@c`Y`holds if`Y`holds at begin or call in some past time points, and since then`X`has held at every begin and call of the methods in the stacks

- [*]

### <PTCaRet State>

<PTCaRet State> instantiates <Logic State> from the MOP Syntax. In a PTCaRet specification, <PTCaRet State> can be either the special state validation or violation. validation corresponds to a situation wherein the trace satisfies the given formula, whereas violation occurs when the trace is not a prefix of any trace that satisfy the give formula.

### <Not>

The PTCaRet plugin supports various kinds of not operators

### <And>

The PTCaRet plugin supports various kinds of and operators

### <Or>

The PTCaRet plugin supports various kinds of or operators

### <Xor>

The PTCaRet plugin supports various kinds of xor operators

### <Implies>

The PTCaRet plugin supports various kinds of implies operators

### Example

<mop>

<Client>Web</Client>

<Events>a b c</Events>

<Property>

<Logic>ptcaret</Logic>

<Formula>a implies (not c Sa b)</Formula>

</Property>

<Categories>validation</Categories>

</mop>