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<T>* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const = 0;
+ virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& 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<T>& modelChecker) const = 0; // {
+ virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& 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<T>& modelChecker) const {
+ virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IAndModelChecker>()->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<T>& modelChecker) const {
+ virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IApModelChecker>()->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<T>* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+ virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IBoundedEventuallyModelChecker>()->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<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+ virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IBoundedNaryUntilModelChecker>()->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<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+ virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IBoundedUntilModelChecker>()->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<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+ virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<ICumulativeRewardModelChecker>()->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<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+ virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IEventuallyModelChecker>()->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<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+ virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IGloballyModelChecker>()->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<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+ virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IInstantaneousRewardModelChecker>()->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<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+ virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<INextModelChecker>()->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<T>* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<INoBoundOperatorModelChecker>()->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<T>& modelChecker) const {
+ virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<INotModelChecker>()->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<T>& modelChecker) const {
+ virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IOrModelChecker>()->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<T>& modelChecker) const {
+ virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IProbabilisticBoundOperatorModelChecker>()->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<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+ virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IReachabilityRewardModelChecker>()->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<T>& modelChecker) const {
+ virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IRewardBoundOperatorModelChecker>()->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<T>& modelChecker) const {
+ virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IStateBoundOperatorModelChecker>()->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<T>& modelChecker) const {
+ virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<ISteadyStateOperatorModelChecker>()->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<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+ virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IUntilModelChecker>()->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 Type> 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<Type> const& modelChecker) : model(modelChecker.model) {
+ explicit AbstractModelChecker(AbstractModelChecker<Type> 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 Type>
-class EigenDtmcPrctlModelChecker : public DtmcPrctlModelChecker<Type> {
+class EigenDtmcPrctlModelChecker : public SparseDtmcPrctlModelChecker<Type> {
typedef Eigen::Matrix<Type, -1, 1, 0, -1, 1> VectorType;
typedef Eigen::Map<VectorType> MapType;
public:
- explicit EigenDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc) : DtmcPrctlModelChecker<Type>(dtmc) {
+ explicit EigenDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc) : SparseDtmcPrctlModelChecker<Type>(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 Type>
class AbstractModelChecker;
-template <class Type>
-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 <cmath>
-
-#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 <cmath>
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 Type>
-class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker<Type> {
+class GmmxxDtmcPrctlModelChecker : public SparseDtmcPrctlModelChecker<Type> {
public:
- explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc) : DtmcPrctlModelChecker<Type>(dtmc) {
+ /*!
+ * Constructs a GmmxxDtmcPrctlModelChecker with the given model.
+ *
+ * @param model The DTMC to be checked.
+ */
+ explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc) : SparseDtmcPrctlModelChecker<Type>(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<Type> const& modelchecker) : SparseDtmcPrctlModelChecker<Type>(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<std::string, std::string> getOptionTrigger() {
return std::pair<std::string, std::string>("matrixlib", "gmm++");
@@ -96,28 +103,33 @@ public:
private:
- virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& vector, std::vector<Type>* summand, uint_fast64_t repetitions = 1) const {
- // Transform the transition probability matrix to the gmm++ format to use its arithmetic.
- gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(matrix);
+ virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type>* b, uint_fast64_t n = 1) const {
+ // Transform the transition probability A to the gmm++ format to use its arithmetic.
+ gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(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<Type>* swap = nullptr;
- std::vector<Type>* currentVector = &vector;
+ std::vector<Type>* currentVector = &x;
std::vector<Type>* tmpVector = new std::vector<Type>(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<Type> const& matrix, std::vector<Type>& vector, std::vector<Type> const& b) const {
+ virtual void solveEquationSystem(storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type> 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<double>("precision"), 0, s->get<unsigned>("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<Type>* A = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(matrix);
+ gmm::csr_matrix<Type>* gmmA = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(A);
if (precond == "ilu") {
- gmm::bicgstab(*A, vector, b, gmm::ilu_precond<gmm::csr_matrix<Type>>(*A), iter);
+ gmm::bicgstab(*gmmA, x, b, gmm::ilu_precond<gmm::csr_matrix<Type>>(*gmmA), iter);
} else if (precond == "diagonal") {
- gmm::bicgstab(*A, vector, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(*A), iter);
+ gmm::bicgstab(*gmmA, x, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(*gmmA), iter);
} else if (precond == "ildlt") {
- gmm::bicgstab(*A, vector, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(*A), iter);
+ gmm::bicgstab(*gmmA, x, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(*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<Type>* A = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(matrix);
+ gmm::csr_matrix<Type>* gmmA = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(A);
if (precond == "ilu") {
- gmm::qmr(*A, vector, b, gmm::ilu_precond<gmm::csr_matrix<Type>>(*A), iter);
+ gmm::qmr(*gmmA, x, b, gmm::ilu_precond<gmm::csr_matrix<Type>>(*gmmA), iter);
} else if (precond == "diagonal") {
- gmm::qmr(*A, vector, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(*A), iter);
+ gmm::qmr(*gmmA, x, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(*gmmA), iter);
} else if (precond == "ildlt") {
- gmm::qmr(*A, vector, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(*A), iter);
+ gmm::qmr(*gmmA, x, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(*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<unsigned>("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<Type> const& matrix, std::vector<Type>& x, std::vector<Type> const& b) const {
+ uint_fast64_t solveLinearEquationSystemWithJacobi(storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b) const {
// Get the settings object to customize linear solving.
storm::settings::Settings* s = storm::settings::instance();
double precision = s->get<double>("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<Type>* jacobiDecomposition = matrix.getJacobiDecomposition();
+ uint_fast64_t maxIterations = s->get<unsigned>("maxiter");
+ bool relative = s->get<bool>("relative");
- // Convert the Input Matrix to GMM Format so we can calculate the Residuum
- gmm::csr_matrix<Type>* A = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(matrix);
+ // Get a Jacobi decomposition of the matrix A.
+ storm::storage::JacobiDecomposition<Type>* jacobiDecomposition = A.getJacobiDecomposition();
- // Convert the Diagonal matrix to GMM format
+ // Convert the (inverted) diagonal matrix to gmm++'s format.
gmm::csr_matrix<Type>* gmmxxDiagonalInverted = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(jacobiDecomposition->getJacobiDInvReference());
- // Convert the LU Matrix to GMM format
+ // Convert the LU matrix to gmm++'s format.
gmm::csr_matrix<Type>* gmmxxLU = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(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<Type>* xNext = new std::vector<Type>(x.size());
const std::vector<Type>* xCopy = xNext;
std::vector<Type>* xCurrent = &x;
- // Target vector for precision calculation
+ // Target vector for precision calculation.
std::vector<Type>* residuum = new std::vector<Type>(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<Type> *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 <cmath>
-
-#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 <cmath>
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 Type>
-class GmmxxMdpPrctlModelChecker : public MdpPrctlModelChecker<Type> {
+class GmmxxMdpPrctlModelChecker : public SparseMdpPrctlModelChecker<Type> {
public:
- explicit GmmxxMdpPrctlModelChecker(storm::models::Mdp<Type>& mdp) : MdpPrctlModelChecker<Type>(mdp) { }
+ /*!
+ * Constructs a GmmxxMdpPrctlModelChecker with the given model.
+ *
+ * @param model The MDP to be checked.
+ */
+ explicit GmmxxMdpPrctlModelChecker(storm::models::Mdp<Type> const& model) : SparseMdpPrctlModelChecker<Type>(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<Type> const& modelchecker) : SparseMdpPrctlModelChecker<Type>(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<Type> const& matrix, std::vector<Type>& vector, std::vector<Type>* summand = nullptr, uint_fast64_t repetitions = 1) const {
+
+ virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type>* 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<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
+ std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = *this->getModel().getNondeterministicChoiceIndices();
// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
- gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(matrix);
+ gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(A);
// Create vector for result of multiplication, which is reduced to the result vector after
// each multiplication.
- std::vector<Type> multiplyResult(matrix.getRowCount());
+ std::vector<Type> 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<Type> const& matrix, std::vector<Type>& x, std::vector<Type> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) const {
+ void solveEquationSystem(storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b, std::vector<uint_fast64_t> 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<bool>("relative");
// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
- gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(matrix);
+ gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(A);
// Set up the environment for the power method.
- std::vector<Type> multiplyResult(matrix.getRowCount());
+ std::vector<Type> multiplyResult(A.getRowCount());
std::vector<Type>* currentX = &x;
std::vector<Type>* newX = new std::vector<Type>(x.size());
std::vector<Type>* 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 <vector>
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<Type> const& modelChecker) : AbstractModelChecker<Type>(modelChecker) {
+ explicit SparseDtmcPrctlModelChecker(storm::modelchecker::SparseDtmcPrctlModelChecker<Type> const& modelChecker) : AbstractModelChecker<Type>(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<Type> const& matrix, std::vector<Type>& vector, std::vector<Type>* summand = nullptr, uint_fast64_t repetitions = 1) const = 0;
-
+ virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type>* 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<Type> const& A, std::vector<Type>& x, std::vector<Type> 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 <vector>
#include <stack>
-#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 Type>
-class MdpPrctlModelChecker :
- public AbstractModelChecker<Type> {
+class SparseMdpPrctlModelChecker : public AbstractModelChecker<Type> {
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<Type>& model)
- : AbstractModelChecker<Type>(model), minimumOperatorStack() {
+ explicit SparseMdpPrctlModelChecker(storm::models::Mdp<Type> const& model) : AbstractModelChecker<Type>(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<Type>* modelChecker)
- : AbstractModelChecker<Type>(modelChecker), minimumOperatorStack() {
-
+ explicit SparseMdpPrctlModelChecker(storm::modelchecker::SparseMdpPrctlModelChecker<Type> const& modelchecker)
+ : AbstractModelChecker<Type>(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<Type>& getModel() const {
+ storm::models::Mdp<Type> const& getModel() const {
return AbstractModelChecker<Type>::template getModel<storm::models::Mdp<Type>>();
}
/*!
- * Sets the DTMC model which is checked
- * @param model
- */
- void setModel(storm::models::Mdp<Type>& model) {
- AbstractModelChecker<Type>::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<Type>& 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<Type>& 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<Type>* 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<Type>& 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<Type>* checkNoBoundOperator(const storm::formula::NoBoundOperator<Type>& 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<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& 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<Type>* checkNext(const storm::formula::Next<Type>& 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<Type>* checkBoundedEventually(const storm::formula::BoundedEventually<Type>& 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<Type>* checkEventually(const storm::formula::Eventually<Type>& 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<Type>* checkGlobally(const storm::formula::Globally<Type>& 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<Type>* checkUntil(const storm::formula::Until<Type>& 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<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
// Get the "new" nondeterministic choice indices for the submatrix.
- std::shared_ptr<std::vector<uint_fast64_t>> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
+ std::vector<uint_fast64_t> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
// Create vector for results for maybe states.
std::vector<Type> 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<Type>(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<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& 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<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& 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<Type>(*this->getModel().getStateRewardVector());
}
- std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
+ // Initialize result to either the state rewards of the model or the null vector.
+ std::vector<Type>* result = nullptr;
+ if (this->getModel().hasStateRewards()) {
+ result = new std::vector<Type>(*this->getModel().getStateRewardVector());
+ } else {
+ result = new std::vector<Type>(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<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& 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<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
// Get the "new" nondeterministic choice indices for the submatrix.
- std::shared_ptr<std::vector<uint_fast64_t>> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
+ std::vector<uint_fast64_t> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
// Create vector for results for maybe states.
std::vector<Type> 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<Type>(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<bool> minimumOperatorStack;
private:
- virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& vector, std::vector<Type>* 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<Type> const& A, std::vector<Type>& x, std::vector<Type>* 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<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
+ std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = *this->getModel().getNondeterministicChoiceIndices();
// Create vector for result of multiplication, which is reduced to the result vector after
// each multiplication.
- std::vector<Type> multiplyResult(matrix.getRowCount());
+ std::vector<Type> 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<Type> const& matrix, std::vector<Type>& x, std::vector<Type> const& b, std::vector<uint_fast64_t> 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<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b, std::vector<uint_fast64_t> 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<bool>("relative");
// Set up the environment for the power method.
- std::vector<Type> multiplyResult(matrix.getRowCount());
+ std::vector<Type> multiplyResult(A.getRowCount());
std::vector<Type>* currentX = &x;
std::vector<Type>* newX = new std::vector<Type>(x.size());
std::vector<Type>* 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<std::vector<uint_fast64_t>> computeNondeterministicChoiceIndicesForConstraint(storm::storage::BitVector constraint) const {
- std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
- std::shared_ptr<std::vector<uint_fast64_t>> subNondeterministicChoiceIndices(new std::vector<uint_fast64_t>(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<uint_fast64_t> computeNondeterministicChoiceIndicesForConstraint(storm::storage::BitVector const& constraint) const {
+ // First, get a reference to the full nondeterministic choice indices.
+ std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = *this->getModel().getNondeterministicChoiceIndices();
+
+ // Reserve the known amount of slots for the resulting vector.
+ std::vector<uint_fast64_t> 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 <cmath>
-
-#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 <cmath>
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 Type>
-class TopologicalValueIterationMdpPrctlModelChecker : public MdpPrctlModelChecker<Type> {
+class TopologicalValueIterationMdpPrctlModelChecker : public SparseMdpPrctlModelChecker<Type> {
public:
- explicit TopologicalValueIterationMdpPrctlModelChecker(storm::models::Mdp<Type>& mdp) : MdpPrctlModelChecker<Type>(mdp) { }
+ /*!
+ * Constructs a SparseMdpPrctlModelChecker with the given model.
+ *
+ * @param model The MDP to be checked.
+ */
+ explicit TopologicalValueIterationMdpPrctlModelChecker(storm::models::Mdp<Type> const& model) : SparseMdpPrctlModelChecker<Type>(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<Type> const& modelchecker)
+ : SparseMdpPrctlModelChecker<Type>(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<unsigned>("maxiter");
bool relative = s->get<bool>("relative");
+ // Now, we need to determine the SCCs of the MDP and a topological sort.
std::vector<std::vector<uint_fast64_t>> stronglyConnectedComponents;
storm::models::GraphTransitions<Type> stronglyConnectedComponentsDependencyGraph;
storm::utility::GraphAnalyzer::performSccDecomposition(matrix, nondeterministicChoiceIndices, stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph);
-
std::vector<uint_fast64_t> 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<uint_fast64_t> 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::modelChecker::GmmxxDtmcPrctlModelChecker<double>>();
+ storm::settings::Settings::registerModule<storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>>();
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<double>& dtmc) {
- storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
+ storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
storm::formula::Ap<double>* oneFormula = new storm::formula::Ap<double>("one");
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(oneFormula);
@@ -177,7 +177,7 @@ void testCheckingCrowds(storm::models::Dtmc<double>& dtmc) {
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(observe0Greater1Formula);
storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
- storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
+ storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
mc->check(*probFormula);
delete probFormula;
@@ -203,7 +203,7 @@ void testCheckingSynchronousLeader(storm::models::Dtmc<double>& dtmc, uint_fast6
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(electedFormula);
storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
- storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
+ storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
mc->check(*probFormula);
delete probFormula;
@@ -229,7 +229,7 @@ void testCheckingDice(storm::models::Mdp<double>& mdp) {
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
- storm::modelChecker::GmmxxMdpPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxMdpPrctlModelChecker<double>(mdp);
+ storm::modelchecker::GmmxxMdpPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxMdpPrctlModelChecker<double>(mdp);
mc->check(*probFormula);
delete probFormula;
@@ -319,7 +319,7 @@ void testCheckingAsynchLeader(storm::models::Mdp<double>& mdp) {
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(electedFormula);
storm::formula::ProbabilisticNoBoundOperator<double>* probMinFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
- storm::modelChecker::GmmxxMdpPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxMdpPrctlModelChecker<double>(mdp);
+ storm::modelchecker::GmmxxMdpPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxMdpPrctlModelChecker<double>(mdp);
mc->check(*probMinFormula);
delete probMinFormula;
@@ -367,7 +367,7 @@ void testCheckingConsensus(storm::models::Mdp<double>& mdp) {
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(finishedFormula);
storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
- storm::modelChecker::GmmxxMdpPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxMdpPrctlModelChecker<double>(mdp);
+ storm::modelchecker::GmmxxMdpPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxMdpPrctlModelChecker<double>(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 <typename T>
- static void performProb01(storm::models::AbstractDeterministicModel<T>& 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<T> 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 <typename T>
- static void performProbGreater0(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbabilityGreater0) {
+ static void performProbGreater0(storm::models::AbstractDeterministicModel<T> 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 <typename T>
- static void performProb1(storm::models::AbstractDeterministicModel<T>& 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<T> 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 <typename T>
- static void performProb1(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
+ static void performProb1(storm::models::AbstractDeterministicModel<T> 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 <typename T>
- static void performProb01Max(storm::models::AbstractNondeterministicModel<T>& 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<T> 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 <typename T>
- static void performProb0A(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
+ static void performProb0A(storm::models::AbstractNondeterministicModel<T> 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 <typename T>
- static void performProb1E(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
+ static void performProb1E(storm::models::AbstractNondeterministicModel<T> 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 <typename T>
- static void performProb01Min(storm::models::AbstractNondeterministicModel<T>& 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<T> 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 <typename T>
- static void performProb0E(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
+ static void performProb0E(storm::models::AbstractNondeterministicModel<T> 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 <typename T>
- static void performProb1A(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
+ static void performProb1A(storm::models::AbstractNondeterministicModel<T> 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<T>* vector) {
}
}
+template<class T>
+void addVectors(std::vector<T>& target, std::vector<T> 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<class T>
void addVectors(std::vector<uint_fast64_t> const& states, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<T>& original, std::vector<T> 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<double> mc(*dtmc);
+ storm::modelchecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("one");
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
@@ -77,7 +77,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) {
ASSERT_EQ(dtmc->getNumberOfStates(), 8607);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460);
- storm::modelChecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
+ storm::modelchecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("observe0Greater1");
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
@@ -125,7 +125,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(dtmc->getNumberOfStates(), 12400);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894);
- storm::modelChecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
+ storm::modelchecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("elected");
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(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<double> mc(*mdp);
+ storm::modelchecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("two");
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
@@ -112,7 +112,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = stateRewardParser.getModel<storm::models::Mdp<double>>();
- storm::modelChecker::GmmxxMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp);
+ storm::modelchecker::GmmxxMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp);
apFormula = new storm::formula::Ap<double>("done");
reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
@@ -142,7 +142,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel<storm::models::Mdp<double>>();
- storm::modelChecker::GmmxxMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
+ storm::modelchecker::GmmxxMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
apFormula = new storm::formula::Ap<double>("done");
reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
@@ -178,7 +178,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(mdp->getNumberOfStates(), 3172);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144);
- storm::modelChecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
+ storm::modelchecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("elected");
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(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::modelChecker::GmmxxDtmcPrctlModelChecker<double>>();
+ storm::settings::Settings::registerModule<storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>>();
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;