Package owl.ltl

## Interface Formula

- All Known Implementing Classes:
    `AbstractFormula`, `Biconditional`, `BinaryModalOperator`, `BooleanConstant`, `Conjunction`, `Disjunction`, `FOperator`, `FrequencyG`, `GOperator`, `Literal`, `MOperator`, `PropositionalFormula`, `ROperator`, `UnaryModalOperator`, `UOperator`, `WOperator`, `XOperator`

      public interface Formula

- - ### Method Summary

    All Methods Instance Methods Abstract Methods
    Modifier and Type | Method | Description
    --- | --- | ---
    `<R,P> R` | `accept​(BinaryVisitor<P,R> visitor, P parameter)` |
    `int` | `accept​(IntVisitor visitor)` |
    `<R> R` | `accept​(Visitor<R> visitor)` |
    `boolean` | `allMatch​(Predicate<Formula> predicate)` |
    `boolean` | `anyMatch​(Predicate<Formula> predicate)` |
    `boolean` | `isPureEventual()` |
    `boolean` | `isPureUniversal()` |
    `boolean` | `isSuspendable()` |
    `Formula` | `nnf()` |
    `Formula` | `not()` | Syntactically negate this formula.
    `Formula` | `temporalStep​(BitSet valuation)` | Do a single temporal step.
    `Formula` | `temporalStepUnfold​(BitSet valuation)` | Short-cut operation to avoid intermediate construction of formula ASTs.
    `Formula` | `unfold()` |
    `Formula` | `unfoldTemporalStep​(BitSet valuation)` | Short-cut operation to avoid intermediate construction of formula ASTs.

- - ### Method Detail

    - #### accept

          int accept​(IntVisitor visitor)

    - #### accept

          <R> R accept​(Visitor<R> visitor)

    - #### accept

          <R,P> R accept​(BinaryVisitor<P,R> visitor,
                         P parameter)

    - #### allMatch

          boolean allMatch​(Predicate<Formula> predicate)

    - #### anyMatch

          boolean anyMatch​(Predicate<Formula> predicate)

    - #### isPureEventual

          boolean isPureEventual()

    - #### isPureUniversal

          boolean isPureUniversal()

    - #### isSuspendable

          boolean isSuspendable()

    - #### nnf

          Formula nnf()

    - #### not

          Formula not()

      Syntactically negate this formula.

      If this formula is in NNF, the returned negation will also be in NNF.

      Returns:
        the negation of this formula.

    - #### temporalStep

          Formula temporalStep​(BitSet valuation)

      Do a single temporal step. This means that one layer of X-operators is removed and literals are replaced by their valuations.

    - #### temporalStepUnfold

          Formula temporalStepUnfold​(BitSet valuation)

      Short-cut operation to avoid intermediate construction of formula ASTs.

    - #### unfold

          Formula unfold()

    - #### unfoldTemporalStep

          Formula unfoldTemporalStep​(BitSet valuation)

      Short-cut operation to avoid intermediate construction of formula ASTs.