Class CTransitionSystemCalculator
- java.lang.Object
-
- net.sf.tweety.action.description.reasoner.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.
-
-
-
Field Detail
-
aspsolver
private ASPSolver aspsolver
-
-
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 failsjava.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 failsjava.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.
-
-