Package owl.ltl
Class Biconditional
- java.lang.Object
-
- owl.ltl.AbstractFormula
-
- owl.ltl.Biconditional
-
- All Implemented Interfaces:
Formula
public class Biconditional extends AbstractFormula
Biconditional.
-
-
Constructor Summary
Constructors Constructor Description Biconditional(Formula leftOperand, Formula rightOperand)
-
Method Summary
All Methods Static Methods Instance Methods Concrete 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)
protected boolean
equals2(AbstractFormula o)
protected int
hashCodeOnce()
boolean
isPureEventual()
boolean
isPureUniversal()
boolean
isSuspendable()
Formula
nnf()
Formula
not()
Syntactically negate this formula.static Formula
of(Formula leftOperand, Formula rightOperand)
Construct a LTL-equivalent formula for (leftOperand)<->(rightOperand).Formula
temporalStep(BitSet valuation)
Do a single temporal step.Formula
temporalStepUnfold(BitSet valuation)
Short-cut operation to avoid intermediate construction of formula ASTs.String
toString()
Formula
unfold()
Formula
unfoldTemporalStep(BitSet valuation)
Short-cut operation to avoid intermediate construction of formula ASTs.-
Methods inherited from class owl.ltl.AbstractFormula
equals, hashCode
-
-
-
-
Method Detail
-
of
public static Formula of(Formula leftOperand, Formula rightOperand)
Construct a LTL-equivalent formula for (leftOperand)<->(rightOperand). The method examines the operands and might choose to construct a simpler formula. However, the size of the syntax tree is not increased. In order to syntactically construct (leftOperand)<->(rightOperand) use the constructor.- Parameters:
leftOperand
- The left operand of the biconditionalrightOperand
- The right operand of the biconditional- Returns:
- a formula equivalent to (leftOperand)<->(rightOperand)
-
accept
public int accept(IntVisitor visitor)
-
accept
public <R> R accept(Visitor<R> visitor)
-
accept
public <R,P> R accept(BinaryVisitor<P,R> visitor, P parameter)
-
isPureEventual
public boolean isPureEventual()
-
isPureUniversal
public boolean isPureUniversal()
-
isSuspendable
public boolean isSuspendable()
-
not
public Formula not()
Description copied from interface:Formula
Syntactically negate this formula.If this formula is in NNF, the returned negation will also be in NNF.
- Returns:
- the negation of this formula.
-
nnf
public Formula nnf()
-
temporalStep
public Formula temporalStep(BitSet valuation)
Description copied from interface:Formula
Do a single temporal step. This means that one layer of X-operators is removed and literals are replaced by their valuations.
-
temporalStepUnfold
public Formula temporalStepUnfold(BitSet valuation)
Description copied from interface:Formula
Short-cut operation to avoid intermediate construction of formula ASTs.
-
unfold
public Formula unfold()
-
unfoldTemporalStep
public Formula unfoldTemporalStep(BitSet valuation)
Description copied from interface:Formula
Short-cut operation to avoid intermediate construction of formula ASTs.
-
equals2
protected boolean equals2(AbstractFormula o)
- Specified by:
equals2
in classAbstractFormula
-
hashCodeOnce
protected int hashCodeOnce()
- Specified by:
hashCodeOnce
in classAbstractFormula
-
-