|
|||||||||
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.Subset
public class Subset
A class for representing the atomic formula which says a variable is a subset of another variable
Constructor Summary | |
---|---|
Subset(SetDenotator subSet,
SetDenotator superSet)
Initialize a new subset formula, involving the variable which is a subset and the variable which is a superset. |
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. |
Set<Predicate> |
getPredicates()
Return all predicates in this formula. |
SetDenotator |
getSubsetVariable()
Returns the subset variable. |
SetDenotator |
getSupersetVariable()
Returns the superset variable. |
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 Subset(SetDenotator subSet, SetDenotator superSet)
subSet
- The variable which is a subset.superSet
- The variable which is a superset.| subSet != null && superSet != null
| new.getSubsetVariable() == subSet
| new.getSupersetVariable() == superSet
Method Detail |
---|
public SetDenotator getSubsetVariable()
public SetDenotator getSupersetVariable()
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.| result == false
public Set<Predicate> getPredicates()
| if ( getSubsetVariable() instanceof Predicate ) | then
result.contains(getSubsetVariable())
| if ( getSupersetVariable() instanceof Predicate ) | then
result.contains(getSupersetVariable())
public boolean equals(Object other)
equals
in class FormulaImpl
| let otherSubset = (Subset)
other in
| if ( otherSubset.getSubsetVariable() == getSubsetVariable() ) | then result == false | else if (
otherSubset.getSupersetVariable() == getSupersetVariable() )
| then result == false | else result == true
public int hashCode()
hashCode
in class FormulaImpl
| result ==
getSubsetVariable().hashCode() + "⊂".hashCode() + getSupersetVariable().hashCode()
public String toString()
toString
in class FormulaImpl
| result == getSubsetVariable().toString() + "⊂" + getSupersetVariable().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 |