de.uni_tuebingen.sfb.lichtenstein.formulas
Class Subset

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

All Implemented Interfaces:

Formula, Visitable, Serializable

public class Subset
extends AtomicFormula

A class for representing the atomic formula which says a variable is a subset of another variable

Author:

Hendrik Maryns

See Also:

Serialized Form

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

Subset

public Subset(SetDenotator subSet,
              SetDenotator superSet)

Initialize a new subset formula, involving the variable which is a subset and the variable which is a superset.

Parameters:

subSet - The variable which is a subset.

superSet - The variable which is a superset.

Precondition:

Both variables must be effective.

| subSet != null && superSet != null

Postcondition:

The subset variable is set to the given subset variable.

| new.getSubsetVariable() == subSet

Postcondition:

The superset variable is set to the given superset variable.

| new.getSupersetVariable() == superSet

Method Detail

getSubsetVariable

public SetDenotator getSubsetVariable()

Returns the subset variable.

getSupersetVariable

public SetDenotator getSupersetVariable()

Returns the superset variable.

getNbVariables

public int getNbVariables()

Returns the number of variables in this formula.

Returns:

Always 2.

| result == 2

getFirstIndexOf

public int getFirstIndexOf(Variable var)

Get the first index at which the given variable occurs.

Parameters:

var - The variable of which the index is wanted.

getVariableAt

public Variable getVariableAt(int index)
                       throws IndexOutOfBoundsException

Get the indexth variable (free or bound).

Parameters:

index - The index of the wanted variable

containsVariable

public boolean containsVariable(Variable var)

Returns whether this formula contains the given variable.

Parameters:

var - The variable to check.

Returns:

A subset formula does not contain any first order variables.

| result == false

getPredicates

public Set<Predicate> getPredicates()

Return all predicates in this formula.

Returns:

Both variables can be a predicate.

| if ( getSubsetVariable() instanceof Predicate ) | then
         result.contains(getSubsetVariable())
| if ( getSupersetVariable() instanceof Predicate ) | then
         result.contains(getSupersetVariable())

equals

public boolean equals(Object other)

Indicates whether some other object is "equal to" this one.

Overrides:

equals in class FormulaImpl

Returns:

Two subset atomic formulas are equal if they compare the same variables.

| let otherSubset = (Subset)
         other in
| if ( otherSubset.getSubsetVariable() == getSubsetVariable() ) | then result == false | else if (
         otherSubset.getSupersetVariable() == getSupersetVariable() )
| then result == false | else result == true

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 ==
         getSubsetVariable().hashCode() + "⊂".hashCode() + getSupersetVariable().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 unicode symbol SUBSET OF: ⊂ in between them.

| result == getSubsetVariable().toString() + "⊂" + getSupersetVariable().toString()

accept

public void accept(FormulaVisitor visitor)
            throws de.uni_tuebingen.sfb.lichtenstein.exceptions.VisitorException

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

Specified by:

accept in interface Visitable

Overrides:

accept in class FormulaImpl

Parameters:

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

Throws:

VisitorException

A visitor can throw an exception.