Package net.sf.tweety.action.query.analysis

Class SActionQuerySatisfactionTester

  • All Implemented Interfaces:
    ActionQuerySatisfactionTester
    public class SActionQuerySatisfactionTester
extends java.lang.Object
implements ActionQuerySatisfactionTester
    This class provides methods capable of checking if a given transition system satisfies a set of action queries in the action query language s. This is acomplished by a translation of action queries to normal logic programms presented in [1]. [1] Bachelor thesis. Action und Change: Update von Aktionsbeschreibungen by Sebastian Homann. TU Dortmund, 2010.
    Author:
    Sebastian Homann

    • Constructor Summary

      Constructors 
      Constructor Description
      SActionQuerySatisfactionTester​(ASPSolver aspsolver)
      Creates a new instance of this satisfaction tester using the given answer set solver.

    • Method Summary

      Modifier and Type Method Description
      private java.lang.String getConstraints​(java.util.Collection<? extends SActionQuery> queries)
      Returns the program C_q which contains a constraint for each query in question.
      private NecessarilyQuery getNecessarilyQueryMinusFirstAction​(NecessarilyQuery q)
      For a given necessarily query of the form necessarily F after A_0 ; A_1 ; ...
      private java.lang.String getQueryPartRules​(PlFormula queryPart)
      Calculates the translation of an action query to rules of a normal logic program according to the translation sheme presented in [1].
      private java.util.Set<PlFormula> getQueryParts​(PlFormula formula)
      Calculates the set of all subformulas of an action query down to propositions (holds, always, necessarily)
      private java.lang.String getQueryPropositionPartRules​(QueryProposition queryProposition)
      Calculatesthe translation of a query proposition (holds, always, necessarily) to rules of a normal logic program.
      private java.util.Set<QueryProposition> getQueryPropositions​(SActionQuery query)
      Calculates the set of all query propositions which appear in the given query.
      private java.lang.String getRules​(java.util.Collection<SActionQuery> queries)
      Returns the basic translation of action query laws to rules in the logic program.
      private java.lang.String getStatePartRules​(FolFormula statePart)
      This function translates a propositional formula into a logic program according to certain rules.
      private java.util.Set<FolFormula> getStateParts​(FolFormula formula)
      Calculates the set of all possible parts of the propositional formula given.
      private java.lang.String getTransitionSystemRules​(TransitionSystem transitionSystem)
      Calculates a normal logic program which consists only of facts describing the transition system given.
      boolean isSatisfied​(TransitionSystem transitionSystem, java.util.Set<ActionQuery> actionQueries)
      Checks whether the given transition system satisfies the given action queries.
      boolean isSatisfied​(TransitionSystem transitionSystem, BeliefBase actionQueries)
      Checks whether the given transition system satisfies the given action queries.
      java.lang.String regainIllegalCharacters​(java.lang.String s)
      This function exists mainly for debug reasons to regain a human readable version of the atoms in a logic program or in a resulting stable model.
      private java.lang.String removeIllegalCharacters​(java.lang.String s)
      For an easy mapping of formulas to atoms in a logic program, this function changes all symbols, which may occur in a string representation of an action query to unique valid characters in the input language of lparse.

      • Methods inherited from class java.lang.Object

        clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

    • Constructor Detail

      • SActionQuerySatisfactionTester

        public SActionQuerySatisfactionTester​(ASPSolver aspsolver)
        Creates a new instance of this satisfaction tester using the given answer set solver.
        Parameters:
        aspsolver - some ASP solver

    • Method Detail

      • isSatisfied

        public boolean isSatisfied​(TransitionSystem transitionSystem,
                           BeliefBase actionQueries)
        Description copied from interface: ActionQuerySatisfactionTester
        Checks whether the given transition system satisfies the given action queries.
        Specified by:
        isSatisfied in interface ActionQuerySatisfactionTester
        Parameters:
        transitionSystem - the transition system, that will be checked for satisfaction.
        actionQueries - a belief base containing action queries, all of which have to be satisfied by the transition system.
        Returns:
        true iff the transition system satisfies all action queries in the given belief base.

      • isSatisfied

        public boolean isSatisfied​(TransitionSystem transitionSystem,
                           java.util.Set<ActionQuery> actionQueries)
        Description copied from interface: ActionQuerySatisfactionTester
        Checks whether the given transition system satisfies the given action queries.
        Specified by:
        isSatisfied in interface ActionQuerySatisfactionTester
        Parameters:
        transitionSystem - the transition system, that will be checked for satisfaction.
        actionQueries - a set of action queries, which have to be satisfied by the transition system.
        Returns:
        true iff the transition system satisfies all action queries in the given set.

      • getConstraints

        private java.lang.String getConstraints​(java.util.Collection<? extends SActionQuery> queries)
        Returns the program C_q which contains a constraint for each query in question. Each query is identified by an atom in the resulting program.
        Parameters:
        queries - a set of queries for which C_q should be constructed.
        Returns:
        the program C_q

      • getRules

        private java.lang.String getRules​(java.util.Collection<SActionQuery> queries)
        Returns the basic translation of action query laws to rules in the logic program.
        Parameters:
        queries - the set of queries that should be translated.
        Returns:
        a string containing a logic program representation of the given action queries.

      • getStatePartRules

        private java.lang.String getStatePartRules​(FolFormula statePart)
        This function translates a propositional formula into a logic program according to certain rules. See [1] for a detailed description of this translation.
        Parameters:
        statePart - a propositional formula.
        Returns:
        a string containing rules of a normal logic program that represent the given formula.

      • getQueryPartRules

        private java.lang.String getQueryPartRules​(PlFormula queryPart)
        Calculates the translation of an action query to rules of a normal logic program according to the translation sheme presented in [1].
        Parameters:
        queryPart - a propositional formula
        Returns:
        a String containing normal logic rules that represent the given action query.

      • getQueryPropositionPartRules

        private java.lang.String getQueryPropositionPartRules​(QueryProposition queryProposition)
        Calculatesthe translation of a query proposition (holds, always, necessarily) to rules of a normal logic program.
        Parameters:
        queryProposition - a query proposition
        Returns:
        the rules of a normal logic program representing the given query proposition.

      • getStateParts

        private java.util.Set<FolFormula> getStateParts​(FolFormula formula)
        Calculates the set of all possible parts of the propositional formula given.
        Parameters:
        formula - a propositional formula in the form of a FolFormula which is used for easy grounding.
        Returns:
        The set of all parts of the given formula.

      • getQueryParts

        private java.util.Set<PlFormula> getQueryParts​(PlFormula formula)
        Calculates the set of all subformulas of an action query down to propositions (holds, always, necessarily)
        Parameters:
        formula - an action query in the form of a propositional formula
        Returns:
        the set of all subformulas of formula.

      • getQueryPropositions

        private java.util.Set<QueryProposition> getQueryPropositions​(SActionQuery query)
        Calculates the set of all query propositions which appear in the given query. A query proposition may either be a holds, always or a necessarily query.
        Parameters:
        query - an action query.
        Returns:
        the set of all query propositions in query.

      • getTransitionSystemRules

        private java.lang.String getTransitionSystemRules​(TransitionSystem transitionSystem)
        Calculates a normal logic program which consists only of facts describing the transition system given.
        Parameters:
        transitionSystem - a transition system.
        Returns:
        a string containing the rules of a logic program that represents the transition system.

      • getNecessarilyQueryMinusFirstAction

        private NecessarilyQuery getNecessarilyQueryMinusFirstAction​(NecessarilyQuery q)
        For a given necessarily query of the form necessarily F after A_0 ; A_1 ; ... ; A_n this function returns a new query of the form necessarily F after A_1 ; ... ; A_n .
        Parameters:
        q - a necessarily query.
        Returns:
        a new necessarily query wich has the same action sequence as q minus the first action.

      • removeIllegalCharacters

        private java.lang.String removeIllegalCharacters​(java.lang.String s)
        For an easy mapping of formulas to atoms in a logic program, this function changes all symbols, which may occur in a string representation of an action query to unique valid characters in the input language of lparse.
        Parameters:
        s - a string, possibly containing invalid characters in the input language of lparse-compatible asp-solvers.
        Returns:
        a new string, containing only valid characters.

      • regainIllegalCharacters

        public java.lang.String regainIllegalCharacters​(java.lang.String s)
        This function exists mainly for debug reasons to regain a human readable version of the atoms in a logic program or in a resulting stable model.
        Parameters:
        s - a string
        Returns:
        a human readable version of the atoms in a logic program or in a resulting stable model.