de.uni_tuebingen.sfb.lichtenstein.formulas
Class SetDenotator

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.formulas.Variable
      de.uni_tuebingen.sfb.lichtenstein.formulas.SetDenotator

All Implemented Interfaces:

Serializable

Direct Known Subclasses:

Predicate, SecondOrderVariable

public abstract class SetDenotator
extends Variable

An abstract superclass for second order variables and predicates, both denotating sets of nodes.

Author:

Hendrik Maryns

See Also:

Serialized Form

Method Summary

Inclusion	contains(FirstOrderVariable that) Return the formula that says that variable is an element of this set.
SecondOrderEquality	logicalEquals(SetDenotator that) Return the formula that says this set is equal to that set.
Subset	subset(SetDenotator that) Return the formula that says this set is a subset of that set.
Subset	superset(SetDenotator that) Return the formula that says this set is a superset of that set.

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.Variable

getName, toString

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Method Detail

logicalEquals

public SecondOrderEquality logicalEquals(SetDenotator that)

Return the formula that says this set is equal to that set.

Parameters:

that - The other variable. `That' is a mnemonic for this.logicalEquals(that).

Returns:

The atomic formula claiming this set is equal to that set.

| result.getFirstVariable() == this && |
         result.getSecondVariable() == that

subset

public Subset subset(SetDenotator that)

Return the formula that says this set is a subset of that set.

Parameters:

that - The other variable. `That' is a mnemonic for this.subset(that).

Returns:

The atomic formula claiming this set is a subset of that set.

| result.getSubsetVariable() == this && |
         result.getSupersetVariable() == that

superset

public Subset superset(SetDenotator that)

Return the formula that says this set is a superset of that set.

Parameters:

that - The other variable. `That' is a mnemonic for this.superset(that).

Returns:

The atomic formula claiming this set is a superset of that set.

| result.getSubsetVariable() == that && |
         result.getSupersetVariable() == this

contains

public Inclusion contains(FirstOrderVariable that)

Return the formula that says that variable is an element of this set.

Parameters:

that - The other variable. `That' is a mnemonic for this.contains(that).

Returns:

The atomic formula claiming that set is an element of this set.

| result.getIncludedVariable() == that && |
         result.getContainingVariable() == this