de.uni_tuebingen.sfb.lichtenstein.formulas
Class ImmediateDominance

java.lang.Object
  extended by de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
      extended by de.uni_tuebingen.sfb.lichtenstein.formulas.AtomicFormula
          extended by de.uni_tuebingen.sfb.lichtenstein.formulas.ImmediateDominance
All Implemented Interfaces:
Formula, Visitable, Serializable

public class ImmediateDominance
extends AtomicFormula

A class representing the atomic formula which says one node immediately dominates another.

Author:
Hendrik Maryns
See Also:
Serialized Form

Constructor Summary
ImmediateDominance(FirstOrderVariable dominator, FirstOrderVariable dominated)
          Initialize a new immediate dominance, taking two variables as arguments.
 
Method Summary
 void accept(FormulaVisitor visitor)
          Accept a formula visitor.
 boolean containsVariable(Variable var)
          Returns whether this formula contains the given variable.
 boolean equals(Object other)
          Indicates whether some other object is "equal to" this one.
 FirstOrderVariable getDominatedVariable()
          Returns the dominated variable.
 FirstOrderVariable getDominatingVariable()
          Returns the dominating variable.
 int getFirstIndexOf(Variable var)
          Get the first index at which the given variable occurs.
 int getNbVariables()
          Returns the number of variables in this formula.
 Set<Predicate> getPredicates()
          Return all predicates that occur in this formula.
 Variable getVariableAt(int index)
          Get the indexth variable (free or bound).
 int hashCode()
          Returns a hash code value for the object.
 String toString()
          Returns a string representation of the object.
 
Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.AtomicFormula
getNbBoundVariables, getNbFreeVariables, getNormalForm, isFreeVariable
 
Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
and, exists, exists, forAll, forAll, getFreeVariables, getVariables, iff, implies, isClosed, not, or
 
Methods inherited from class java.lang.Object
getClass, notify, notifyAll, wait, wait, wait
 

Constructor Detail

ImmediateDominance

public ImmediateDominance(FirstOrderVariable dominator,
                          FirstOrderVariable dominated)
Initialize a new immediate dominance, taking two variables as arguments.

Parameters:
dominator - The variable which is dominating the other variable.
dominated - The variable which is dominated by the other variable.
Precondition:
Both variables must be effective.
| dominator != null && dominated != null
Postcondition:
The dominator variable is set to the given dominator variable.
| new.getDominatingVariable() == dominator
Postcondition:
The dominated variable is set to the given dominated variable.
| new.getDominatedVariable() == dominated
Method Detail

getDominatingVariable

public FirstOrderVariable getDominatingVariable()
Returns the dominating variable.

Returns:
This is the first variable.
| result == getVariableAt(0)

getDominatedVariable

public FirstOrderVariable getDominatedVariable()
Returns the dominated variable.

Returns:
This is the second variable.
| result == getVariableAt(0)

getNbVariables

public int getNbVariables()
Returns the number of variables in this formula.

Returns:
Always 2.
| result == 2

getFirstIndexOf

public int getFirstIndexOf(Variable var)
Get the first index at which the given variable occurs.

Parameters:
var - The variable of which the index is wanted.

getVariableAt

public Variable getVariableAt(int index)
                       throws IndexOutOfBoundsException
Get the indexth variable (free or bound).

Parameters:
index - The index of the wanted variable

containsVariable

public boolean containsVariable(Variable var)
Returns whether this formula contains the given variable.

Parameters:
var - The variable to check.

getPredicates

public Set<Predicate> getPredicates()
Return all predicates that occur in this formula. TODO

Returns:
An immediate dominance cannot contain predicates.
| result.isEmpty()

equals

public boolean equals(Object other)
Indicates whether some other object is "equal to" this one.

Overrides:
equals in class FormulaImpl
Returns:
Two equalities are equal if they compare the same variables.
| let otherEquals = (Dominance) other in | if ( otherEquals.getDominatingVariable() != getDominatingVariable() ) | then result == false | if ( otherEquals.getDominatedVariable() != getDominatedVariable() ) | then result == false

hashCode

public int hashCode()
Returns a hash code value for the object.

Specified by:
hashCode in class FormulaImpl
Returns:
The hash code is based on the hash codes of the variables and of the characteristic symbol.
| result == getDominatingVariable().hashCode() + "⊲".hashCode() + getDominatedVariable().hashCode()

toString

public String toString()
Returns a string representation of the object.

Specified by:
toString in class FormulaImpl
Returns:
The string representations of the variables are given, with the equal sign: = in between them.
| result == getDominatingVariable().toString() + "⊲" + getDominatedVariable().toString()

accept

public void accept(FormulaVisitor visitor)
            throws de.uni_tuebingen.sfb.lichtenstein.exceptions.VisitorException
Accept a formula visitor. The iteration is done by the visitor, not by the composed formulas.

Specified by:
accept in interface Visitable
Overrides:
accept in class FormulaImpl
Parameters:
visitor - The visitor that is to be accepted to do its work.
Throws:
VisitorException
A visitor can throw an exception.