Package owl.ltl

Class XOperator

java.lang.Object

owl.ltl.Formula

owl.ltl.Formula.TemporalOperator

owl.ltl.Formula.UnaryTemporalOperator

owl.ltl.XOperator

All Implemented Interfaces:

Comparable<Formula>

public final class XOperator
extends Formula.UnaryTemporalOperator

Next.

Nested Class Summary

Nested classes/interfaces inherited from class owl.ltl.Formula

Formula.BinaryTemporalOperator, Formula.NaryPropositionalOperator, Formula.PropositionalOperator, Formula.TemporalOperator, Formula.UnaryTemporalOperator

Field Summary

Fields inherited from class owl.ltl.Formula

operands

Constructor Summary

Constructors

Constructor	Description
XOperator(Formula operand)

Method Summary

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)
boolean	isPureEventual()
boolean	isPureUniversal()
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).
String	operatorSymbol()
Formula	unfold()

Methods inherited from class owl.ltl.Formula.UnaryTemporalOperator

operand, toString

Methods inherited from class owl.ltl.Formula.TemporalOperator

compareValue, equalsValue, substitute, temporalStep

Methods inherited from class owl.ltl.Formula

allMatch, anyMatch, atomicPropositions, compareTo, equals, hashCode, height, isSuspendable, subformulas, subformulas, subformulas

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

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-operator

n - The number of X-operators to add

Returns:

a formula equivalent to X^n(operand)

accept

public int accept(IntVisitor v)

Specified by:

accept in class Formula

accept

public <R> R accept(Visitor<R> v)

Specified by:

accept in class Formula

accept

public <A,B> A accept(BinaryVisitor<B,A> v,
                            B parameter)

Specified by:

accept in class Formula

operatorSymbol

public String operatorSymbol()

Specified by:

operatorSymbol in class Formula.TemporalOperator

isPureEventual

public boolean isPureEventual()

Specified by:

isPureEventual in class Formula

isPureUniversal

public boolean isPureUniversal()

Specified by:

isPureUniversal in class Formula

nnf

public Formula nnf()

Specified by:

nnf in class Formula

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.

Specified by:

not in class Formula

Returns:

the negation of this formula.

unfold

public Formula unfold()

Specified by:

unfold in class Formula