de.upb.swt.mcie.parser
Class Parser

java.lang.Object
  extended by de.upb.swt.mcie.parser.Parser

public class Parser
extends java.lang.Object

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.

Author:
Ekkart Kindler, kindler@upb.de
See Also:
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

scanner

private Scanner scanner
The corresponding scanner.

Constructor Detail

Parser

public Parser(java.io.Reader reader)
       throws java.io.IOException
Constructs a new parser for the Reader. In particular, it instantiates a scanner with this Reader.

Parameters:
reader - the Reader with the text to be parsed
Throws:
java.io.IOException - if an IO problem occurs
See Also:
Scanner
Method Detail

parseEnd

public void parseEnd()
              throws java.io.IOException,
                     ParseException
Checks whether the end of the parser's input is reached. If the end is not reached a ParseException is thrown. This method does not return any result.

Throws:
ParseException - if there is any input left
java.io.IOException - if an IO problem occurs

parseToEnd

public Formula parseToEnd()
                   throws java.io.IOException,
                          ParseException
Parses the remaining part of the text in the 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.

Returns:
the internal representation of the parsed formula
Throws:
ParseException - if the remaining text is not a formula
java.io.IOException - if an IO problem occurs

parse

public Formula parse()
              throws java.io.IOException,
                     ParseException
Parses the reader starting from the current position. If there are characters left after completely parsing a formula, this is not considered as a parse error. Subsequent parse operations will start from this position. This way, this method can be used for parsing a sequence of formulas.

Returns:
the internal representation of the parsed formula
Throws:
ParseException - if the character sequence does not start with a formula
java.io.IOException - if an IO problem occurs

parse

private Formula parse(int bindlevel)
               throws java.io.IOException,
                      ParseException
The internal recursive decent parse method. The bindlevel indicates which binary and unary operations are considered at this level. This way operators, with the lowest binding level have highest binding priority.

Parameters:
bindlevel - defines the bind level of operators to be considered
Returns:
the formula parsed on this bindlevel
Throws:
ParseException - if a parse error is encountered
java.io.IOException - if an IO problem occurs

parseAtoms

private Formula parseAtoms()
                    throws java.io.IOException,
                           ParseException
Parses the atoms of a formula. An atom is either a variable resp. an identifier, a constant, or a formula in parenthesis.

Returns:
the internal representation of the atom
Throws:
ParseException - if a parse error occurs
java.io.IOException - if an IO problem occurs

parseFormulaList

public Formula[] parseFormulaList()
                           throws java.io.IOException,
                                  ParseException
Parses and returns a list of formulas. The formulas must be separated by a separator 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.

Returns:
an array of formulas
Throws:
ParseException - if the character sequence does not start with list of formulas
java.io.IOException - if an IO problem occurs

parseKripkestructure

public Kripkestructure parseKripkestructure(Context context)
                                     throws java.io.IOException,
                                            ParseException
Parses a Kripke structure and returns it as result. A Kripke structure must have the following form:

( < state formula > , < transition formula > )

The first state formula represents the initial state and the transition formula represents the transition relation.

Parameters:
context - the context for the Kripke structure
Returns:
the parsed Kripke structure
Throws:
java.io.IOException - if an IO problem occurs
ParseException - if a parse error occurs

parseFairKripkestructure

public FairModel parseFairKripkestructure(Context context)
                                   throws java.io.IOException,
                                          ParseException
Parses a fair Kripke structure and returns it as result. A fair Kripke structure must have the following form:

( < 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.

Parameters:
context - the context for the Kripke structure
Returns:
the parsed Kripke structure
Throws:
java.io.IOException - if an IO problem occurs
ParseException - if a parse error occurs

parseTransitionsystem

public Transitionsystem parseTransitionsystem(Context context)
                                       throws java.io.IOException,
                                              ParseException
Parses a transition system and returns it as result. A transition system must have the following form:

( < 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.

Parameters:
context - the context for the transition system
Returns:
the parsed transition structure
Throws:
java.io.IOException - if an IO problem occurs
ParseException - if a parse error occurs

parseFairTransitionsystem

public FairModel parseFairTransitionsystem(Context context)
                                    throws java.io.IOException,
                                           ParseException
Parses a fair transition system and returns it as result. A transition system must have the following form:

( < 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.

Parameters:
context - the context for the fair transition system
Returns:
the parsed fair transition system
Throws:
java.io.IOException - if an IO problem occurs
ParseException - if a parse error occurs