Package owl.ltl
Class Formula.LogicalOperator
- java.lang.Object
-
- owl.ltl.Formula
-
- owl.ltl.Formula.LogicalOperator
-
- All Implemented Interfaces:
Comparable<Formula>
- Direct Known Subclasses:
Biconditional
,BooleanConstant
,PropositionalFormula
- Enclosing class:
- Formula
public abstract static class Formula.LogicalOperator extends Formula
-
-
Nested Class Summary
-
Nested classes/interfaces inherited from class owl.ltl.Formula
Formula.LogicalOperator, Formula.ModalOperator, Formula.TemporalOperator
-
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description Formula
temporalStep()
Formula
temporalStep(int atom, boolean valuation)
Formula
temporalStep(BitSet valuation)
Do a single temporal step.Formula
temporalStepUnfold(BitSet valuation)
Short-cut operation to avoid intermediate construction of formula ASTs.Formula
unfold()
Formula
unfoldTemporalStep(BitSet valuation)
Short-cut operation to avoid intermediate construction of formula ASTs.-
Methods inherited from class owl.ltl.Formula
accept, accept, accept, allMatch, anyMatch, atomicPropositions, children, compareTo, compareToImpl, equals, equalsImpl, hashCode, height, isPureEventual, isPureUniversal, isSuspendable, nnf, not, subformulas, subformulas, subformulas, substitute
-
-
-
-
Method Detail
-
temporalStep
public final Formula temporalStep()
- Specified by:
temporalStep
in classFormula
-
temporalStep
public final Formula temporalStep(int atom, boolean valuation)
- Specified by:
temporalStep
in classFormula
-
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 classFormula
-
temporalStepUnfold
public final Formula temporalStepUnfold(BitSet valuation)
Description copied from class:Formula
Short-cut operation to avoid intermediate construction of formula ASTs.- Specified by:
temporalStepUnfold
in classFormula
-
unfoldTemporalStep
public final Formula unfoldTemporalStep(BitSet valuation)
Description copied from class:Formula
Short-cut operation to avoid intermediate construction of formula ASTs.- Specified by:
unfoldTemporalStep
in classFormula
-
-