|
|||||||||
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.Precedence
public class Precedence
A class representing the atomic formula which says one node precedes another.
Constructor Summary | |
---|---|
Precedence(FirstOrderVariable preceder,
FirstOrderVariable preceded)
Initialize a new precedence, 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. |
int |
getFirstIndexOf(Variable var)
Get the first index at which the given variable occurs. |
int |
getNbVariables()
Returns the number of variables in this formula. |
FirstOrderVariable |
getPrecededVariable()
Returns the preceded variable. |
FirstOrderVariable |
getPrecedingVariable()
Returns the preceding variable. |
Set<Predicate> |
getPredicates()
Return all predicates in this formula. |
Variable |
getVariableAt(int index)
Get the indexth 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 |
---|
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 Precedence(FirstOrderVariable preceder, FirstOrderVariable preceded)
preceder
- The variable which is preceding the other variable.preceded
- The variable which is preceded by the other variable.| preceding != null && preceded != null
| new.getPrecedingVariable() == preceding
| new.getPrecededVariable() == preceded
Method Detail |
---|
public FirstOrderVariable getPrecedingVariable()
| result == getVariableAt(0)
public FirstOrderVariable getPrecededVariable()
| 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.getPrecedingVariable() != getPrecedingVariable() )
| then result == false | else if (
otherEquals.getPrecededVariable() != getPrecededVariable() )
| then result == false | else result ==true
public int hashCode()
hashCode
in class FormulaImpl
| result ==
getPrecedingVariable().hashCode() + "≺*".hashCode() + getPrecededVariable().hashCode()
public String toString()
toString
in class FormulaImpl
| result == getPrecedingVariable().toString() + "≺*" + getPrecededVariable().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 |