Package owl.ltl
Class Formula.TemporalOperator
- java.lang.Object
-
- owl.ltl.Formula
-
- owl.ltl.Formula.TemporalOperator
-
- All Implemented Interfaces:
Comparable<Formula>
- Direct Known Subclasses:
Formula.BinaryTemporalOperator,Formula.UnaryTemporalOperator
- Enclosing class:
- Formula
public abstract static class Formula.TemporalOperator extends Formula
-
-
Nested Class Summary
-
Nested classes/interfaces inherited from class owl.ltl.Formula
Formula.BinaryTemporalOperator, Formula.NaryPropositionalOperator, Formula.PropositionalOperator, Formula.TemporalOperator, Formula.UnaryTemporalOperator
-
-
Method Summary
All Methods Instance Methods Abstract Methods Concrete Methods Modifier and Type Method Description protected intcompareValue(Formula o)protected booleanequalsValue(Formula o)abstract StringoperatorSymbol()Formulasubstitute(Function<? super Formula.TemporalOperator,? extends Formula> substitution)FormulatemporalStep(BitSet valuation)Do a single temporal step.-
Methods inherited from class owl.ltl.Formula
accept, accept, accept, allMatch, anyMatch, atomicPropositions, compareTo, equals, hashCode, height, isPureEventual, isPureUniversal, isSuspendable, nnf, not, subformulas, subformulas, subformulas, unfold
-
-
-
-
Method Detail
-
operatorSymbol
public abstract String operatorSymbol()
-
substitute
public final Formula substitute(Function<? super Formula.TemporalOperator,? extends Formula> substitution)
- Specified by:
substitutein classFormula
-
temporalStep
public final Formula temporalStep(BitSet valuation)
Description copied from class:FormulaDo a single temporal step. This means that one layer of X-operators is removed and literals are replaced by their valuations.- Specified by:
temporalStepin classFormula
-
compareValue
protected final int compareValue(Formula o)
- Overrides:
compareValuein classFormula
-
equalsValue
protected final boolean equalsValue(Formula o)
- Overrides:
equalsValuein classFormula
-
-