Package owl.ltl
Class Formula
- java.lang.Object
-
- owl.ltl.Formula
-
- All Implemented Interfaces:
Comparable<Formula>
- Direct Known Subclasses:
Formula.PropositionalOperator,Formula.TemporalOperator
public abstract class Formula extends Object implements Comparable<Formula>
-
-
Nested Class Summary
Nested Classes Modifier and Type Class Description static classFormula.BinaryTemporalOperatorstatic classFormula.NaryPropositionalOperatorstatic classFormula.PropositionalOperatorstatic classFormula.TemporalOperatorstatic classFormula.UnaryTemporalOperator
-
Method Summary
All Methods Instance Methods Abstract Methods Concrete Methods Modifier and Type Method Description abstract <R,P>
Raccept(BinaryVisitor<P,R> visitor, P parameter)abstract intaccept(IntVisitor visitor)abstract <R> Raccept(Visitor<R> visitor)booleanallMatch(Predicate<Formula> predicate)booleananyMatch(Predicate<Formula> predicate)BitSetatomicPropositions(boolean includeNested)intcompareTo(Formula that)protected intcompareValue(Formula o)booleanequals(Object o)protected booleanequalsValue(Formula o)inthashCode()intheight()abstract booleanisPureEventual()abstract booleanisPureUniversal()booleanisSuspendable()abstract Formulannf()abstract Formulanot()Syntactically negate this formula.<E extends Formula>
Set<E>subformulas(Class<? extends E> clazz)Set<Formula>subformulas(Predicate<? super Formula> predicate)<E extends Formula>
Set<E>subformulas(Predicate<? super Formula> predicate, Function<? super Formula,E> cast)abstract Formulasubstitute(Function<? super Formula.TemporalOperator,? extends Formula> substitution)abstract FormulatemporalStep(BitSet valuation)Do a single temporal step.abstract Formulaunfold()
-
-
-
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)
-
compareTo
public final int compareTo(Formula that)
- Specified by:
compareToin interfaceComparable<Formula>
-
compareValue
protected int compareValue(Formula o)
-
equalsValue
protected boolean equalsValue(Formula o)
-
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.
- Returns:
- the negation of this formula.
-
subformulas
public final <E extends Formula> Set<E> subformulas(Predicate<? super Formula> predicate, Function<? super Formula,E> cast)
-
substitute
public abstract Formula substitute(Function<? super Formula.TemporalOperator,? extends Formula> substitution)
-
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()
-
-