From 7095f8e67fc1c9fa097b44300f2376755cbcc3c4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 18 Jun 2013 23:13:42 +0200 Subject: [PATCH] Fixed a lot of issues introduced by refactoring. Former-commit-id: c3a51770089a2dad9e66adf3a29894a4526282a1 --- .../prctl/SparseDtmcPrctlModelChecker.h | 5 +- .../prctl/SparseMdpPrctlModelChecker.h | 26 ++-- ...ractNondeterministicLinearEquationSolver.h | 115 ++++++------------ src/solver/GmmxxLinearEquationSolver.h | 1 + ...mmxxNondeterministicLinearEquationSolver.h | 13 +- src/storm.cpp | 12 +- src/utility/Settings.cpp | 27 ++++ src/utility/Settings.h | 6 +- .../GmmxxDtmcPrctlModelCheckerTest.cpp | 9 +- .../GmmxxMdpPrctlModelCheckerTest.cpp | 13 +- .../SparseMdpPrctlModelCheckerTest.cpp | 10 +- test/functional/storm-functional-tests.cpp | 2 - .../GmmxxDtmcPrctModelCheckerTest.cpp | 7 +- .../GmmxxMdpPrctModelCheckerTest.cpp | 7 +- .../SparseMdpPrctlModelCheckerTest.cpp | 5 +- test/performance/storm-performance-tests.cpp | 2 - 16 files changed, 127 insertions(+), 133 deletions(-) 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 SparseDtmcPrctlModelChecker : public AbstractModelChecker { - /*! +public: + /*! * Constructs a SparseDtmcPrctlModelChecker with the given model. * * @param model The DTMC to be checked. @@ -36,8 +37,6 @@ class SparseDtmcPrctlModelChecker : public AbstractModelChecker { // 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 #include @@ -614,15 +615,20 @@ namespace storm { * @param submatrix The matrix that will be used for value iteration later. */ std::vector getInitialValueIterationValues(storm::storage::SparseMatrix const& submatrix, std::vector const& subNondeterministicChoiceIndices, std::vector const& rightHandSide) const { - // std::vector scheduler(submatrix.getColumnCount()); - // std::vector result(scheduler.size(), Type(0.5)); - // std::vector b(scheduler.size()); - // storm::utility::vector::selectVectorValues(b, scheduler, subNondeterministicChoiceIndices, rightHandSide); - // storm::storage::SparseMatrix A(submatrix.getSubmatrix(scheduler, subNondeterministicChoiceIndices)); - // A.convertToEquationSystem(); - // this->solveEquationSystem(A, result, b); - std::vector result(submatrix.getColumnCount()); - return result; + storm::settings::Settings* s = storm::settings::instance(); + if (s->get("use-heuristic-presolve")) { + std::vector scheduler(submatrix.getColumnCount()); + std::vector result(scheduler.size(), Type(0.5)); + std::vector b(scheduler.size()); + storm::utility::vector::selectVectorValues(b, scheduler, subNondeterministicChoiceIndices, rightHandSide); + storm::storage::SparseMatrix A(submatrix.getSubmatrix(scheduler, subNondeterministicChoiceIndices)); + A.convertToEquationSystem(); + std::unique_ptr> solver(new storm::solver::GmmxxLinearEquationSolver()); + solver->solveEquationSystem(A, result, b); + return result; + } else { + return std::vector(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 @@ -16,6 +18,43 @@ namespace storm { return new AbstractNondeterministicLinearEquationSolver(); } + /*! + * 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 const& A, std::vector& x, std::vector const& nondeterministicChoiceIndices, std::vector* 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 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 const& A, std::vector& x, std::vector const& nondeterministicChoiceIndices, std::vector* 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 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()->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()->default_value(10000), "Sets the maximal number of iterations for iterative equation solving."); - desc->add_options()("precision", boost::program_options::value()->default_value(1e-6), "Sets the precision for iterative equation solving."); - desc->add_options()("precond", boost::program_options::value()->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()->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 { public: - virtual AbstractLinearEquationSolver* clone() const { + virtual AbstractNondeterministicLinearEquationSolver* clone() const { return new GmmxxNondeterministicLinearEquationSolver(); } - virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& nondeterministicChoiceIndices, std::vector* b = nullptr, uint_fast64_t n = 1) const { + virtual void performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& nondeterministicChoiceIndices, std::vector* 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* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(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 const& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, std::vector* takenChoices = nullptr) const override { + virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector 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* createPrctlModelChecke // Create the appropriate model checker. storm::settings::Settings* s = storm::settings::instance(); if (s->getString("matrixlib") == "gmm++") { - return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker(dtmc, new storm::solver::AbstractLinearEquationSolver()); + return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker(dtmc, new storm::solver::GmmxxLinearEquationSolver()); } // The control flow should never reach this point, as there is a default setting for matrixlib. @@ -218,9 +220,9 @@ storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecke // Create the appropriate model checker. storm::settings::Settings* s = storm::settings::instance(); if (s->getString("matrixlib") == "gmm++") { - return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker(mdp, new storm::solver::GmmxxNondeterministicEquationSolver()); + return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker(mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); } else if (s->getString("matrixlib") == "native") { - return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker(mdp, new storm::solver::AbstractNondeterministicEquationSolver()); + return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker(mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); } // 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& 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()->default_value(""), "name of transition reward file") ("staterew", bpo::value()->default_value(""), "name of state reward file") ("fix-deadlocks", "insert self-loops for states without outgoing transitions") + ("lemethod", boost::program_options::value()->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()->default_value(10000), "Sets the maximal number of iterations for iterative equation solving.") + ("precision", boost::program_options::value()->default_value(1e-6), "Sets the precision for iterative equation solving.") + ("precond", boost::program_options::value()->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()->default_value(true), "Sets whether the relative or absolute error is considered for detecting convergence.") + ("use-heuristic-presolve", boost::program_options::value()->default_value(false), "Sets whether heuristic methods should be applied to get better initial values for value iteration.") + ("matrixlib", boost::program_options::value()->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 - 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> modules; + static std::map< std::pair, std::shared_ptr> 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 mc(*dtmc); + storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("one"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); @@ -84,7 +85,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(dtmc->getNumberOfStates(), 8607u); ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460u); - storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker mc(*dtmc); + storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("observe0Greater1"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); @@ -138,7 +139,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(dtmc->getNumberOfStates(), 12400u); ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894u); - storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker mc(*dtmc); + storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(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 mc(*mdp); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("two"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); @@ -114,7 +115,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateRewardMdp = stateRewardParser.getModel>(); - storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); @@ -144,8 +145,8 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel>(); - storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp); - + storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); + apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); @@ -180,7 +181,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(mdp->getNumberOfStates(), 3172u); ASSERT_EQ(mdp->getNumberOfTransitions(), 7144u); - storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker mc(*mdp); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(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 mc(*mdp); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("two"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); @@ -113,8 +113,8 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateRewardMdp = stateRewardParser.getModel>(); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp); - + storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); + apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); @@ -143,7 +143,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel>(); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); @@ -179,7 +179,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(mdp->getNumberOfStates(), 3172u); ASSERT_EQ(mdp->getNumberOfTransitions(), 7144u); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(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>(); 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 mc(*dtmc); + storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("observe0Greater1"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); @@ -77,7 +78,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(dtmc->getNumberOfStates(), 1312334u); ASSERT_EQ(dtmc->getNumberOfTransitions(), 2886810u); - storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker mc(*dtmc); + storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(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 mc(*mdp); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); @@ -120,7 +121,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(mdp->getNumberOfStates(), 63616u); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472u); - storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker mc(*mdp); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("finished"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(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 mc(*mdp); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); @@ -119,7 +120,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(mdp->getNumberOfStates(), 63616u); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472u); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("finished"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(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>(); const char* newArgv[] = {"storm-performance-tests"}; storm::settings::Settings* s = storm::settings::newInstance(1, newArgv, nullptr, true); }