PTLTL Plugin Input Syntax

From FSL
Jump to: navigation, search

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

Variants
Actions
Navigation