Package org.svvrl.goal.core.logic.ltl

Class LTL

java.lang.Object
org.svvrl.goal.core.logic.Logic
org.svvrl.goal.core.logic.ltl.LTL
All Implemented Interfaces:
java.io.Serializable, java.lang.Cloneable, NegationNormalForm<LTL>
Direct Known Subclasses:
LTLAtomic, LTLBinary, LTLUnary
public abstract class LTL
extends Logic
implements java.lang.Cloneable, java.io.Serializable, NegationNormalForm<LTL>
This class provides common methods for LTL formulae.
Author:
Ming-Hsien Tsai
See Also:
Serialized Form

  • Field Summary

    Fields 
    Modifier and Type Field Description
    static int ARITY_ATOMIC
    Indicates this formula is an atomic proposition.
    static int ARITY_BINARY
    Indicates this formula is a binary formula.
    static int ARITY_UNARY
    Indicates this formula is a unary formula.
    static int CONJUNCTION_DISJUNCTION_OUTPUT_FORMAT_C_STYLE
    Outputs boolean operators in C style, i.e., !, &&.
    static int CONJUNCTION_DISJUNCTION_OUTPUT_FORMAT_LOGIC_STYLE
    Outputs boolean operators in logic style, i.e., ~, /\, \/.
    static LTL FALSE
    The LTL formula which is always false.
    protected static java.lang.String FALSE_STRING
    The name of #FALSE.
    static int IMPLICATION_OUTOUT_FORMAT_1
    Outputs implication and bi-implication with two dashes, i.e., -> and <-->
    static int IMPLICATION_OUTOUT_FORMAT_2
    Outputs implication and bi-implication with one dash, i.e., -> and <->
    static java.lang.String O_CONJUNCTION_DISJUNCTION_OUTPUT_FORMAT
    The option of outputting format for boolean operators.
    static java.lang.String O_DUAL_MODE
    The option of dual mode of temporal operators.
    static java.lang.String O_IMPLICATION_OUTPUT_FORMAT
    The option of outputting format for implication and bi-implication.
    static java.lang.String O_TEMPORAL_OPERATOR_OUTPUT_FORMAT
    The option of outputting format for temporal operators.
    static int PATH_FORMULA
    Indicates this formula is a path formula.
    static int STATE_FORMULA
    Indicates this formula is a state formula.
    static int TEMPORAL_OPERATOR_OUTPUT_FORMAT_LETTER
    Outputs temporal operators as letters, i.e., X, F, G, Y, Z, O, and H.
    static int TEMPORAL_OPERATOR_OUTPUT_FORMAT_SYMBOL
    Outputs temporal operators as symbols, i.e., (), <>, [], (-), (~), <->, and [-].
    static LTL TRUE
    The LTL formula which is always true.
    protected static java.lang.String TRUE_STRING
    The name of #TRUE.

  • Constructor Summary

    Constructors 
    Constructor Description
    LTL()
    Constructor.

  • Method Summary

    Modifier and Type Method Description
    abstract LTL clone()
    Makes a clone of this formula.
    abstract boolean containsPromising()
    Returns true if this formula contains a promising sub-formula.
    boolean equals​(java.lang.Object obj)  
    abstract int getArity()
    Returns the arity of this formula, which can be #ARITY_ATOMIC , #ARITY_UNARY, or #ARITY_BINARY.
    abstract java.lang.String getFormat1OperatorString()
    Returns the string representation format of the first operator of this formula in format 1.
    abstract java.lang.String getFormat2OperatorString()
    Returns the string representation format of the first operator of this formula in format 2.
    abstract int getFormulaType()
    Returns the type of this formula, which can be #STATE_FORMULA or #PATH_FORMULA.
    abstract java.util.Set<Proposition> getFreeVariables()
    Returns all free propositions.
    abstract int getLength()
    Returns the length of this formula.
    LTL getNegationNormalForm()
    Returns the LTL formula in negation normal form (NNF).
    abstract LTL getNegationNormalForm​(DualMode mode)
    Returns the LTL formula in negation normal form (NNF).
    abstract java.lang.String getOperatorString()
    Returns the string representation of the first operator of this formula.
    abstract Tense getOperatorTense()
    Returns the tense of the operator of this formula.
    abstract int getPrecedence()
    Returns the precedence of the operator of this formula.
    LTL getPromisedFormula()
    Returns the formula promised by this formula.
    abstract LTLSet getPromisingSubformulae()
    Returns a set of promising sub-formulae of this formula.
    abstract java.lang.String getSPINOperatorString()
    Returns the string representation format of the first operator of this formula in SPIN.
    abstract int getSPINPrecedence()
    Returns the precedence of the operator of this formula in SPIN.
    abstract java.lang.String getUnicodeOperatorString()
    Returns the unicode string representation of the first operator of this formula.
    int hashCode()  
    boolean isBasic()
    Returns true if this formula is a basic formula, which is a literal or a next formula.
    abstract boolean isLiteral()
    Returns true if this formula is a literal.
    abstract boolean isPromising()
    Returns true if this formula is a promising formula, which is p U q, <> p, ~ [] ~p, ~(p W q), or ~(p R q).
    abstract boolean isPureBoolean()
    Returns true if this formula contains only boolean operators.
    abstract boolean isPureFuture()
    Returns true if this formula contains only future operators.
    abstract boolean isPurePast()
    Returns true if this formula contains only past operators.
    LTL pushNegation()
    Pushes a negation as deeply as possible into this LTL formula.
    abstract LTL pushNegation​(DualMode mode)
    Pushes a negation as deeply as possible into this LTL formula.
    abstract LTL renameFreeVariable​(Proposition p, Proposition q)
    Renames a free proposition.
    abstract LTL substitute​(java.util.Map<Proposition,​LTL> subst)
    Returns an LTL formula obtained by substituting an LTL formula for a proposition where the formulae and propositions are specified by a map.
    abstract LTL substitute​(Proposition p, LTL formula)
    Replaces a specified proposition by a specified formula.
    abstract java.lang.String toFormat1String()
    Returns a string for this formula in format 1.
    abstract java.lang.String toFormat2String()
    Returns a string for this formula in format 2.
    abstract java.lang.String toSPINString()
    Returns a string for this formula in SPIN format.
    abstract java.lang.String toUnicodeString()
    Returns a unicode string for this formula.

    Methods inherited from class java.lang.Object

    finalize, getClass, notify, notifyAll, toString, wait, wait, wait

  • Field Details

  • Constructor Details

    • LTL

      public LTL()
      Constructor.

  • Method Details

    • clone

      public abstract LTL clone()
      Makes a clone of this formula.
      Overrides:
      clone in class java.lang.Object

    • containsPromising

      public abstract boolean containsPromising()
      Returns true if this formula contains a promising sub-formula.
      Returns:
      true if this formula contains a promising sub-formula

    • getPromisingSubformulae

      public abstract LTLSet getPromisingSubformulae()
      Returns a set of promising sub-formulae of this formula.
      Returns:
      a set of promising sub-formulae of this formula

    • getArity

      public abstract int getArity()
      Returns the arity of this formula, which can be #ARITY_ATOMIC , #ARITY_UNARY, or #ARITY_BINARY. .
      Returns:
      the arity of this formula

    • getFormulaType

      public abstract int getFormulaType()
      Returns the type of this formula, which can be #STATE_FORMULA or #PATH_FORMULA.
      Returns:
      the type of this formula

    • getFreeVariables

      public abstract java.util.Set<Proposition> getFreeVariables()
      Returns all free propositions.
      Returns:
      free propositions

    • getLength

      public abstract int getLength()
      Returns the length of this formula.
      Returns:
      the length of this formula

    • getNegationNormalForm

      public LTL getNegationNormalForm()
      Returns the LTL formula in negation normal form (NNF). The dual of an until formula will be an unless formula and the dual of a since formula will be a backto formula.
      Specified by:
      getNegationNormalForm in interface NegationNormalForm<LTL>
      Returns:
      the LTL formula in negation normal form

    • getNegationNormalForm

      public abstract LTL getNegationNormalForm​(DualMode mode)
      Returns the LTL formula in negation normal form (NNF). The dual of an until formula or a since formula depends on the dual mode.
      Parameters:
      mode - the mode of duality of temporal operators
      Returns:
      the LTL formula in negation normal form

    • getPrecedence

      public abstract int getPrecedence()
      Returns the precedence of the operator of this formula.
      Returns:
      the precedence of the operator of this formula

    • getSPINPrecedence

      public abstract int getSPINPrecedence()
      Returns the precedence of the operator of this formula in SPIN.
      Returns:
      the precedence of the operator of this formula in SPIN

    • getOperatorTense

      public abstract Tense getOperatorTense()
      Returns the tense of the operator of this formula.
      Returns:
      the tense of the operator of this formula

    • getOperatorString

      public abstract java.lang.String getOperatorString()
      Returns the string representation of the first operator of this formula.
      Returns:
      the string representation of the first operator of this formula

    • getFormat1OperatorString

      public abstract java.lang.String getFormat1OperatorString()
      Returns the string representation format of the first operator of this formula in format 1.
      Returns:
      the string representation of the first operator of this formula in format 1

    • getFormat2OperatorString

      public abstract java.lang.String getFormat2OperatorString()
      Returns the string representation format of the first operator of this formula in format 2.
      Returns:
      the string representation of the first operator of this formula in format 2

    • getSPINOperatorString

      public abstract java.lang.String getSPINOperatorString()
      Returns the string representation format of the first operator of this formula in SPIN.
      Returns:
      the string representation of the first operator of this formula in SPIN format

    • getUnicodeOperatorString

      public abstract java.lang.String getUnicodeOperatorString()
      Returns the unicode string representation of the first operator of this formula.
      Returns:
      the unicode string representation of the first operator of this formula

    • isBasic

      public boolean isBasic()
      Returns true if this formula is a basic formula, which is a literal or a next formula.
      Returns:
      true if this formula is a basic formula

    • isLiteral

      public abstract boolean isLiteral()
      Returns true if this formula is a literal. Note that ~~p is not a literal.
      Returns:
      true if this formula is a literal

    • isPromising

      public abstract boolean isPromising()
      Returns true if this formula is a promising formula, which is p U q, <> p, ~ [] ~p, ~(p W q), or ~(p R q).
      Returns:
      true if this formula is a promising formula

    • getPromisedFormula

      public LTL getPromisedFormula()
      Returns the formula promised by this formula. If this formula is q U p, <> p, or ~ [] ~p, the promised formula is p. If this formula is ~(p W q), the promised formula is (~p /\ ~q). If this formula is ~(p R q), the promised formula is ~q.
      Returns:
      the formula promised by this formula, or null if this formula is not promising

    • isPureFuture

      public abstract boolean isPureFuture()
      Returns true if this formula contains only future operators.
      Returns:
      true if this formula contains only future operators

    • isPurePast

      public abstract boolean isPurePast()
      Returns true if this formula contains only past operators.
      Returns:
      true if this formula contains only past operators

    • isPureBoolean

      public abstract boolean isPureBoolean()
      Returns true if this formula contains only boolean operators.
      Returns:
      true if this formula contains only boolean operators

    • pushNegation

      public LTL pushNegation()
      Pushes a negation as deeply as possible into this LTL formula. The dual of an until formula will be an unless formula and the dual of a since formula will be a backto formula.
      Returns:
      the negation of this formula in negation normal form

    • pushNegation

      public abstract LTL pushNegation​(DualMode mode)
      Pushes a negation as deeply as possible into this LTL formula. The dual of an until formula or a since formula depends on the dual mode.
      Parameters:
      mode - the duality mode of temporal operators
      Returns:
      the negation of this formula in negation normal form

    • renameFreeVariable

      public abstract LTL renameFreeVariable​(Proposition p, Proposition q)
      Renames a free proposition.
      Parameters:
      p - the proposition to be renamed
      q - the new proposition after renaming
      Returns:
      the formula obtained by renaming p to q in this formula

    • substitute

      public abstract LTL substitute​(Proposition p, LTL formula)
      Replaces a specified proposition by a specified formula.
      Parameters:
      p - a proposition
      formula - a formula
      Returns:
      the formula obtained by replacing p with formula

    • substitute

      public abstract LTL substitute​(java.util.Map<Proposition,​LTL> subst)
      Returns an LTL formula obtained by substituting an LTL formula for a proposition where the formulae and propositions are specified by a map.
      Parameters:
      subst - a map from a proposition to its replacement
      Returns:
      the expression obtained by replacing the domain of subst with the range of subst in formula

    • hashCode

      public int hashCode()
      Overrides:
      hashCode in class java.lang.Object

    • equals

      public boolean equals​(java.lang.Object obj)
      Overrides:
      equals in class java.lang.Object

    • toFormat1String

      public abstract java.lang.String toFormat1String()
      Returns a string for this formula in format 1. The unary temporal operators will be in ASCII symbols.
      Returns:
      a string for this formula

    • toFormat2String

      public abstract java.lang.String toFormat2String()
      Returns a string for this formula in format 2. The unary temporal operators will be in letters.
      Returns:
      a string for this formula

    • toUnicodeString

      public abstract java.lang.String toUnicodeString()
      Returns a unicode string for this formula. The temporal operators will be in letters.
      Returns:
      a unicode string for this formula

    • toSPINString

      public abstract java.lang.String toSPINString()
      Returns a string for this formula in SPIN format. Note that some operators are not supported by SPIN.
      Returns:
      a string for this formula in SPIN format