Package owl.ltl
Interface Formula
-
- All Known Implementing Classes:
AbstractFormula
,Biconditional
,BinaryModalOperator
,BooleanConstant
,Conjunction
,Disjunction
,FOperator
,FrequencyG
,GOperator
,Literal
,MOperator
,PropositionalFormula
,ROperator
,UnaryModalOperator
,UOperator
,WOperator
,XOperator
public interface Formula
-
-
Method Summary
All Methods Instance Methods Abstract Methods Modifier and Type Method Description <R,P> R
accept(BinaryVisitor<P,R> visitor, P parameter)
int
accept(IntVisitor visitor)
<R> R
accept(Visitor<R> visitor)
boolean
allMatch(Predicate<Formula> predicate)
boolean
anyMatch(Predicate<Formula> predicate)
boolean
isPureEventual()
boolean
isPureUniversal()
boolean
isSuspendable()
Formula
nnf()
Formula
not()
Syntactically negate this formula.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.
-
-
-
Method Detail
-
accept
int accept(IntVisitor visitor)
-
accept
<R> R accept(Visitor<R> visitor)
-
accept
<R,P> R accept(BinaryVisitor<P,R> visitor, P parameter)
-
isPureEventual
boolean isPureEventual()
-
isPureUniversal
boolean isPureUniversal()
-
isSuspendable
boolean isSuspendable()
-
nnf
Formula nnf()
-
not
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.
-
temporalStep
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
Formula temporalStepUnfold(BitSet valuation)
Short-cut operation to avoid intermediate construction of formula ASTs.
-
unfold
Formula unfold()
-
-