# FTLTL Plugin2.0 Input Syntax

From FSL

FTLTL 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

<FTLTL Syntax> ::= {"event" <Event Name>} "ftltl:" <FTLTL Formula>

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

| <Event Name> // events are atomic propositions

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

| <FTLTL Formula> <And> <FTLTL Formula> // conjunction

| <FTLTL Formula> <Or> <FTLTL Formula> // disjunction

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

| <FTLTL Formula> <Implies> <FTLTL Formula> // implies

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

| "[]" <FTLTL Formula> // always

| "<>" <FTLTL Formula> // eventually

| "o" <FTLTL Formula> | "()" <FTLTL Formula> // next

| <FTLTL Formula> "U" <Formula> // until

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

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

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

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

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

Events are the *atomic propositions* of the FTLTL formula. The different operators in decreasing order of precedence are
[]`,`
<>`,`
o`,`
()`>`
!`,`
not `>`
U `>`
<And> `>`
<Xor> `>`
<Or>
`>` <Implies>
<->`>`.
The last four operators are called *temporal* and have the following interpretation:

- []
`X`holds if`X`holds in all future time points - <>
`X`holds if`X`holds in some future time point -
`X`U`Y`holds if`Y`holds in some future time point, and until then`X`holds (strict until) - o
`X`or ()`X`holds if`X`holds at the next time point

- []

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

Consider the traffic light controller safety property "green implies no red until yellow":

event green event yellow event red ftltl : green -> (! red U yellow)