de.uni_tuebingen.sfb.lichtenstein.formulas
Class UnaryJunctor

java.lang.Object
  de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
      de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula
          de.uni_tuebingen.sfb.lichtenstein.formulas.UnaryJunctor

All Implemented Interfaces:

Formula, Visitable, Serializable

Direct Known Subclasses:

Negation

public abstract class UnaryJunctor
extends ComposedFormula

A class representing a unary junctor, having one argument.

Author:

Hendrik Maryns

See Also:

Serialized Form

Constructor Summary

protected

UnaryJunctor(Formula argument) Initialize a new unary junctor, taking a formula as argument.

Method Summary

protected Set<Predicate>	computePredicates() Return all predicates in this formula.
protected Set<Variable>	computeVariables() Compute the set of variables in this formula.
boolean	containsVariable(Variable var) Returns whether this formula contains the given variable.
boolean	equals(Object other) An object is equal to a unary junctor if it has the same class (i.e., not only it is a unary junctor, but it really has the same leaf-level class), and the arguments are equal.
Formula	getArgument() Returns the argument.
int	getNbSubformulas() Returns the number of subformulas.
Formula	getSubformulaAt(int index) Returns the indexth subformula of this formula.
int	hashCode() Returns a hash code value for the object.
boolean	isFree(Variable variable) Check whether the given variable is free in this formula.
String	toString() Returns a string representation of the object.

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

getAllSubformulas, getSymbol

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

and, exists, exists, forAll, forAll, getFreeVariables, getPredicates, getVariables, iff, implies, isClosed, not, or

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Formula

getNormalForm

Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Visitable

accept

Constructor Detail

UnaryJunctor

protected UnaryJunctor(Formula argument)

Initialize a new unary junctor, taking a formula as argument.

Parameters:

argument - The argument.

Postcondition:

The argument is set to the given argument. | new.getArgument() == argument

Method Detail

getArgument

public Formula getArgument()

Returns the argument.

Returns:

This is the only subformula. | result == getSubformulaAt(0)

computeVariables

protected Set<Variable> computeVariables()

Compute the set of variables in this formula.

Specified by:

computeVariables in class FormulaImpl

containsVariable

public boolean containsVariable(Variable var)

Returns whether this formula contains the given variable.

Parameters:

var - The variable to check.

Returns:

All variables are contained in the argument. | result == getArgument().containsVariable(var)

isFree

public boolean isFree(Variable variable)

Check whether the given variable is free in this formula.

Parameters:

variable - The variable to check.

Returns:

The argument decides. | result == getArgument().isFreeVariable(variable)

computePredicates

protected Set<Predicate> computePredicates()

Return all predicates in this formula.

Specified by:

computePredicates in class FormulaImpl

getNbSubformulas

public final int getNbSubformulas()

Returns the number of subformulas.

Specified by:

getNbSubformulas in class ComposedFormula

Returns:

A unary junctor always contains only one subformula. | result == 1

getSubformulaAt

public Formula getSubformulaAt(int index)
                        throws IndexOutOfBoundsException

Returns the indexth subformula of this formula.

Specified by:

getSubformulaAt in class ComposedFormula

Parameters:

index - The index of the wanted subformula. Indices start from 0.

Returns:

A unary junctor has only one subformula; if the index is different from 0, an error is thrown. Thus, this formula is equivalent to getArgument().

Throws:

IndexOutOfBoundsException - [CAN] The index is bigger than or equal to the number of subformulas of this formula, or less than zero | index < 0 || index >= getNbSubformulas()

equals

public boolean equals(Object other)

An object is equal to a unary junctor if it has the same class (i.e., not only it is a unary junctor, but it really has the same leaf-level class), and the arguments are equal.

Overrides:

equals in class FormulaImpl

Returns:

If the argument of the other object, viewed as a unary junctor is not equal to the argument of this binary junctor, then false. | let otherJunctor = (UnaryJunctor) other in | if ( ! getArgument().equals(otherJunctor.getArgument()) ) | then result == false

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 argument and of the characteristic symbol. | result == getSymbol().hashCode() + getArgument().hashCode()

toString

public String toString()

Returns a string representation of the object.

Specified by:

toString in class FormulaImpl

Returns:

The string representation of a unary junctor is the string representation of its arguments prepended with an appropriate sign. | result == getSymbol() + getArgument().toString()