PTCaRet Plugin3 Input Syntax

From FSL
Jump to: navigation, search

The MOP PTCaRet 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
<PTCaRet Name> ::= "ptcaret"
<PTCaRet Syntax> ::= "true" | "false"
| <Event Name> // events are atomic propositions
| <Not> <PTCaRet Syntax> // negation
| <PTCaRet Syntax> <And> <PTCaRet Syntax> // conjunction
| <PTCaRet Syntax> <Or> <PTCaRet Syntax> // disjunction
| <PTCaRet Syntax> <Xor> <PTCaRet Syntax> // XOR: eXclusive OR
| <PTCaRet Syntax> <Implies> <PTCaRet Syntax> // implies
| <PTCaRet Syntax> "<->" <PTCaRet Syntax> // if and only if
| "[*]" <PTCaRet Syntax> // always in the past
| "<*>" <PTCaRet Syntax> // eventually in the past
| "(*)" <PTCaRet Syntax> // previously
| <PTCaRet Syntax> "S" <PTCaRet Syntax> // since
| "[*a]" <PTCaRet Syntax> // abstract always in the past
| "<*a>" <PTCaRet Syntax> // abstract eventually in the past
| "(*a)" <PTCaRet Syntax> // abstract previously
| <PTCaRet Syntax> "Sa" <PTCaRet Syntax> // abstract since
| "@b" <PTCaRet Syntax> // at begin
| "@c" <PTCaRet Syntax> // at call
| "<*s@b>" <PTCaRet Syntax> // eventually at begin in the stack
| "[*s@b]" <PTCaRet Syntax> // always at begin in the stack
| <PTCaRet Syntax> "Ss@b" <PTCaRet Syntax> // since at begin in the stack
| "<*s@c>" <PTCaRet Syntax> // eventually at call in the stack
| "[*s@c]" <PTCaRet Syntax> // always at call in the stack
| <PTCaRet Syntax> "Ss@c" <PTCaRet Syntax> // since at call in the stack
| "<*s@bc>" <PTCaRet Syntax> // eventually at begin or call
// in the stack
| "[*s@bc]" <PTCaRet Syntax> // always at begin or call
// in the stack
| <PTCaRet Syntax> "Ss@bc" <PTCaRet Syntax> // since at begin or call
// in the stack
 
<PTCaRet State> ::= "violation" | "validation"
 
// The auxiliary elements for the logic syntax
<Not> ::= "!" | "not"
<And> ::= "/\" | "and" | "&&"
<Or> ::= "\/" | "or" | "||"
<Xor> ::= "++" | "xor" | "^"
<Implies> ::= "->" | "=>" | "implies"

<PTCaRet Name>

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

<PTCaRet Syntax>

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

The last nineteen operators from <PTCaRet 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)
  • [*a] X holds if X holds in all past time points except time points in the method which already returned
  • <*a> X holds if X holds in some past time point except time points in the method which already returned
  • (*a) X holds if X holds at the previous time point except time points in the method which already returned
  • X Sa Y holds if Y holds in some past time point except time points in the method which already returned, and since then X has held (strict since)
  • @b X holds if X holds at every begin of the methods in the current stack
  • @c X holds if X holds at every call to the methods in the current stack
  • <*s@b> X holds if X holds at every begin of the methods in the stacks of some past time points
  • [*s@b] X holds if X holds at every begin of the methods in the stacks of all past time points
  • X Ss@b Y holds if Y holds at begin in some past time points, and since then X has held at every begin of the methods in the stacks
  • <*s@c> X holds if X holds at every call of the methods in the stacks of some past time points
  • [*s@c] X holds if X holds at every call of the methods in the stacks of all past time points
  • X Ss@c Y holds if Y holds at call in some past time points, and since then X has held at every call of the methods in the stacks
  • <*s@c> X holds if X holds at every begin or call of the methods in the stacks of some past time points
  • [*s@c] X holds if X holds at every begin or call of the methods in the stacks of all past time points
  • X Ss@c Y holds if Y holds at begin or call in some past time points, and since then X has held at every begin and call of the methods in the stacks

<PTCaRet State>

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

<And>

The PTCaRet plugin supports various kinds of and operators

<Or>

The PTCaRet plugin supports various kinds of or operators

<Xor>

The PTCaRet plugin supports various kinds of xor operators

<Implies>

The PTCaRet plugin supports various kinds of implies operators


Example

<mop>
<Client>Web</Client>
<Events>a b c</Events>
<Property>
<Logic>ptcaret</Logic>
<Formula>a implies (not c Sa b)</Formula>
</Property>
<Categories>validation</Categories>
</mop>
Personal tools
Namespaces

Variants
Actions
Navigation