FTLTL Plugin2.0 Input Syntax

From FSL
Jump to: navigation, search

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)
Personal tools
Namespaces

Variants
Actions
Navigation