From 47cb1aa4d9edf2871eec2e256fde3634207f0e57 Mon Sep 17 00:00:00 2001 From: gereon Date: Wed, 6 Feb 2013 21:15:36 +0100 Subject: [PATCH 1/6] renamed BoundOperator to PathBoundOperator (StateBoundOperator is coming soon...) renamed modelChecker to modelchecker --- src/formula/AbstractFormula.h | 2 +- src/formula/AbstractPathFormula.h | 2 +- src/formula/AbstractStateFormula.h | 4 +- src/formula/And.h | 2 +- src/formula/Ap.h | 2 +- src/formula/BoundedEventually.h | 6 +- src/formula/BoundedNaryUntil.h | 9 +- src/formula/BoundedUntil.h | 2 +- src/formula/Eventually.h | 6 +- src/formula/Formulas.h | 4 +- src/formula/NoBoundOperator.h | 6 +- src/formula/Not.h | 2 +- .../{BoundOperator.h => PathBoundOperator.h} | 28 +-- src/formula/ProbabilisticBoundOperator.h | 14 +- src/formula/ReachabilityReward.h | 2 +- src/formula/RewardBoundOperator.h | 12 +- src/formula/StateBoundOperator.h | 197 ++++++++++++++++++ src/formula/SteadyStateOperator.h | 161 ++++++++++++++ .../AbstractModelChecker.h | 0 .../DtmcPrctlModelChecker.h | 4 +- .../EigenDtmcPrctlModelChecker.h | 2 +- .../ForwardDeclarations.h | 0 .../GmmxxDtmcPrctlModelChecker.h | 2 +- src/parser/PrctlParser.cpp | 16 +- src/storm.cpp | 4 +- test/parser/PrctlParserTest.cpp | 4 +- test/parser/output.dot | 35 ++++ test/storm-tests.cpp | 2 +- 28 files changed, 461 insertions(+), 69 deletions(-) rename src/formula/{BoundOperator.h => PathBoundOperator.h} (84%) create mode 100644 src/formula/StateBoundOperator.h create mode 100644 src/formula/SteadyStateOperator.h rename src/{modelChecker => modelchecker}/AbstractModelChecker.h (100%) rename src/{modelChecker => modelchecker}/DtmcPrctlModelChecker.h (98%) rename src/{modelChecker => modelchecker}/EigenDtmcPrctlModelChecker.h (99%) rename src/{modelChecker => modelchecker}/ForwardDeclarations.h (100%) rename src/{modelChecker => modelchecker}/GmmxxDtmcPrctlModelChecker.h (99%) create mode 100644 test/parser/output.dot diff --git a/src/formula/AbstractFormula.h b/src/formula/AbstractFormula.h index 42ba7bc02..186415965 100644 --- a/src/formula/AbstractFormula.h +++ b/src/formula/AbstractFormula.h @@ -14,7 +14,7 @@ namespace storm { namespace formula { template class AbstractFormula; }} -#include "src/modelChecker/AbstractModelChecker.h" +#include "src/modelchecker/AbstractModelChecker.h" #include "src/formula/AbstractFormulaChecker.h" namespace storm { diff --git a/src/formula/AbstractPathFormula.h b/src/formula/AbstractPathFormula.h index 4337cbe19..eeffcb4c1 100644 --- a/src/formula/AbstractPathFormula.h +++ b/src/formula/AbstractPathFormula.h @@ -13,8 +13,8 @@ template class AbstractPathFormula; }} #include "src/formula/AbstractFormula.h" +#include "src/modelchecker/AbstractModelChecker.h" -#include "modelChecker/AbstractModelChecker.h" #include #include #include diff --git a/src/formula/AbstractStateFormula.h b/src/formula/AbstractStateFormula.h index 9309bf610..9f4750f06 100644 --- a/src/formula/AbstractStateFormula.h +++ b/src/formula/AbstractStateFormula.h @@ -12,9 +12,9 @@ namespace storm { namespace formula { template class AbstractStateFormula; }} -#include "AbstractFormula.h" +#include "src/formula/AbstractFormula.h" #include "src/storage/BitVector.h" -#include "src/modelChecker/AbstractModelChecker.h" +#include "src/modelchecker/AbstractModelChecker.h" namespace storm { namespace formula { diff --git a/src/formula/And.h b/src/formula/And.h index d8078cd15..f92830c52 100644 --- a/src/formula/And.h +++ b/src/formula/And.h @@ -10,7 +10,7 @@ #include "src/formula/AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" -#include "src/modelChecker/AbstractModelChecker.h" +#include "src/modelchecker/AbstractModelChecker.h" #include namespace storm { diff --git a/src/formula/Ap.h b/src/formula/Ap.h index ba5c13287..80bf54fcb 100644 --- a/src/formula/Ap.h +++ b/src/formula/Ap.h @@ -10,7 +10,7 @@ #include "src/formula/AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" -#include "src/modelChecker/AbstractModelChecker.h" +#include "src/modelchecker/AbstractModelChecker.h" namespace storm { namespace formula { diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h index 4be075840..3d1f85e0b 100644 --- a/src/formula/BoundedEventually.h +++ b/src/formula/BoundedEventually.h @@ -8,12 +8,12 @@ #ifndef STORM_FORMULA_BOUNDEDEVENTUALLY_H_ #define STORM_FORMULA_BOUNDEDEVENTUALLY_H_ -#include "AbstractPathFormula.h" -#include "AbstractStateFormula.h" +#include "src/formula/AbstractPathFormula.h" +#include "src/formula/AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" #include "boost/integer/integer_mask.hpp" #include -#include "src/modelChecker/AbstractModelChecker.h" +#include "src/modelchecker/AbstractModelChecker.h" namespace storm { diff --git a/src/formula/BoundedNaryUntil.h b/src/formula/BoundedNaryUntil.h index c42dab12b..fad114101 100644 --- a/src/formula/BoundedNaryUntil.h +++ b/src/formula/BoundedNaryUntil.h @@ -10,7 +10,7 @@ #include "src/formula/AbstractPathFormula.h" #include "src/formula/AbstractStateFormula.h" -#include "src/modelChecker/AbstractModelChecker.h" +#include "src/modelchecker/AbstractModelChecker.h" #include "boost/integer/integer_mask.hpp" #include #include @@ -68,7 +68,7 @@ public: * Empty constructor */ BoundedNaryUntil() { - this->left = NULL; + this->left = nullptr; this->right = new std::vector*,T,T>>(); } @@ -91,10 +91,10 @@ public: * (this behaviour can be prevented by setting the subtrees to NULL before deletion) */ virtual ~BoundedNaryUntil() { - if (left != NULL) { + if (left != nullptr) { delete left; } - if (right != NULL) { + if (right != nullptr) { delete right; } } @@ -205,7 +205,6 @@ private: }; } //namespace formula - } //namespace storm #endif /* STORM_FORMULA_BOUNDEDNARYUNTIL_H_ */ diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h index e00acac74..0c3323b61 100644 --- a/src/formula/BoundedUntil.h +++ b/src/formula/BoundedUntil.h @@ -10,7 +10,7 @@ #include "src/formula/AbstractPathFormula.h" #include "src/formula/AbstractStateFormula.h" -#include "src/modelChecker/AbstractModelChecker.h" +#include "src/modelchecker/AbstractModelChecker.h" #include "boost/integer/integer_mask.hpp" #include #include "src/formula/AbstractFormulaChecker.h" diff --git a/src/formula/Eventually.h b/src/formula/Eventually.h index 4b2ca1ba3..91623d353 100644 --- a/src/formula/Eventually.h +++ b/src/formula/Eventually.h @@ -8,9 +8,9 @@ #ifndef STORM_FORMULA_EVENTUALLY_H_ #define STORM_FORMULA_EVENTUALLY_H_ -#include "AbstractPathFormula.h" -#include "AbstractStateFormula.h" -#include "src/modelChecker/AbstractModelChecker.h" +#include "src/formula/AbstractPathFormula.h" +#include "src/formula/AbstractStateFormula.h" +#include "src/modelchecker/AbstractModelChecker.h" namespace storm { diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index 9af1fed84..f7630a113 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -8,7 +8,7 @@ #ifndef STORM_FORMULA_FORMULAS_H_ #define STORM_FORMULA_FORMULAS_H_ -#include "modelChecker/ForwardDeclarations.h" +#include "modelchecker/ForwardDeclarations.h" #include "AbstractFormula.h" #include "AbstractPathFormula.h" @@ -35,6 +35,6 @@ #include "RewardBoundOperator.h" #include "RewardNoBoundOperator.h" -#include "modelChecker/DtmcPrctlModelChecker.h" +#include "modelchecker/DtmcPrctlModelChecker.h" #endif /* STORM_FORMULA_FORMULAS_H_ */ diff --git a/src/formula/NoBoundOperator.h b/src/formula/NoBoundOperator.h index 1a28b89d4..79578fee2 100644 --- a/src/formula/NoBoundOperator.h +++ b/src/formula/NoBoundOperator.h @@ -8,11 +8,11 @@ #ifndef STORM_FORMULA_NOBOUNDOPERATOR_H_ #define STORM_FORMULA_NOBOUNDOPERATOR_H_ -#include "AbstractFormula.h" -#include "AbstractPathFormula.h" +#include "src/formula/AbstractFormula.h" +#include "src/formula/AbstractPathFormula.h" #include "src/formula/AbstractFormulaChecker.h" -#include "modelChecker/ForwardDeclarations.h" +#include "src/modelchecker/ForwardDeclarations.h" namespace storm { diff --git a/src/formula/Not.h b/src/formula/Not.h index cd7a20399..824e6e03b 100644 --- a/src/formula/Not.h +++ b/src/formula/Not.h @@ -10,7 +10,7 @@ #include "AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" -#include "src/modelChecker/AbstractModelChecker.h" +#include "src/modelchecker/AbstractModelChecker.h" namespace storm { diff --git a/src/formula/BoundOperator.h b/src/formula/PathBoundOperator.h similarity index 84% rename from src/formula/BoundOperator.h rename to src/formula/PathBoundOperator.h index 512d48d2a..72bcc6d56 100644 --- a/src/formula/BoundOperator.h +++ b/src/formula/PathBoundOperator.h @@ -1,35 +1,35 @@ /* - * BoundOperator.h + * PathBoundOperator.h * * Created on: 27.12.2012 * Author: Christian Dehnert */ -#ifndef STORM_FORMULA_BOUNDOPERATOR_H_ -#define STORM_FORMULA_BOUNDOPERATOR_H_ +#ifndef STORM_FORMULA_PATHBOUNDOPERATOR_H_ +#define STORM_FORMULA_PATHBOUNDOPERATOR_H_ #include "src/formula/AbstractStateFormula.h" #include "src/formula/AbstractPathFormula.h" #include "src/formula/AbstractFormulaChecker.h" -#include "src/modelChecker/AbstractModelChecker.h" +#include "src/modelchecker/AbstractModelChecker.h" #include "src/utility/ConstTemplates.h" namespace storm { namespace formula { -template class BoundOperator; +template class PathBoundOperator; /*! - * @brief Interface class for model checkers that support BoundOperator. + * @brief Interface class for model checkers that support PathBoundOperator. * - * All model checkers that support the formula class BoundOperator must inherit + * All model checkers that support the formula class PathBoundOperator must inherit * this pure virtual class. */ template -class IBoundOperatorModelChecker { +class IPathBoundOperatorModelChecker { public: - virtual storm::storage::BitVector* checkBoundOperator(const BoundOperator& obj) const = 0; + virtual storm::storage::BitVector* checkPathBoundOperator(const PathBoundOperator& obj) const = 0; }; /*! @@ -54,7 +54,7 @@ class IBoundOperatorModelChecker { * @see AbstractFormula */ template -class BoundOperator : public AbstractStateFormula { +class PathBoundOperator : public AbstractStateFormula { public: enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL }; @@ -66,7 +66,7 @@ public: * @param bound The bound for the probability * @param pathFormula The child node */ - BoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula* pathFormula) + PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula* pathFormula) : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) { // Intentionally left empty } @@ -77,7 +77,7 @@ public: * The subtree is deleted with the object * (this behavior can be prevented by setting them to NULL before deletion) */ - virtual ~BoundOperator() { + virtual ~PathBoundOperator() { if (pathFormula != nullptr) { delete pathFormula; } @@ -173,7 +173,7 @@ public: * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkBoundOperator(*this); + return modelChecker.template as()->checkPathBoundOperator(*this); } /*! @@ -196,4 +196,4 @@ private: } //namespace storm -#endif /* STORM_FORMULA_BOUNDOPERATOR_H_ */ +#endif /* STORM_FORMULA_PATHBOUNDOPERATOR_H_ */ diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/ProbabilisticBoundOperator.h index f679293d4..e9183950d 100644 --- a/src/formula/ProbabilisticBoundOperator.h +++ b/src/formula/ProbabilisticBoundOperator.h @@ -10,7 +10,7 @@ #include "AbstractStateFormula.h" #include "AbstractPathFormula.h" -#include "BoundOperator.h" +#include "src/formula/PathBoundOperator.h" #include "utility/ConstTemplates.h" namespace storm { @@ -38,14 +38,14 @@ namespace formula { * @see AbstractFormula */ template -class ProbabilisticBoundOperator : public BoundOperator { +class ProbabilisticBoundOperator : public PathBoundOperator { public: /*! * Empty constructor */ - ProbabilisticBoundOperator() : BoundOperator - (BoundOperator::LESS_EQUAL, storm::utility::constGetZero(), nullptr) { + ProbabilisticBoundOperator() : PathBoundOperator + (PathBoundOperator::LESS_EQUAL, storm::utility::constGetZero(), nullptr) { // Intentionally left empty } @@ -58,8 +58,8 @@ public: * @param pathFormula The child node */ ProbabilisticBoundOperator( - typename BoundOperator::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula) : - BoundOperator(comparisonRelation, bound, pathFormula) { + typename PathBoundOperator::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula) : + PathBoundOperator(comparisonRelation, bound, pathFormula) { // Intentionally left empty } @@ -68,7 +68,7 @@ public: */ virtual std::string toString() const { std::string result = "P "; - result += BoundOperator::toString(); + result += PathBoundOperator::toString(); return result; } diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h index 54e2f447b..ad8171642 100644 --- a/src/formula/ReachabilityReward.h +++ b/src/formula/ReachabilityReward.h @@ -11,7 +11,7 @@ #include "src/formula/AbstractPathFormula.h" #include "src/formula/AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" -#include "src/modelChecker/AbstractModelChecker.h" +#include "src/modelchecker/AbstractModelChecker.h" namespace storm { namespace formula { diff --git a/src/formula/RewardBoundOperator.h b/src/formula/RewardBoundOperator.h index 611280483..3d08c6c95 100644 --- a/src/formula/RewardBoundOperator.h +++ b/src/formula/RewardBoundOperator.h @@ -10,7 +10,7 @@ #include "AbstractStateFormula.h" #include "AbstractPathFormula.h" -#include "BoundOperator.h" +#include "PathBoundOperator.h" #include "utility/ConstTemplates.h" namespace storm { @@ -37,13 +37,13 @@ namespace formula { * @see AbstractFormula */ template -class RewardBoundOperator : public BoundOperator { +class RewardBoundOperator : public PathBoundOperator { public: /*! * Empty constructor */ - RewardBoundOperator() : BoundOperator(BoundOperator::LESS_EQUAL, storm::utility::constGetZero(), nullptr) { + RewardBoundOperator() : PathBoundOperator(PathBoundOperator::LESS_EQUAL, storm::utility::constGetZero(), nullptr) { // Intentionally left empty } @@ -55,8 +55,8 @@ public: * @param pathFormula The child node */ RewardBoundOperator( - typename BoundOperator::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula) : - BoundOperator(comparisonRelation, bound, pathFormula) { + typename PathBoundOperator::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula) : + PathBoundOperator(comparisonRelation, bound, pathFormula) { // Intentionally left empty } @@ -65,7 +65,7 @@ public: */ virtual std::string toString() const { std::string result = "R "; - result += BoundOperator::toString(); + result += PathBoundOperator::toString(); return result; } diff --git a/src/formula/StateBoundOperator.h b/src/formula/StateBoundOperator.h new file mode 100644 index 000000000..05c213c07 --- /dev/null +++ b/src/formula/StateBoundOperator.h @@ -0,0 +1,197 @@ +/* + * BoundOperator.h + * + * Created on: 27.12.2012 + * Author: Christian Dehnert + */ + +#ifndef STORM_FORMULA_STATEBOUNDOPERATOR_H_ +#define STORM_FORMULA_STATEBOUNDOPERATOR_H_ + +#include "src/formula/AbstractStateFormula.h" +#include "src/formula/AbstractPathFormula.h" +#include "src/formula/AbstractFormulaChecker.h" +#include "src/modelChecker/AbstractModelChecker.h" +#include "src/utility/ConstTemplates.h" + +namespace storm { +namespace formula { + +template class StateBoundOperator; + +/*! + * @brief Interface class for model checkers that support StateBoundOperator. + * + * All model checkers that support the formula class StateBoundOperator must inherit + * this pure virtual class. + */ +template +class IStateBoundOperatorModelChecker { + public: + virtual storm::storage::BitVector* checkStateBoundOperator(const StateBoundOperator& obj) const = 0; +}; + +/*! + * @brief + * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval + * as root. + * + * Has one Abstract state formula as sub formula/tree. + * + * @par Semantics + * The formula holds iff the probability that the state formula holds is inside the bounds + * specified in this operator + * + * The subtree is seen as part of the object and deleted with it + * (this behavior can be prevented by setting them to NULL before deletion) + * + * + * @see AbstractStateFormula + * @see AbstractPathFormula + * @see ProbabilisticOperator + * @see ProbabilisticNoBoundsOperator + * @see AbstractFormula + */ +template +class StateBoundOperator : public AbstractStateFormula { + +public: + enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL }; + + /*! + * Constructor + * + * @param comparisonOperator The relation for the bound. + * @param bound The bound for the probability + * @param stateFormula The child node + */ + StateBoundOperator(ComparisonType comparisonOperator, T bound, AbstractStateFormula* stateFormula) + : comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) { + // Intentionally left empty + } + + /*! + * Destructor + * + * The subtree is deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + */ + virtual ~StateBoundOperator() { + if (stateFormula != nullptr) { + delete stateFormula; + } + } + + /*! + * @returns the child node (representation of a Abstract state formula) + */ + const AbstractStateFormula& getStateFormula () const { + return *stateFormula; + } + + /*! + * Sets the child node + * + * @param stateFormula the state formula that becomes the new child node + */ + void setStateFormula(AbstractStateFormula* stateFormula) { + this->stateFormula = stateFormula; + } + + /*! + * @returns the comparison relation + */ + const ComparisonType getComparisonOperator() const { + return comparisonOperator; + } + + void setComparisonOperator(ComparisonType comparisonOperator) { + this->comparisonOperator = comparisonOperator; + } + + /*! + * @returns the bound for the measure + */ + const T& getBound() const { + return bound; + } + + /*! + * Sets the interval in which the probability that the path formula holds may lie in. + * + * @param bound The bound for the measure + */ + void setBound(T bound) { + this->bound = bound; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = ""; + switch (comparisonOperator) { + case LESS: result += "< "; break; + case LESS_EQUAL: result += "<= "; break; + case GREATER: result += "> "; break; + case GREATER_EQUAL: result += ">= "; break; + } + result += std::to_string(bound); + result += " ["; + result += stateFormula->toString(); + result += "]"; + return result; + } + + bool meetsBound(T value) const { + switch (comparisonOperator) { + case LESS: return value < bound; break; + case LESS_EQUAL: return value <= bound; break; + case GREATER: return value > bound; break; + case GREATER_EQUAL: return value >= bound; break; + default: return false; + } + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @returns a new AND-object that is identical the called object. + */ + virtual AbstractStateFormula* clone() const = 0; + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkStateBoundOperator(*this); + } + + /*! + * @brief Checks if the subtree conforms to some logic. + * + * @param checker Formula checker object. + * @return true iff the subtree conforms to some logic. + */ + virtual bool conforms(const AbstractFormulaChecker& checker) const { + return checker.conforms(this->stateFormula); + } + +private: + ComparisonType comparisonOperator; + T bound; + AbstractStateFormula* stateFormula; +}; + +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_STATEBOUNDOPERATOR_H_ */ diff --git a/src/formula/SteadyStateOperator.h b/src/formula/SteadyStateOperator.h new file mode 100644 index 000000000..0c0543016 --- /dev/null +++ b/src/formula/SteadyStateOperator.h @@ -0,0 +1,161 @@ +/* + * SteadyState.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_STEADYSTATEOPERATOR_H_ +#define STORM_FORMULA_STEADYSTATEOPERATOR_H_ + +#include "AbstractPathFormula.h" +#include "AbstractStateFormula.h" +#include "BoundOperator.h" +#include "src/formula/AbstractFormulaChecker.h" + +namespace storm { + +namespace formula { + +template class SteadyStateOperator; + +/*! + * @brief Interface class for model checkers that support SteadyStateOperator. + * + * All model checkers that support the formula class SteadyStateOperator must inherit + * this pure virtual class. + */ +template +class ISteadyStateOperatorModelChecker { + public: + /*! + * @brief Evaluates SteadyStateOperator formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual storm::storage::BitVector* checkSteadyStateOperator(const SteadyStateOperator& obj) const = 0; +}; + +/*! + * @brief + * Class for a Abstract (path) formula tree with a SteadyStateOperator node as root. + * + * Has two Abstract state formulas as sub formulas/trees. + * + * @par Semantics + * The formula holds iff \e child holds SteadyStateOperator step, \e child holds + * + * The subtree is seen as part of the object and deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + * + * @see AbstractPathFormula + * @see AbstractFormula + */ +template +class SteadyStateOperator : public BoundOperator { + +public: + /*! + * Empty constructor + */ + SteadyStateOperator() : BoundOperator + (BoundOperator::LESS_EQUAL, storm::utility::constGetZero(), nullptr) { + // Intentionally left empty + } + + /*! + * Constructor + * + * @param child The child node + */ + SteadyStateOperator( + BoundOperator::ComparisonType comparisonRelation, T bound, AbstractStateFormula* child) { + this->child = child; + } + + /*! + * Constructor. + * + * Also deletes the subtree. + * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + */ + virtual ~SteadyStateOperator() { + if (child != NULL) { + delete child; + } + } + + /*! + * @returns the child node + */ + const AbstractStateFormula& getChild() const { + return *child; + } + + /*! + * Sets the subtree + * @param child the new child node + */ + void setChild(AbstractStateFormula* child) { + this->child = child; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = "("; + result += " S "; + result += child->toString(); + result += ")"; + return result; + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @returns a new BoundedUntil-object that is identical the called object. + */ + virtual AbstractPathFormula* clone() const { + SteadyStateOperator* result = new SteadyStateOperator(); + if (child != NULL) { + result->setChild(child); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual storm::storage::BitVector* check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkSteadyStateOperator(*this); + } + + /*! + * @brief Checks if the subtree conforms to some logic. + * + * @param checker Formula checker object. + * @return true iff the subtree conforms to some logic. + */ + virtual bool conforms(const AbstractFormulaChecker& checker) const { + return checker.conforms(this->child); + } + +private: + AbstractStateFormula* child; +}; + +} //namespace formula + +} //namespace storm + +#endif /* STORM_FORMULA_STEADYSTATEOPERATOR_H_ */ diff --git a/src/modelChecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h similarity index 100% rename from src/modelChecker/AbstractModelChecker.h rename to src/modelchecker/AbstractModelChecker.h diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelchecker/DtmcPrctlModelChecker.h similarity index 98% rename from src/modelChecker/DtmcPrctlModelChecker.h rename to src/modelchecker/DtmcPrctlModelChecker.h index 77648de2a..cb9256f48 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelchecker/DtmcPrctlModelChecker.h @@ -16,7 +16,7 @@ #include "src/storage/BitVector.h" #include "src/exceptions/InvalidPropertyException.h" #include "src/utility/Vector.h" -#include "src/modelChecker/AbstractModelChecker.h" +#include "src/modelchecker/AbstractModelChecker.h" #include #include "log4cplus/logger.h" @@ -222,7 +222,7 @@ public: * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - storm::storage::BitVector* checkBoundOperator(const storm::formula::BoundOperator& formula) const { + storm::storage::BitVector* checkPathBoundOperator(const storm::formula::PathBoundOperator& formula) const { // First, we need to compute the probability for satisfying the path formula for each state. std::vector* quantitativeResult = this->checkPathFormula(formula.getPathFormula()); diff --git a/src/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelchecker/EigenDtmcPrctlModelChecker.h similarity index 99% rename from src/modelChecker/EigenDtmcPrctlModelChecker.h rename to src/modelchecker/EigenDtmcPrctlModelChecker.h index 25bf4984b..a7b749129 100644 --- a/src/modelChecker/EigenDtmcPrctlModelChecker.h +++ b/src/modelchecker/EigenDtmcPrctlModelChecker.h @@ -11,7 +11,7 @@ #include "src/utility/Vector.h" #include "src/models/Dtmc.h" -#include "src/modelChecker/DtmcPrctlModelChecker.h" +#include "src/modelchecker/DtmcPrctlModelChecker.h" #include "src/solver/GraphAnalyzer.h" #include "src/utility/ConstTemplates.h" #include "src/exceptions/NoConvergenceException.h" diff --git a/src/modelChecker/ForwardDeclarations.h b/src/modelchecker/ForwardDeclarations.h similarity index 100% rename from src/modelChecker/ForwardDeclarations.h rename to src/modelchecker/ForwardDeclarations.h diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h similarity index 99% rename from src/modelChecker/GmmxxDtmcPrctlModelChecker.h rename to src/modelchecker/GmmxxDtmcPrctlModelChecker.h index 0c54d63cf..009ecd678 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h @@ -11,7 +11,7 @@ #include #include "src/models/Dtmc.h" -#include "src/modelChecker/DtmcPrctlModelChecker.h" +#include "src/modelchecker/DtmcPrctlModelChecker.h" #include "src/solver/GraphAnalyzer.h" #include "src/utility/Vector.h" #include "src/utility/ConstTemplates.h" diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 6f84aa89c..eb90d2550 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -51,23 +51,23 @@ struct PrctlParser::PrctlGrammar : qi::grammar>(qi::_1)]; probabilisticBoundOperator = ( (qi::lit("P") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::formula::BoundOperator::GREATER, qi::_1, qi::_2)] | + phoenix::new_ >(storm::formula::PathBoundOperator::GREATER, qi::_1, qi::_2)] | (qi::lit("P") >> qi::lit(">=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::formula::BoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | + phoenix::new_ >(storm::formula::PathBoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | (qi::lit("P") >> qi::lit("<") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::formula::BoundOperator::LESS, qi::_1, qi::_2)] | + phoenix::new_ >(storm::formula::PathBoundOperator::LESS, qi::_1, qi::_2)] | (qi::lit("P") >> qi::lit("<=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::formula::BoundOperator::LESS_EQUAL, qi::_1, qi::_2)] + phoenix::new_ >(storm::formula::PathBoundOperator::LESS_EQUAL, qi::_1, qi::_2)] ); rewardBoundOperator = ( (qi::lit("R") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::formula::BoundOperator::GREATER, qi::_1, qi::_2)] | + phoenix::new_ >(storm::formula::PathBoundOperator::GREATER, qi::_1, qi::_2)] | (qi::lit("R") >> qi::lit(">=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::formula::BoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | + phoenix::new_ >(storm::formula::PathBoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | (qi::lit("R") >> qi::lit("<") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::formula::BoundOperator::LESS, qi::_1, qi::_2)] | + phoenix::new_ >(storm::formula::PathBoundOperator::LESS, qi::_1, qi::_2)] | (qi::lit("R") >> qi::lit("<=")>> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::formula::BoundOperator::LESS_EQUAL, qi::_1, qi::_2)] + phoenix::new_ >(storm::formula::PathBoundOperator::LESS_EQUAL, qi::_1, qi::_2)] ); //This block defines rules for parsing formulas with noBoundOperators diff --git a/src/storm.cpp b/src/storm.cpp index 9d2fff6d7..2015e85e4 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -22,8 +22,8 @@ #include "src/models/Dtmc.h" #include "src/storage/SparseMatrix.h" #include "src/models/AtomicPropositionsLabeling.h" -#include "src/modelChecker/EigenDtmcPrctlModelChecker.h" -#include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h" +#include "src/modelchecker/EigenDtmcPrctlModelChecker.h" +#include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h" #include "src/parser/AutoParser.h" #include "src/parser/PrctlParser.h" #include "src/solver/GraphAnalyzer.h" diff --git a/test/parser/PrctlParserTest.cpp b/test/parser/PrctlParserTest.cpp index 5a2dd3cf2..7a2957344 100644 --- a/test/parser/PrctlParserTest.cpp +++ b/test/parser/PrctlParserTest.cpp @@ -53,7 +53,7 @@ TEST(PrctlParserTest, parseProbabilisticFormulaTest) { storm::formula::ProbabilisticBoundOperator* op = static_cast*>(prctlFileParser->getFormula()); - ASSERT_EQ(storm::formula::BoundOperator::GREATER, op->getComparisonOperator()); + ASSERT_EQ(storm::formula::PathBoundOperator::GREATER, op->getComparisonOperator()); ASSERT_EQ(0.5, op->getBound()); ASSERT_EQ(prctlFileParser->getFormula()->toString(), "P > 0.500000 [F a]"); @@ -73,7 +73,7 @@ TEST(PrctlParserTest, parseRewardFormulaTest) { storm::formula::RewardBoundOperator* op = static_cast*>(prctlFileParser->getFormula()); - ASSERT_EQ(storm::formula::BoundOperator::GREATER_EQUAL, op->getComparisonOperator()); + ASSERT_EQ(storm::formula::PathBoundOperator::GREATER_EQUAL, op->getComparisonOperator()); ASSERT_EQ(15.0, op->getBound()); ASSERT_EQ(prctlFileParser->getFormula()->toString(), "R >= 15.000000 [(a U !b)]"); diff --git a/test/parser/output.dot b/test/parser/output.dot new file mode 100644 index 000000000..7e0e80061 --- /dev/null +++ b/test/parser/output.dot @@ -0,0 +1,35 @@ +digraph dtmc { + 1[label="1\n{ phi }"]; + 2[label="2\n{ phi }"]; + 3[label="3\n{ phi }"]; + 4[label="4\n{ smth }"]; + 5[label="5\n{ phi,smth }"]; + 6[label="6\n{ psi }"]; + 7[label="7\n{ phi,psi }"]; + 8[label="8\n{ phi,psi }"]; + 9[label="9\n{ phi }"]; + 10[label="10\n{ phi }"]; + 11[label="11\n{ phi }"]; + 0 -> 0 [label=1] + 1 -> 3 [label=0.5] + 1 -> 4 [label=0.5] + 2 -> 1 [label=0.3] + 2 -> 7 [label=0.7] + 3 -> 2 [label=0.05] + 3 -> 3 [label=0.7] + 3 -> 6 [label=0.05] + 3 -> 8 [label=0.2] + 4 -> 1 [label=0.3] + 4 -> 5 [label=0.3] + 4 -> 6 [label=0.4] + 5 -> 4 [label=1] + 6 -> 7 [label=1] + 7 -> 2 [label=0.2] + 7 -> 6 [label=0.8] + 8 -> 9 [label=1] + 9 -> 8 [label=0.3] + 9 -> 9 [label=0.7] + 10 -> 4 [label=1] + 11 -> 5 [label=0.7] + 11 -> 9 [label=0.3] +} diff --git a/test/storm-tests.cpp b/test/storm-tests.cpp index 9165b68a8..0fdcbb456 100644 --- a/test/storm-tests.cpp +++ b/test/storm-tests.cpp @@ -7,7 +7,7 @@ #include "log4cplus/fileappender.h" #include "src/utility/Settings.h" -#include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h" +#include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h" log4cplus::Logger logger; From cc9b11d7e41e01fa533f6ff6961d015bed1aea58 Mon Sep 17 00:00:00 2001 From: gereon Date: Wed, 6 Feb 2013 21:28:36 +0100 Subject: [PATCH 2/6] added StateBoundOperator and SteadyStateOperator --- src/formula/Formulas.h | 1 + src/formula/StateBoundOperator.h | 2 +- src/formula/SteadyStateOperator.h | 64 ++++++------------------------- 3 files changed, 13 insertions(+), 54 deletions(-) diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index f7630a113..980c3ca34 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -34,6 +34,7 @@ #include "ReachabilityReward.h" #include "RewardBoundOperator.h" #include "RewardNoBoundOperator.h" +#include "SteadyStateOperator.h" #include "modelchecker/DtmcPrctlModelChecker.h" diff --git a/src/formula/StateBoundOperator.h b/src/formula/StateBoundOperator.h index 05c213c07..9cfcfb862 100644 --- a/src/formula/StateBoundOperator.h +++ b/src/formula/StateBoundOperator.h @@ -11,7 +11,7 @@ #include "src/formula/AbstractStateFormula.h" #include "src/formula/AbstractPathFormula.h" #include "src/formula/AbstractFormulaChecker.h" -#include "src/modelChecker/AbstractModelChecker.h" +#include "src/modelchecker/AbstractModelChecker.h" #include "src/utility/ConstTemplates.h" namespace storm { diff --git a/src/formula/SteadyStateOperator.h b/src/formula/SteadyStateOperator.h index 0c0543016..bce02ff5c 100644 --- a/src/formula/SteadyStateOperator.h +++ b/src/formula/SteadyStateOperator.h @@ -8,9 +8,9 @@ #ifndef STORM_FORMULA_STEADYSTATEOPERATOR_H_ #define STORM_FORMULA_STEADYSTATEOPERATOR_H_ -#include "AbstractPathFormula.h" -#include "AbstractStateFormula.h" -#include "BoundOperator.h" +#include "src/formula/AbstractPathFormula.h" +#include "src/formula/AbstractStateFormula.h" +#include "src/formula/StateBoundOperator.h" #include "src/formula/AbstractFormulaChecker.h" namespace storm { @@ -53,14 +53,14 @@ class ISteadyStateOperatorModelChecker { * @see AbstractFormula */ template -class SteadyStateOperator : public BoundOperator { +class SteadyStateOperator : public StateBoundOperator { public: /*! * Empty constructor */ - SteadyStateOperator() : BoundOperator - (BoundOperator::LESS_EQUAL, storm::utility::constGetZero(), nullptr) { + SteadyStateOperator() : StateBoundOperator + (StateBoundOperator::LESS_EQUAL, storm::utility::constGetZero(), nullptr) { // Intentionally left empty } @@ -70,35 +70,8 @@ public: * @param child The child node */ SteadyStateOperator( - BoundOperator::ComparisonType comparisonRelation, T bound, AbstractStateFormula* child) { - this->child = child; - } - - /*! - * Constructor. - * - * Also deletes the subtree. - * (this behaviour can be prevented by setting the subtrees to NULL before deletion) - */ - virtual ~SteadyStateOperator() { - if (child != NULL) { - delete child; - } - } - - /*! - * @returns the child node - */ - const AbstractStateFormula& getChild() const { - return *child; - } - - /*! - * Sets the subtree - * @param child the new child node - */ - void setChild(AbstractStateFormula* child) { - this->child = child; + typename StateBoundOperator::ComparisonType comparisonRelation, T bound, AbstractStateFormula* stateFormula) : + StateBoundOperator(comparisonRelation, bound, stateFormula) { } /*! @@ -107,7 +80,7 @@ public: virtual std::string toString() const { std::string result = "("; result += " S "; - result += child->toString(); + result += StateBoundOperator::toString(); result += ")"; return result; } @@ -119,11 +92,9 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractStateFormula* clone() const { SteadyStateOperator* result = new SteadyStateOperator(); - if (child != NULL) { - result->setChild(child); - } + result->setStateFormula(this->getStateFormula().clone()); return result; } @@ -140,22 +111,9 @@ public: return modelChecker.template as()->checkSteadyStateOperator(*this); } - /*! - * @brief Checks if the subtree conforms to some logic. - * - * @param checker Formula checker object. - * @return true iff the subtree conforms to some logic. - */ - virtual bool conforms(const AbstractFormulaChecker& checker) const { - return checker.conforms(this->child); - } - -private: - AbstractStateFormula* child; }; } //namespace formula - } //namespace storm #endif /* STORM_FORMULA_STEADYSTATEOPERATOR_H_ */ From 718608622fa456e83fa451aa03dc3a39b2f8e4eb Mon Sep 17 00:00:00 2001 From: gereon Date: Wed, 6 Feb 2013 22:12:29 +0100 Subject: [PATCH 3/6] added Ctmdp model, changed MdpParser to NonDetModelParser --- src/models/Ctmdp.h | 251 ++++++++++++++++++ src/parser/AutoParser.cpp | 9 +- src/parser/MdpParser.h | 40 --- ...er.cpp => NonDeterministicModelParser.cpp} | 20 +- src/parser/NonDeterministicModelParser.h | 62 +++++ test/parser/ParseMdpTest.cpp | 6 +- 6 files changed, 333 insertions(+), 55 deletions(-) create mode 100644 src/models/Ctmdp.h delete mode 100644 src/parser/MdpParser.h rename src/parser/{MdpParser.cpp => NonDeterministicModelParser.cpp} (73%) create mode 100644 src/parser/NonDeterministicModelParser.h diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h new file mode 100644 index 000000000..137095e9f --- /dev/null +++ b/src/models/Ctmdp.h @@ -0,0 +1,251 @@ +/* + * Ctmdp.h + * + * Created on: 14.01.2013 + * Author: Philipp Berger + */ + +#ifndef STORM_MODELS_CTMDP_H_ +#define STORM_MODELS_CTMDP_H_ + +#include +#include +#include +#include + +#include "AtomicPropositionsLabeling.h" +#include "GraphTransitions.h" +#include "src/storage/SparseMatrix.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/utility/CommandLine.h" +#include "src/utility/Settings.h" +#include "src/models/AbstractModel.h" +#include "src/parser/NonDeterministicSparseTransitionParser.h" + +namespace storm { + +namespace models { + +/*! + * This class represents a Markov Decision Process (CTMDP) whose states are + * labeled with atomic propositions. + */ +template +class Ctmdp : public storm::models::AbstractModel { + +public: + //! Constructor + /*! + * Constructs a CTMDP object from the given transition probability matrix and + * the given labeling of the states. + * @param probabilityMatrix The transition probability relation of the + * CTMDP given by a matrix. + * @param stateLabeling The labeling that assigns a set of atomic + * propositions to each state. + */ + Ctmdp(std::shared_ptr> probabilityMatrix, + std::shared_ptr stateLabeling, + std::shared_ptr> rowMapping, + std::shared_ptr> stateRewards = nullptr, + std::shared_ptr> transitionRewardMatrix = nullptr) + : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), rowMapping(rowMapping), + stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix), + backwardTransitions(nullptr) { + if (!this->checkValidityOfProbabilityMatrix()) { + LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); + throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; + } + } + + //! Copy Constructor + /*! + * Copy Constructor. Performs a deep copy of the given CTMDP. + * @param ctmdp A reference to the CTMDP that is to be copied. + */ + Ctmdp(const Ctmdp &ctmdp) : probabilityMatrix(ctmdp.probabilityMatrix), + stateLabeling(ctmdp.stateLabeling), rowMapping(ctmdp.rowMapping), stateRewards(ctmdp.stateRewards), + transitionRewardMatrix(ctmdp.transitionRewardMatrix) { + if (ctmdp.backwardTransitions != nullptr) { + this->backwardTransitions = new storm::models::GraphTransitions(*ctmdp.backwardTransitions); + } + if (!this->checkValidityOfProbabilityMatrix()) { + LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); + throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; + } + } + + //! Destructor + /*! + * Destructor. Frees the matrix and labeling associated with this CTMDP. + */ + ~Ctmdp() { + if (this->backwardTransitions != nullptr) { + delete this->backwardTransitions; + } + } + + /*! + * Returns the state space size of the CTMDP. + * @return The size of the state space of the CTMDP. + */ + uint_fast64_t getNumberOfStates() const { + return this->probabilityMatrix->getColumnCount(); + } + + /*! + * Returns the number of (non-zero) transitions of the CTMDP. + * @return The number of (non-zero) transitions of the CTMDP. + */ + uint_fast64_t getNumberOfTransitions() const { + return this->probabilityMatrix->getNonZeroEntryCount(); + } + + /*! + * Returns a bit vector in which exactly those bits are set to true that + * correspond to a state labeled with the given atomic proposition. + * @param ap The atomic proposition for which to get the bit vector. + * @return A bit vector in which exactly those bits are set to true that + * correspond to a state labeled with the given atomic proposition. + */ + storm::storage::BitVector* getLabeledStates(std::string ap) const { + return this->stateLabeling->getAtomicProposition(ap); + } + + /*! + * Returns a pointer to the matrix representing the transition probability + * function. + * @return A pointer to the matrix representing the transition probability + * function. + */ + std::shared_ptr> getTransitionProbabilityMatrix() const { + return this->probabilityMatrix; + } + + /*! + * Returns a pointer to the matrix representing the transition rewards. + * @return A pointer to the matrix representing the transition rewards. + */ + std::shared_ptr> getTransitionRewardMatrix() const { + return this->transitionRewardMatrix; + } + + /*! + * Returns a pointer to the vector representing the state rewards. + * @return A pointer to the vector representing the state rewards. + */ + std::shared_ptr> getStateRewards() const { + return this->stateRewards; + } + + /*! + * + */ + std::set const getPropositionsForState(uint_fast64_t const &state) const { + return stateLabeling->getPropositionsForState(state); + } + + /*! + * Retrieves a reference to the backwards transition relation. + * @return A reference to the backwards transition relation. + */ + storm::models::GraphTransitions& getBackwardTransitions() { + if (this->backwardTransitions == nullptr) { + this->backwardTransitions = new storm::models::GraphTransitions(this->probabilityMatrix, false); + } + return *this->backwardTransitions; + } + + /*! + * Retrieves whether this CTMDP has a state reward model. + * @return True if this CTMDP has a state reward model. + */ + bool hasStateRewards() { + return this->stateRewards != nullptr; + } + + /*! + * Retrieves whether this CTMDP has a transition reward model. + * @return True if this CTMDP has a transition reward model. + */ + bool hasTransitionRewards() { + return this->transitionRewardMatrix != nullptr; + } + + /*! + * Retrieves whether the given atomic proposition is a valid atomic proposition in this model. + * @param atomicProposition The atomic proposition to be checked for validity. + * @return True if the given atomic proposition is valid in this model. + */ + bool hasAtomicProposition(std::string const& atomicProposition) { + return this->stateLabeling->containsAtomicProposition(atomicProposition); + } + + /*! + * Prints information about the model to the specified stream. + * @param out The stream the information is to be printed to. + */ + void printModelInformationToStream(std::ostream& out) const { + storm::utility::printSeparationLine(out); + out << std::endl; + out << "Model type: \t\tCTMDP" << std::endl; + out << "States: \t\t" << this->getNumberOfStates() << std::endl; + out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; + this->stateLabeling->printAtomicPropositionsInformationToStream(out); + out << "Size in memory: \t" + << (this->probabilityMatrix->getSizeInMemory() + + this->stateLabeling->getSizeInMemory() + + sizeof(*this))/1024 << " kbytes" << std::endl; + out << std::endl; + storm::utility::printSeparationLine(out); + } + + storm::models::ModelType getType() { + return CTMDP; + } + +private: + + /*! + * @brief Perform some sanity checks. + * + * Checks probability matrix if all rows sum up to one. + */ + bool checkValidityOfProbabilityMatrix() { + // Get the settings object to customize linear solving. + storm::settings::Settings* s = storm::settings::instance(); + double precision = s->get("precision"); + for (uint_fast64_t row = 0; row < this->probabilityMatrix->getRowCount(); row++) { + T sum = this->probabilityMatrix->getRowSum(row); + if (sum == 0) continue; + if (std::abs(sum - 1) > precision) return false; + } + return true; + } + + /*! A matrix representing the transition probability function of the CTMDP. */ + std::shared_ptr> probabilityMatrix; + + /*! The labeling of the states of the CTMDP. */ + std::shared_ptr stateLabeling; + + /*! The mapping from states to rows. */ + std::shared_ptr> rowMapping; + + /*! The state-based rewards of the CTMDP. */ + std::shared_ptr> stateRewards; + + /*! The transition-based rewards of the CTMDP. */ + std::shared_ptr> transitionRewardMatrix; + + /*! + * A data structure that stores the predecessors for all states. This is + * needed for backwards directed searches. + */ + storm::models::GraphTransitions* backwardTransitions; +}; + +} // namespace models + +} // namespace storm + +#endif /* STORM_MODELS_CTMDP_H_ */ diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index 110831ff6..6c0d5cc40 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -6,7 +6,7 @@ #include "src/exceptions/WrongFileFormatException.h" #include "src/models/AbstractModel.h" #include "src/parser/DeterministicModelParser.h" -#include "src/parser/MdpParser.h" +#include "src/parser/NonDeterministicModelParser.h" namespace storm { namespace parser { @@ -37,12 +37,15 @@ AutoParser::AutoParser(std::string const & transitionSystemFile, std::string con break; } case storm::models::MDP: { - MdpParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); this->model = parser.getMdp(); break; } - case storm::models::CTMDP: + case storm::models::CTMDP: { + NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + this->model = parser.getCtmdp(); break; + } default: ; // Unknown } diff --git a/src/parser/MdpParser.h b/src/parser/MdpParser.h deleted file mode 100644 index e64356dc9..000000000 --- a/src/parser/MdpParser.h +++ /dev/null @@ -1,40 +0,0 @@ -/* - * MdpParser.h - * - * Created on: 14.01.2013 - * Author: thomas - */ - -#ifndef STORM_PARSER_MDPPARSER_H_ -#define STORM_PARSER_MDPPARSER_H_ - -#include "src/parser/Parser.h" -#include "src/models/Mdp.h" - -namespace storm { -namespace parser { - -/*! - * @brief Load label and transition file and return initialized mdp object - * - * @Note This class creates a new Mdp object that can - * be accessed via getMdp(). However, it will not delete this object! - * - * @Note The labeling representation in the file may use at most as much nodes as are specified in the mdp. - */ -class MdpParser: public storm::parser::Parser { -public: - MdpParser(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); - - std::shared_ptr> getMdp() { - return this->mdp; - } - -private: - std::shared_ptr> mdp; -}; - -} /* namespace parser */ -} /* namespace storm */ -#endif /* STORM_PARSER_MDPPARSER_H_ */ diff --git a/src/parser/MdpParser.cpp b/src/parser/NonDeterministicModelParser.cpp similarity index 73% rename from src/parser/MdpParser.cpp rename to src/parser/NonDeterministicModelParser.cpp index ac73b4e40..017d3b31e 100644 --- a/src/parser/MdpParser.cpp +++ b/src/parser/NonDeterministicModelParser.cpp @@ -1,11 +1,11 @@ /* - * MdpParser.cpp + * NonDeterministicModelParser.cpp * * Created on: 14.01.2013 * Author: Philipp Berger */ -#include "src/parser/MdpParser.h" +#include "src/parser/NonDeterministicModelParser.h" #include #include @@ -27,25 +27,27 @@ namespace parser { * @param stateRewardFile String containing the location of the state reward file (...srew) * @param transitionRewardFile String containing the location of the transition reward file (...trew) */ -MdpParser::MdpParser(std::string const & transitionSystemFile, std::string const & labelingFile, +NonDeterministicModelParser::NonDeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { storm::parser::NonDeterministicSparseTransitionParser tp(transitionSystemFile); uint_fast64_t stateCount = tp.getMatrix()->getRowCount(); - std::shared_ptr> stateRewards = nullptr; - std::shared_ptr> transitionRewards = nullptr; - storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile); if (stateRewardFile != "") { storm::parser::SparseStateRewardParser srp(stateCount, stateRewardFile); - stateRewards = srp.getStateRewards(); + this->stateRewards = srp.getStateRewards(); } if (transitionRewardFile != "") { storm::parser::NonDeterministicSparseTransitionParser trp(transitionRewardFile); - transitionRewards = trp.getMatrix(); + this->transitionRewardMatrix = trp.getMatrix(); } - mdp = std::shared_ptr>(new storm::models::Mdp(tp.getMatrix(), lp.getLabeling(), tp.getRowMapping(), stateRewards, transitionRewards)); + this->probabilityMatrix = tp.getMatrix(); + this->stateLabeling = lp.getLabeling(); + this->rowMapping = tp.getRowMapping(); + + this->mdp = nullptr; + this->ctmdp = nullptr; } } /* namespace parser */ diff --git a/src/parser/NonDeterministicModelParser.h b/src/parser/NonDeterministicModelParser.h new file mode 100644 index 000000000..b203154a7 --- /dev/null +++ b/src/parser/NonDeterministicModelParser.h @@ -0,0 +1,62 @@ +/* + * NonDeterministicModelParser.h + * + * Created on: 14.01.2013 + * Author: thomas + */ + +#ifndef STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ +#define STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ + +#include "src/parser/Parser.h" +#include "src/models/Mdp.h" +#include "src/models/Ctmdp.h" + +namespace storm { +namespace parser { + +/*! + * @brief Load label and transition file and return initialized mdp object + * + * @Note This class creates a new Mdp object that can + * be accessed via getMdp(). However, it will not delete this object! + * + * @Note The labeling representation in the file may use at most as much nodes as are specified in the mdp. + */ +class NonDeterministicModelParser: public storm::parser::Parser { +public: + NonDeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); + + std::shared_ptr> getMdp() { + if (this->mdp == nullptr) { + this->mdp = std::shared_ptr>(new storm::models::Mdp( + this->probabilityMatrix, this->stateLabeling, this->rowMapping, this->stateRewards, this->transitionRewardMatrix + )); + } + return this->mdp; + } + + std::shared_ptr> getCtmdp() { + if (this->ctmdp == nullptr) { + this->ctmdp = std::shared_ptr>(new storm::models::Ctmdp( + this->probabilityMatrix, this->stateLabeling, this->rowMapping, this->stateRewards, this->transitionRewardMatrix + )); + } + return this->ctmdp; + } + +private: + std::shared_ptr> probabilityMatrix; + std::shared_ptr stateLabeling; + std::shared_ptr> rowMapping; + std::shared_ptr> stateRewards; + std::shared_ptr> transitionRewardMatrix; + + std::shared_ptr> mdp; + std::shared_ptr> ctmdp; +}; + +} /* namespace parser */ +} /* namespace storm */ +#endif /* STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ */ diff --git a/test/parser/ParseMdpTest.cpp b/test/parser/ParseMdpTest.cpp index 53100426b..353b470c2 100644 --- a/test/parser/ParseMdpTest.cpp +++ b/test/parser/ParseMdpTest.cpp @@ -8,12 +8,12 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/parser/MdpParser.h" +#include "src/parser/NonDeterministicModelParser.h" #include "src/utility/IoUtility.h" TEST(ParseMdpTest, parseAndOutput) { - storm::parser::MdpParser* mdpParser = nullptr; - ASSERT_NO_THROW(mdpParser = new storm::parser::MdpParser( + storm::parser::NonDeterministicModelParser* mdpParser = nullptr; + ASSERT_NO_THROW(mdpParser = new storm::parser::NonDeterministicModelParser( STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")); From 96a833d60515a8d0b43fd57ceef2b29c6fd2604b Mon Sep 17 00:00:00 2001 From: Lanchid Date: Thu, 7 Feb 2013 16:22:07 +0100 Subject: [PATCH 4/6] Added /test/parser/output.dot to gitignore (output file is automatically generated by ParseDtmcTest and should not be in the repository) --- test/parser/.gitignore | 1 + 1 file changed, 1 insertion(+) create mode 100644 test/parser/.gitignore diff --git a/test/parser/.gitignore b/test/parser/.gitignore new file mode 100644 index 000000000..651b60f10 --- /dev/null +++ b/test/parser/.gitignore @@ -0,0 +1 @@ +/output.dot From b5fcc7e590ef34baa1079b03f2f2ccf4bc450c22 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Thu, 7 Feb 2013 16:24:45 +0100 Subject: [PATCH 5/6] Also, deleted the output.dot file... --- test/parser/output.dot | 35 ----------------------------------- 1 file changed, 35 deletions(-) delete mode 100644 test/parser/output.dot diff --git a/test/parser/output.dot b/test/parser/output.dot deleted file mode 100644 index 7e0e80061..000000000 --- a/test/parser/output.dot +++ /dev/null @@ -1,35 +0,0 @@ -digraph dtmc { - 1[label="1\n{ phi }"]; - 2[label="2\n{ phi }"]; - 3[label="3\n{ phi }"]; - 4[label="4\n{ smth }"]; - 5[label="5\n{ phi,smth }"]; - 6[label="6\n{ psi }"]; - 7[label="7\n{ phi,psi }"]; - 8[label="8\n{ phi,psi }"]; - 9[label="9\n{ phi }"]; - 10[label="10\n{ phi }"]; - 11[label="11\n{ phi }"]; - 0 -> 0 [label=1] - 1 -> 3 [label=0.5] - 1 -> 4 [label=0.5] - 2 -> 1 [label=0.3] - 2 -> 7 [label=0.7] - 3 -> 2 [label=0.05] - 3 -> 3 [label=0.7] - 3 -> 6 [label=0.05] - 3 -> 8 [label=0.2] - 4 -> 1 [label=0.3] - 4 -> 5 [label=0.3] - 4 -> 6 [label=0.4] - 5 -> 4 [label=1] - 6 -> 7 [label=1] - 7 -> 2 [label=0.2] - 7 -> 6 [label=0.8] - 8 -> 9 [label=1] - 9 -> 8 [label=0.3] - 9 -> 9 [label=0.7] - 10 -> 4 [label=1] - 11 -> 5 [label=0.7] - 11 -> 9 [label=0.3] -} From afce8c9d1272d89ab4deb2a36090396450f9aa99 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Thu, 7 Feb 2013 17:34:53 +0100 Subject: [PATCH 6/6] Fixed some doxygen warnings (Remaining warnings all appear because of undocumented function parameters) --- src/formula/BoundedNaryUntil.h | 1 - src/formula/SteadyStateOperator.h | 2 +- src/modelchecker/DtmcPrctlModelChecker.h | 2 +- src/models/GraphTransitions.h | 2 +- src/parser/DeterministicModelParser.h | 4 ++-- src/parser/NonDeterministicModelParser.h | 4 ++-- 6 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/formula/BoundedNaryUntil.h b/src/formula/BoundedNaryUntil.h index fad114101..849274000 100644 --- a/src/formula/BoundedNaryUntil.h +++ b/src/formula/BoundedNaryUntil.h @@ -77,7 +77,6 @@ public: * * @param left The left formula subtree * @param right The left formula subtree - * @param bound The maximal number of steps */ BoundedNaryUntil(AbstractStateFormula* left, std::vector*,T,T>>* right) { this->left = left; diff --git a/src/formula/SteadyStateOperator.h b/src/formula/SteadyStateOperator.h index bce02ff5c..755f12249 100644 --- a/src/formula/SteadyStateOperator.h +++ b/src/formula/SteadyStateOperator.h @@ -67,7 +67,7 @@ public: /*! * Constructor * - * @param child The child node + * @param stateFormula The child node */ SteadyStateOperator( typename StateBoundOperator::ComparisonType comparisonRelation, T bound, AbstractStateFormula* stateFormula) : diff --git a/src/modelchecker/DtmcPrctlModelChecker.h b/src/modelchecker/DtmcPrctlModelChecker.h index cb9256f48..17ae608c1 100644 --- a/src/modelchecker/DtmcPrctlModelChecker.h +++ b/src/modelchecker/DtmcPrctlModelChecker.h @@ -117,7 +117,7 @@ public: /*! * Checks the given operator (with no bound) on the DTMC and prints the result * (probability/rewards) for all initial states. - * @param probabilisticNoBoundFormula The formula to be checked. + * @param noBoundFormula The formula to be checked. */ void check(const storm::formula::NoBoundOperator& noBoundFormula) const { std::cout << std::endl; diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h index 6605f1983..579bf7832 100644 --- a/src/models/GraphTransitions.h +++ b/src/models/GraphTransitions.h @@ -73,7 +73,7 @@ public: /*! * Returns an iterator referring to the element after the successors of * the given state. - * @param row The state for which to get the iterator. + * @param state The state for which to get the iterator. * @return An iterator referring to the element after the successors of * the given state. */ diff --git a/src/parser/DeterministicModelParser.h b/src/parser/DeterministicModelParser.h index 3065b0eb4..04d637dce 100644 --- a/src/parser/DeterministicModelParser.h +++ b/src/parser/DeterministicModelParser.h @@ -18,10 +18,10 @@ namespace parser { /*! * @brief Load label and transition file and return initialized dtmc or ctmc object. * - * @Note This class creates a new Dtmc or Ctmc object that can + * @note This class creates a new Dtmc or Ctmc object that can * be accessed via getDtmc() or getCtmc(). However, it will not delete this object! * - * @Note The labeling representation in the file may use at most as much nodes as are specified in the transition system. + * @note The labeling representation in the file may use at most as much nodes as are specified in the transition system. */ class DeterministicModelParser: public storm::parser::Parser { public: diff --git a/src/parser/NonDeterministicModelParser.h b/src/parser/NonDeterministicModelParser.h index b203154a7..379fdf07c 100644 --- a/src/parser/NonDeterministicModelParser.h +++ b/src/parser/NonDeterministicModelParser.h @@ -18,10 +18,10 @@ namespace parser { /*! * @brief Load label and transition file and return initialized mdp object * - * @Note This class creates a new Mdp object that can + * @note This class creates a new Mdp object that can * be accessed via getMdp(). However, it will not delete this object! * - * @Note The labeling representation in the file may use at most as much nodes as are specified in the mdp. + * @note The labeling representation in the file may use at most as much nodes as are specified in the mdp. */ class NonDeterministicModelParser: public storm::parser::Parser { public: