rwth.i2.ltlrv.formula.impl
Class Finally

java.lang.Object
  rwth.i2.ltlrv.formula.base.AbstractFormula
      rwth.i2.ltlrv.formula.base.UnaryFormula
          rwth.i2.ltlrv.formula.impl.Finally

All Implemented Interfaces:

IFinally, IFormula, IUnaryTerm

public class Finally
extends UnaryFormula
implements IFinally

Finally - Implements the Finally formula constructor of LTL.

Author:

Eric Bodden

Field Summary

Fields inherited from class rwth.i2.ltlrv.formula.base.UnaryFormula

subformula

Fields inherited from class rwth.i2.ltlrv.formula.base.AbstractFormula

factory

Constructor Summary

Finally(IFormula subFormula)
Constructs a new formula with the given subformula.

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.UnaryFormula

getSubformula, 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.IUnaryTerm

getSubformula

Constructor Detail

Finally

public Finally(IFormula subFormula)

Constructs a new formula with the given subformula.

Parameters:

subFormula - the 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.