Package owl.ltl
Class GOperator
-
- All Implemented Interfaces:
Comparable<Formula>
- Direct Known Subclasses:
FrequencyG
public class GOperator extends UnaryModalOperator
Globally.
-
-
Nested Class Summary
-
Nested classes/interfaces inherited from class owl.ltl.Formula
Formula.LogicalOperator, Formula.ModalOperator, Formula.TemporalOperator
-
-
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>
Aaccept(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 G(operand).String
operatorSymbol()
Formula
unfold()
Formula
unfoldTemporalStep(BitSet valuation)
Short-cut operation to avoid intermediate construction of formula ASTs.-
Methods inherited from class owl.ltl.UnaryModalOperator
children, compareToImpl, equalsImpl, toString
-
Methods inherited from class owl.ltl.Formula.TemporalOperator
substitute, temporalStep, temporalStep, temporalStep, temporalStepUnfold
-
Methods inherited from class owl.ltl.Formula
allMatch, anyMatch, atomicPropositions, compareTo, equals, hashCode, height, isSuspendable, subformulas, subformulas, subformulas
-
-
-
-
Constructor Detail
-
GOperator
public GOperator(Formula operand)
-
-
Method Detail
-
of
public static Formula of(Formula operand)
Construct a LTL-equivalent formula for G(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 G(operand) use the constructor.- Parameters:
operand
- The operand of the G-operator- Returns:
- a formula equivalent to G(operand)
-
accept
public int accept(IntVisitor v)
-
accept
public <A,B> A accept(BinaryVisitor<B,A> v, B parameter)
-
operatorSymbol
public String operatorSymbol()
- Specified by:
operatorSymbol
in classUnaryModalOperator
-
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.
-
unfoldTemporalStep
public Formula unfoldTemporalStep(BitSet valuation)
Description copied from class:Formula
Short-cut operation to avoid intermediate construction of formula ASTs.- Specified by:
unfoldTemporalStep
in classFormula
-
-