|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl de.uni_tuebingen.sfb.lichtenstein.formulas.AtomicFormula de.uni_tuebingen.sfb.lichtenstein.formulas.Dominance
public class Dominance
A class representing the atomic formula which says one node dominates another. This is the transitive, reflexive closure of immediate dominance.
Constructor Summary | |
---|---|
Dominance(FirstOrderVariable dominator,
FirstOrderVariable dominated)
Initialize a new 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 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 |
---|
public Dominance(FirstOrderVariable dominator, FirstOrderVariable dominated)
dominator
- The variable which is dominating the other variable.dominated
- The variable which is dominated by the other variable.| dominator != null && dominated != null
| new.getDominatingVariable() == dominator
| new.getDominatedVariable() == dominated
Method Detail |
---|
public FirstOrderVariable getDominatingVariable()
| result == getVariableAt(0)
public FirstOrderVariable getDominatedVariable()
| result == getVariableAt(0)
public int getNbVariables()
| result == 2
public int getFirstIndexOf(Variable var)
var
- The variable of which the index is wanted.public Variable getVariableAt(int index) throws IndexOutOfBoundsException
index
- The index of the wanted variablepublic boolean containsVariable(Variable var)
var
- The variable to check.public Set<Predicate> getPredicates()
| result.isEmpty()
public boolean equals(Object other)
equals
in class FormulaImpl
| let otherEquals = (Dominance) other in |
if ( otherEquals.getDominatingVariable() != getDominatingVariable() )
| then result == false | if (
otherEquals.getDominatedVariable() != getDominatedVariable() )
| then result == false
public int hashCode()
hashCode
in class FormulaImpl
| result ==
getDominatingVariable().hashCode() + "⊲*".hashCode() + getDominatedVariable().hashCode()
public String toString()
toString
in class FormulaImpl
| result == getDominatingVariable().toString() + "⊲*" + getDominatedVariable().toString()
public void accept(FormulaVisitor visitor) throws de.uni_tuebingen.sfb.lichtenstein.exceptions.VisitorException
accept
in interface Visitable
accept
in class FormulaImpl
visitor
- The visitor that is to be accepted to do its work.
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |