Package owl.ltl

Class XOperator

    • Constructor Detail

      • XOperator

        public XOperator​(Formula operand)
    • Method Detail

      • of

        public static Formula of​(Formula operand)
        Construct a LTL-equivalent formula for X(operand). The method examines the operand and might choose to construct a simpler formula. However, the size of the syntax tree is not increased. In order to syntactically construct X(operand) use the constructor.
        Parameters:
        operand - The operand of the X-operator
        Returns:
        a formula equivalent to X(operand)
      • of

        public static Formula of​(Formula operand,
                                 int n)
        Construct a LTL-equivalent formula for X^n(operand). The method examines the operand and might choose to construct a simpler formula. However, the size of the syntax tree is not increased. In order to syntactically construct X^n(operand) use the constructor.
        Parameters:
        operand - The operand of the X-operator
        n - The number of X-operators to add
        Returns:
        a formula equivalent to X^n(operand)
      • accept

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

        public <A,B> A accept​(BinaryVisitor<B,A> v,
                              B 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.
      • unfoldTemporalStep

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