LTL Plugin2.2 Input Syntax

From FSL
Jump to: navigation, search

The LTL 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
<LTL Name> ::= "ltl"
<LTL Syntax> ::= "true" | "false"
| <Event Name> // events are atomic propositions
| <Not> <LTL Syntax> // negation
| <LTL Syntax> "and" <LTL Syntax> // conjunction
| <LTL Syntax> "or" <LTL Syntax> // disjunction
| <LTL Syntax> "xor" <LTL Syntax> // XOR: eXclusive OR
| <LTL Syntax> "=>" <LTL Syntax> // implies
| <LTL Syntax> "<=>" <LTL Syntax> // if and only if
| "[]" <LTL Syntax> // always
| "<>" <LTL Syntax> // eventually
| "o" <LTL Syntax> // next
| <LTL Syntax> "U" <LTL Syntax> // until
| "[*]" <LTL Syntax> // always in the past
| "<*>" <LTL Syntax> // eventually in the past
| "(*)" <LTL Syntax> // previously
| <LTL Syntax> "S" <LTL Syntax> // since
<LTL State> ::= "violation"

<LTL Name>

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

<LTL Syntax>

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

The last eight operators from <LTL Syntax> are called temporal and have the following interpretation:

  • [] X holds if X holds in all 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 X has holds until Y holds (strict since)
  • o X holds if X holds at the next time point
  • [*] 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 in some past time point, and since then X has held (strict since)
  • (*) X holds if X holds at the previous time point

<LTL State>

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

<And>

The LTL plugin supports various kinds of and operators

<Or>

The LTL plugin supports various kinds of or operators

<Xor>

The LTL plugin supports various kinds of xor operators

<Implies>

The LTL plugin supports various kinds of implies operators

Example

<mop>
<Client>Web</Client>
<Events>acquire request</Events>
<Property>
<Logic>ltl</Logic>
<Formula>[](acquire => (*) request)</Formula>
</Property>
<Categories>violation</Categories>
</mop>
Personal tools
Namespaces

Variants
Actions
Navigation