SRS Plugin3 Input Syntax

From FSL
Jump to: navigation, search

The MOP SRS 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
<SRS Name> ::= "srs"
<SRS Syntax> ::= <Rule> {"." <Rule>}
<SRS State> ::= "succeed" | "fail"
// The auxiliary elements for the logic syntax
<Rule> ::= <Left Hand Side> "->" <Right Hand Side>
<Left Hand Side> ::= ["^"] <String> ["$"]
<Right Hand Side> ::= <String> | "#" <SRS State> | "#epsilon"
<String> ::= <Symbol> | <Event Name> { <Symbol> | <Event Name> }
<Symbol> ::= // user defined strings of characters that are not
// predefined events

This page describes only the input syntax of the SRS plugin. The operation of SRS monitors can be found on the SRS Monitoring Algorithm page.

<SRS Name>

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

<SRS Syntax>

<SRS Syntax> instantiates <Logic Syntax> from the MOP Syntax. It defines a string rewriting system, which is composed of multiple <Rule>s.

<SRS State>

<SRS State> instantiates <Logic State> from the MOP Syntax. In a SRS specification, <SRS State> can be either the special state succeed or fail. succeed corresponds to a situation wherein the rewriting has succeeded for some success criterion, whereas fail occurs when some user defined failure criterion is met. The SRS monitor is unable to leave the fail or succeed states once they are reached.


A <Rule> is generally a pair of <Strings> separated by ->. When rewriting is performed, the left hand side of a pair is rewritten to the right hand side, if the left hand side matches anywhere in the current buffer of symbols. The left hand side may also contain the ^ and $, which denote the beginning and end of the character buffer, respectively. The right hand side of a rule may be the empty string, #epsilon, or one of the two <SRS State> preceded by # instead of a normal string.


A <String> is any number of <Event Name>s or <Symbols>s.

<NonTerminal Name>

<NonTerminal Name> is a user defined identifier that is not one of the event names.


<Events>a b</Events>
hasnexttrue hasnexttrue -> hasnexttrue .
hasnexttrue next -> #epsilon .
^ next -> #fail .

This example monitors the HasNext property, which states that hasNext must be called and return true before every call to the next method.

Personal tools