Class CTransitionSystemCalculator


  • public class CTransitionSystemCalculator
    extends java.lang.Object
    This class calculates the transition system as it is described by an action description in the action language C using extended logic programming with an approach from: Representing Transition Systems by Logic Programs. by Vladimir Lifschitz and Hudson Turner, LPNMR '99: Proceedings of the 5th International Conference on Logic Programming and Nonmonotonic Reasoning. Pages 92-106, 1999.
    Author:
    Sebastian Homann, Tim Janus (modifictions for asp library)
    • Constructor Summary

      Constructors 
      Constructor Description
      CTransitionSystemCalculator​(ASPSolver aspsolver)
      Creates a new transition system calculator with the given interface to an answer set solver.
    • Method Summary

      Modifier and Type Method Description
      java.util.Set<State> calculateStates​(CActionDescription actionDescription, ActionSignature signature)
      calculates the set of all states of the transition system described by an action description.
      TransitionSystem calculateTransitionSystem​(CActionDescription actionDescription, ActionSignature signature)
      Calculates a transition system as described by the given action description using all symbols in the given action signature.
      private java.lang.String getAtomString​(RelationalFormula f, int t)
      Utility function representing a given atom, either an actionname or a fluentname, to be used in a rule in an extended logic program.
      private java.lang.String getCompletenessEnforcementRules​(java.util.Set<FolAtom> atoms, int t)
      Returns rules, that enforce the existence of each atom in the given set in all answer sets of an extended logic program.
      private java.lang.String getDefaultNegationRules​(java.util.Set<FolAtom> atoms, int t)
      Returns rules of an extended logic program for the given set of atoms and a parameter t.
      private java.lang.String getLiteralString​(FolFormula f, int t, boolean negated)
      Utility function representing a single literal either in a direct manner or using default negation.
      java.lang.String getLpT​(CActionDescription d, ActionSignature signature, int T)
      Calculates an extended logic programm lp_T(D) for a given action description D and a parameter T, which corresponds to the length of histories in the transition system described by D.
      private java.lang.String getRuleBodyString​(FolFormula f, int t, boolean negated)
      Calculates the representation of an inner formula of a causal rule according to the translation in "Representing Transition Systems by Logic Programs.".
      private java.util.Set<java.util.Map<java.lang.Integer,​java.util.Set<FolAtom>>> parseLpT​(java.lang.String[] lines, ActionSignature signature)
      Parses the resulting answer sets of an lp_T(D) program as a set.
      private java.util.Map<java.lang.Integer,​java.util.Set<FolAtom>> parseLpTSingleLine​(java.lang.String s, ActionSignature signature)
      Utility function parsing a single answer set to a map from timestamp to the set of atoms with that particular timestamp.
      private java.lang.String regainIllegalChars​(java.lang.String s)
      Regains all illegal characters from answer sets.
      private java.lang.String removeIllegalChars​(java.lang.String s)
      Removes illegal characters from atom names, which are not parsable by an lparse compatible answer set solver.
      • Methods inherited from class java.lang.Object

        clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
    • Constructor Detail

      • CTransitionSystemCalculator

        public CTransitionSystemCalculator​(ASPSolver aspsolver)
        Creates a new transition system calculator with the given interface to an answer set solver.
        Parameters:
        aspsolver - some ASP solver
    • Method Detail

      • calculateTransitionSystem

        public TransitionSystem calculateTransitionSystem​(CActionDescription actionDescription,
                                                          ActionSignature signature)
                                                   throws java.io.IOException
        Calculates a transition system as described by the given action description using all symbols in the given action signature.
        Parameters:
        actionDescription - an action description.
        signature - an action signature.
        Returns:
        a transition system.
        Throws:
        java.io.IOException - if IO fails
        java.lang.IllegalArgumentException - is thrown, when the given action description is not definite, as this method only works for definite action descriptions.
      • calculateStates

        public java.util.Set<State> calculateStates​(CActionDescription actionDescription,
                                                    ActionSignature signature)
                                             throws java.io.IOException
        calculates the set of all states of the transition system described by an action description.
        Parameters:
        actionDescription - an action description.
        signature - an action signature.
        Returns:
        the set of all states of the transition system described by an action description.
        Throws:
        java.io.IOException - if IO fails
        java.lang.IllegalArgumentException - is thrown, when the given action description is not definite.
      • getLpT

        public java.lang.String getLpT​(CActionDescription d,
                                       ActionSignature signature,
                                       int T)
        Calculates an extended logic programm lp_T(D) for a given action description D and a parameter T, which corresponds to the length of histories in the transition system described by D. See "Representing Transition Systems by Logic Programs." for more information.
        Parameters:
        d - an action description.
        signature - an action signature.
        T - length of histories of the transition system of D, that correspond to answer sets of lp_T(D).
        Returns:
        an extended logic program.
      • getDefaultNegationRules

        private java.lang.String getDefaultNegationRules​(java.util.Set<FolAtom> atoms,
                                                         int t)
        Returns rules of an extended logic program for the given set of atoms and a parameter t. For each atom a, the result contains the rules -a(t) :- not a(t). a(t) :- not -a(t).
        Parameters:
        atoms - set of atoms.
        t - parameter t.
        Returns:
        rules.
      • getCompletenessEnforcementRules

        private java.lang.String getCompletenessEnforcementRules​(java.util.Set<FolAtom> atoms,
                                                                 int t)
        Returns rules, that enforce the existence of each atom in the given set in all answer sets of an extended logic program.
        Parameters:
        atoms - a set of atoms.
        t - parameter to be added to each atom.
        Returns:
        rules of an extended logic program.
      • removeIllegalChars

        private java.lang.String removeIllegalChars​(java.lang.String s)
        Removes illegal characters from atom names, which are not parsable by an lparse compatible answer set solver.
        Parameters:
        s - an atom name.
        Returns:
        the same atom name with removed illegal characters.
      • regainIllegalChars

        private java.lang.String regainIllegalChars​(java.lang.String s)
        Regains all illegal characters from answer sets. This regains the original names for each literal in an answer set.
        Parameters:
        s - an atom name in lparse-compatible format.
        Returns:
        the original atom name.
      • parseLpT

        private java.util.Set<java.util.Map<java.lang.Integer,​java.util.Set<FolAtom>>> parseLpT​(java.lang.String[] lines,
                                                                                                      ActionSignature signature)
        Parses the resulting answer sets of an lp_T(D) program as a set. Each answer set is parsed as a map from integers to sets of atoms, where the integer represents the timestamp for each atom in the corresponding set.
        Parameters:
        lines - the output of the answer set solver.
        signature - the action signature of the original description.
        Returns:
        a set of maps each mapping timestamps to sets of atoms.
      • parseLpTSingleLine

        private java.util.Map<java.lang.Integer,​java.util.Set<FolAtom>> parseLpTSingleLine​(java.lang.String s,
                                                                                                 ActionSignature signature)
                                                                                          throws ParserException
        Utility function parsing a single answer set to a map from timestamp to the set of atoms with that particular timestamp.
        Parameters:
        s - a single answer set from the output of a solver.
        signature - the action signature of the original action description.
        Returns:
        a map from timestamps to sets of atoms.
        Throws:
        ParserException - if parsing fails
      • getRuleBodyString

        private java.lang.String getRuleBodyString​(FolFormula f,
                                                   int t,
                                                   boolean negated)
        Calculates the representation of an inner formula of a causal rule according to the translation in "Representing Transition Systems by Logic Programs.". Since the "if"-part of a rule has to be represented by default negation and the "after"-part by a direct translation, this function allows both kinds of translations which may be selected by the boolean parameter "negated".
        Parameters:
        f - the inner formula of a causal rule.
        t - the timestamp for this translation.
        negated - true iff the formula should be represented using default negation.
        Returns:
        a part of a logic rule representing the given formula.
      • getLiteralString

        private java.lang.String getLiteralString​(FolFormula f,
                                                  int t,
                                                  boolean negated)
        Utility function representing a single literal either in a direct manner or using default negation.
        Parameters:
        f - the literal to be represented.
        t - a timestamp.
        negated - true, iff the literal should be represented using default negation.
        Returns:
        a representation of the given literal.
      • getAtomString

        private java.lang.String getAtomString​(RelationalFormula f,
                                               int t)
        Utility function representing a given atom, either an actionname or a fluentname, to be used in a rule in an extended logic program.
        Parameters:
        f - an atom.
        t - a timestamp.
        Returns:
        the string representation of the atom.