Fixed a lot of issues introduced by refactoring.

Former-commit-id: c3a5177008

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.

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.

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

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"

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) {

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.

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.")
 	;
 }
 

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.

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);

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);

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);

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);
 }

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);

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);

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);

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);
 }