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> Raccept(BinaryVisitor<P,R> visitor, P parameter)intaccept(IntVisitor visitor)<R> Raccept(Visitor<R> visitor)booleanallMatch(Predicate<Formula> predicate)booleananyMatch(Predicate<Formula> predicate)booleanisPureEventual()booleanisPureUniversal()booleanisSuspendable()Formulannf()Formulanot()Syntactically negate this formula.FormulatemporalStep(BitSet valuation)Do a single temporal step.FormulatemporalStepUnfold(BitSet valuation)Short-cut operation to avoid intermediate construction of formula ASTs.Formulaunfold()FormulaunfoldTemporalStep(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()
-
-