Package org.svvrl.goal.core.logic.qptl

Class QPTL

java.lang.Object
org.svvrl.goal.core.logic.Logic
org.svvrl.goal.core.logic.qptl.QPTL
All Implemented Interfaces:
java.io.Serializable, java.lang.Cloneable, NegationNormalForm<QPTL>, PrenexNormalForm<QPTL>
Direct Known Subclasses:
QPTLAtomic, QPTLBinary, QPTLQuantification, QPTLUnary
public abstract class QPTL
extends Logic
implements java.lang.Cloneable, NegationNormalForm<QPTL>, PrenexNormalForm<QPTL>
This class provides common methods for QPTL 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_QUANTIFICATION
    Indicates this formula is a quantified formula.
    static int ARITY_UNARY
    Indicates this formula is a unary formula.
    protected static java.lang.String ERROR_PRENEX
    A string says that this formula cannot be converted to prenex normal form.
    static QPTL FALSE
    The QPTL formula which is always false.
    protected static java.lang.String FALSE_STRING
    The name of #FALSE.
    static int PATH_FORMULA
    Indicates this formula is a path formula.
    static int STATE_FORMULA
    Indicates this formula is a state formula.
    static QPTL TRUE
    The QPTL formula which is always true.
    protected static java.lang.String TRUE_STRING
    The name of #TRUE.

  • Constructor Summary

    Constructors 
    Constructor Description
    QPTL()
    Constructor.

  • Method Summary

    Modifier and Type Method Description
    abstract QPTL clone()  
    boolean equals​(java.lang.Object obj)  
    abstract int getArity()
    Returns the arity of this formula, which can be #ARITY_ATOMIC , #ARITY_UNARY, #ARITY_BINARY, or #ARITY_QUANTIFICATION .
    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.
    QPTL getNegationNormalForm()
    Returns the QPTL formula in negation normal form (NNF).
    abstract QPTL getNegationNormalForm​(DualMode mode)
    Returns the QPTL 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.
    QPTL getPrenexNormalForm()
    Returns the QPTL formula in prenex normal form.
    QPTL getPrenexNormalForm​(DualMode mode)
    Returns the QPTL formula in prenex normal form.
    protected abstract QPTL getPrenexNormalForm2​(DualMode mode)
    A helper method for #getPrenexNormalForm(DualMode).
    abstract QPTL getPromisedFormula()
    Returns the formula promised by this formula.
    java.util.List<Proposition> getPropositions()
    Returns all propositions (both free and bound) ordered in the sequence of their occurrence.
    protected abstract void getPropositions​(java.util.List<Proposition> props)
    Collects all propositions (both free and bound) ordered in the sequence of their occurrence.
    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.
    abstract boolean hasBoundVariable​(Proposition x)
    Returns true if a specified proposition is bound (quantified) in this formula.
    abstract boolean hasFreeVariable​(Proposition x)
    Returns true if a specified proposition occurs freely (not quantified) in this formula.
    int hashCode()  
    abstract boolean hasQuantification()
    Returns true if this formula contains quantification.
    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.
    boolean isPrenexNormalForm()
    Returns true if this formula is in prenex normal form.
    protected abstract boolean isPrenexNormalForm​(boolean inside)
    Returns true if some larger formula containing this formula is in prenex normal form.
    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 isPureFuture()
    Returns true if this formula contains only future operators.
    abstract boolean isPurePast()
    Returns true if this formula contains only past operators.
    QPTL pushNegation()
    Pushes a negation as deeply as possible into this QPTL formula.
    abstract QPTL pushNegation​(DualMode mode)
    Pushes a negation as deeply as possible into this QPTL formula.
    abstract QPTL renameBoundVariable​(Proposition p, Proposition q)
    Renames a bound proposition.
    QPTL renameBoundVariables()
    Renames bound variables such that there is no variable bound at difference places.
    protected abstract QPTL renameBoundVariables​(java.util.Collection<Proposition> seen)
    Renames bound variables with the information of bound variables already seen such that there is no variable bound at difference places.
    abstract QPTL renameFreeVariable​(Proposition p, Proposition q)
    Renames a free proposition.
    abstract QPTL replace​(java.util.Map<Proposition,​QPTL> subst)
    Returns a QPTL formula obtained by substituting a QPTL formula for a proposition where the formulae and propositions are specified by a map.
    abstract QPTL replace​(Proposition p, QPTL 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

    • QPTL

      public QPTL()
      Constructor.

  • Method Details

    • clone

      public abstract QPTL clone()
      Overrides:
      clone in class java.lang.Object

    • getArity

      public abstract int getArity()
      Returns the arity of this formula, which can be #ARITY_ATOMIC , #ARITY_UNARY, #ARITY_BINARY, or #ARITY_QUANTIFICATION .
      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

    • getPromisedFormula

      public abstract QPTL getPromisedFormula()
      Returns the formula promised by this formula.
      Returns:
      the formula promised by this formula, or null if this formula is not promising

    • getNegationNormalForm

      public QPTL getNegationNormalForm()
      Returns the QPTL 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<QPTL>
      Returns:
      the QPTL formula in negation normal form

    • getNegationNormalForm

      public abstract QPTL getNegationNormalForm​(DualMode mode)
      Returns the QPTL 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 QPTL formula in negation normal form

    • getPrenexNormalForm

      public QPTL getPrenexNormalForm()
      Returns the QPTL formula in prenex normal form. 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:
      getPrenexNormalForm in interface PrenexNormalForm<QPTL>
      Returns:
      the QPTL formula in prenex normal form
      Throws:
      java.lang.IllegalArgumentException - if this formula cannot be converted into prenex normal form

    • getPrenexNormalForm

      public QPTL getPrenexNormalForm​(DualMode mode)
      Returns the QPTL formula in prenex normal form. 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 QPTL formula in prenex normal form
      Throws:
      java.lang.IllegalArgumentException - if this formula cannot be converted into prenex normal form

    • getPrenexNormalForm2

      protected abstract QPTL getPrenexNormalForm2​(DualMode mode) throws java.lang.IllegalArgumentException
      A helper method for #getPrenexNormalForm(DualMode). Before invoking this method, the bound variables are already renamed such that there is no variable bound at difference places. For example, before invoking method on the formula "(E t, [](t --> y)) ∧ (E : t, [] (t --> x))", the second bound t will be renamed.
      Parameters:
      mode - the mode of duality of temporal operators
      Returns:
      this formula in prenex normal form
      Throws:
      java.lang.IllegalArgumentException - if this formula cannot be converted into prenex 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

    • hasBoundVariable

      public abstract boolean hasBoundVariable​(Proposition x)
      Returns true if a specified proposition is bound (quantified) in this formula. For example, "t ∧ E : t, [] (t --> x)" has a quantified variable t.
      Parameters:
      x - a proposition
      Returns:
      true if x is bound in this formula

    • hasFreeVariable

      public abstract boolean hasFreeVariable​(Proposition x)
      Returns true if a specified proposition occurs freely (not quantified) in this formula. For example, "t ∧ E : t, [] (t --> x)" has two free variables t and x.
      Parameters:
      x - a proposition
      Returns:
      true if x is free in this formula

    • hasQuantification

      public abstract boolean hasQuantification()
      Returns true if this formula contains quantification.
      Returns:
      true if this formula contains quantification

    • 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

    • 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

    • isPrenexNormalForm

      public boolean isPrenexNormalForm()
      Returns true if this formula is in prenex normal form.
      Returns:
      true if this formula is in prenex normal form

    • isPrenexNormalForm

      protected abstract boolean isPrenexNormalForm​(boolean inside)
      Returns true if some larger formula containing this formula is in prenex normal form.
      Parameters:
      inside - indicates if this formula is inside some temporal operator in the larger formula
      Returns:
      true if the larger formula containing this formula is in prenex normal form

    • pushNegation

      public QPTL pushNegation()
      Pushes a negation as deeply as possible into this QPTL 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 QPTL pushNegation​(DualMode mode)
      Pushes a negation as deeply as possible into this QPTL 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

    • renameBoundVariables

      public QPTL renameBoundVariables()
      Renames bound variables such that there is no variable bound at difference places.
      Returns:
      a QPTL formula obtained from this formula by renaming bound propositions to different names

    • renameBoundVariables

      protected abstract QPTL renameBoundVariables​(java.util.Collection<Proposition> seen)
      Renames bound variables with the information of bound variables already seen such that there is no variable bound at difference places.
      Parameters:
      seen - a set of bound variables already seen
      Returns:
      a QPTL formula obtained from this formula by renaming bound propositions to different names

    • renameFreeVariable

      public abstract QPTL 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

    • renameBoundVariable

      public abstract QPTL renameBoundVariable​(Proposition p, Proposition q)
      Renames a bound 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

    • replace

      public abstract QPTL replace​(Proposition p, QPTL 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

    • replace

      public abstract QPTL replace​(java.util.Map<Proposition,​QPTL> subst)
      Returns a QPTL formula obtained by substituting a QPTL 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

    • getPropositions

      public java.util.List<Proposition> getPropositions()
      Returns all propositions (both free and bound) ordered in the sequence of their occurrence. Note that if a proposition name is both free and bound at difference places, it will be counted as one single proposition.
      Returns:
      all propositions ordered in the sequence of their occurrence

    • getPropositions

      protected abstract void getPropositions​(java.util.List<Proposition> props)
      Collects all propositions (both free and bound) ordered in the sequence of their occurrence.
      Parameters:
      props - a list for storing all propositions ordered in the sequence of their occurrence

    • 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