Package owl.ltl
Class XOperator
- java.lang.Object
-
- owl.ltl.AbstractFormula
-
- owl.ltl.UnaryModalOperator
-
- owl.ltl.XOperator
-
- All Implemented Interfaces:
Formula
public final class XOperator extends UnaryModalOperator
Next.
-
-
Field Summary
-
Fields inherited from class owl.ltl.UnaryModalOperator
operand
-
-
Method Summary
All Methods Static Methods Instance Methods Concrete Methods Modifier and Type Method Description <A,B> A
accept(BinaryVisitor<B,A> v, B parameter)
int
accept(IntVisitor v)
<R> R
accept(Visitor<R> v)
String
getOperator()
boolean
isPureEventual()
boolean
isPureUniversal()
boolean
isSuspendable()
Formula
nnf()
Formula
not()
Syntactically negate this formula.static Formula
of(Formula operand)
Construct a LTL-equivalent formula for X(operand).static Formula
of(Formula operand, int n)
Construct a LTL-equivalent formula for X^n(operand).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.-
Methods inherited from class owl.ltl.AbstractFormula
equals, hashCode
-
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
-
Methods inherited from class owl.ltl.UnaryModalOperator
allMatch, anyMatch, equals2, getOperand, hashCodeOnce, toString
-
-
-
-
Constructor Detail
-
XOperator
public XOperator(Formula operand)
-
-
Method Detail
-
of
public static Formula of(Formula operand)
Construct a LTL-equivalent formula for X(operand). The method examines the operand and might choose to construct a simpler formula. However, the size of the syntax tree is not increased. In order to syntactically construct X(operand) use the constructor.- Parameters:
operand
- The operand of the X-operator- Returns:
- a formula equivalent to X(operand)
-
of
public static Formula of(Formula operand, int n)
Construct a LTL-equivalent formula for X^n(operand). The method examines the operand and might choose to construct a simpler formula. However, the size of the syntax tree is not increased. In order to syntactically construct X^n(operand) use the constructor.- Parameters:
operand
- The operand of the X-operatorn
- The number of X-operators to add- Returns:
- a formula equivalent to X^n(operand)
-
accept
public int accept(IntVisitor v)
-
accept
public <R> R accept(Visitor<R> v)
-
accept
public <A,B> A accept(BinaryVisitor<B,A> v, B parameter)
-
getOperator
public String getOperator()
- Specified by:
getOperator
in classUnaryModalOperator
-
isPureEventual
public boolean isPureEventual()
-
isPureUniversal
public boolean isPureUniversal()
-
isSuspendable
public boolean isSuspendable()
-
nnf
public Formula nnf()
-
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.
-
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.- Specified by:
temporalStep
in interfaceFormula
- Overrides:
temporalStep
in classUnaryModalOperator
-
temporalStepUnfold
public Formula temporalStepUnfold(BitSet valuation)
Description copied from interface:Formula
Short-cut operation to avoid intermediate construction of formula ASTs.- Specified by:
temporalStepUnfold
in interfaceFormula
- Overrides:
temporalStepUnfold
in classUnaryModalOperator
-
unfold
public Formula unfold()
-
-