Package owl.ltl
Class Formula
- java.lang.Object
-
- owl.ltl.Formula
-
- All Implemented Interfaces:
Comparable<Formula>
- Direct Known Subclasses:
Formula.LogicalOperator
,Formula.TemporalOperator
public abstract class Formula extends Object implements Comparable<Formula>
-
-
Nested Class Summary
Nested Classes Modifier and Type Class Description static class
Formula.LogicalOperator
static class
Formula.ModalOperator
static class
Formula.TemporalOperator
-
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 int
accept(IntVisitor visitor)
abstract <R> R
accept(Visitor<R> visitor)
boolean
allMatch(Predicate<Formula> predicate)
boolean
anyMatch(Predicate<Formula> predicate)
BitSet
atomicPropositions(boolean includeNested)
abstract Set<Formula>
children()
int
compareTo(Formula o)
protected abstract int
compareToImpl(Formula o)
boolean
equals(Object o)
protected abstract boolean
equalsImpl(Formula o)
int
hashCode()
int
height()
abstract boolean
isPureEventual()
abstract boolean
isPureUniversal()
boolean
isSuspendable()
abstract Formula
nnf()
abstract Formula
not()
Syntactically negate this formula.<E extends Formula.TemporalOperator>
Set<E>subformulas(Class<E> clazz)
Set<Formula.TemporalOperator>
subformulas(Predicate<? super Formula.TemporalOperator> predicate)
<E extends Formula.TemporalOperator>
Set<E>subformulas(Predicate<? super Formula.TemporalOperator> predicate, Function<? super Formula.TemporalOperator,E> cast)
abstract Formula
substitute(Function<? super Formula.TemporalOperator,? extends Formula> substitution)
abstract Formula
temporalStep()
abstract Formula
temporalStep(int atom, boolean valuation)
abstract Formula
temporalStep(BitSet valuation)
Do a single temporal step.abstract Formula
temporalStepUnfold(BitSet valuation)
Short-cut operation to avoid intermediate construction of formula ASTs.abstract Formula
unfold()
abstract Formula
unfoldTemporalStep(BitSet valuation)
Short-cut operation to avoid intermediate construction of formula ASTs.
-
-
-
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 o)
- Specified by:
compareTo
in interfaceComparable<Formula>
-
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.TemporalOperator> Set<E> subformulas(Class<E> clazz)
-
subformulas
public final Set<Formula.TemporalOperator> subformulas(Predicate<? super Formula.TemporalOperator> predicate)
-
subformulas
public final <E extends Formula.TemporalOperator> Set<E> subformulas(Predicate<? super Formula.TemporalOperator> predicate, Function<? super Formula.TemporalOperator,E> cast)
-
substitute
public abstract Formula substitute(Function<? super Formula.TemporalOperator,? extends Formula> substitution)
-
temporalStep
public abstract Formula temporalStep()
-
temporalStep
public abstract Formula temporalStep(int atom, boolean valuation)
-
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.
-
temporalStepUnfold
public abstract Formula temporalStepUnfold(BitSet valuation)
Short-cut operation to avoid intermediate construction of formula ASTs.
-
unfold
public abstract Formula unfold()
-
unfoldTemporalStep
public abstract Formula unfoldTemporalStep(BitSet valuation)
Short-cut operation to avoid intermediate construction of formula ASTs.
-
compareToImpl
protected abstract int compareToImpl(Formula o)
-
equalsImpl
protected abstract boolean equalsImpl(Formula o)
-
-