Package owl.ltl

Class Biconditional

    • Constructor Detail

      • Biconditional

        public Biconditional​(Formula leftOperand,
                             Formula rightOperand)
    • Method Detail

      • of

        public static Formula of​(Formula leftOperand,
                                 Formula rightOperand)
        Construct a LTL-equivalent formula for (leftOperand)<->(rightOperand). The method examines the operands and might choose to construct a simpler formula. However, the size of the syntax tree is not increased. In order to syntactically construct (leftOperand)<->(rightOperand) use the constructor.
        Parameters:
        leftOperand - The left operand of the biconditional
        rightOperand - The right operand of the biconditional
        Returns:
        a formula equivalent to (leftOperand)<->(rightOperand)
      • accept

        public int accept​(IntVisitor visitor)
      • accept

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

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

        public boolean isPureEventual()
      • isPureUniversal

        public boolean isPureUniversal()
      • isSuspendable

        public boolean isSuspendable()
      • not

        public Formula not()
        Description copied from interface: Formula
        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

        public Formula temporalStep​(BitSet valuation)
        Description copied from interface: Formula
        Do a single temporal step. This means that one layer of X-operators is removed and literals are replaced by their valuations.
      • temporalStepUnfold

        public Formula temporalStepUnfold​(BitSet valuation)
        Description copied from interface: Formula
        Short-cut operation to avoid intermediate construction of formula ASTs.
      • unfoldTemporalStep

        public Formula unfoldTemporalStep​(BitSet valuation)
        Description copied from interface: Formula
        Short-cut operation to avoid intermediate construction of formula ASTs.