PTLTL Plugin3 Input Syntax

From FSL
Jump to: navigation, search

The MOP PTLTL plugin syntax instantiates the generic <Logic Name>, <Logic Syntax>, and <Logic State> from the Logic Repository Syntax. It is used in conjunction with the <Logic Repository I/O> syntax, and defined using 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
<PTLTL Name> ::= "ptltl"
<PTLTL Syntax> ::= "true" | "false"
| <Event Name> // events are atomic propositions
| <Not> <PTLTL Syntax> // negation
| <PTLTL Syntax> <And> <PTLTL Syntax> // conjunction
| <PTLTL Syntax> <Or> <PTLTL Syntax> // disjunction
| <PTLTL Syntax> <Xor> <PTLTL Syntax> // XOR: eXclusive OR
| <PTLTL Syntax> <Implies> <PTLTL Syntax> // implies
| <PTLTL Syntax> "<->" <PTLTL Syntax> // if and only if
| "[*]" <PTLTL Syntax> // always in the past
| "<*>" <PTLTL Syntax> // eventually in the past
| "(*)" <PTLTL Syntax> // previously
| <PTLTL Syntax> "S" <PTLTL Syntax> // since
<PTLTL State> ::= "violation" | "validation"
 
// The auxiliary elements for the logic syntax
<Not> ::= "!" | "not"
<And> ::= "/\" | "and" | "&&"
<Or> ::= "\/" | "or" | "||"
<Xor> ::= "++" | "xor" | "^"
<Implies> ::= "=>" | "implies"

<PTLTL Name>

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

<PTLTL Syntax>

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

The last four operators from <PTLTL Syntax> 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 holds if X holds at the previous time point
  • X S Y holds if Y holds in some past time point, and since then X has held (strict since)

<PTLTL State>

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

<And>

The PTLTL plugin supports various kinds of and operators

<Or>

The PTLTL plugin supports various kinds of or operators

<Xor>

The PTLTL plugin supports various kinds of xor operators

<Implies>

The PTLTL plugin supports various kinds of implies operators

Example

<mop>
<Client>Web</Client>
<Events>create updatesource next</Events>
<Property>
<Logic>ptltl</Logic>
<Formula>next and (<*> (updatesource and (<*> (next and (<*> create)))))</Formula>
</Property>
<Categories>validation</Categories>
</mop>
Personal tools
Namespaces

Variants
Actions
Navigation