de.uni_tuebingen.sfb.lichtenstein.binarytrees
Class MonaFormulaBuilder

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaVisitor
      de.uni_tuebingen.sfb.lichtenstein.binarytrees.MonaFormulaBuilder

All Implemented Interfaces:

MonaFormulaParser

public class MonaFormulaBuilder
extends FormulaVisitor
implements MonaFormulaParser

A class which visits a Formula and converts it to a Mona formula. It uses a mapping of predicates to variable names which do not conflict with Mona syntax.

Author:

Hendrik Maryns

Invariant:

The predicates mapping may not be null. | getPredicates() != null

Constructor Summary

MonaFormulaBuilder(Map<String,String> predicates)
Initialize a builder for MONA formulas.

Method Summary

String	parse() Parse the formula.
String	randomVarName() Create a random variable name.
protected void	visit(Conjunction form) Visit a conjunction.
protected void	visit(Disjunction form) Visit a disjunction.
protected void	visit(Dominance form) Visit a dominance atomic formula.
protected void	visit(Equivalence form) Visit an equivalence atomic formula.
protected void	visit(FirstOrderEquality form) Visit a first order equality atomic formula.
protected void	visit(FirstOrderExistentialQuantification form) Visit an existential quantification.
protected void	visit(FirstOrderUniversalQuantification form) Visit a universal quantification.
void	visit(Formula form) Visit a formula.
protected void	visit(ImmediateDominance form) Visit an immediate dominance atomic formula.
protected void	visit(Implication form) Visit an implication.
protected void	visit(Inclusion form) Visit an inclusion.
protected void	visit(Negation form) Visit a negation.
protected void	visit(Precedence form) Visit a precedence atomic formula.
protected void	visit(ProperDominance form) Visit a proper dominance atomic formula.
protected void	visit(SecondOrderEquality form) Visit a second order equality atomic formula.
protected void	visit(SecondOrderExistentialQuantification form) Visit an existential quantification.
protected void	visit(SecondOrderUniversalQuantification form) Visit a universal quantification.
protected void	visit(Subset form) Visit a subset atomic formula.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

MonaFormulaBuilder

public MonaFormulaBuilder(Map<String,String> predicates)

Initialize a builder for MONA formulas.

Parameters:

predicates -

Method Detail

parse

public String parse()

Parse the formula.

Specified by:

parse in interface MonaFormulaParser

visit

public void visit(Formula form)
           throws VisitorException

Visit a formula. Generally, subclasses will provide enough more specific methods to make sure the whole Formula compositum is visited properly.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(Negation form)
              throws VisitorException

Visit a negation.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(Conjunction form)
              throws VisitorException

Visit a conjunction.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(Disjunction form)
              throws VisitorException

Visit a disjunction.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(Implication form)
              throws VisitorException

Visit an implication.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(Equivalence form)
              throws VisitorException

Visit an equivalence atomic formula.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(FirstOrderExistentialQuantification form)
              throws VisitorException

Visit an existential quantification.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(FirstOrderUniversalQuantification form)
              throws VisitorException

Visit a universal quantification.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(SecondOrderExistentialQuantification form)
              throws VisitorException

Visit an existential quantification.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(SecondOrderUniversalQuantification form)
              throws VisitorException

Visit a universal quantification.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(FirstOrderEquality form)
              throws VisitorException

Visit a first order equality atomic formula.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(SecondOrderEquality form)
              throws VisitorException

Visit a second order equality atomic formula.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(Inclusion form)
              throws VisitorException

Visit an inclusion.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(Subset form)
              throws VisitorException

Visit a subset atomic formula.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(Dominance form)
              throws VisitorException

Visit a dominance atomic formula.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(ImmediateDominance form)
              throws VisitorException

Visit an immediate dominance atomic formula.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(ProperDominance form)
              throws VisitorException

Visit a proper dominance atomic formula.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

visit

protected void visit(Precedence form)
              throws VisitorException

Visit a precedence atomic formula.

Specified by:

visit in class FormulaVisitor

Parameters:

form - The formula to be visited.

Throws:

VisitorException - [CAN] A visitor can throw any exception. Visitors should thoroughly document this behaviour.

randomVarName

public String randomVarName()

Create a random variable name. This is important for not having different variables with the same name in the Mona file.

Postcondition:

The varNumber is increased by one. | new.varNumber == varNumber + 1

Returns:

A variable name that has not been used yet.