Package owl.ltl

## Class Formula.TemporalOperator

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

- All Implemented Interfaces:
    `Comparable<Formula>`
  Direct Known Subclasses:
    `Formula.ModalOperator`, `Literal`
  Enclosing class:
    Formula

      public abstract static class Formula.TemporalOperator
      extends Formula

- - ### Nested Class Summary

    - ### Nested classes/interfaces inherited from class owl.ltl.Formula

      `Formula.LogicalOperator, Formula.ModalOperator, Formula.TemporalOperator`

  - ### Method Summary

    All Methods Instance Methods Concrete Methods
    Modifier and Type | Method | Description
    --- | --- | ---
    `Formula` | `substitute​(Function<? super Formula.TemporalOperator,​? extends Formula> substitution)` |
    `Formula` | `temporalStep()` |
    `Formula` | `temporalStep​(int atom, boolean valuation)` |
    `Formula` | `temporalStep​(BitSet valuation)` | Do a single temporal step.
    `Formula` | `temporalStepUnfold​(BitSet valuation)` | Short-cut operation to avoid intermediate construction of formula ASTs.

    - ### Methods inherited from class owl.ltl.Formula

      `accept, accept, accept, allMatch, anyMatch, atomicPropositions, children, compareTo, compareToImpl, equals, equalsImpl, hashCode, height, isPureEventual, isPureUniversal, isSuspendable, nnf, not, subformulas, subformulas, subformulas, unfold, unfoldTemporalStep`

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

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

- - ### Method Detail

    - #### substitute

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

      Specified by:
        `substitute` in class `Formula`

    - #### temporalStep

          public final Formula temporalStep()

      Specified by:
        `temporalStep` in class `Formula`

    - #### temporalStep

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

      Specified by:
        `temporalStep` in class `Formula`

    - #### temporalStep

          public final Formula temporalStep​(BitSet valuation)

      Description copied from class: `Formula`
      Do a single temporal step. This means that one layer of X-operators is removed and literals are replaced by their valuations.
      Specified by:
        `temporalStep` in class `Formula`

    - #### temporalStepUnfold

          public final Formula temporalStepUnfold​(BitSet valuation)

      Description copied from class: `Formula`
      Short-cut operation to avoid intermediate construction of formula ASTs.
      Specified by:
        `temporalStepUnfold` in class `Formula`