Class Implies

  extended by rwth.i2.ltlrv.formula.base.AbstractFormula
      extended by rwth.i2.ltlrv.formula.base.BinaryFormula
          extended by rwth.i2.ltlrv.formula.impl.Implies
All Implemented Interfaces:
IBinaryTerm, IFormula, IImplies

public class Implies
extends BinaryFormula
implements IImplies

Implies - Implements the Implies relation as subformula.

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
Implies(IFormula subFormula1, IFormula subFormula2)
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.BinaryFormula
getSubformula1, getSubformula2, toString
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
Methods inherited from interface rwth.i2.ltlrv.formula.interfaze.IBinaryTerm
getSubformula1, getSubformula2

Constructor Detail


public Implies(IFormula subFormula1,
               IFormula subFormula2)
subFormula1 - left subformula
subFormula2 - right subformula
Method Detail


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.


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