BinaryModalOperator
, BooleanConstant
, Conjunction
, Disjunction
, FOperator
, FrequencyG
, GOperator
, Literal
, MOperator
, PropositionalFormula
, ROperator
, UnaryModalOperator
, UOperator
, WOperator
, XOperator
public interface Formula
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(java.util.function.Predicate<Formula> predicate) |
|
boolean |
anyMatch(java.util.function.Predicate<Formula> predicate) |
|
boolean |
isPureEventual() |
|
boolean |
isPureUniversal() |
|
boolean |
isSuspendable() |
|
Formula |
not() |
Syntactically negate this formula.
|
Formula |
temporalStep(java.util.BitSet valuation) |
Do a single temporal step.
|
Formula |
temporalStepUnfold(java.util.BitSet valuation) |
Short-cut operation to avoid intermediate construction of formula ASTs.
|
Formula |
unfold() |
|
Formula |
unfoldTemporalStep(java.util.BitSet valuation) |
Short-cut operation to avoid intermediate construction of formula ASTs.
|
int accept(IntVisitor visitor)
<R> R accept(Visitor<R> visitor)
<R,P> R accept(BinaryVisitor<P,R> visitor, P parameter)
boolean allMatch(java.util.function.Predicate<Formula> predicate)
boolean anyMatch(java.util.function.Predicate<Formula> predicate)
boolean isPureEventual()
boolean isPureUniversal()
boolean isSuspendable()
Formula not()
Formula temporalStep(java.util.BitSet valuation)
Formula temporalStepUnfold(java.util.BitSet valuation)
Formula unfold()
Formula unfoldTemporalStep(java.util.BitSet valuation)