Class Equivalent

  extended by rwth.i2.ltlrv.formula.base.AbstractFormula
      extended by rwth.i2.ltlrv.formula.base.BinaryFormula
          extended by rwth.i2.ltlrv.formula.base.CommutativeBinaryFormula
              extended by rwth.i2.ltlrv.formula.impl.Equivalent
All Implemented Interfaces:
IBinaryTerm, IEquivalent, IFormula

public class Equivalent
extends CommutativeBinaryFormula
implements IEquivalent

Equivalent - Implements the equivalent relation as subformula. The relation is commutative and thus extends CommutativeBinaryFormula.

Eric Bodden

Field Summary
Fields inherited from class rwth.i2.ltlrv.formula.base.BinaryFormula
subformula1, subformula2
Fields inherited from class rwth.i2.ltlrv.formula.base.AbstractFormula
Constructor Summary
Equivalent(IFormula subFormula1, IFormula subFormula2)
          Constructs an equivalent relation for the two subformulae.
Method Summary
 IAFAState negationNormalForm()
          Produces a formula in negation normal form, where negations occur only in front of propositions.
 String symbol()
          Returns the symbol for this term constructor.
Methods inherited from class rwth.i2.ltlrv.formula.base.CommutativeBinaryFormula
equals, hashCode
Methods inherited from class rwth.i2.ltlrv.formula.base.BinaryFormula
getSubformula1, getSubformula2, toString
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
Methods inherited from interface rwth.i2.ltlrv.formula.interfaze.IBinaryTerm
getSubformula1, getSubformula2

Constructor Detail


public Equivalent(IFormula subFormula1,
                  IFormula subFormula2)
Constructs an equivalent relation for the two subformulae.

subFormula1 - left subformula
subFormula2 - right subformula
Method Detail


public IAFAState negationNormalForm()
Produces a formula in negation normal form, where negations occur only in front of propositions. This form also holds only IUntil, IRelease, IAnd, IOr, INot, IProposition subformulae. This must return a copy of the original formula. The major work is done in Not.negationNormalForm().

Specified by:
negationNormalForm in interface IFormula
the formula in negation normal form
See Also:
IUntil, IRelease, IAnd, IOr, IProposition


public String symbol()
Returns the symbol for this term constructor. Propositions should return their label. All symbols, including those for nullary term constructors should be distinct.

Specified by:
symbol in interface IFormula
The symbol for this term constructor.