Package owl.ltl

## Class Formula

- java.lang.Object
- - owl.ltl.Formula

- All Implemented Interfaces:
    `Comparable<Formula>`
  Direct Known Subclasses:
    `Formula.LogicalOperator`, `Formula.TemporalOperator`

      public abstract class Formula
      extends Object
      implements Comparable<Formula>

- - ### Nested Class Summary

    Nested Classes
    Modifier and Type | Class | Description
    --- | --- | ---
    `static class` | `Formula.LogicalOperator` |
    `static class` | `Formula.ModalOperator` |
    `static class` | `Formula.TemporalOperator` |

  - ### Method Summary

    All Methods Instance Methods Abstract Methods Concrete Methods
    Modifier and Type | Method | Description
    --- | --- | ---
    `abstract <R,​P> R` | `accept​(BinaryVisitor<P,​R> visitor, P parameter)` |
    `abstract int` | `accept​(IntVisitor visitor)` |
    `abstract <R> R` | `accept​(Visitor<R> visitor)` |
    `boolean` | `allMatch​(Predicate<Formula> predicate)` |
    `boolean` | `anyMatch​(Predicate<Formula> predicate)` |
    `BitSet` | `atomicPropositions​(boolean includeNested)` |
    `abstract Set<Formula>` | `children()` |
    `int` | `compareTo​(Formula o)` |
    `protected abstract int` | `compareToImpl​(Formula o)` |
    `boolean` | `equals​(Object o)` |
    `protected abstract boolean` | `equalsImpl​(Formula o)` |
    `int` | `hashCode()` |
    `int` | `height()` |
    `abstract boolean` | `isPureEventual()` |
    `abstract boolean` | `isPureUniversal()` |
    `boolean` | `isSuspendable()` |
    `abstract Formula` | `nnf()` |
    `abstract Formula` | `not()` | Syntactically negate this formula.
    `<E extends Formula.TemporalOperator> Set<E>` | `subformulas​(Class<E> clazz)` |
    `Set<Formula.TemporalOperator>` | `subformulas​(Predicate<? super Formula.TemporalOperator> predicate)` |
    `<E extends Formula.TemporalOperator> Set<E>` | `subformulas​(Predicate<? super Formula.TemporalOperator> predicate, Function<? super Formula.TemporalOperator,​E> cast)` |
    `abstract Formula` | `substitute​(Function<? super Formula.TemporalOperator,​? extends Formula> substitution)` |
    `abstract Formula` | `temporalStep()` |
    `abstract Formula` | `temporalStep​(int atom, boolean valuation)` |
    `abstract Formula` | `temporalStep​(BitSet valuation)` | Do a single temporal step.
    `abstract Formula` | `temporalStepUnfold​(BitSet valuation)` | Short-cut operation to avoid intermediate construction of formula ASTs.
    `abstract Formula` | `unfold()` |
    `abstract Formula` | `unfoldTemporalStep​(BitSet valuation)` | Short-cut operation to avoid intermediate construction of formula ASTs.

    - ### Methods inherited from class java.lang.Object

      `clone, finalize, getClass, notify, notifyAll, toString, wait, wait, wait`

- - ### Method Detail

    - #### accept

          public abstract int accept​(IntVisitor visitor)

    - #### accept

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

    - #### accept

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

    - #### atomicPropositions

          public final BitSet atomicPropositions​(boolean includeNested)

    - #### allMatch

          public final boolean allMatch​(Predicate<Formula> predicate)

    - #### anyMatch

          public final boolean anyMatch​(Predicate<Formula> predicate)

    - #### children

          public abstract Set<Formula> children()

    - #### compareTo

          public final int compareTo​(Formula o)

      Specified by:
        `compareTo` in interface `Comparable<Formula>`

    - #### equals

          public final boolean equals​(Object o)

      Overrides:
        `equals` in class `Object`

    - #### hashCode

          public final int hashCode()

      Overrides:
        `hashCode` in class `Object`

    - #### height

          public final int height()

    - #### isPureEventual

          public abstract boolean isPureEventual()

    - #### isPureUniversal

          public abstract boolean isPureUniversal()

    - #### isSuspendable

          public final boolean isSuspendable()

    - #### nnf

          public abstract Formula nnf()

    - #### not

          public abstract 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.

    - #### subformulas

          public final <E extends Formula.TemporalOperator> Set<E> subformulas​(Class<E> clazz)

    - #### subformulas

          public final Set<Formula.TemporalOperator> subformulas​(Predicate<? super Formula.TemporalOperator> predicate)

    - #### subformulas

          public final <E extends Formula.TemporalOperator> Set<E> subformulas​(Predicate<? super Formula.TemporalOperator> predicate,
                                                                               Function<? super Formula.TemporalOperator,​E> cast)

    - #### substitute

          public abstract Formula substitute​(Function<? super Formula.TemporalOperator,​? extends Formula> substitution)

    - #### temporalStep

          public abstract Formula temporalStep()

    - #### temporalStep

          public abstract Formula temporalStep​(int atom,
                                               boolean valuation)

    - #### temporalStep

          public abstract 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

          public abstract Formula temporalStepUnfold​(BitSet valuation)

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

    - #### unfold

          public abstract Formula unfold()

    - #### unfoldTemporalStep

          public abstract Formula unfoldTemporalStep​(BitSet valuation)

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

    - #### compareToImpl

          protected abstract int compareToImpl​(Formula o)

    - #### equalsImpl

          protected abstract boolean equalsImpl​(Formula o)