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
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. |
Finally
public Finally(IFormula subFormula)
- Constructs a new formula with the given subformula.
- Parameters:
subFormula
- the subformula
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.