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 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.
-
-
-
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 interfaceActionQuerySatisfactionTester
- 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 interfaceActionQuerySatisfactionTester
- 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.
-
-