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

Field Summary

Fields inherited from class owl.ltl.Formula

operands

Method Summary

Modifier and Type	Method	Description
protected int	compareValue(Formula o)
protected boolean	equalsValue(Formula o)
abstract String	operatorSymbol()
Formula	substitute(Function<? super Formula.TemporalOperator,? extends Formula> substitution)
Formula	temporalStep(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

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, toString, wait, wait, wait

Method Detail

operatorSymbol

public abstract String operatorSymbol()

substitute

public final Formula substitute(Function<? super Formula.TemporalOperator,? extends Formula> substitution)

Specified by:

substitute in class Formula

temporalStep

public final Formula temporalStep(BitSet valuation)

Description copied from class: Formula

Do a single temporal step. This means that one layer of X-operators is removed and literals are replaced by their valuations.

Specified by:

temporalStep in class Formula

compareValue

protected final int compareValue(Formula o)

Overrides:

compareValue in class Formula

equalsValue

protected final boolean equalsValue(Formula o)

Overrides:

equalsValue in class Formula