From 43f11ccc5f118d25a3d18cbdb3608003469feb75 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 26 Mar 2013 18:18:07 +0100 Subject: [PATCH] Refactoring of modelchecker folder. --- src/formula/AbstractPathFormula.h | 2 +- src/formula/AbstractStateFormula.h | 2 +- src/formula/And.h | 2 +- src/formula/Ap.h | 2 +- src/formula/BoundedEventually.h | 2 +- src/formula/BoundedNaryUntil.h | 2 +- src/formula/BoundedUntil.h | 2 +- src/formula/CumulativeReward.h | 2 +- src/formula/Eventually.h | 2 +- src/formula/Formulas.h | 3 - src/formula/Globally.h | 2 +- src/formula/InstantaneousReward.h | 2 +- src/formula/Next.h | 2 +- src/formula/NoBoundOperator.h | 2 +- src/formula/Not.h | 2 +- src/formula/Or.h | 2 +- src/formula/ProbabilisticBoundOperator.h | 2 +- src/formula/ReachabilityReward.h | 2 +- src/formula/RewardBoundOperator.h | 2 +- src/formula/StateBoundOperator.h | 2 +- src/formula/SteadyStateOperator.h | 2 +- src/formula/Until.h | 2 +- src/modelchecker/AbstractModelChecker.h | 17 +- src/modelchecker/EigenDtmcPrctlModelChecker.h | 12 +- src/modelchecker/ForwardDeclarations.h | 14 +- src/modelchecker/GmmxxDtmcPrctlModelChecker.h | 219 +++++----- src/modelchecker/GmmxxMdpPrctlModelChecker.h | 83 ++-- .../SparseDtmcPrctlModelChecker.h | 35 +- ...Checker.h => SparseMdpPrctlModelChecker.h} | 380 +++++++++--------- ...ogicalValueIterationMdpPrctlModelChecker.h | 68 ++-- src/storm.cpp | 14 +- src/utility/GraphAnalyzer.h | 20 +- src/utility/Vector.h | 12 + .../GmmxxDtmcPrctModelCheckerTest.cpp | 6 +- .../GmmxxMdpPrctModelCheckerTest.cpp | 8 +- test/storm-tests.cpp | 2 +- 36 files changed, 481 insertions(+), 454 deletions(-) rename src/modelchecker/{MdpPrctlModelChecker.h => SparseMdpPrctlModelChecker.h} (57%) diff --git a/src/formula/AbstractPathFormula.h b/src/formula/AbstractPathFormula.h index d0ee74efd..459cbd057 100644 --- a/src/formula/AbstractPathFormula.h +++ b/src/formula/AbstractPathFormula.h @@ -61,7 +61,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const = 0; + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const = 0; }; } //namespace formula diff --git a/src/formula/AbstractStateFormula.h b/src/formula/AbstractStateFormula.h index 9947c5df6..cf15fdb30 100644 --- a/src/formula/AbstractStateFormula.h +++ b/src/formula/AbstractStateFormula.h @@ -58,7 +58,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 = 0; // { + virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const = 0; // { }; } //namespace formula diff --git a/src/formula/And.h b/src/formula/And.h index f5d758c2b..80f46a821 100644 --- a/src/formula/And.h +++ b/src/formula/And.h @@ -162,7 +162,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 { + virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkAnd(*this); } diff --git a/src/formula/Ap.h b/src/formula/Ap.h index 4950b4b72..0cb0d2480 100644 --- a/src/formula/Ap.h +++ b/src/formula/Ap.h @@ -98,7 +98,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 { + virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkAp(*this); } diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h index fe7776f33..33c42f1ba 100644 --- a/src/formula/BoundedEventually.h +++ b/src/formula/BoundedEventually.h @@ -157,7 +157,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { return modelChecker.template as()->checkBoundedEventually(*this, qualitative); } diff --git a/src/formula/BoundedNaryUntil.h b/src/formula/BoundedNaryUntil.h index 7c98af61e..9f83df869 100644 --- a/src/formula/BoundedNaryUntil.h +++ b/src/formula/BoundedNaryUntil.h @@ -179,7 +179,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { return modelChecker.template as()->checkBoundedNaryUntil(*this, qualitative); } diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h index de0a88d2c..2298c3d6e 100644 --- a/src/formula/BoundedUntil.h +++ b/src/formula/BoundedUntil.h @@ -186,7 +186,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { return modelChecker.template as()->checkBoundedUntil(*this, qualitative); } diff --git a/src/formula/CumulativeReward.h b/src/formula/CumulativeReward.h index 6275621db..73ec230d3 100644 --- a/src/formula/CumulativeReward.h +++ b/src/formula/CumulativeReward.h @@ -121,7 +121,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { return modelChecker.template as()->checkCumulativeReward(*this, qualitative); } diff --git a/src/formula/Eventually.h b/src/formula/Eventually.h index 668546f0c..8db4f1b01 100644 --- a/src/formula/Eventually.h +++ b/src/formula/Eventually.h @@ -131,7 +131,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { return modelChecker.template as()->checkEventually(*this, qualitative); } diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index 193114cb1..6dc3b2ed5 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -35,7 +35,4 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" -// FIXME: Why is this needed? To me this makes no sense. -#include "modelchecker/DtmcPrctlModelChecker.h" - #endif /* STORM_FORMULA_FORMULAS_H_ */ diff --git a/src/formula/Globally.h b/src/formula/Globally.h index 7b58580e9..31d06bd05 100644 --- a/src/formula/Globally.h +++ b/src/formula/Globally.h @@ -132,7 +132,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { return modelChecker.template as()->checkGlobally(*this, qualitative); } diff --git a/src/formula/InstantaneousReward.h b/src/formula/InstantaneousReward.h index ed0f7affa..c2001540f 100644 --- a/src/formula/InstantaneousReward.h +++ b/src/formula/InstantaneousReward.h @@ -121,7 +121,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { return modelChecker.template as()->checkInstantaneousReward(*this, qualitative); } diff --git a/src/formula/Next.h b/src/formula/Next.h index 91d68d05a..5f36b053e 100644 --- a/src/formula/Next.h +++ b/src/formula/Next.h @@ -133,7 +133,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { return modelChecker.template as()->checkNext(*this, qualitative); } diff --git a/src/formula/NoBoundOperator.h b/src/formula/NoBoundOperator.h index 55661093c..83da13813 100644 --- a/src/formula/NoBoundOperator.h +++ b/src/formula/NoBoundOperator.h @@ -136,7 +136,7 @@ public: * * @returns A vector indicating all states that satisfy the formula represented by the called object. */ - virtual std::vector* check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkNoBoundOperator(*this); } diff --git a/src/formula/Not.h b/src/formula/Not.h index 0ddb803c9..dde509ec8 100644 --- a/src/formula/Not.h +++ b/src/formula/Not.h @@ -127,7 +127,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 { + virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkNot(*this); } diff --git a/src/formula/Or.h b/src/formula/Or.h index 52cc1d8a8..bb91bfa59 100644 --- a/src/formula/Or.h +++ b/src/formula/Or.h @@ -160,7 +160,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 { + virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkOr(*this); } diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/ProbabilisticBoundOperator.h index 14429c677..8d651ef2c 100644 --- a/src/formula/ProbabilisticBoundOperator.h +++ b/src/formula/ProbabilisticBoundOperator.h @@ -117,7 +117,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 { + virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkProbabilisticBoundOperator(*this); } }; diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h index ff8155eb5..f88deb30e 100644 --- a/src/formula/ReachabilityReward.h +++ b/src/formula/ReachabilityReward.h @@ -127,7 +127,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { return modelChecker.template as()->checkReachabilityReward(*this, qualitative); } diff --git a/src/formula/RewardBoundOperator.h b/src/formula/RewardBoundOperator.h index f602f89b9..18d715fbc 100644 --- a/src/formula/RewardBoundOperator.h +++ b/src/formula/RewardBoundOperator.h @@ -113,7 +113,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 { + virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkRewardBoundOperator(*this); } }; diff --git a/src/formula/StateBoundOperator.h b/src/formula/StateBoundOperator.h index 9cfcfb862..323994c76 100644 --- a/src/formula/StateBoundOperator.h +++ b/src/formula/StateBoundOperator.h @@ -171,7 +171,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 { + virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkStateBoundOperator(*this); } diff --git a/src/formula/SteadyStateOperator.h b/src/formula/SteadyStateOperator.h index 755f12249..402a33c01 100644 --- a/src/formula/SteadyStateOperator.h +++ b/src/formula/SteadyStateOperator.h @@ -107,7 +107,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual storm::storage::BitVector* check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkSteadyStateOperator(*this); } diff --git a/src/formula/Until.h b/src/formula/Until.h index 29c0e497d..d85898f1d 100644 --- a/src/formula/Until.h +++ b/src/formula/Until.h @@ -160,7 +160,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker, bool qualitative) const { + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { return modelChecker.template as()->checkUntil(*this, qualitative); } diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index d7538defc..f3f014cb5 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -10,10 +10,8 @@ // Forward declaration of abstract model checker class needed by the formula classes. namespace storm { -namespace modelChecker { - +namespace modelchecker { template class AbstractModelChecker; - } } @@ -30,7 +28,7 @@ namespace modelChecker { extern log4cplus::Logger logger; namespace storm { -namespace modelChecker { +namespace modelchecker { /*! * @brief @@ -73,10 +71,17 @@ public: * Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly * constructed model checker will have the model of the given model checker as its associated model. */ - explicit AbstractModelChecker(AbstractModelChecker const& modelChecker) : model(modelChecker.model) { + explicit AbstractModelChecker(AbstractModelChecker const& modelchecker) : model(modelchecker.model) { // Intentionally left empty. } + /*! + * Virtual destructor. Needs to be virtual, because this class has virtual methods. + */ + virtual ~AbstractModelChecker() { + // Intentionally left empty. + } + /*! * Returns a pointer to the model checker object that is of the requested type as given by the template parameters. * @returns A pointer to the model checker object that is of the requested type as given by the template parameters. @@ -110,7 +115,6 @@ public: LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(this->model).name() << " to " << typeid(Model).name() << "."); throw bc; } - return nullptr; } /*! @@ -300,7 +304,6 @@ private: }; } // namespace modelchecker - } // namespace storm #endif /* STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/modelchecker/EigenDtmcPrctlModelChecker.h b/src/modelchecker/EigenDtmcPrctlModelChecker.h index 167b02f72..311b69448 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/SparseDtmcPrctlModelChecker.h" #include "src/utility/GraphAnalyzer.h" #include "src/utility/ConstTemplates.h" #include "src/exceptions/NoConvergenceException.h" @@ -29,20 +29,19 @@ extern log4cplus::Logger logger; namespace storm { - -namespace modelChecker { +namespace modelchecker { /* * A model checking engine that makes use of the eigen backend. */ template -class EigenDtmcPrctlModelChecker : public DtmcPrctlModelChecker { +class EigenDtmcPrctlModelChecker : public SparseDtmcPrctlModelChecker { typedef Eigen::Matrix VectorType; typedef Eigen::Map MapType; public: - explicit EigenDtmcPrctlModelChecker(storm::models::Dtmc& dtmc) : DtmcPrctlModelChecker(dtmc) { + explicit EigenDtmcPrctlModelChecker(storm::models::Dtmc& dtmc) : SparseDtmcPrctlModelChecker(dtmc) { // Intentionally left empty. } @@ -136,8 +135,7 @@ private: } }; -} //namespace modelChecker - +} //namespace modelchecker } //namespace storm #endif /* STORM_MODELCHECKER_EIGENDTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/modelchecker/ForwardDeclarations.h b/src/modelchecker/ForwardDeclarations.h index 8239e2023..014d5eec0 100644 --- a/src/modelchecker/ForwardDeclarations.h +++ b/src/modelchecker/ForwardDeclarations.h @@ -2,25 +2,21 @@ * ForwardDeclarations.h * * Created on: 14.01.2013 - * Author: thomas + * Author: Thomas Heinemann */ #ifndef STORM_MODELCHECKER_FORWARDDECLARATIONS_H_ #define STORM_MODELCHECKER_FORWARDDECLARATIONS_H_ - +// Forward declare the abstract model checker. This is used by the formula classes that need this declaration for +// the callback methods (i.e., the check methods). namespace storm { - -namespace modelChecker { +namespace modelchecker { template class AbstractModelChecker; -template -class DtmcPrctlModelChecker; - -} //namespace modelChecker - +} //namespace modelchecker } //namespace storm #endif /* STORM_MODELCHECKER_FORWARDDECLARATIONS_H_ */ diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h index 8c88d0a30..7e818a20c 100644 --- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h @@ -8,47 +8,54 @@ #ifndef STORM_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_ #define STORM_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_ -#include - -#include "src/models/Dtmc.h" -#include "src/modelchecker/DtmcPrctlModelChecker.h" -#include "src/utility/Vector.h" -#include "src/utility/ConstTemplates.h" -#include "src/utility/Settings.h" +#include "src/modelchecker/SparseDtmcPrctlModelChecker.h" #include "src/adapters/GmmxxAdapter.h" -#include "src/exceptions/InvalidPropertyException.h" #include "src/storage/JacobiDecomposition.h" +#include "src/utility/ConstTemplates.h" +#include "src/utility/Settings.h" #include "gmm/gmm_matrix.h" #include "gmm/gmm_iter_solvers.h" -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" - -extern log4cplus::Logger logger; +#include namespace storm { - -namespace modelChecker { +namespace modelchecker { /* - * A model checking engine that makes use of the gmm++ backend. + * An implementation of the SparseDtmcPrctlModelChecker interface that uses gmm++ as the solving backend. */ template -class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker { +class GmmxxDtmcPrctlModelChecker : public SparseDtmcPrctlModelChecker { public: - explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc& dtmc) : DtmcPrctlModelChecker(dtmc) { + /*! + * Constructs a GmmxxDtmcPrctlModelChecker with the given model. + * + * @param model The DTMC to be checked. + */ + explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc& dtmc) : SparseDtmcPrctlModelChecker(dtmc) { // Intentionally left empty. } - virtual ~GmmxxDtmcPrctlModelChecker() { + /*! + * Copy constructs a GmmxxDtmcPrctlModelChecker from the given model checker. In particular, this means that the newly + * constructed model checker will have the model of the given model checker as its associated model. + */ + explicit GmmxxDtmcPrctlModelChecker(storm::modelchecker::GmmxxDtmcPrctlModelChecker const& modelchecker) : SparseDtmcPrctlModelChecker(modelchecker) { + // Intentionally left empty. + } + /*! + * Virtual destructor. Needs to be virtual, because this class has virtual methods. + */ + virtual ~GmmxxDtmcPrctlModelChecker() { + // Intentionally left empty. } /*! * Returns the name of this module. - * @return The name of this module. + * @returns The name of this module. */ static std::string getModuleName() { return "gmm++"; @@ -57,7 +64,7 @@ public: /*! * Returns a trigger such that if the option "matrixlib" is set to "gmm++", this model checker * is to be used. - * @return An option trigger for this module. + * @returns An option trigger for this module. */ static std::pair getOptionTrigger() { return std::pair("matrixlib", "gmm++"); @@ -96,28 +103,33 @@ public: private: - virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& matrix, std::vector& vector, std::vector* summand, uint_fast64_t repetitions = 1) const { - // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(matrix); + virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& A, std::vector& x, std::vector* b, uint_fast64_t n = 1) const { + // Transform the transition probability A to the gmm++ format to use its arithmetic. + gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A); - // Now perform matrix-vector multiplication as long as we meet the bound. + // Set up some temporary variables so that we can just swap pointers instead of copying the result after each + // iteration. std::vector* swap = nullptr; - std::vector* currentVector = &vector; + std::vector* currentVector = &x; std::vector* tmpVector = new std::vector(this->getModel().getNumberOfStates()); - for (uint_fast64_t i = 0; i < repetitions; ++i) { + + // Now perform matrix-vector multiplication as long as we meet the bound. + for (uint_fast64_t i = 0; i < n; ++i) { gmm::mult(*gmmxxMatrix, *currentVector, *tmpVector); swap = tmpVector; tmpVector = currentVector; currentVector = swap; // If requested, add an offset to the current result vector. - if (summand != nullptr) { - gmm::add(*summand, *currentVector); + if (b != nullptr) { + gmm::add(*b, *currentVector); } } - if (repetitions % 2 == 1) { - std::swap(vector, *currentVector); + // If we performed an odd number of repetitions, we need to swap the contents of currentVector and x, because + // the output is supposed to be stored in x. + if (n % 2 == 1) { + std::swap(x, *currentVector); delete currentVector; } else { delete tmpVector; @@ -126,17 +138,7 @@ private: delete gmmxxMatrix; } - /*! - * Solves the linear equation system Ax=b with the given parameters. - * - * @param A The matrix A specifying the coefficients of the linear equations. - * @param x The vector x for which to solve the equations. The initial value of the elements of - * this vector are used as the initial guess and might thus influence performance and convergence. - * @param b The vector b specifying the values on the right-hand-sides of the equations. - * @return The solution of the system of linear equations in form of the elements of the vector - * x. - */ - virtual void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector& vector, std::vector const& b) const { + virtual void solveEquationSystem(storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b) const { // Get the settings object to customize linear solving. storm::settings::Settings* s = storm::settings::instance(); @@ -144,31 +146,38 @@ private: // and the like. gmm::iteration iter(s->get("precision"), 0, s->get("maxiter")); - // Now do the actual solving. - LOG4CPLUS_INFO(logger, "Starting iterative solver."); + // Print some information about the used preconditioner. const std::string& precond = s->getString("precond"); - if (precond == "ilu") { - LOG4CPLUS_INFO(logger, "Using ILU preconditioner."); - } else if (precond == "diagonal") { - LOG4CPLUS_INFO(logger, "Using diagonal preconditioner."); - } else if (precond == "ildlt") { - LOG4CPLUS_INFO(logger, "Using ILDLT preconditioner."); - } else if (precond == "none") { - LOG4CPLUS_INFO(logger, "Using no preconditioner."); + LOG4CPLUS_INFO(logger, "Starting iterative solver."); + if (s->getString("lemethod") == "jacobi") { + if (precond != "none") { + LOG4CPLUS_WARN(logger, "Requested preconditioner '" << precond << "', which is unavailable for the Jacobi method. Dropping preconditioner."); + } + } else { + if (precond == "ilu") { + LOG4CPLUS_INFO(logger, "Using ILU preconditioner."); + } else if (precond == "diagonal") { + LOG4CPLUS_INFO(logger, "Using diagonal preconditioner."); + } else if (precond == "ildlt") { + LOG4CPLUS_INFO(logger, "Using ILDLT preconditioner."); + } else if (precond == "none") { + LOG4CPLUS_INFO(logger, "Using no preconditioner."); + } } + // Now do the actual solving. if (s->getString("lemethod") == "bicgstab") { LOG4CPLUS_INFO(logger, "Using BiCGStab method."); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* A = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(matrix); + gmm::csr_matrix* gmmA = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A); if (precond == "ilu") { - gmm::bicgstab(*A, vector, b, gmm::ilu_precond>(*A), iter); + gmm::bicgstab(*gmmA, x, b, gmm::ilu_precond>(*gmmA), iter); } else if (precond == "diagonal") { - gmm::bicgstab(*A, vector, b, gmm::diagonal_precond>(*A), iter); + gmm::bicgstab(*gmmA, x, b, gmm::diagonal_precond>(*gmmA), iter); } else if (precond == "ildlt") { - gmm::bicgstab(*A, vector, b, gmm::ildlt_precond>(*A), iter); + gmm::bicgstab(*gmmA, x, b, gmm::ildlt_precond>(*gmmA), iter); } else if (precond == "none") { - gmm::bicgstab(*A, vector, b, gmm::identity_matrix(), iter); + gmm::bicgstab(*gmmA, x, b, gmm::identity_matrix(), iter); } // Check if the solver converged and issue a warning otherwise. @@ -177,19 +186,19 @@ private: } else { LOG4CPLUS_WARN(logger, "Iterative solver did not converge."); } - delete A; + delete gmmA; } else if (s->getString("lemethod") == "qmr") { LOG4CPLUS_INFO(logger, "Using QMR method."); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* A = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(matrix); + gmm::csr_matrix* gmmA = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A); if (precond == "ilu") { - gmm::qmr(*A, vector, b, gmm::ilu_precond>(*A), iter); + gmm::qmr(*gmmA, x, b, gmm::ilu_precond>(*gmmA), iter); } else if (precond == "diagonal") { - gmm::qmr(*A, vector, b, gmm::diagonal_precond>(*A), iter); + gmm::qmr(*gmmA, x, b, gmm::diagonal_precond>(*gmmA), iter); } else if (precond == "ildlt") { - gmm::qmr(*A, vector, b, gmm::ildlt_precond>(*A), iter); + gmm::qmr(*gmmA, x, b, gmm::ildlt_precond>(*gmmA), iter); } else if (precond == "none") { - gmm::qmr(*A, vector, b, gmm::identity_matrix(), iter); + gmm::qmr(*gmmA, x, b, gmm::identity_matrix(), iter); } // Check if the solver converged and issue a warning otherwise. @@ -198,58 +207,62 @@ private: } else { LOG4CPLUS_WARN(logger, "Iterative solver did not converge."); } - delete A; + delete gmmA; } else if (s->getString("lemethod") == "jacobi") { LOG4CPLUS_INFO(logger, "Using Jacobi method."); - solveLinearEquationSystemWithJacobi(matrix, vector, b); + uint_fast64_t iterations = solveLinearEquationSystemWithJacobi(A, x, b); + + // Check if the solver converged and issue a warning otherwise. + if (iterations < s->get("maxiter")) { + LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations."); + } else { + LOG4CPLUS_WARN(logger, "Iterative solver did not converge."); + } } } /*! - * Solves the linear equation system Ax=b with the given parameters - * using the Jacobi Method and therefor the Jacobi Decomposition of A. + * Solves the linear equation system A*x = b given by the parameters using the Jacobi method. * - * @param A The matrix A specifying the coefficients of the linear equations. - * @param x The vector x for which to solve the equations. The initial value of the elements of - * this vector are used as the initial guess and might thus influence performance and convergence. - * @param b The vector b specifying the values on the right-hand-sides of the equations. - * @return The solution of the system of linear equations in form of the elements of the vector - * x. + * @param A The matrix specifying the coefficients of the linear equations. + * @param x The solution vector x. The initial values of x represent a guess of the real values to the solver, but + * may be ignored. + * @param b The right-hand side of the equation system. + * @returns The solution vector x of the system of linear equations as the content of the parameter x. + * @returns The number of iterations needed until convergence. */ - void solveLinearEquationSystemWithJacobi(storm::storage::SparseMatrix const& matrix, std::vector& x, std::vector const& b) const { + uint_fast64_t solveLinearEquationSystemWithJacobi(storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b) const { // Get the settings object to customize linear solving. storm::settings::Settings* s = storm::settings::instance(); double precision = s->get("precision"); - if (precision <= 0) { - LOG4CPLUS_ERROR(logger, "Selected precision for linear equation solving must be strictly greater than zero for Jacobi method."); - } - - // Get a Jacobi Decomposition of the Input Matrix - storm::storage::JacobiDecomposition* jacobiDecomposition = matrix.getJacobiDecomposition(); + uint_fast64_t maxIterations = s->get("maxiter"); + bool relative = s->get("relative"); - // Convert the Input Matrix to GMM Format so we can calculate the Residuum - gmm::csr_matrix* A = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(matrix); + // Get a Jacobi decomposition of the matrix A. + storm::storage::JacobiDecomposition* jacobiDecomposition = A.getJacobiDecomposition(); - // Convert the Diagonal matrix to GMM format + // Convert the (inverted) diagonal matrix to gmm++'s format. gmm::csr_matrix* gmmxxDiagonalInverted = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(jacobiDecomposition->getJacobiDInvReference()); - // Convert the LU Matrix to GMM format + // Convert the LU matrix to gmm++'s format. gmm::csr_matrix* gmmxxLU = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(jacobiDecomposition->getJacobiLUReference()); - LOG4CPLUS_INFO(logger, "Starting iterative Jacobi Solver."); // x_(k + 1) = D^-1 * (b - R * x_k) - // In x we keep a copy of the result for swapping in the loop (e.g. less copy-back) + // In x we keep a copy of the result for swapping in the loop (e.g. less copy-back). std::vector* xNext = new std::vector(x.size()); const std::vector* xCopy = xNext; std::vector* xCurrent = &x; - // Target vector for precision calculation + // Target vector for precision calculation. std::vector* residuum = new std::vector(x.size()); + // Set up additional environment variables. uint_fast64_t iterationCount = 0; - do { + bool converged = false; + + while (!converged && iterationCount < maxIterations) { // R * x_k (xCurrent is x_k) -> xNext gmm::mult(*gmmxxLU, *xCurrent, *xNext); // b - R * x_k (xNext contains R * x_k) -> xNext @@ -257,39 +270,39 @@ private: // D^-1 * (b - R * x_k) -> xNext gmm::mult(*gmmxxDiagonalInverted, *xNext, *xNext); - // swap xNext with xCurrent so that the next iteration can use xCurrent again without having to copy the vector + // Swap xNext with xCurrent so that the next iteration can use xCurrent again without having to copy the + // vector. std::vector *const swap = xNext; xNext = xCurrent; xCurrent = swap; + // Now check if the process already converged within our precision. + converged = storm::utility::equalModuloPrecision(*xCurrent, *xNext, precision, relative); + + // Increase iteration count so we can abort if convergence is too slow. ++iterationCount; - // Precision calculation via ||A * x_k - b|| < precision - gmm::mult(*A, *xCurrent, *residuum); - gmm::add(gmm::scaled(*residuum, -1.0), b, *residuum); - } while (gmm::vect_norminf(*residuum) > precision); + } - // If the last iteration did not write to the original x - // we have to swith them + // If the last iteration did not write to the original x we have to swap the contents, because the output has to + // be written to the parameter x. if (xCurrent == xCopy) { - x.swap(*xCurrent); + std::swap(x, *xCurrent); } - // xCopy always points to the Swap-Copy of x we created + // As xCopy always points to the copy of x used for swapping, we can safely delete it. delete xCopy; - // Delete the residuum vector + + // Also delete the other dynamically allocated variables. delete residuum; - // Delete the decompositions delete jacobiDecomposition; - // and the GMM Matrices delete gmmxxDiagonalInverted; delete gmmxxLU; - LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterationCount << " iterations."); + return iterationCount; } }; -} //namespace modelChecker - -} //namespace storm +} // namespace modelchecker +} // namespace storm #endif /* STORM_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/modelchecker/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/GmmxxMdpPrctlModelChecker.h index bacece187..7ee652385 100644 --- a/src/modelchecker/GmmxxMdpPrctlModelChecker.h +++ b/src/modelchecker/GmmxxMdpPrctlModelChecker.h @@ -8,64 +8,72 @@ #ifndef STORM_MODELCHECKER_GMMXXMDPPRCTLMODELCHECKER_H_ #define STORM_MODELCHECKER_GMMXXMDPPRCTLMODELCHECKER_H_ -#include - -#include "src/models/Mdp.h" -#include "src/modelchecker/MdpPrctlModelChecker.h" -#include "src/utility/GraphAnalyzer.h" -#include "src/utility/Vector.h" -#include "src/utility/ConstTemplates.h" -#include "src/utility/Settings.h" +#include "src/modelchecker/SparseMdpPrctlModelChecker.h" #include "src/adapters/GmmxxAdapter.h" -#include "src/exceptions/InvalidPropertyException.h" -#include "src/storage/JacobiDecomposition.h" #include "gmm/gmm_matrix.h" #include "gmm/gmm_iter_solvers.h" -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" - -extern log4cplus::Logger logger; +#include namespace storm { - -namespace modelChecker { +namespace modelchecker { /* - * A model checking engine that makes use of the gmm++ backend. + * An implementation of the SparseMdpPrctlModelChecker interface that uses gmm++ as the solving backend. */ template -class GmmxxMdpPrctlModelChecker : public MdpPrctlModelChecker { +class GmmxxMdpPrctlModelChecker : public SparseMdpPrctlModelChecker { public: - explicit GmmxxMdpPrctlModelChecker(storm::models::Mdp& mdp) : MdpPrctlModelChecker(mdp) { } + /*! + * Constructs a GmmxxMdpPrctlModelChecker with the given model. + * + * @param model The MDP to be checked. + */ + explicit GmmxxMdpPrctlModelChecker(storm::models::Mdp const& model) : SparseMdpPrctlModelChecker(model) { + // Intentionally left empty. + } - virtual ~GmmxxMdpPrctlModelChecker() { } + /*! + * Copy constructs a GmmxxDtmcPrctlModelChecker from the given model checker. In particular, this means that the newly + * constructed model checker will have the model of the given model checker as its associated model. + */ + explicit GmmxxMdpPrctlModelChecker(storm::modelchecker::GmmxxMdpPrctlModelChecker const& modelchecker) : SparseMdpPrctlModelChecker(modelchecker) { + // Intentionally left empty. + } + + /*! + * Virtual destructor. Needs to be virtual, because this class has virtual methods. + */ + virtual ~GmmxxMdpPrctlModelChecker() { + // Intentionally left empty. + } private: - virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& matrix, std::vector& vector, std::vector* summand = nullptr, uint_fast64_t repetitions = 1) const { + + virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& A, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1) const { // Get the starting row indices for the non-deterministic choices to reduce the resulting // vector properly. - std::shared_ptr> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); + std::vector const& nondeterministicChoiceIndices = *this->getModel().getNondeterministicChoiceIndices(); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(matrix); + gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A); // Create vector for result of multiplication, which is reduced to the result vector after // each multiplication. - std::vector multiplyResult(matrix.getRowCount()); + std::vector multiplyResult(A.getRowCount()); // Now perform matrix-vector multiplication as long as we meet the bound of the formula. - for (uint_fast64_t i = 0; i < repetitions; ++i) { - gmm::mult(*gmmxxMatrix, vector, multiplyResult); - if (summand != nullptr) { - gmm::add(*summand, multiplyResult); + for (uint_fast64_t i = 0; i < n; ++i) { + gmm::mult(*gmmxxMatrix, x, multiplyResult); + if (b != nullptr) { + gmm::add(*b, multiplyResult); } if (this->minimumOperatorStack.top()) { - storm::utility::reduceVectorMin(multiplyResult, &vector, *nondeterministicChoiceIndices); + storm::utility::reduceVectorMin(multiplyResult, &x, nondeterministicChoiceIndices); } else { - storm::utility::reduceVectorMax(multiplyResult, &vector, *nondeterministicChoiceIndices); + storm::utility::reduceVectorMax(multiplyResult, &x, nondeterministicChoiceIndices); } } @@ -83,7 +91,7 @@ private: * @return The solution of the system of linear equations in form of the elements of the vector * x. */ - void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) const { + void solveEquationSystem(storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) const { // Get the settings object to customize solving. storm::settings::Settings* s = storm::settings::instance(); @@ -93,18 +101,18 @@ private: bool relative = s->get("relative"); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(matrix); + gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A); // Set up the environment for the power method. - std::vector multiplyResult(matrix.getRowCount()); + std::vector multiplyResult(A.getRowCount()); std::vector* currentX = &x; std::vector* newX = new std::vector(x.size()); std::vector* swap = nullptr; uint_fast64_t iterations = 0; bool converged = false; - // Proceed with the iterations as long as the method did not converge or reach the - // user-specified maximum number of iterations. + // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number + // of iterations. while (!converged && iterations < maxIterations) { // Compute x' = A*x + b. gmm::mult(*gmmxxMatrix, *currentX, multiplyResult); @@ -127,6 +135,8 @@ private: ++iterations; } + // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result + // is currently stored in currentX, but x is the output vector. if (iterations % 2 == 1) { std::swap(x, *currentX); delete currentX; @@ -144,8 +154,7 @@ private: } }; -} //namespace modelChecker - +} //namespace modelchecker } //namespace storm #endif /* STORM_MODELCHECKER_GMMXXMDPPRCTLMODELCHECKER_H_ */ diff --git a/src/modelchecker/SparseDtmcPrctlModelChecker.h b/src/modelchecker/SparseDtmcPrctlModelChecker.h index ff239cdb4..5e7b6aed9 100644 --- a/src/modelchecker/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/SparseDtmcPrctlModelChecker.h @@ -10,14 +10,13 @@ #include "src/modelchecker/AbstractModelChecker.h" #include "src/models/Dtmc.h" -#include "src/storage/SparseMatrix.h" #include "src/utility/Vector.h" #include "src/utility/GraphAnalyzer.h" #include namespace storm { -namespace modelChecker { +namespace modelchecker { /*! * @brief @@ -37,10 +36,17 @@ public: } /*! - * Copy constructs an SparseDtmcPrctlModelChecker from the given model checker. In particular, this means that the newly + * Copy constructs a SparseDtmcPrctlModelChecker from the given model checker. In particular, this means that the newly * constructed model checker will have the model of the given model checker as its associated model. */ - explicit SparseDtmcPrctlModelChecker(storm::modelChecker::SparseDtmcPrctlModelChecker const& modelChecker) : AbstractModelChecker(modelChecker) { + explicit SparseDtmcPrctlModelChecker(storm::modelchecker::SparseDtmcPrctlModelChecker const& modelChecker) : AbstractModelChecker(modelChecker) { + // Intentionally left empty. + } + + /*! + * Virtual destructor. Needs to be virtual, because this class has virtual methods. + */ + virtual ~SparseDtmcPrctlModelChecker() { // Intentionally left empty. } @@ -426,22 +432,22 @@ public: private: /*! - * Performs (repeated) matrix-vector multiplication with the given parameters. + * Performs (repeated) matrix-vector multiplication with the given parameters, i.e. computes x[i+1] = A*x[i] + b + * until x[n], where x[0] = x. * - * @param matrix The matrix that is to be multiplied against the vector. - * @param vector The initial vector that is to be multiplied against the matrix. This is also the output parameter, + * @param A The matrix that is to be multiplied against the vector. + * @param x The initial vector that is to be multiplied against the matrix. This is also the output parameter, * i.e. after the method returns, this vector will contain the computed values. - * @param summand If not null, this vector is being added to the result after each matrix-vector multplication. - * @param repetitions Specifies the number of iterations the matrix-vector multiplication is performed. + * @param b If not null, this vector is being added to the result after each matrix-vector multiplication. + * @param n Specifies the number of iterations the matrix-vector multiplication is performed. * @returns The result of the repeated matrix-vector multiplication as the content of the parameter vector. */ - virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& matrix, std::vector& vector, std::vector* summand = nullptr, uint_fast64_t repetitions = 1) const = 0; - + virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& A, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1) const = 0; /*! * Solves the equation system A*x = b given by the parameters. * - * @param A The matrix specifying the coefficients of the linear eqations. + * @param A The matrix specifying the coefficients of the linear equations. * @param x The solution vector x. The initial values of x represent a guess of the real values to the solver, but * may be ignored. * @param b The right-hand side of the equation system. @@ -450,8 +456,7 @@ private: virtual void solveEquationSystem(storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b) const = 0; }; -} //namespace modelChecker - -} //namespace storm +} // namespace modelchecker +} // namespace storm #endif /* STORM_MODELCHECKER_SPARSEDTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/modelchecker/MdpPrctlModelChecker.h b/src/modelchecker/SparseMdpPrctlModelChecker.h similarity index 57% rename from src/modelchecker/MdpPrctlModelChecker.h rename to src/modelchecker/SparseMdpPrctlModelChecker.h index acc75b2fb..389ffdaa3 100644 --- a/src/modelchecker/MdpPrctlModelChecker.h +++ b/src/modelchecker/SparseMdpPrctlModelChecker.h @@ -1,175 +1,70 @@ /* - * MdpPrctlModelChecker.h + * SparseMdpPrctlModelChecker.h * * Created on: 15.02.2013 * Author: Christian Dehnert */ -#ifndef STORM_MODELCHECKER_MDPPRCTLMODELCHECKER_H_ -#define STORM_MODELCHECKER_MDPPRCTLMODELCHECKER_H_ - -#include "src/formula/Formulas.h" -#include "src/utility/Vector.h" -#include "src/storage/SparseMatrix.h" +#ifndef STORM_MODELCHECKER_SPARSEMDPPRCTLMODELCHECKER_H_ +#define STORM_MODELCHECKER_SPARSEMDPPRCTLMODELCHECKER_H_ +#include "src/modelchecker/AbstractModelChecker.h" #include "src/models/Mdp.h" -#include "src/storage/BitVector.h" -#include "src/exceptions/InvalidPropertyException.h" #include "src/utility/Vector.h" -#include "src/modelchecker/AbstractModelChecker.h" +#include "src/utility/GraphAnalyzer.h" + #include #include -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" - -extern log4cplus::Logger logger; - namespace storm { - -namespace modelChecker { +namespace modelchecker { /*! * @brief - * Interface for model checker classes. - * - * This class provides basic functions that are the same for all subclasses, but mainly only declares - * abstract methods that are to be implemented in concrete instances. - * - * @attention This class is abstract. + * Interface for all model checkers that can verify PRCTL formulae over MDPs represented as a sparse matrix. */ template -class MdpPrctlModelChecker : - public AbstractModelChecker { +class SparseMdpPrctlModelChecker : public AbstractModelChecker { public: /*! - * Constructor + * Constructs a SparseMdpPrctlModelChecker with the given model. * - * @param model The dtmc model which is checked. + * @param model The MDP to be checked. */ - explicit MdpPrctlModelChecker(storm::models::Mdp& model) - : AbstractModelChecker(model), minimumOperatorStack() { + explicit SparseMdpPrctlModelChecker(storm::models::Mdp const& model) : AbstractModelChecker(model), minimumOperatorStack() { + // Intentionally left empty. } /*! - * Copy constructor - * - * @param modelChecker The model checker that is copied. + * Copy constructs a SparseMdpPrctlModelChecker from the given model checker. In particular, this means that the newly + * constructed model checker will have the model of the given model checker as its associated model. */ - explicit MdpPrctlModelChecker(const storm::modelChecker::MdpPrctlModelChecker* modelChecker) - : AbstractModelChecker(modelChecker), minimumOperatorStack() { - + explicit SparseMdpPrctlModelChecker(storm::modelchecker::SparseMdpPrctlModelChecker const& modelchecker) + : AbstractModelChecker(modelchecker), minimumOperatorStack() { + // Intentionally left empty. } /*! - * Destructor + * Virtual destructor. Needs to be virtual, because this class has virtual methods. */ - virtual ~MdpPrctlModelChecker() { + virtual ~SparseMdpPrctlModelChecker() { // Intentionally left empty. } /*! - * @returns A reference to the dtmc of the model checker. + * Returns a constant reference to the MDP associated with this model checker. + * @returns A constant reference to the MDP associated with this model checker. */ - storm::models::Mdp& getModel() const { + storm::models::Mdp const& getModel() const { return AbstractModelChecker::template getModel>(); } /*! - * Sets the DTMC model which is checked - * @param model - */ - void setModel(storm::models::Mdp& model) { - AbstractModelChecker::setModel(model); - } - - /*! - * Checks the given state formula on the DTMC and prints the result (true/false) for all initial - * states. - * @param stateFormula The formula to be checked. - */ - void check(const storm::formula::AbstractStateFormula& stateFormula) const { - std::cout << std::endl; - LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString()); - std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl; - storm::storage::BitVector* result = nullptr; - try { - result = stateFormula.check(*this); - LOG4CPLUS_INFO(logger, "Result for initial states:"); - std::cout << "Result for initial states:" << std::endl; - for (auto initialState : *this->getModel().getLabeledStates("init")) { - LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied")); - std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl; - } - delete result; - } catch (std::exception& e) { - std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; - if (result != nullptr) { - delete result; - } - } - std::cout << std::endl; - storm::utility::printSeparationLine(std::cout); - } - - /*! - * Checks the given operator (with no bound) on the DTMC and prints the result - * (probability/rewards) for all initial states. - * @param noBoundFormula The formula to be checked. - */ - void check(const storm::formula::NoBoundOperator& noBoundFormula) const { - std::cout << std::endl; - LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString()); - std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl; - std::vector* result = nullptr; - try { - result = noBoundFormula.check(*this); - LOG4CPLUS_INFO(logger, "Result for initial states:"); - std::cout << "Result for initial states:" << std::endl; - for (auto initialState : *this->getModel().getLabeledStates("init")) { - LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]); - std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl; - } - delete result; - } catch (std::exception& e) { - std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl; - if (result != nullptr) { - delete result; - } - } - std::cout << std::endl; - storm::utility::printSeparationLine(std::cout); - } - - /*! - * The check method for a formula with an AP node as root in its formula tree - * - * @param formula The Ap state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - storm::storage::BitVector* checkAp(const storm::formula::Ap& formula) const { - if (formula.getAp().compare("true") == 0) { - return new storm::storage::BitVector(this->getModel().getNumberOfStates(), true); - } else if (formula.getAp().compare("false") == 0) { - return new storm::storage::BitVector(this->getModel().getNumberOfStates()); - } - - if (!this->getModel().hasAtomicProposition(formula.getAp())) { - LOG4CPLUS_ERROR(logger, "Atomic proposition '" << formula.getAp() << "' is invalid."); - throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid."; - return nullptr; - } - - return new storm::storage::BitVector(*this->getModel().getLabeledStates(formula.getAp())); - } - - /*! - * The check method for a state formula with a probabilistic operator node without bounds as root - * in its formula tree + * Checks the given formula that is a P/R operator without a bound. * - * @param formula The state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector + * @param formula The formula to check. + * @returns The set of states satisfying the formula represented by a bit vector. */ std::vector* checkNoBoundOperator(const storm::formula::NoBoundOperator& formula) const { // Check if the operator was an non-optimality operator and report an error in that case. @@ -184,10 +79,15 @@ public: } /*! - * The check method for a path formula with a Bounded Until operator node as root in its formula tree + * Checks the given formula that is a bounded-until formula. * - * @param formula The Bounded Until path formula to check - * @returns for each state the probability that the path formula holds. + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula, bool qualitative) const { // First, we need to compute the states that satisfy the sub-formulas of the until-formula. @@ -213,10 +113,15 @@ public: } /*! - * The check method for a path formula with a Next operator node as root in its formula tree + * Checks the given formula that is a next formula. * - * @param formula The Next path formula to check - * @returns for each state the probability that the path formula holds. + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector* checkNext(const storm::formula::Next& formula, bool qualitative) const { // First, we need to compute the states that satisfy the sub-formula of the next-formula. @@ -236,11 +141,15 @@ public: } /*! - * The check method for a path formula with a Bounded Eventually operator node as root in its - * formula tree + * Checks the given formula that is a bounded-eventually formula. * - * @param formula The Bounded Eventually path formula to check - * @returns for each state the probability that the path formula holds + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector* checkBoundedEventually(const storm::formula::BoundedEventually& formula, bool qualitative) const { // Create equivalent temporary bounded until formula and check it. @@ -249,10 +158,15 @@ public: } /*! - * The check method for a path formula with an Eventually operator node as root in its formula tree + * Checks the given formula that is an eventually formula. * - * @param formula The Eventually path formula to check - * @returns for each state the probability that the path formula holds + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector* checkEventually(const storm::formula::Eventually& formula, bool qualitative) const { // Create equivalent temporary until formula and check it. @@ -261,10 +175,15 @@ public: } /*! - * The check method for a path formula with a Globally operator node as root in its formula tree + * Checks the given formula that is a globally formula. * - * @param formula The Globally path formula to check - * @returns for each state the probability that the path formula holds + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector* checkGlobally(const storm::formula::Globally& formula, bool qualitative) const { // Create "equivalent" temporary eventually formula and check it. @@ -277,10 +196,15 @@ public: } /*! - * The check method for a path formula with an Until operator node as root in its formula tree + * Check the given formula that is an until formula. * - * @param formula The Until path formula to check - * @returns for each state the probability that the path formula holds. + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector* checkUntil(const storm::formula::Until& formula, bool qualitative) const { // First, we need to compute the states that satisfy the sub-formulas of the until-formula. @@ -317,7 +241,7 @@ public: storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices()); // Get the "new" nondeterministic choice indices for the submatrix. - std::shared_ptr> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); + std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); // Create vector for results for maybe states. std::vector x(maybeStatesSetBitCount); @@ -328,7 +252,7 @@ public: this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, *this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, &b); // Solve the corresponding system of equations. - this->solveEquationSystem(*submatrix, x, b, *subNondeterministicChoiceIndices); + this->solveEquationSystem(*submatrix, x, b, subNondeterministicChoiceIndices); // Set values of resulting vector according to result. storm::utility::setVectorValues(result, maybeStates, x); @@ -345,11 +269,15 @@ public: } /*! - * The check method for a path formula with an Instantaneous Reward operator node as root in its - * formula tree + * Checks the given formula that is an instantaneous reward formula. * - * @param formula The Instantaneous Reward formula to check - * @returns for each state the reward that the instantaneous reward yields + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bound 0. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bound 0. + * @returns The reward values for the given formula for every state of the model associated with this model + * checker. If the qualitative flag is set, exact values might not be computed. */ virtual std::vector* checkInstantaneousReward(const storm::formula::InstantaneousReward& formula, bool qualitative) const { // Only compute the result if the model has a state-based reward model. @@ -368,11 +296,15 @@ public: } /*! - * The check method for a path formula with a Cumulative Reward operator node as root in its - * formula tree + * Check the given formula that is a cumulative reward formula. * - * @param formula The Cumulative Reward formula to check - * @returns for each state the reward that the cumulative reward yields + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bound 0. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bound 0. + * @returns The reward values for the given formula for every state of the model associated with this model + * checker. If the qualitative flag is set, exact values might not be computed. */ virtual std::vector* checkCumulativeReward(const storm::formula::CumulativeReward& formula, bool qualitative) const { // Only compute the result if the model has at least one reward model. @@ -392,7 +324,13 @@ public: totalRewardVector = new std::vector(*this->getModel().getStateRewardVector()); } - std::vector* result = new std::vector(*this->getModel().getStateRewardVector()); + // Initialize result to either the state rewards of the model or the null vector. + std::vector* result = nullptr; + if (this->getModel().hasStateRewards()) { + result = new std::vector(*this->getModel().getStateRewardVector()); + } else { + result = new std::vector(this->getModel().getNumberOfStates()); + } this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, totalRewardVector, formula.getBound()); @@ -402,11 +340,15 @@ public: } /*! - * The check method for a path formula with a Reachability Reward operator node as root in its - * formula tree + * Checks the given formula that is a reachability reward formula. * - * @param formula The Reachbility Reward formula to check - * @returns for each state the reward that the reachability reward yields + * @param formula The formula to check. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bound 0. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bound 0. + * @returns The reward values for the given formula for every state of the model associated with this model + * checker. If the qualitative flag is set, exact values might not be computed. */ virtual std::vector* checkReachabilityReward(const storm::formula::ReachabilityReward& formula, bool qualitative) const { // Only compute the result if the model has at least one reward model. @@ -444,7 +386,7 @@ public: storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices()); // Get the "new" nondeterministic choice indices for the submatrix. - std::shared_ptr> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); + std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); // Create vector for results for maybe states. std::vector x(maybeStatesSetBitCount); @@ -480,7 +422,7 @@ public: } // Solve the corresponding system of equations. - this->solveEquationSystem(*submatrix, x, b, *subNondeterministicChoiceIndices); + this->solveEquationSystem(*submatrix, x, b, subNondeterministicChoiceIndices); // Set values of resulting vector according to result. storm::utility::setVectorValues(result, maybeStates, x); @@ -497,33 +439,62 @@ public: } protected: + /*! + * A stack used for storing whether we are currently computing min or max probabilities or rewards, respectively. + * The topmost element is true if and only if we are currently computing minimum probabilities or rewards. + */ mutable std::stack minimumOperatorStack; private: - virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& matrix, std::vector& vector, std::vector* summand = nullptr, uint_fast64_t repetitions = 1) const { + /*! + * Performs (repeated) matrix-vector multiplication with the given parameters, i.e. computes x[i+1] = A*x[i] + b + * until x[n], where x[0] = x. + * + * @param A The matrix that is to be multiplied against the vector. + * @param x The initial vector that is to be multiplied against the matrix. This is also the output parameter, + * i.e. after the method returns, this vector will contain the computed values. + * @param b If not null, this vector is being added to the result after each matrix-vector multiplication. + * @param n Specifies the number of iterations the matrix-vector multiplication is performed. + * @returns The result of the repeated matrix-vector multiplication as the content of the parameter vector. + */ + virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& A, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1) const { // Get the starting row indices for the non-deterministic choices to reduce the resulting // vector properly. - std::shared_ptr> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); + std::vector const& nondeterministicChoiceIndices = *this->getModel().getNondeterministicChoiceIndices(); // Create vector for result of multiplication, which is reduced to the result vector after // each multiplication. - std::vector multiplyResult(matrix.getRowCount()); + std::vector multiplyResult(A.getRowCount()); // Now perform matrix-vector multiplication as long as we meet the bound of the formula. - for (uint_fast64_t i = 0; i < repetitions; ++i) { - matrix.multiplyWithVector(vector, multiplyResult); - if (summand != nullptr) { - gmm::add(*summand, multiplyResult); + for (uint_fast64_t i = 0; i < n; ++i) { + A.multiplyWithVector(x, multiplyResult); + + // Add b if it is non-null. + if (b != nullptr) { + storm::utility::addVectors(multiplyResult, *b); } + + // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost + // element of the min/max operator stack. if (this->minimumOperatorStack.top()) { - storm::utility::reduceVectorMin(multiplyResult, &vector, *nondeterministicChoiceIndices); + storm::utility::reduceVectorMin(multiplyResult, &x, nondeterministicChoiceIndices); } else { - storm::utility::reduceVectorMax(multiplyResult, &vector, *nondeterministicChoiceIndices); + storm::utility::reduceVectorMax(multiplyResult, &x, nondeterministicChoiceIndices); } } } - virtual void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) const { + /*! + * Solves the equation system A*x = b given by the parameters. + * + * @param A The matrix specifying the coefficients of the linear equations. + * @param x The solution vector x. The initial values of x represent a guess of the real values to the solver, but + * may be ignored. + * @param b The right-hand side of the equation system. + * @returns The solution vector x of the system of linear equations as the content of the parameter x. + */ + virtual void solveEquationSystem(storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) const { // Get the settings object to customize solving. storm::settings::Settings* s = storm::settings::instance(); @@ -533,7 +504,7 @@ private: bool relative = s->get("relative"); // Set up the environment for the power method. - std::vector multiplyResult(matrix.getRowCount()); + std::vector multiplyResult(A.getRowCount()); std::vector* currentX = &x; std::vector* newX = new std::vector(x.size()); std::vector* swap = nullptr; @@ -544,12 +515,11 @@ private: // user-specified maximum number of iterations. while (!converged && iterations < maxIterations) { // Compute x' = A*x + b. - matrix.multiplyWithVector(*currentX, multiplyResult); - // matrix.multiplyAddAndReduceInPlace(nondeterministicChoiceIndices, *currentX, b, this->minimumOperatorStack.top()); + A.multiplyWithVector(*currentX, multiplyResult); + storm::utility::addVectors(multiplyResult, b); - gmm::add(b, multiplyResult); - - // Reduce the vector x' by applying min/max for all non-deterministic choices. + // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost + // element of the min/max operator stack. if (this->minimumOperatorStack.top()) { storm::utility::reduceVectorMin(multiplyResult, newX, nondeterministicChoiceIndices); } else { @@ -559,17 +529,15 @@ private: // Determine whether the method converged. converged = storm::utility::equalModuloPrecision(*currentX, *newX, precision, relative); - // Update environment variables. swap = currentX; currentX = newX; newX = swap; ++iterations; - - // *newX = *currentX, - } + // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result + // is currently stored in currentX, but x is the output vector. if (iterations % 2 == 1) { std::swap(x, *currentX); delete currentX; @@ -585,25 +553,41 @@ private: } } - std::shared_ptr> computeNondeterministicChoiceIndicesForConstraint(storm::storage::BitVector constraint) const { - std::shared_ptr> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); - std::shared_ptr> subNondeterministicChoiceIndices(new std::vector(constraint.getNumberOfSetBits() + 1)); + /*! + * Computes the nondeterministic choice indices vector resulting from reducing the full system to the states given + * by the parameter constraint. + * + * @param constraint A bit vector specifying which states are kept. + * @returns A vector of the nondeterministic choice indices of the subsystem induced by the given constraint. + */ + std::vector computeNondeterministicChoiceIndicesForConstraint(storm::storage::BitVector const& constraint) const { + // First, get a reference to the full nondeterministic choice indices. + std::vector const& nondeterministicChoiceIndices = *this->getModel().getNondeterministicChoiceIndices(); + + // Reserve the known amount of slots for the resulting vector. + std::vector subNondeterministicChoiceIndices(constraint.getNumberOfSetBits() + 1); uint_fast64_t currentRowCount = 0; uint_fast64_t currentIndexCount = 1; - (*subNondeterministicChoiceIndices)[0] = 0; + + // Set the first element as this will clearly begin at offset 0. + subNondeterministicChoiceIndices[0] = 0; + + // Loop over all states that need to be kept and copy the relative indices of the nondeterministic choices over + // to the resulting vector. for (auto index : constraint) { - (*subNondeterministicChoiceIndices)[currentIndexCount] = currentRowCount + (*nondeterministicChoiceIndices)[index + 1] - (*nondeterministicChoiceIndices)[index]; - currentRowCount += (*nondeterministicChoiceIndices)[index + 1] - (*nondeterministicChoiceIndices)[index]; + subNondeterministicChoiceIndices[currentIndexCount] = currentRowCount + nondeterministicChoiceIndices[index + 1] - nondeterministicChoiceIndices[index]; + currentRowCount += nondeterministicChoiceIndices[index + 1] - nondeterministicChoiceIndices[index]; ++currentIndexCount; } - (*subNondeterministicChoiceIndices)[constraint.getNumberOfSetBits()] = currentRowCount; + + // Put a sentinel element at the end. + subNondeterministicChoiceIndices[constraint.getNumberOfSetBits()] = currentRowCount; return subNondeterministicChoiceIndices; } }; -} //namespace modelChecker - -} //namespace storm +} // namespace modelchecker +} // namespace storm -#endif /* STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */ +#endif /* STORM_MODELCHECKER_SPARSEMDPPRCTLMODELCHECKER_H_ */ diff --git a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h index 23b1ac6fc..248749624 100644 --- a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h +++ b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h @@ -8,39 +8,42 @@ #ifndef STORM_MODELCHECKER_TOPOLOGICALVALUEITERATIONSMDPPRCTLMODELCHECKER_H_ #define STORM_MODELCHECKER_TOPOLOGICALVALUEITERATIONSMDPPRCTLMODELCHECKER_H_ -#include - -#include "src/models/Mdp.h" -#include "src/modelchecker/MdpPrctlModelChecker.h" -#include "src/utility/GraphAnalyzer.h" -#include "src/utility/Vector.h" -#include "src/utility/ConstTemplates.h" -#include "src/utility/Settings.h" -#include "src/adapters/GmmxxAdapter.h" +#include "src/modelchecker/SparseMdpPrctlModelChecker.h" #include "src/exceptions/InvalidPropertyException.h" -#include "src/storage/JacobiDecomposition.h" - -#include "gmm/gmm_matrix.h" -#include "gmm/gmm_iter_solvers.h" - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" - -extern log4cplus::Logger logger; +#include namespace storm { - -namespace modelChecker { +namespace modelchecker { /* - * A model checking engine that makes use of the gmm++ backend. + * An implementation of the SparseMdpPrctlModelChecker interface that uses topoligical value iteration for solving + * equation systems. */ template -class TopologicalValueIterationMdpPrctlModelChecker : public MdpPrctlModelChecker { +class TopologicalValueIterationMdpPrctlModelChecker : public SparseMdpPrctlModelChecker { public: - explicit TopologicalValueIterationMdpPrctlModelChecker(storm::models::Mdp& mdp) : MdpPrctlModelChecker(mdp) { } + /*! + * Constructs a SparseMdpPrctlModelChecker with the given model. + * + * @param model The MDP to be checked. + */ + explicit TopologicalValueIterationMdpPrctlModelChecker(storm::models::Mdp const& model) : SparseMdpPrctlModelChecker(model) { + // Intentionally left empty. + } + + /*! + * Copy constructs a SparseMdpPrctlModelChecker from the given model checker. In particular, this means that the newly + * constructed model checker will have the model of the given model checker as its associated model. + */ + explicit TopologicalValueIterationMdpPrctlModelChecker(storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker const& modelchecker) + : SparseMdpPrctlModelChecker(modelchecker), minimumOperatorStack() { + // Intentionally left empty. + } + /*! + * Virtual destructor. Needs to be virtual, because this class has virtual methods. + */ virtual ~TopologicalValueIterationMdpPrctlModelChecker() { } private: @@ -63,10 +66,10 @@ private: unsigned maxIterations = s->get("maxiter"); bool relative = s->get("relative"); + // Now, we need to determine the SCCs of the MDP and a topological sort. std::vector> stronglyConnectedComponents; storm::models::GraphTransitions stronglyConnectedComponentsDependencyGraph; storm::utility::GraphAnalyzer::performSccDecomposition(matrix, nondeterministicChoiceIndices, stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); - std::vector topologicalSort; storm::utility::GraphAnalyzer::getTopologicalSort(stronglyConnectedComponentsDependencyGraph, topologicalSort); @@ -80,9 +83,12 @@ private: uint_fast64_t globalIterations = 0; bool converged = true; + // Iterate over all SCCs of the MDP as specified by the topological sort. This guarantees that an SCC is only + // solved after all SCCs it depends on have been solved. for (auto sccIndexIt = topologicalSort.begin(); sccIndexIt != topologicalSort.end() && converged; ++sccIndexIt) { std::vector const& scc = stronglyConnectedComponents[*sccIndexIt]; + // For the current SCC, we need to perform value iteration until convergence. localIterations = 0; converged = false; while (!converged && localIterations < maxIterations) { @@ -98,6 +104,8 @@ private: } // Determine whether the method converged. + // TODO: It seems that the equalModuloPrecision call that compares all values should have a higher + // running time. In fact, it is faster. This has to be investigated. // converged = storm::utility::equalModuloPrecision(*currentX, *newX, scc, precision, relative); converged = storm::utility::equalModuloPrecision(*currentX, *newX, precision, relative); @@ -109,13 +117,16 @@ private: ++globalIterations; } - std::cout << "converged locally for scc of size " << scc.size() << std::endl; - + // As the "number of iterations" of the full method is the maximum of the local iterations, we need to keep + // track of the maximum. if (localIterations > currentMaxLocalIterations) { currentMaxLocalIterations = localIterations; } } + // If we performed an odd number of global iterations, we need to swap the x and currentX, because the newest + // result is currently stored in currentX, but x is the output vector. + // TODO: Check whether this is correct or should be put into the for-loop over SCCs. if (globalIterations % 2 == 1) { std::swap(x, *currentX); delete currentX; @@ -132,8 +143,7 @@ private: } }; -} //namespace modelChecker - -} //namespace storm +} // namespace modelchecker +} // namespace storm #endif /* STORM_MODELCHECKER_TOPOLOGICALVALUEITERATIONSMDPPRCTLMODELCHECKER_H_ */ diff --git a/src/storm.cpp b/src/storm.cpp index 4ae79224f..dfedb0954 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -96,7 +96,7 @@ void printFooter() { bool parseOptions(const int argc, const char* argv[]) { storm::settings::Settings* s = nullptr; try { - storm::settings::Settings::registerModule>(); + storm::settings::Settings::registerModule>(); s = storm::settings::newInstance(argc, argv, nullptr); } catch (storm::exceptions::InvalidSettingsException& e) { std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; @@ -140,7 +140,7 @@ void cleanUp() { } void testCheckingDie(storm::models::Dtmc& dtmc) { - storm::modelChecker::GmmxxDtmcPrctlModelChecker* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker(dtmc); + storm::modelchecker::GmmxxDtmcPrctlModelChecker* mc = new storm::modelchecker::GmmxxDtmcPrctlModelChecker(dtmc); storm::formula::Ap* oneFormula = new storm::formula::Ap("one"); storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(oneFormula); @@ -177,7 +177,7 @@ void testCheckingCrowds(storm::models::Dtmc& dtmc) { storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(observe0Greater1Formula); storm::formula::ProbabilisticNoBoundOperator* probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); - storm::modelChecker::GmmxxDtmcPrctlModelChecker* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker(dtmc); + storm::modelchecker::GmmxxDtmcPrctlModelChecker* mc = new storm::modelchecker::GmmxxDtmcPrctlModelChecker(dtmc); mc->check(*probFormula); delete probFormula; @@ -203,7 +203,7 @@ void testCheckingSynchronousLeader(storm::models::Dtmc& dtmc, uint_fast6 storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(electedFormula); storm::formula::ProbabilisticNoBoundOperator* probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); - storm::modelChecker::GmmxxDtmcPrctlModelChecker* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker(dtmc); + storm::modelchecker::GmmxxDtmcPrctlModelChecker* mc = new storm::modelchecker::GmmxxDtmcPrctlModelChecker(dtmc); mc->check(*probFormula); delete probFormula; @@ -229,7 +229,7 @@ void testCheckingDice(storm::models::Mdp& mdp) { storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(twoFormula); storm::formula::ProbabilisticNoBoundOperator* probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula, true); - storm::modelChecker::GmmxxMdpPrctlModelChecker* mc = new storm::modelChecker::GmmxxMdpPrctlModelChecker(mdp); + storm::modelchecker::GmmxxMdpPrctlModelChecker* mc = new storm::modelchecker::GmmxxMdpPrctlModelChecker(mdp); mc->check(*probFormula); delete probFormula; @@ -319,7 +319,7 @@ void testCheckingAsynchLeader(storm::models::Mdp& mdp) { storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(electedFormula); storm::formula::ProbabilisticNoBoundOperator* probMinFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula, true); - storm::modelChecker::GmmxxMdpPrctlModelChecker* mc = new storm::modelChecker::GmmxxMdpPrctlModelChecker(mdp); + storm::modelchecker::GmmxxMdpPrctlModelChecker* mc = new storm::modelchecker::GmmxxMdpPrctlModelChecker(mdp); mc->check(*probMinFormula); delete probMinFormula; @@ -367,7 +367,7 @@ void testCheckingConsensus(storm::models::Mdp& mdp) { storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(finishedFormula); storm::formula::ProbabilisticNoBoundOperator* probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula, true); - storm::modelChecker::GmmxxMdpPrctlModelChecker* mc = new storm::modelChecker::GmmxxMdpPrctlModelChecker(mdp); + storm::modelchecker::GmmxxMdpPrctlModelChecker* mc = new storm::modelchecker::GmmxxMdpPrctlModelChecker(mdp); mc->check(*probFormula); delete probFormula; diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index f99c3e319..b432d0b2a 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -35,7 +35,7 @@ public: * probability 1 after the invocation of the function. */ template - static void performProb01(storm::models::AbstractDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { + static void performProb01(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameters. if (statesWithProbability0 == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null."); @@ -63,7 +63,7 @@ public: * a positive probability of satisfying phi until psi. */ template - static void performProbGreater0(storm::models::AbstractDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbabilityGreater0) { + static void performProbGreater0(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbabilityGreater0) { // Check for valid parameter. if (statesWithProbabilityGreater0 == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbabilityGreater0' must not be null."); @@ -110,7 +110,7 @@ public: * have paths satisfying phi until psi. */ template - static void performProb1(storm::models::AbstractDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0, storm::storage::BitVector* statesWithProbability1) { + static void performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameter. if (statesWithProbability1 == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null."); @@ -134,7 +134,7 @@ public: * have paths satisfying phi until psi. */ template - static void performProb1(storm::models::AbstractDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { + static void performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameter. if (statesWithProbability1 == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null."); @@ -149,7 +149,7 @@ public: } template - static void performProb01Max(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { + static void performProb01Max(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameters. if (statesWithProbability0 == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null."); @@ -166,7 +166,7 @@ public: } template - static void performProb0A(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) { + static void performProb0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) { // Check for valid parameter. if (statesWithProbability0 == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null."); @@ -201,7 +201,7 @@ public: } template - static void performProb1E(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { + static void performProb1E(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameters. if (statesWithProbability1 == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null."); @@ -271,7 +271,7 @@ public: } template - static void performProb01Min(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { + static void performProb01Min(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameters. if (statesWithProbability0 == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null."); @@ -288,7 +288,7 @@ public: } template - static void performProb0E(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) { + static void performProb0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) { // Check for valid parameter. if (statesWithProbability0 == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null."); @@ -348,7 +348,7 @@ public: } template - static void performProb1A(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { + static void performProb1A(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameters. if (statesWithProbability1 == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null."); diff --git a/src/utility/Vector.h b/src/utility/Vector.h index ab1fc461a..b3748d9ea 100644 --- a/src/utility/Vector.h +++ b/src/utility/Vector.h @@ -78,6 +78,18 @@ void subtractFromConstantOneVector(std::vector* vector) { } } +template +void addVectors(std::vector& target, std::vector const& summand) { + if (target.size() != target.size()) { + LOG4CPLUS_ERROR(logger, "Lengths of vectors does not match and makes operation impossible."); + throw storm::exceptions::InvalidArgumentException() << "Length of vectors does not match and makes operation impossible."; + } + + for (uint_fast64_t i = 0; i < target.size(); ++i) { + target[i] += summand[i]; + } +} + template void addVectors(std::vector const& states, std::vector const& nondeterministicChoiceIndices, std::vector& original, std::vector const& summand) { for (auto stateIt = states.cbegin(), stateIte = states.cend(); stateIt != stateIte; ++stateIt) { diff --git a/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp b/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp index 3050b3e49..059a7f295 100644 --- a/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp @@ -17,7 +17,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) { ASSERT_EQ(dtmc->getNumberOfStates(), 13); ASSERT_EQ(dtmc->getNumberOfTransitions(), 27); - storm::modelChecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); + storm::modelchecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); storm::formula::Ap* apFormula = new storm::formula::Ap("one"); storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(apFormula); @@ -77,7 +77,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { ASSERT_EQ(dtmc->getNumberOfStates(), 8607); ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460); - storm::modelChecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); + storm::modelchecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); storm::formula::Ap* apFormula = new storm::formula::Ap("observe0Greater1"); storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(apFormula); @@ -125,7 +125,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { ASSERT_EQ(dtmc->getNumberOfStates(), 12400); ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894); - storm::modelChecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); + storm::modelchecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); storm::formula::Ap* apFormula = new storm::formula::Ap("elected"); storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(apFormula); diff --git a/test/functional/GmmxxMdpPrctModelCheckerTest.cpp b/test/functional/GmmxxMdpPrctModelCheckerTest.cpp index 1fee30acd..ab6099d62 100644 --- a/test/functional/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/functional/GmmxxMdpPrctModelCheckerTest.cpp @@ -16,7 +16,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { ASSERT_EQ(mdp->getNumberOfStates(), 169); ASSERT_EQ(mdp->getNumberOfTransitions(), 436); - storm::modelChecker::GmmxxMdpPrctlModelChecker mc(*mdp); + storm::modelchecker::GmmxxMdpPrctlModelChecker mc(*mdp); storm::formula::Ap* apFormula = new storm::formula::Ap("two"); storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(apFormula); @@ -112,7 +112,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { std::shared_ptr> stateRewardMdp = stateRewardParser.getModel>(); - storm::modelChecker::GmmxxMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp); + storm::modelchecker::GmmxxMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp); apFormula = new storm::formula::Ap("done"); reachabilityRewardFormula = new storm::formula::ReachabilityReward(apFormula); @@ -142,7 +142,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { std::shared_ptr> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel>(); - storm::modelChecker::GmmxxMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp); + storm::modelchecker::GmmxxMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp); apFormula = new storm::formula::Ap("done"); reachabilityRewardFormula = new storm::formula::ReachabilityReward(apFormula); @@ -178,7 +178,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(mdp->getNumberOfStates(), 3172); ASSERT_EQ(mdp->getNumberOfTransitions(), 7144); - storm::modelChecker::GmmxxMdpPrctlModelChecker mc(*mdp); + storm::modelchecker::GmmxxMdpPrctlModelChecker mc(*mdp); storm::formula::Ap* apFormula = new storm::formula::Ap("elected"); storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(apFormula); diff --git a/test/storm-tests.cpp b/test/storm-tests.cpp index 0fdcbb456..e5d78bb5e 100644 --- a/test/storm-tests.cpp +++ b/test/storm-tests.cpp @@ -37,7 +37,7 @@ void setUpLogging() { bool parseOptions(int const argc, char const * const argv[]) { storm::settings::Settings* s = nullptr; try { - storm::settings::Settings::registerModule>(); + storm::settings::Settings::registerModule>(); s = storm::settings::newInstance(argc, argv, nullptr, true); } catch (storm::exceptions::InvalidSettingsException& e) { std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;