Package owl.ltl

Class Formula

    • Method Detail

      • accept

        public abstract int accept​(IntVisitor visitor)
      • accept

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

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

        public final BitSet atomicPropositions​(boolean includeNested)
      • compareValue

        protected int compareValue​(Formula o)
      • equalsValue

        protected boolean equalsValue​(Formula o)
      • hashCode

        public final int hashCode()
        hashCode in class Object
      • height

        public final int height()
      • isPureEventual

        public abstract boolean isPureEventual()
      • isPureUniversal

        public abstract boolean isPureUniversal()
      • isSuspendable

        public final boolean isSuspendable()
      • nnf

        public abstract Formula nnf()
      • not

        public abstract Formula not()
        Syntactically negate this formula.

        If this formula is in NNF, the returned negation will also be in NNF.

        the negation of this formula.
      • subformulas

        public final <E extends FormulaSet<E> subformulas​(Class<? extends E> clazz)
      • temporalStep

        public abstract 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.
      • unfold

        public abstract Formula unfold()