de.uni_tuebingen.sfb.lichtenstein.formulas
Class ImmediateDominance

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
      de.uni_tuebingen.sfb.lichtenstein.formulas.AtomicFormula
          de.uni_tuebingen.sfb.lichtenstein.formulas.ImmediateDominance

All Implemented Interfaces:

Formula, Visitable, Serializable

public final 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.
protected Set<Predicate>	computePredicates() Compute the set of predicates in this formula.
protected Set<Variable>	computeVariables() Simply return the two variables.
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	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

getNormalForm, isFree

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl

and, exists, exists, forAll, forAll, getFreeVariables, getPredicates, getVariables, iff, implies, isClosed, not, or

Methods inherited from class java.lang.Object

clone, finalize, 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

Postconditions:

The dominator variable is set to the given dominator variable. | new.getDominatingVariable() == dominator

The dominated variable is set to the given dominated variable. | new.getDominatedVariable() == dominated

Method Detail

getDominatingVariable

public FirstOrderVariable getDominatingVariable()

Returns the dominating variable.

Returns:

The first variable.

getDominatedVariable

public FirstOrderVariable getDominatedVariable()

Returns the dominated variable.

Returns:

The second variable.

computeVariables

protected Set<Variable> computeVariables()

Simply return the two variables.

Specified by:

computeVariables in class FormulaImpl

Returns:

The two variables in the right order. | result.size() == 2 && | result.contains(getDominatingVariable()) && | result.contains(getDominatedVariable())

containsVariable

public boolean containsVariable(Variable var)

Returns whether this formula contains the given variable.

Parameters:

var - The variable to check.

computePredicates

protected Set<Predicate> computePredicates()

Compute the set of predicates in this formula.

Specified by:

computePredicates in class FormulaImpl

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 VisitorException

Accept a formula visitor. The iteration is done by the visitor, not by the composed formulas.

Parameters:

visitor - The visitor that is to be accepted to do its work.

Throws:

VisitorException - [CAN] A visitor can throw an exception.