|
|||||||||
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.Inclusion
public class Inclusion
A class representing inclusion of a first order variable in a set denotator.
Constructor Summary | |
---|---|
Inclusion(FirstOrderVariable included,
SetDenotator containing)
Initialize a new inclusion, 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. |
SetDenotator |
getContainingVariable()
Returns the containing variable. |
int |
getFirstIndexOf(Variable var)
Get the first index at which the given variable occurs. |
FirstOrderVariable |
getIncludedVariable()
Returns the included variable. |
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 Inclusion(FirstOrderVariable included, SetDenotator containing)
included
- The variable which is included in the other variable.containing
- The variable which includes the other variable.| included != null && containing != null
| new.getIncludedVariable() == included
| new.getContainingVariable() ==
containing
Method Detail |
---|
public FirstOrderVariable getIncludedVariable()
| result == getVariableAt(0)
public SetDenotator getContainingVariable()
| result == getVariableAt(1)
public int getNbVariables()
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 ==
getIncludedVariable().equals(var)
|| getContainingVariable().equals(var)
public Set<Predicate> getPredicates()
| if ( getIncludingVariable() instanceof Predicate ) |
then result.contains(getContainingVariable())
| else result.isEmpty()
public boolean equals(Object other)
equals
in class FormulaImpl
| let otherIn = (Inclusion)
other in
| if ( otherIn.getIncludedVariable() == getIncludedVariable() ) | then result == false | else if (
otherIn.getContainingVariable() == getContainingVariable() )
| then result == false | else result == true
public int hashCode()
hashCode
in class FormulaImpl
| result ==
getIncludedVariable().hashCode() + "∈".hashCode() + getContainingVariable().hashCode()
public String toString()
toString
in class FormulaImpl
| result == getIncludedVariable().toString() + "∈" +
getContainingVariable().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 |