rwth.i2.ltlrv.formula.interfaze
Interface IFormula

All Known Subinterfaces:

IAFAState, IAnd, IBinaryAFAState, IBinaryTerm, IEquivalent, IFF, IFinally, IGlobally, IImplies, INext, INot, INullaryAFAState, IOr, IProposition, IRelease, ITT, IUnaryAFAState, IUnaryTerm, IUntil

All Known Implementing Classes:

AbstractAFAState, AbstractFormula, And, BinaryAFAState, BinaryFormula, CommutativeBinaryAFAState, CommutativeBinaryFormula, Equivalent, FF, Finally, Globally, Implies, Next, Not, NullaryAFAState, Or, Proposition, Release, TT, UnaryAFAState, UnaryFormula, Until

public interface IFormula

Author:

Eric Bodden Reflects a formula in the system. Some formulae can also be a state in an alternating finite automaton (AFA).

See Also:

IAFAState

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.

Method Detail

negationNormalForm

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().

Returns:

the formula in negation normal form

See Also:

IUntil, IRelease, IAnd, IOr, IProposition

symbol

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.

Returns:

The symbol for this term constructor.