|
||||||||||
PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES |
See:
Description
Class Summary | |
---|---|
Parser | This class implementing the parser. |
Scanner | This class implements the scanner. |
Exception Summary | |
---|---|
ParseException | Represents a parse exception. |
This package implements a parser and compiler for formulas and models. It parses
a given text from some Reader
and, if syntactically correct,
returns the internal representation of this Formula
or Model
.
The formula can be a state formulas, a transition formulas, or a temporal formula.
A state formula does not contain temporal operators and no primed variables. A
transition formula must not contain temporal operators, but may contain primed
variables. A temporal formula may contain temporal operators (CTL operators), but
must not contain primed variables (see Formula
for
details).
Concerning models, there are methods for parsing
Kripkestructures
and
Transitionsystems
as well as
the fair versions of them.
The parser is defined in a generic way such that it is easy to extend formulas
with new unary and binary operations. In particular, the binding priority of
all operators is defined in the classes BinaryOp
and
UnaryOp
. Also the information, which operators are
temporal operators is not known to the parser. The lexical representation of
the operations is defined in the class Scanner
.
The only information encoded directly into the parser is that all binary operators
associate from the left to the right; for example, the formula
a1 & a2 & a3 &... & an
is parsed in the following way
((... ((a1 & a2) & a3) & ... )
& an ).
Moreover, the parser resp. the scanner defines legal brackets. Currently, there
are parenthesis and square brackets, which must be properly matched. But,
there is no other meaning in the different brackets. The use of different
brackets should help to make formulas more readable.
Note that the binary CTL-formulas are represented as a single operator. So an until formula reads f EU g instead of E[ f U g ].
The parser is a simple recursive descend procedure with one token look ahead.
To be more precise, the parser may return the last token to the scanner
(see method revert
of class
Scanner
).
The tokens returned by the scanner are provided in the package
de.upb.swt.mcie.parser.token
.
Within the text the scanner will ignore the rest of a line, when it encounters the symbol #. So, # indicates a line comment.
de.upb.swt.mcie.formulas
,
de.upb.swt.mcie.parser.token
|
||||||||||
PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES |