FTLTL Plugin2.0 Output Syntax

From FSL
Jump to: navigation, search

The MOP FTLTL 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
 
<FTLTL Plugin Output> ::= "Starting state:" <Nat> "Transitions:" <Switch>
<Nat> ::= //Any natural number
<Switch> ::= "switch (state) {" { <Transition> } "}"
<Transition> ::= "case " <Nat> ": state <- " <ConditionalExpression>
<ConditionalExpression> ::= <Identifier> "?" <ConditionalExpression> ":" <ConditionalExpression>
| <Nat>

The FTLTL 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 natural number. The Starting state identifies which state the monitor should begin in. "?" is the standard conditional operator of C-like languages.


Example

Starting state: 1
Transitions:
switch (state) {
  case 1: state <- yellow ? 1 : green ? red ?  false  : 2 : 1
  case 2: state <- yellow ? 1 : red ?  false  : 2
}
Personal tools
Namespaces

Variants
Actions
Navigation