|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectde.upb.swt.mcie.parser.Parser
public class Parser
This class implementing the parser. Upon creation, the parser will
be provided with a Reader
with the text to be parsed.
Then, the class provides different parse operations to convert this
text to a formula, to a list of formulas, or to a Kripke structrue.
Note that the parser does not work directly on the reader. It instantiates
a Scanner
on the reader, and then works on
the tokens produced by the this scanner.
Scanner
Field Summary | |
---|---|
private Scanner |
scanner
The corresponding scanner. |
Constructor Summary | |
---|---|
Parser(java.io.Reader reader)
Constructs a new parser for the Reader . |
Method Summary | |
---|---|
Formula |
parse()
Parses the reader starting from the current position. |
private Formula |
parse(int bindlevel)
The internal recursive decent parse method. |
private Formula |
parseAtoms()
Parses the atoms of a formula. |
void |
parseEnd()
Checks whether the end of the parser's input is reached. |
FairModel |
parseFairKripkestructure(Context context)
Parses a fair Kripke structure and returns it as result. |
FairModel |
parseFairTransitionsystem(Context context)
Parses a fair transition system and returns it as result. |
Formula[] |
parseFormulaList()
Parses and returns a list of formulas. |
Kripkestructure |
parseKripkestructure(Context context)
Parses a Kripke structure and returns it as result. |
Formula |
parseToEnd()
Parses the remaining part of the text in the Reader . |
Transitionsystem |
parseTransitionsystem(Context context)
Parses a transition system and returns it as result. |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
---|
private Scanner scanner
Constructor Detail |
---|
public Parser(java.io.Reader reader) throws java.io.IOException
Reader
. In
particular, it instantiates a scanner with this Reader
.
reader
- the Reader
with the text to be parsed
java.io.IOException
- if an IO problem occursScanner
Method Detail |
---|
public void parseEnd() throws java.io.IOException, ParseException
ParseException
is thrown. This method does not return
any result.
ParseException
- if there is any input left
java.io.IOException
- if an IO problem occurspublic Formula parseToEnd() throws java.io.IOException, ParseException
Reader
.
If the remaining part is a formula, this formula is returned. If the reader
has not reached its end after completely parsing the formula, a
ParseException
is thrown.
ParseException
- if the remaining text is not a formula
java.io.IOException
- if an IO problem occurspublic Formula parse() throws java.io.IOException, ParseException
ParseException
- if the character sequence does not start with
a formula
java.io.IOException
- if an IO problem occursprivate Formula parse(int bindlevel) throws java.io.IOException, ParseException
bindlevel
- defines the bind level of operators to be considered
ParseException
- if a parse error is encountered
java.io.IOException
- if an IO problem occursprivate Formula parseAtoms() throws java.io.IOException, ParseException
ParseException
- if a parse error occurs
java.io.IOException
- if an IO problem occurspublic Formula[] parseFormulaList() throws java.io.IOException, ParseException
Sep
.
If the list ends with a token other than a separator, the
parser returns the list of formulas parsed up to that point,
leaving the rest of the sequence untouched. This way, it is
possible to parse the remaining part of the input with a different
method.
ParseException
- if the character sequence does not
start with list of formulas
java.io.IOException
- if an IO problem occurspublic Kripkestructure parseKripkestructure(Context context) throws java.io.IOException, ParseException
( < state formula > , < transition formula > )
The first state formula represents the initial state and the transition formula represents the transition relation.
context
- the context for the Kripke structure
java.io.IOException
- if an IO problem occurs
ParseException
- if a parse error occurspublic FairModel parseFairKripkestructure(Context context) throws java.io.IOException, ParseException
( < state formula > , < transition formula > , { < state formula > , ... , < state formula > } )
The first state formula represents the initial state, the transition formula represents the transition relation, the state formulas in braces represent the set of fairness conditions.
context
- the context for the Kripke structure
java.io.IOException
- if an IO problem occurs
ParseException
- if a parse error occurspublic Transitionsystem parseTransitionsystem(Context context) throws java.io.IOException, ParseException
( < state formula > , { < transition formula > , ... , < transition formula > } )
The first state formula represents the initial state and the transition formulas in braces represent the transitions. Note that a transition does only change those variables that do occur primed in the transition. All other variables will not be changed by this particular transition.
context
- the context for the transition system
java.io.IOException
- if an IO problem occurs
ParseException
- if a parse error occurspublic FairModel parseFairTransitionsystem(Context context) throws java.io.IOException, ParseException
( < state formula > , { < transition formula > , ... , < transition formula > } , { < state formula > , ... , < state formula > } )
The first state formula represents the initial state, the transition formulas in braces represent the transitions, the state formulas in braces represent the set of fairness conditions. Note that a transition does only change those variables that do occur primed in the transition. All other variables will not be changed by this particular transition.
context
- the context for the fair transition system
java.io.IOException
- if an IO problem occurs
ParseException
- if a parse error occurs
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |