Package owl.ltl

Interface Formula

    • Method Detail

      • accept

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

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

        boolean isPureEventual()
      • isPureUniversal

        boolean isPureUniversal()
      • isSuspendable

        boolean isSuspendable()
      • 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.
      • unfoldTemporalStep

        Formula unfoldTemporalStep​(BitSet valuation)
        Short-cut operation to avoid intermediate construction of formula ASTs.