diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
index 50ab036c1..0f5a5c074 100644
--- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
@@ -27,7 +27,8 @@ namespace prctl {
template<class Type>
class SparseDtmcPrctlModelChecker : public AbstractModelChecker<Type> {
- /*!
+public:
+ /*!
* Constructs a SparseDtmcPrctlModelChecker with the given model.
*
* @param model The DTMC to be checked.
@@ -36,8 +37,6 @@ class SparseDtmcPrctlModelChecker : public AbstractModelChecker<Type> {
// Intentionally left empty.
}
-public:
-
/*!
* 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.
diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
index 42173d0b7..8a7d1c1aa 100644
--- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
@@ -9,11 +9,12 @@
#define STORM_MODELCHECKER_PRCTL_SPARSEMDPPRCTLMODELCHECKER_H_
#include "src/modelchecker/prctl/AbstractModelChecker.h"
-#include "src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h"
#include "src/solver/AbstractNondeterministicLinearEquationSolver.h"
+#include "src/solver/GmmxxLinearEquationSolver.h"
#include "src/models/Mdp.h"
#include "src/utility/vector.h"
#include "src/utility/graph.h"
+#include "src/utility/Settings.h"
#include <vector>
#include <stack>
@@ -614,15 +615,20 @@ namespace storm {
* @param submatrix The matrix that will be used for value iteration later.
*/
std::vector<Type> getInitialValueIterationValues(storm::storage::SparseMatrix<Type> const& submatrix, std::vector<uint_fast64_t> const& subNondeterministicChoiceIndices, std::vector<Type> const& rightHandSide) const {
- // std::vector<uint_fast64_t> scheduler(submatrix.getColumnCount());
- // std::vector<Type> result(scheduler.size(), Type(0.5));
- // std::vector<Type> b(scheduler.size());
- // storm::utility::vector::selectVectorValues(b, scheduler, subNondeterministicChoiceIndices, rightHandSide);
- // storm::storage::SparseMatrix<Type> A(submatrix.getSubmatrix(scheduler, subNondeterministicChoiceIndices));
- // A.convertToEquationSystem();
- // this->solveEquationSystem(A, result, b);
- std::vector<Type> result(submatrix.getColumnCount());
- return result;
+ storm::settings::Settings* s = storm::settings::instance();
+ if (s->get<bool>("use-heuristic-presolve")) {
+ std::vector<uint_fast64_t> scheduler(submatrix.getColumnCount());
+ std::vector<Type> result(scheduler.size(), Type(0.5));
+ std::vector<Type> b(scheduler.size());
+ storm::utility::vector::selectVectorValues(b, scheduler, subNondeterministicChoiceIndices, rightHandSide);
+ storm::storage::SparseMatrix<Type> A(submatrix.getSubmatrix(scheduler, subNondeterministicChoiceIndices));
+ A.convertToEquationSystem();
+ std::unique_ptr<storm::solver::GmmxxLinearEquationSolver<Type>> solver(new storm::solver::GmmxxLinearEquationSolver<Type>());
+ solver->solveEquationSystem(A, result, b);
+ return result;
+ } else {
+ return std::vector<Type>(submatrix.getColumnCount(), Type(0.5));
+ }
}
// An object that is used for solving linear equations and performing matrix-vector multiplication.
diff --git a/src/solver/AbstractNondeterministicLinearEquationSolver.h b/src/solver/AbstractNondeterministicLinearEquationSolver.h
index 09ee98574..4f9545e0c 100644
--- a/src/solver/AbstractNondeterministicLinearEquationSolver.h
+++ b/src/solver/AbstractNondeterministicLinearEquationSolver.h
@@ -2,6 +2,8 @@
#define STORM_SOLVER_ABSTRACTNONDETERMINISTICLINEAREQUATIONSOLVER_H_
#include "src/storage/SparseMatrix.h"
+#include "src/utility/vector.h"
+#include "src/utility/Settings.h"
#include <vector>
@@ -16,6 +18,43 @@ namespace storm {
return new AbstractNondeterministicLinearEquationSolver<Type>();
}
+ /*!
+ * 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 minimize If set, all choices are resolved such that the solution value becomes minimal and maximal otherwise.
+ * @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 nondeterministicChoiceIndices The assignment of states to their rows in the matrix.
+ * @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(bool minimize, storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<Type>* b = nullptr, uint_fast64_t n = 1) const {
+ // Create vector for result of multiplication, which is reduced to the result vector after
+ // each multiplication.
+ 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 < n; ++i) {
+ A.multiplyWithVector(x, multiplyResult);
+
+ // Add b if it is non-null.
+ if (b != nullptr) {
+ storm::utility::vector::addVectorsInPlace(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 (minimize) {
+ storm::utility::vector::reduceVectorMin(multiplyResult, x, nondeterministicChoiceIndices);
+ } else {
+ storm::utility::vector::reduceVectorMax(multiplyResult, x, nondeterministicChoiceIndices);
+ }
+ }
+ }
+
/*!
* Solves the equation system A*x = b given by the parameters.
*
@@ -91,82 +130,6 @@ namespace storm {
}
}
- /*!
- * 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 minimize If set, all choices are resolved such that the solution value becomes minimal and maximal otherwise.
- * @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 nondeterministicChoiceIndices The assignment of states to their rows in the matrix.
- * @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(bool minimize, storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<Type>* b = nullptr, uint_fast64_t n = 1) const {
- // Create vector for result of multiplication, which is reduced to the result vector after
- // each multiplication.
- 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 < n; ++i) {
- A.multiplyWithVector(x, multiplyResult);
-
- // Add b if it is non-null.
- if (b != nullptr) {
- storm::utility::vector::addVectorsInPlace(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 (minimize) {
- storm::utility::vector::reduceVectorMin(multiplyResult, x, nondeterministicChoiceIndices);
- } else {
- storm::utility::vector::reduceVectorMax(multiplyResult, x, nondeterministicChoiceIndices);
- }
- }
- }
-
- /*!
- * Returns the name of this solver.
- *
- * @returns The name of this solver.
- */
- static std::string getName() {
- return "native";
- }
-
- /*!
- * Registers all options associated with the gmm++ matrix library.
- */
- static void putOptions(boost::program_options::options_description* desc) {
- desc->add_options()("lemethod", boost::program_options::value<std::string>()->default_value("bicgstab")->notifier(&validateLeMethod), "Sets the method used for linear equation solving. Must be in {bicgstab, qmr, jacobi}.");
- desc->add_options()("maxiter", boost::program_options::value<unsigned>()->default_value(10000), "Sets the maximal number of iterations for iterative equation solving.");
- desc->add_options()("precision", boost::program_options::value<double>()->default_value(1e-6), "Sets the precision for iterative equation solving.");
- desc->add_options()("precond", boost::program_options::value<std::string>()->default_value("ilu")->notifier(&validatePreconditioner), "Sets the preconditioning technique for linear equation solving. Must be in {ilu, diagonal, ildlt, none}.");
- desc->add_options()("relative", boost::program_options::value<bool>()->default_value(true), "Sets whether the relative or absolute error is considered for detecting convergence.");
- }
-
- /*!
- * Validates whether the given lemethod matches one of the available ones.
- * Throws an exception of type InvalidSettings in case the selected method is illegal.
- */
- static void validateLeMethod(const std::string& lemethod) {
- if ((lemethod != "bicgstab") && (lemethod != "qmr") && (lemethod != "jacobi")) {
- throw exceptions::InvalidSettingsException() << "Argument " << lemethod << " for option 'lemethod' is invalid.";
- }
- }
-
- /*!
- * Validates whether the given preconditioner matches one of the available ones.
- * Throws an exception of type InvalidSettings in case the selected preconditioner is illegal.
- */
- static void validatePreconditioner(const std::string& preconditioner) {
- if ((preconditioner != "ilu") && (preconditioner != "diagonal") && (preconditioner != "ildlt") && (preconditioner != "none")) {
- throw exceptions::InvalidSettingsException() << "Argument " << preconditioner << " for option 'precond' is invalid.";
- }
- }
};
} // namespace solver
diff --git a/src/solver/GmmxxLinearEquationSolver.h b/src/solver/GmmxxLinearEquationSolver.h
index 0c1570722..66db7df94 100644
--- a/src/solver/GmmxxLinearEquationSolver.h
+++ b/src/solver/GmmxxLinearEquationSolver.h
@@ -5,6 +5,7 @@
#include "src/adapters/GmmxxAdapter.h"
#include "src/utility/ConstTemplates.h"
#include "src/utility/Settings.h"
+#include "src/utility/vector.h"
#include "gmm/gmm_matrix.h"
#include "gmm/gmm_iter_solvers.h"
diff --git a/src/solver/GmmxxNondeterministicLinearEquationSolver.h b/src/solver/GmmxxNondeterministicLinearEquationSolver.h
index e2cf5afb4..d6c34e327 100644
--- a/src/solver/GmmxxNondeterministicLinearEquationSolver.h
+++ b/src/solver/GmmxxNondeterministicLinearEquationSolver.h
@@ -16,11 +16,11 @@ namespace storm {
class GmmxxNondeterministicLinearEquationSolver : public AbstractNondeterministicLinearEquationSolver<Type> {
public:
- virtual AbstractLinearEquationSolver<Type>* clone() const {
+ virtual AbstractNondeterministicLinearEquationSolver<Type>* clone() const {
return new GmmxxNondeterministicLinearEquationSolver<Type>();
}
- virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<Type>* b = nullptr, uint_fast64_t n = 1) const {
+ virtual void performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<Type>* b = nullptr, uint_fast64_t n = 1) const override {
// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(A);
@@ -36,7 +36,7 @@ namespace storm {
gmm::add(*b, multiplyResult);
}
- if (this->minimumOperatorStack.top()) {
+ if (minimize) {
storm::utility::vector::reduceVectorMin(multiplyResult, x, nondeterministicChoiceIndices);
} else {
storm::utility::vector::reduceVectorMax(multiplyResult, x, nondeterministicChoiceIndices);
@@ -47,7 +47,7 @@ namespace storm {
delete gmmxxMatrix;
}
- void solveEquationSystem(bool minimize, storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<uint_fast64_t>* takenChoices = nullptr) const override {
+ virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) const override {
// Get the settings object to customize solving.
storm::settings::Settings* s = storm::settings::instance();
@@ -91,11 +91,6 @@ namespace storm {
++iterations;
}
- // If we were requested to record the taken choices, we have to construct the vector now.
- if (takenChoices != nullptr) {
- this->computeTakenChoices(minimize, multiplyResult, *takenChoices, nondeterministicChoiceIndices);
- }
-
// 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) {
diff --git a/src/storm.cpp b/src/storm.cpp
index f45f274fc..8fec52c6c 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -22,10 +22,12 @@
#include "src/models/Dtmc.h"
#include "src/storage/SparseMatrix.h"
#include "src/models/AtomicPropositionsLabeling.h"
-#include "src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h"
+#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+#include "src/solver/GmmxxLinearEquationSolver.h"
+#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
#include "src/parser/AutoParser.h"
#include "src/parser/PrctlParser.h"
-//#include "src/solver/GraphAnalyzer.h"
#include "src/utility/Settings.h"
#include "src/utility/ErrorHandling.h"
#include "src/formula/Prctl.h"
@@ -199,7 +201,7 @@ storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecke
// Create the appropriate model checker.
storm::settings::Settings* s = storm::settings::instance();
if (s->getString("matrixlib") == "gmm++") {
- return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double>(dtmc, new storm::solver::AbstractLinearEquationSolver<double>());
+ return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double>(dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
}
// The control flow should never reach this point, as there is a default setting for matrixlib.
@@ -218,9 +220,9 @@ storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecke
// Create the appropriate model checker.
storm::settings::Settings* s = storm::settings::instance();
if (s->getString("matrixlib") == "gmm++") {
- return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double>(mdp, new storm::solver::GmmxxNondeterministicEquationSolver<double>());
+ return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double>(mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
} else if (s->getString("matrixlib") == "native") {
- return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double>(mdp, new storm::solver::AbstractNondeterministicEquationSolver<double>());
+ return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double>(mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
}
// The control flow should never reach this point, as there is a default setting for matrixlib.
diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp
index 55e802811..6fbfa07de 100644
--- a/src/utility/Settings.cpp
+++ b/src/utility/Settings.cpp
@@ -124,6 +124,26 @@ void checkExplicit(const std::vector<std::string>& filenames) {
}
}
+ /*!
+ * Validates whether the given lemethod matches one of the available ones.
+ * Throws an exception of type InvalidSettings in case the selected method is illegal.
+ */
+ static void validateLeMethod(const std::string& lemethod) {
+ if ((lemethod != "bicgstab") && (lemethod != "qmr") && (lemethod != "jacobi")) {
+ throw exceptions::InvalidSettingsException() << "Argument " << lemethod << " for option 'lemethod' is invalid.";
+ }
+ }
+
+ /*!
+ * Validates whether the given preconditioner matches one of the available ones.
+ * Throws an exception of type InvalidSettings in case the selected preconditioner is illegal.
+ */
+ static void validatePreconditioner(const std::string& preconditioner) {
+ if ((preconditioner != "ilu") && (preconditioner != "diagonal") && (preconditioner != "ildlt") && (preconditioner != "none")) {
+ throw exceptions::InvalidSettingsException() << "Argument " << preconditioner << " for option 'precond' is invalid.";
+ }
+ }
+
/*!
* Initially fill options_description objects.
*/
@@ -145,6 +165,13 @@ void Settings::initDescriptions() {
("transrew", bpo::value<std::string>()->default_value(""), "name of transition reward file")
("staterew", bpo::value<std::string>()->default_value(""), "name of state reward file")
("fix-deadlocks", "insert self-loops for states without outgoing transitions")
+ ("lemethod", boost::program_options::value<std::string>()->default_value("bicgstab")->notifier(&storm::settings::validateLeMethod), "Sets the method used for linear equation solving. Must be in {bicgstab, qmr, jacobi}.")
+ ("maxiter", boost::program_options::value<unsigned>()->default_value(10000), "Sets the maximal number of iterations for iterative equation solving.")
+ ("precision", boost::program_options::value<double>()->default_value(1e-6), "Sets the precision for iterative equation solving.")
+ ("precond", boost::program_options::value<std::string>()->default_value("ilu")->notifier(&validatePreconditioner), "Sets the preconditioning technique for linear equation solving. Must be in {ilu, diagonal, ildlt, none}.")
+ ("relative", boost::program_options::value<bool>()->default_value(true), "Sets whether the relative or absolute error is considered for detecting convergence.")
+ ("use-heuristic-presolve", boost::program_options::value<bool>()->default_value(false), "Sets whether heuristic methods should be applied to get better initial values for value iteration.")
+ ("matrixlib", boost::program_options::value<std::string>()->default_value("gmm++"), "Sets which matrix library is to be used for numerical solving.")
;
}
diff --git a/src/utility/Settings.h b/src/utility/Settings.h
index b3af50138..4a57265b1 100644
--- a/src/utility/Settings.h
+++ b/src/utility/Settings.h
@@ -125,7 +125,7 @@ namespace settings {
* @endcode
*/
template <typename T>
- static void registerSolver() {
+ static void registerOptions() {
// Get trigger values.
std::string const& name = T::getName();
// Build description name.
@@ -135,7 +135,7 @@ namespace settings {
// Put options into description.
T::putOptions(desc.get());
// Store module.
- Settings::modules[name] = desc;
+ // Settings::modules[name] = desc;
}
friend std::ostream& help(std::ostream& os);
@@ -185,7 +185,7 @@ namespace settings {
/*!
* @brief Contains option descriptions for all modules.
*/
- static std::map<std::string, std::shared_ptr<bpo::options_description>> modules;
+ static std::map< std::pair<std::string, std::string>, std::shared_ptr<bpo::options_description>> modules;
/*!
* @brief option mapping.
diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
index 604bf1289..52606b71f 100644
--- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
@@ -1,8 +1,9 @@
#include "gtest/gtest.h"
#include "storm-config.h"
+#include "src/solver/GmmxxLinearEquationSolver.h"
+#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "src/utility/Settings.h"
-#include "src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h"
#include "src/parser/AutoParser.h"
TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
@@ -17,7 +18,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
ASSERT_EQ(dtmc->getNumberOfStates(), 13u);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 27u);
- storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("one");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -84,7 +85,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(dtmc->getNumberOfStates(), 8607u);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460u);
- storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("observe0Greater1");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -138,7 +139,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(dtmc->getNumberOfStates(), 12400u);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894u);
- storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
index 4578ae369..829c516ea 100644
--- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
@@ -1,8 +1,9 @@
#include "gtest/gtest.h"
#include "storm-config.h"
+#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
#include "src/utility/Settings.h"
-#include "src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h"
#include "src/parser/AutoParser.h"
TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
@@ -16,7 +17,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
ASSERT_EQ(mdp->getNumberOfStates(), 169u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436u);
- storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
+ storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -114,7 +115,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = stateRewardParser.getModel<storm::models::Mdp<double>>();
- storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp);
+ storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -144,8 +145,8 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel<storm::models::Mdp<double>>();
- storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
-
+ storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
+
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
@@ -180,7 +181,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(mdp->getNumberOfStates(), 3172u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144u);
- storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
+ storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
index 5944f02e3..0c63bf741 100644
--- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
@@ -16,7 +16,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
ASSERT_EQ(mdp->getNumberOfStates(), 169u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436u);
- storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp);
+ storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -113,8 +113,8 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = stateRewardParser.getModel<storm::models::Mdp<double>>();
- storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp);
-
+ storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
+
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
@@ -143,7 +143,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel<storm::models::Mdp<double>>();
- storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
+ storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -179,7 +179,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(mdp->getNumberOfStates(), 3172u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144u);
- storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp);
+ storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
diff --git a/test/functional/storm-functional-tests.cpp b/test/functional/storm-functional-tests.cpp
index 433f84ea7..c826b04e9 100644
--- a/test/functional/storm-functional-tests.cpp
+++ b/test/functional/storm-functional-tests.cpp
@@ -7,7 +7,6 @@
#include "log4cplus/fileappender.h"
#include "src/utility/Settings.h"
-#include "src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h"
log4cplus::Logger logger;
@@ -34,7 +33,6 @@ void setUpLogging() {
* Creates an empty settings object as the standard instance of the Settings class.
*/
void createEmptyOptions() {
- storm::settings::Settings::registerModule<storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker<double>>();
const char* newArgv[] = {"storm-performance-tests"};
storm::settings::Settings* s = storm::settings::newInstance(1, newArgv, nullptr, true);
}
diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
index e13458016..a7229b594 100644
--- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
+++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
@@ -1,7 +1,8 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/utility/Settings.h"
-#include "src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h"
+#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "src/solver/GmmxxLinearEquationSolver.h"
#include "src/parser/AutoParser.h"
TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
@@ -16,7 +17,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(dtmc->getNumberOfStates(), 2036647u);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8973900u);
- storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("observe0Greater1");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -77,7 +78,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(dtmc->getNumberOfStates(), 1312334u);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 2886810u);
- storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
diff --git a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp
index b8cdb104b..a3d016f6c 100644
--- a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp
+++ b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp
@@ -2,7 +2,8 @@
#include "storm-config.h"
#include "src/utility/Settings.h"
-#include "src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h"
+#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
#include "src/parser/AutoParser.h"
TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
@@ -16,7 +17,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(mdp->getNumberOfStates(), 2095783u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385u);
- storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
+ storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -120,7 +121,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(mdp->getNumberOfStates(), 63616u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472u);
- storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
+ storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
diff --git a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
index 4f2598d3c..315546b5c 100644
--- a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
+++ b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
@@ -3,6 +3,7 @@
#include "src/utility/Settings.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+#include "src/solver/AbstractNondeterministicLinearEquationSolver.h"
#include "src/parser/AutoParser.h"
TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
@@ -16,7 +17,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(mdp->getNumberOfStates(), 2095783u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385u);
- storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp);
+ storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -119,7 +120,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(mdp->getNumberOfStates(), 63616u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472u);
- storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp);
+ storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
diff --git a/test/performance/storm-performance-tests.cpp b/test/performance/storm-performance-tests.cpp
index a17252099..0f22c1dc2 100644
--- a/test/performance/storm-performance-tests.cpp
+++ b/test/performance/storm-performance-tests.cpp
@@ -7,7 +7,6 @@
#include "log4cplus/fileappender.h"
#include "src/utility/Settings.h"
-#include "src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h"
log4cplus::Logger logger;
@@ -34,7 +33,6 @@ void setUpLogging() {
* Creates an empty settings object as the standard instance of the Settings class.
*/
void createEmptyOptions() {
- storm::settings::Settings::registerModule<storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker<double>>();
const char* newArgv[] = {"storm-performance-tests"};
storm::settings::Settings* s = storm::settings::newInstance(1, newArgv, nullptr, true);
}