rwth.i2.ltlrv.formula.impl
Class Equivalent

java.lang.Object
  rwth.i2.ltlrv.formula.base.AbstractFormula
      rwth.i2.ltlrv.formula.base.BinaryFormula
          rwth.i2.ltlrv.formula.base.CommutativeBinaryFormula
              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.

Author:

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

factory

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

Equivalent

public Equivalent(IFormula subFormula1,
                  IFormula subFormula2)

Constructs an equivalent relation for the two subformulae.

Parameters:

subFormula1 - left subformula

subFormula2 - right subformula

Method Detail

negationNormalForm

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

Returns:

the formula in negation normal form

See Also:

IUntil, IRelease, IAnd, IOr, IProposition

symbol

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

Returns:

The symbol for this term constructor.