Package owl.ltl

## Class Formula.LogicalOperator

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

- All Implemented Interfaces:
    `Comparable<Formula>`
  Direct Known Subclasses:
    `Biconditional`, `BooleanConstant`, `PropositionalFormula`
  Enclosing class:
    Formula

      public abstract static class Formula.LogicalOperator
      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` | `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.
    `Formula` | `unfold()` |
    `Formula` | `unfoldTemporalStep​(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, substitute`

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

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

- - ### Method Detail

    - #### 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`

    - #### unfold

          public final Formula unfold()

      Specified by:
        `unfold` in class `Formula`

    - #### unfoldTemporalStep

          public final Formula unfoldTemporalStep​(BitSet valuation)

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