rwth.i2.ltlrv.formula.impl
Class Implies

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

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

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

Implies

public Implies(IFormula subFormula1,
               IFormula subFormula2)

Parameters:

subFormula1 - left subformula

subFormula2 - right subformula

Method Detail

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.

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