# PTLTL Plugin2.2 Input Syntax

The PTLTL plugin uses the following syntax, which is defined in 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

<PTLTL Name> ::= "ptltl"

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

| <Event Name> // events are atomic propositions

| <Not> <PTLTL Syntax> // negation

| <PTLTL Syntax> <And> <PTLTL Syntax> // conjunction

| <PTLTL Syntax> <Or> <PTLTL Syntax> // disjunction

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

| <PTLTL Syntax> <Implies> <PTLTL Syntax> // implies

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

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

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

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

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

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

// The auxiliary elements for the logic syntax

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

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

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

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

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

### <PTLTL Name>

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

### <PTLTL Syntax>

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

The last four operators from <PTLTL 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)

- [*]

### <PTLTL State>

<PTLTL State> instantiates <Logic State> from the MOP Syntax. In a PTLTL specification, <PTLTL 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 PTLTL plugin supports various kinds of not operators

### <And>

The PTLTL plugin supports various kinds of and operators

### <Or>

The PTLTL plugin supports various kinds of or operators

### <Xor>

The PTLTL plugin supports various kinds of xor operators

### <Implies>

The PTLTL plugin supports various kinds of implies operators

### Example

<mop>

<Client>Web</Client>

<Events>create updatesource next</Events>

<Property>

<Logic>ptltl</Logic>

<Formula>next and (<*> (updatesource and (<*> (next and (<*> create)))))</Formula>

</Property>

<Categories>validation</Categories>

</mop>