PTCaRet Plugin2.0 Output Syntax

From FSL
Jump to: navigation, search

The MOP PTCaRet 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
 
<PTCaRet Plugin Output> ::= "monitor contains:"
<Nat> "global bits"
<Nat> "stack bits"
"initialization of monitor state"
<Code>
"monitoring code"
<Code>
"accepting condition:"
<Expression>
<Nat> ::= //Natural Number
<Code> ::= { "if begin then {" <Code> "}"
| "if end then {" <Code> "}"
| "push(beta)" | "pop(beta)" | "exit"
| <Assignment> }
<Assignment> ::= <BitIndex> ":=" <Expression>
<Expression> ::= <Expression> "or" <Expression
| <Expression> "and" <Expression>
| "not" <Expression>
| <Atom>
<Atom> ::= <BitIndex> | <Identifier> | "true" | "false"
<BitIndex> ::= "beta[" <Nat> "]" | "alpha[" <Nat> "]"


The PTCaRet plugin generates a monitor from the input formula, which updates its state according to the observed event and the previous state. The state of the monitor is represented as two arrays of bits, namely, one for standard temporal operators and one for abstract temporal operators.


Example

monitor contains:
	1 global bits 
	2 stack bits 
initialization of monitor state 
	beta[0] := false 
	beta[1] := false 
	alpha[0] := false 
monitoring code 
	if begin then {
	  push(beta) 
	  exit
	} 
	if end then {
	  pop(beta) 
	  exit
	} 
	beta[0] := open or not close and beta[0] 
	beta[1] := begin or not open and beta[1] 
	alpha[0] := alpha[0] or end and not beta[1] and beta[0] 
accepting condition:
	not alpha[0]
Personal tools
Namespaces

Variants
Actions
Navigation