net.sf.tweety.action.query.analysis

Class SActionQuerySatisfactionTester

java.lang.Object

net.sf.tweety.action.query.analysis.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 and Description
SActionQuerySatisfactionTester(AspInterface aspsolver) Creates a new instance of this satisfaction tester using the given answer set solver.

Method Summary

Modifier and Type	Method and 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(PropositionalFormula 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<PropositionalFormula>	getQueryParts(PropositionalFormula 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, BeliefBase actionQueries) Checks whether the given transition system satisfies the given action queries.
boolean	isSatisfied(TransitionSystem transitionSystem, java.util.Set<ActionQuery> 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(AspInterface aspsolver)

Creates a new instance of this satisfaction tester using the given answer set solver.

Parameters:

aspsolver -

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.

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(PropositionalFormula 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 -

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 -

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<PropositionalFormula> getQueryParts(PropositionalFormula 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 -