public class SActionQuerySatisfactionTester extends java.lang.Object implements ActionQuerySatisfactionTester
Constructor and Description |
---|
SActionQuerySatisfactionTester(AspInterface aspsolver)
Creates a new instance of this satisfaction tester using the given answer
set solver.
|
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.
|
public SActionQuerySatisfactionTester(AspInterface aspsolver)
aspsolver
- public boolean isSatisfied(TransitionSystem transitionSystem, BeliefBase actionQueries)
ActionQuerySatisfactionTester
isSatisfied
in interface ActionQuerySatisfactionTester
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.public boolean isSatisfied(TransitionSystem transitionSystem, java.util.Set<ActionQuery> actionQueries)
ActionQuerySatisfactionTester
isSatisfied
in interface ActionQuerySatisfactionTester
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.private java.lang.String getConstraints(java.util.Collection<? extends SActionQuery> queries)
queries
- a set of queries for which C_q should be constructed.private java.lang.String getRules(java.util.Collection<SActionQuery> queries)
queries
- the set of queries that should be translated.private java.lang.String getStatePartRules(FolFormula statePart)
statePart
- a propositional formula.private java.lang.String getQueryPartRules(PropositionalFormula queryPart)
queryPart
- private java.lang.String getQueryPropositionPartRules(QueryProposition queryProposition)
queryProposition
- private java.util.Set<FolFormula> getStateParts(FolFormula formula)
formula
- a propositional formula in the form of a FolFormula which is
used for easy grounding.private java.util.Set<PropositionalFormula> getQueryParts(PropositionalFormula formula)
formula
- an action query in the form of a propositional formulaprivate java.util.Set<QueryProposition> getQueryPropositions(SActionQuery query)
query
- an action query.private java.lang.String getTransitionSystemRules(TransitionSystem transitionSystem)
transitionSystem
- a transition system.private NecessarilyQuery getNecessarilyQueryMinusFirstAction(NecessarilyQuery q)
q
- a necessarily query.private java.lang.String removeIllegalCharacters(java.lang.String s)
s
- a string, possibly containing invalid characters in the input
language of lparse-compatible asp-solvers.public java.lang.String regainIllegalCharacters(java.lang.String s)
s
-