Package org.svvrl.goal.core.aut

Enum AlphabetType

java.lang.Object
java.lang.Enum<AlphabetType>
org.svvrl.goal.core.aut.AlphabetType
All Implemented Interfaces:
java.io.Serializable, java.lang.Comparable<AlphabetType>, java.lang.constant.Constable
public enum AlphabetType
extends java.lang.Enum<AlphabetType>
This enumeration defines types of alphabet, including classical alphabet and propositional alphabet.
Author:
Ming-Hsien Tsai

  • Nested Class Summary

    Nested classes/interfaces inherited from class java.lang.Enum

    java.lang.Enum.EnumDesc<E extends java.lang.Enum<E>>

  • Enum Constant Summary

    Enum Constants 
    Enum Constant Description
    CLASSICAL
    The classical alphabet.
    PROPOSITIONAL
    The propositional alphabet.

  • Field Summary

    Fields 
    Modifier and Type Field Description
    static java.lang.String DELIMITER
    The delimiter of propositions.

  • Method Summary

    Modifier and Type Method Description
    java.util.Set<java.lang.String> completeLabels​(java.lang.String[] props, java.lang.String[] symbols)
    Returns a collection of complete symbols for propositional alphabet.
    java.util.Set<java.lang.String> completeLabels​(Proposition[] props, java.lang.String[] symbols)
    Returns a collection of complete symbols for propositional alphabet.
    static void convertAlphabetType​(Automaton aut, AlphabetType type, java.util.Map<java.lang.String,​java.lang.String> map)
    Deprecated.
    Use convertFrom(Automaton, Map) instead
    void convertFrom​(Automaton aut)
    Converts an automaton in some alphabet type to an automaton with this alphabet type.
    void convertFrom​(Automaton aut, java.util.Map<java.lang.String,​java.lang.String> map)
    Converts an automaton in some alphabet type to an automaton with this alphabet type.
    java.lang.String expandLabel​(java.lang.String label, java.lang.String literal)
    Expands a label with a literal.
    java.lang.String formatLabel​(java.lang.Object[] literals)
    Formats a label by giving its literals.
    java.lang.String formatLabel​(java.lang.String label)
    Formats a label by sorting propositions and putting a space between literals.
    java.lang.String formatLabel​(java.util.Collection<?> literals)
    Formats a label by giving its literals.
    static AlphabetType fromString​(java.lang.String str)
    Parses a string as an AlphabetType.
    java.util.List<java.lang.String> genAlphabet​(int n)
    Generates an alphabet with a specified size in this type.
    java.lang.String[] genAlphabet​(java.lang.String[] aps)
    Returns the alphabet defined by a sorted array of atomic propositions or classical symbols.
    java.lang.String getEmptyLabel()
    Returns the display string for an empty label.
    java.util.Set<Literal> getLiterals​(java.lang.String label)
    Splits a label into literals.
    java.util.Set<java.lang.String> getLiteralStrings​(java.lang.String label)
    Splits a label into literals.
    java.lang.String getPropositionFromLiteral​(java.lang.String literal)
    Returns the proposition/symbol in a specified literal
    java.lang.String getPropositionName()
    Returns the meta-name of a proposition or a classical symbol.
    java.util.Set<java.lang.String> getPropositions​(java.lang.String label)
    Returns the set of propositions used in a label.
    java.lang.String getShortPropositionName()
    Returns the short meta-name of a proposition or a classical symbol.
    java.util.Comparator<java.lang.String> getSymbolComparator()
    Returns a comparator of symbols in this alphabet type.
    boolean implies​(java.lang.String l1, java.lang.String l2)
    Tests if the first non-false symbol semantically implies the second symbol.
    boolean isValidLiteral​(java.lang.String lit)
    Checks if a literal is valid or not.
    boolean isValidProposition​(java.lang.String prop)
    Checks if a proposition or a classical symbol is valid or not.
    boolean isValidProposition​(Proposition prop)
    Checks if a proposition or a classical symbol is valid or not.
    boolean isValidPropositionName​(java.lang.String prop)
    Checks if the name of a proposition or a classical symbol is valid or not.
    boolean isValidSymbol​(java.lang.String symbol)
    Checks if a symbol is valid or not.
    java.lang.String removeProposition​(java.lang.String label, java.lang.String prop)
    Removes a proposition from a label.
    java.lang.String replaceLiteral​(java.lang.String label, java.lang.String from, java.lang.String to)
    Renames a literal in a label to another literal.
    java.util.Set<java.lang.String> simplifySymbols​(java.lang.String[] props, java.lang.String[] symbols)
    Returns a collection of simplified symbols for propositional alphabet.
    java.util.Set<java.lang.String> simplifySymbols​(Proposition[] props, java.lang.String[] symbols)
    Returns a collection of simplified symbols for propositional alphabet.
    java.lang.String toString()  
    static AlphabetType valueOf​(java.lang.String name)
    Returns the enum constant of this type with the specified name.
    static AlphabetType[] values()
    Returns an array containing the constants of this enum type, in the order they are declared.

    Methods inherited from class java.lang.Enum

    clone, compareTo, describeConstable, equals, finalize, getDeclaringClass, hashCode, name, ordinal, valueOf

    Methods inherited from class java.lang.Object

    getClass, notify, notifyAll, wait, wait, wait

  • Enum Constant Details

  • Field Details

    • DELIMITER

      public static java.lang.String DELIMITER
      The delimiter of propositions.

  • Method Details

    • values

      public static AlphabetType[] values()
      Returns an array containing the constants of this enum type, in the order they are declared.
      Returns:
      an array containing the constants of this enum type, in the order they are declared

    • valueOf

      public static AlphabetType valueOf​(java.lang.String name)
      Returns the enum constant of this type with the specified name. The string must match exactly an identifier used to declare an enum constant in this type. (Extraneous whitespace characters are not permitted.)
      Parameters:
      name - the name of the enum constant to be returned.
      Returns:
      the enum constant with the specified name
      Throws:
      java.lang.IllegalArgumentException - if this enum type has no constant with the specified name
      java.lang.NullPointerException - if the argument is null

    • getPropositionName

      public java.lang.String getPropositionName()
      Returns the meta-name of a proposition or a classical symbol.
      Returns:
      the meta-name of a proposition or the meta-name of a symbol

    • getShortPropositionName

      public java.lang.String getShortPropositionName()
      Returns the short meta-name of a proposition or a classical symbol.
      Returns:
      the short meta-name of a proposition or a symbol

    • isValidPropositionName

      public boolean isValidPropositionName​(java.lang.String prop)
      Checks if the name of a proposition or a classical symbol is valid or not. For propositional alphabet, the special propositions true, tt, false, and ff are not considered as valid proposition names.
      Parameters:
      prop - a proposition or a classical symbol
      Returns:
      true if the name of the proposition or the classical symbol is valid

    • isValidLiteral

      public boolean isValidLiteral​(java.lang.String lit)
      Checks if a literal is valid or not. For a proposition p, the literal can be p or ~p. For a classical symbol a, the literal can only be a.
      Parameters:
      lit - a literal to be checked
      Returns:
      true if the literal is valid

    • isValidProposition

      public boolean isValidProposition​(java.lang.String prop)
      Checks if a proposition or a classical symbol is valid or not.
      Parameters:
      prop - the proposition or the classical symbol to be checked
      Returns:
      true if the proposition or the classical symbol is valid

    • isValidProposition

      public boolean isValidProposition​(Proposition prop)
      Checks if a proposition or a classical symbol is valid or not.
      Parameters:
      prop - the proposition or the classical symbol to be checked
      Returns:
      true if the proposition or the classical symbol is valid

    • isValidSymbol

      public boolean isValidSymbol​(java.lang.String symbol)
      Checks if a symbol is valid or not.
      Parameters:
      symbol - the symbol to be checked.
      Returns:
      true if the symbol is valid.

    • fromString

      public static AlphabetType fromString​(java.lang.String str)
      Parses a string as an AlphabetType.
      Parameters:
      str - the string to be parsed
      Returns:
      the alphabet type represented by the string

    • formatLabel

      public java.lang.String formatLabel​(java.lang.String label) throws java.lang.IllegalArgumentException
      Formats a label by sorting propositions and putting a space between literals.
      Parameters:
      label - the label to be formatted
      Returns:
      the formatted label
      Throws:
      java.lang.IllegalArgumentException - if the label is invalid

    • formatLabel

      public java.lang.String formatLabel​(java.util.Collection<?> literals) throws java.lang.IllegalArgumentException
      Formats a label by giving its literals.
      Parameters:
      literals - the literals that form the label
      Returns:
      the formatted label
      Throws:
      java.lang.IllegalArgumentException - if there is any invalid literal

    • formatLabel

      public java.lang.String formatLabel​(java.lang.Object[] literals) throws java.lang.IllegalArgumentException
      Formats a label by giving its literals.
      Parameters:
      literals - the literals that form the label
      Returns:
      the formatted label
      Throws:
      java.lang.IllegalArgumentException - if there is any invalid literal

    • getLiteralStrings

      public java.util.Set<java.lang.String> getLiteralStrings​(java.lang.String label)
      Splits a label into literals.
      Parameters:
      label - the label to be split
      Returns:
      the split literals

    • getLiterals

      public java.util.Set<Literal> getLiterals​(java.lang.String label)
      Splits a label into literals.
      Parameters:
      label - the label to be split
      Returns:
      the split literals

    • getPropositionFromLiteral

      public java.lang.String getPropositionFromLiteral​(java.lang.String literal)
      Returns the proposition/symbol in a specified literal
      Parameters:
      literal - a valid literal
      Returns:
      the proposition/symbol in literal

    • getPropositions

      public java.util.Set<java.lang.String> getPropositions​(java.lang.String label)
      Returns the set of propositions used in a label.
      Parameters:
      label - a label
      Returns:
      propositions used in the label

    • replaceLiteral

      public java.lang.String replaceLiteral​(java.lang.String label, java.lang.String from, java.lang.String to)
      Renames a literal in a label to another literal.
      Parameters:
      label - a label
      from - the literal to be renamed
      to - the new literal
      Returns:
      a new label obtained by replacing from with to in label

    • removeProposition

      public java.lang.String removeProposition​(java.lang.String label, java.lang.String prop)
      Removes a proposition from a label.
      Parameters:
      label - a label
      prop - the proposition to be removed
      Returns:
      a new label obtained by removing prop from label

    • expandLabel

      public java.lang.String expandLabel​(java.lang.String label, java.lang.String literal) throws java.lang.IllegalArgumentException
      Expands a label with a literal. If the alphabet type is classical, this method does nothing.
      Parameters:
      label - the label to be expended
      literal - the literal to be inserted
      Returns:
      a new label obtained by inserting the literal in an appropriate position in the label
      Throws:
      java.lang.IllegalArgumentException - if the label or the literal is invalid

    • getEmptyLabel

      public java.lang.String getEmptyLabel()
      Returns the display string for an empty label. For propositional alphabet, an empty label represents true. For classical alphabet, the empty label represents ε.
      Returns:
      a string for displaying an empty label

    • implies

      public boolean implies​(java.lang.String l1, java.lang.String l2)
      Tests if the first non-false symbol semantically implies the second symbol. For a propositional alphabet, l1 implies l2 if l1 contains all literals of l2. For a classical alphabet, l1 implies l2 if they are equal.
      Parameters:
      l1 - a symbol
      l2 - a symbol
      Returns:
      true if the first symbol implies the second symbol

    • toString

      public java.lang.String toString()
      Overrides:
      toString in class java.lang.Enum<AlphabetType>

    • convertFrom

      public void convertFrom​(Automaton aut)
      Converts an automaton in some alphabet type to an automaton with this alphabet type. Default proposition and classical symbol mapping will be used.
      Parameters:
      aut - the automaton to be converted

    • convertFrom

      public void convertFrom​(Automaton aut, java.util.Map<java.lang.String,​java.lang.String> map)
      Converts an automaton in some alphabet type to an automaton with this alphabet type.
      Parameters:
      aut - the automaton to be converted
      map - a map from a symbol in the original alphabet type to a symbol in this alphabet type

    • convertAlphabetType

      @Deprecated public static void convertAlphabetType​(Automaton aut, AlphabetType type, java.util.Map<java.lang.String,​java.lang.String> map)
      Deprecated.
      Use convertFrom(Automaton, Map) instead
      Converts an automaton in some alphabet type to an automaton with another alphabet type.
      Parameters:
      aut - the automaton to be converted
      type - the new alphabet type
      map - a map from a symbol in the original alphabet type to a symbol in the new alphabet type

    • genAlphabet

      public java.lang.String[] genAlphabet​(java.lang.String[] aps)
      Returns the alphabet defined by a sorted array of atomic propositions or classical symbols.
      Parameters:
      aps - a sorted array of atomic propositions or classical symbols
      Returns:
      the alphabet defined by the array of atomic propositions or classical symbols

    • genAlphabet

      public java.util.List<java.lang.String> genAlphabet​(int n) throws java.lang.IllegalArgumentException
      Generates an alphabet with a specified size in this type. For propositional alphabet, the alphabet size cannot be larger than 211.
      Parameters:
      n - the number of symbols in the alphabet
      Returns:
      an alphabet with n symbols
      Throws:
      java.lang.IllegalArgumentException - if the alphabet size is larger than 211

    • getSymbolComparator

      public java.util.Comparator<java.lang.String> getSymbolComparator()
      Returns a comparator of symbols in this alphabet type.
      Returns:
      a comparator of symbols in this alphabet type

    • completeLabels

      public java.util.Set<java.lang.String> completeLabels​(Proposition[] props, java.lang.String[] symbols)
      Returns a collection of complete symbols for propositional alphabet. For example, if there are two atomic propositions p and q, this method will return {"p q", "p ~q"} for {"p"}.
      Parameters:
      props - atomic propositions in consideration
      symbols - the symbols to be completed
      Returns:
      the complete symbols

    • completeLabels

      public java.util.Set<java.lang.String> completeLabels​(java.lang.String[] props, java.lang.String[] symbols)
      Returns a collection of complete symbols for propositional alphabet. For example, if there are two atomic propositions p and q, this method will return {"p q", "p ~q"} for {"p"}.
      Parameters:
      props - atomic propositions in consideration
      symbols - the symbols to be completed
      Returns:
      the complete symbols

    • simplifySymbols

      public java.util.Set<java.lang.String> simplifySymbols​(Proposition[] props, java.lang.String[] symbols)
      Returns a collection of simplified symbols for propositional alphabet. If the input symbols are s0, s1, …, sn and the returned symbols are t0, t1, …, tm, then s0 ∨ s1 ∨ … ∨ sn holds if and only if t0 ∨ t1 ∨ … ∨ tm holds.
      Parameters:
      props - atomic propositions of which the symbols are constructed from
      symbols - symbols
      Returns:
      simplified symbols

    • simplifySymbols

      public java.util.Set<java.lang.String> simplifySymbols​(java.lang.String[] props, java.lang.String[] symbols)
      Returns a collection of simplified symbols for propositional alphabet. If the input symbols are s0, s1, …, sn and the returned symbols are t0, t1, …, tm, then s0 ∨ s1 ∨ … ∨ sn holds if and only if t0 ∨ t1 ∨ … ∨ tm holds.
      Parameters:
      props - atomic propositions of which the symbols are constructed from
      symbols - symbols
      Returns:
      simplified symbols