Package owl.ltl
Class Biconditional
- java.lang.Object
-
- owl.ltl.Formula
-
- owl.ltl.Formula.LogicalOperator
-
- owl.ltl.Biconditional
-
- All Implemented Interfaces:
Comparable<Formula>
public final class Biconditional extends Formula.LogicalOperator
Biconditional.
-
-
Nested Class Summary
-
Nested classes/interfaces inherited from class owl.ltl.Formula
Formula.LogicalOperator, Formula.ModalOperator, Formula.TemporalOperator
-
-
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>
Raccept(BinaryVisitor<P,R> visitor, P parameter)
int
accept(IntVisitor visitor)
<R> R
accept(Visitor<R> visitor)
Set<Formula>
children()
protected int
compareToImpl(Formula o)
protected boolean
equalsImpl(Formula o)
boolean
isPureEventual()
boolean
isPureUniversal()
Formula
nnf()
Formula
not()
Syntactically negate this formula.static Formula
of(Formula leftOperand, Formula rightOperand)
Construct a LTL-equivalent formula for (leftOperand)<->(rightOperand).Formula
substitute(Function<? super Formula.TemporalOperator,? extends Formula> substitution)
String
toString()
-
Methods inherited from class owl.ltl.Formula.LogicalOperator
temporalStep, temporalStep, temporalStep, temporalStepUnfold, unfold, unfoldTemporalStep
-
Methods inherited from class owl.ltl.Formula
allMatch, anyMatch, atomicPropositions, compareTo, equals, hashCode, height, isSuspendable, subformulas, subformulas, subformulas
-
-
-
-
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,P> R accept(BinaryVisitor<P,R> visitor, P parameter)
-
isPureEventual
public boolean isPureEventual()
- Specified by:
isPureEventual
in classFormula
-
isPureUniversal
public boolean isPureUniversal()
- Specified by:
isPureUniversal
in classFormula
-
not
public Formula not()
Description copied from class:Formula
Syntactically negate this formula.If this formula is in NNF, the returned negation will also be in NNF.
-
substitute
public Formula substitute(Function<? super Formula.TemporalOperator,? extends Formula> substitution)
- Specified by:
substitute
in classFormula
-
compareToImpl
protected int compareToImpl(Formula o)
- Specified by:
compareToImpl
in classFormula
-
equalsImpl
protected boolean equalsImpl(Formula o)
- Specified by:
equalsImpl
in classFormula
-
-