- 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
- Eric Bodden
Reflects a formula in the system. Some formulae can also
be a state in an alternating finite automaton (AFA).
- See Also:
Produces a formula in negation normal form, where negations
occur only in front of propositions.
Returns the symbol for this term constructor.
- 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
- the formula in negation normal form
- See Also:
- Returns the symbol for this term constructor.
Propositions should return their label.
All symbols, including those for nullary term constructors
should be distinct.
- The symbol for this term constructor.