# PTLTL Plugin Input Syntax

From FSL

PTLTL formulae use 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

<PTLTL Syntax> ::= {"event" <Event Name>} "ptltl" ":" <PTLTL Formula>

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

| <Event Name> // events are atomic propositions

| "!" <PTLTL Formula> | "not" <PTLTL Formula> // negation

| <PTLTL Formula> <And> <PTLTL Formula> // conjunction

| <PTLTL Formula> <Or> <PTLTL Formula> // disjunction

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

| <PTLTL Formula> <Implies> <PTLTL Formula> // implies

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

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

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

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

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

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

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

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

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

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

Events are the *atomic propositions* of the PTLTL formula. The different operators in decreasing order of precedence are
[*]`,`
<*>`,`
(*)`>`
!`,`
not `>`
S `>`
<And> `>`
<Xor> `>`
<Or>
`>` <Implies>
<->`>`.
The last five operators 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`S`Y`holds if`Y`holds now, or if`Y`holds in some past time point and since then`X`has held (strict since) - (*)
`X`holds if`X`holds at the previous time point - [
`X`,`Y`} holds if`Y`has not held since`X`held, and`Y`did not hold at the same time as`X`. It can be written as (not Y) S ((not Y) and X)

- [*]

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.

### Example

event create event updatesource event next ptltl : next and (<*> (updatesource and (<*> (next and (<*> create)))))