LogicRepository3 Syntax

From FSL
Jump to: navigation, search

Links:
MOP

The syntax below uses BNF. Since the LogicRepository consists of several logics, the LogicRepository syntax is composed of two kinds of constructs, generic XML constructs and logic-specific constructs. We define the generic ones on this page, and also describe which constructs need to be instantiated for a specific logic.

// BNF below is extended with {p} for zero or more and [p] for zero or one
 
// The generic syntax
<Logic Repository I/O> ::= "<mop>"
[ <Client Name> ]
[ <Events> ]
[ <Property> ]
[ <Categories> ]
[ <CreationEvents> ]
[ <EnableSets> ]
[ <Statistics> ]
{ <Message> }
"</mop>"
 
<Client Name> ::= "<Client>" <Id> "</Client>"
<Events> ::= "<Events>" <Id> {<Id>} "</Events>"
<Property> ::= "<Property>"
"<Logic>" <Logic Name> "</Logic>"
"<Formula>" <Logic Syntax> "</Formula>"
"</Property>"
<Categories> ::= "<Categories>" <Logic State> {<Logic State>} "</Categories>"
<CreationEvents> ::= "<CreationEvents>" <Id> {<Id>} "</CreationEvents>"
<EnableSets> ::= "<EnableSets>" {"//" <Id> "Enables" <EnableSet>} "</EnableSets>"
<Statistics> ::= "<Statistics>"
"<TotalMOPCount>" <Int> "</TotalMOPCount>"
"<CurrentClient>" <String> "</CurrentClient>"
"<ClientCount>" <Int> "</ClientCount>"
"<CurrentLogic>" <String> "</CurrentLogic>"
"<LogicCount>" <Int> "</LogicCount>"
"<ClientAndLogicCount>" <Int> "</ClientAndLogicCount>"
"<TotalExecutionTime>" <String> "</TotalExecutionTime>"
"</Statistics>"
<Message> ::= "<Message>" <String> "</Message>"
<EnableSet> ::= "{" [{ <EnableMap> ","} <EnableMap>] "}"
<EnableMap> ::= <Id> "=" "[" [{<Id> ","} <Id>] "]"
<String> ::= // any string that does not include the closing tag which
terminates it
<Int> ::= // an integer number
 
// The logic-plugin-specific syntax
<Logic Name> ::= <Id>
<Logic Syntax> ::= // the requirements syntax provided by the logic plugin
specified by the Logic Name
<Logic State> ::= // identifiers denoting states to which handlers can be
associated, e.g., violation

Generic Syntax Constructs

The following syntax constructs are shared by different logics:


<Logic Repository I/O>

<Logic Repository I/O> describes the generic input and output Logic Repository syntax which can be extended for MOP logic plugins.

Logic Repository Input Mandatory Constructs

The following constructs must be present in an input file to the Logic Repository. It would be impossible to generate a monitor without these constructs.

<Client Name>

<Client Name> is used to tell the Logic Repository which client it is communicating with. This is useful for keeping statistics. Current clients include the website, JavaMOP, and BusMOP, but more will follow.

<Events>

<Events> are the events with which the property is concerned. <Events> must be specified in the input sent to the logic repository for monitor generation.

<Property>

<Property> contains two parts: the <Logic Name> which denotes which logic the property is written in, and the <Formula>, which is the formal representation of the property, itself. The <Property> must be specified in the input sent to the logic repository for monitor generation.

<Categories>

<Categories> alert the logic plugin as to which categories are relevant. This allows it to compute the necessary creation events and enable sets. Possible categories include (but are not limited to): fail and match. The <Categories> must be specified in the input sent to the logic repository for monitor generation.

Input Example

The following Logic Repository input states that a program always calls the hasNext method before the next method of an iterator :

<mop>
<Client>Web</Client>
<Events>hasNext next</Events>
<Property>
<Logic>ere</Logic>
<Formula>(hasNext hasNext* next)*</Formula>
</Property>
<Categories>fail</Categories>
</mop>

Other Constructs

These constructs are totally optional, and are more likely to be found in output from the Logic Repository than in input to it.

<Creation Events>

<Creation Events> denote which events may create new monitors. They are determined based on which categories the property is interested in, i.e., creation events are the first event that may appear in any trace which leads to a given category. These are generated by the logic plugins, rather than specified by a client.

<Enable Sets>

<Enables Sets> are another item specified by the logic plugins rather than the clients. They are the set of events that may be seen in a trace leading to a given state which has a path to a state in a given category. They are very similar to creation events.

<Statistics>

<Statistics> are different statistics kept by the Logic Repository. This item is used to convey these statistics to or from clients. <TotalMOPCount> is the number of MOP monitors generated for any client.<CurrentClient> is a string representing the current client which requested the monitor. <ClientCount> is the number of monitors generated for the given client. <CurrentLogic> is the current logic in use, e.g. fsm, ere, cfg. <LogicCount> is the number of monitors generated for a given logic. <ClientAndLogicCount> is the number of monitors generated for a given logic and client. <TotalExecutionTime> is the elapsed time of monitor generation.

<Meesage>

<Message> may be any arbitrary message to or from the Logic Repository.

Output Example

The following Logic Repository output uses the same syntax as the input, but different portions are instantiated. It is a valid output for the HasNext property seen above as an Input Example:

<mop>
<Client>Web</Client>
<Events>hasNext next</Events>
<Property>
<Logic>fsm</Logic>
<Formula>
s0[
hasNext -> s1
]
s1[
hasNext -> s1
next -> s0
]
</Formula>
<CreationEvents> hasNext </CreationEvents>
<EnableSets>
//fail Enables
{hasnext=[[], [hasnext], [hasnext, next], [next]],
next=[[], [hasnext], [hasnext, next], [next]]}
</EnableSets>
</mop>

Logic-Specific Syntax Constructs

What follows are the syntactic constructs that need be extended by every logic plugin. The following links show how they are extended for the current MOP logic plugins:

<Logic Name>

An identifier to indicate in which logic a property is defined.

<Logic Syntax>

This refers to the syntax of the actual property definition, and is defined on the syntax page for each plugin.

<Logic State>

<Logic State>s are constants defined for each plugin, telling for which monitor states a handler may be written.

Personal tools
Namespaces

Variants
Actions
Navigation