From 1086ffc1cc76a53eea4672bdad8eb37d8b945815 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 26 Aug 2015 14:57:42 +0200 Subject: [PATCH] Added allow early termination for min/max solvers Former-commit-id: eaad511158cef680b1119e97d0d02b09c444a4eb --- src/solver/AllowEarlyTerminationCondition.cpp | 54 ++++++++++++++++ src/solver/AllowEarlyTerminationCondition.h | 54 ++++++++++++++++ .../GmmxxMinMaxLinearEquationSolver.cpp | 4 +- src/solver/MinMaxLinearEquationSolver.cpp | 4 ++ src/solver/MinMaxLinearEquationSolver.h | 9 ++- .../NativeMinMaxLinearEquationSolver.cpp | 4 +- src/solver/SolverSelectionOptions.h | 3 +- src/utility/solver.cpp | 62 +++++++++++++------ src/utility/solver.h | 34 ++++------ .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 4 +- .../GmmxxMdpPrctlModelCheckerTest.cpp | 8 +-- .../NativeHybridMdpPrctlModelCheckerTest.cpp | 5 +- .../NativeMdpPrctlModelCheckerTest.cpp | 18 +++--- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 8 +-- .../GmmxxMinMaxLinearEquationSolverTest.cpp | 29 +++++++++ .../GmmxxMdpPrctlModelCheckerTest.cpp | 4 +- .../NativeMdpPrctlModelCheckerTest.cpp | 4 +- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 4 +- 18 files changed, 238 insertions(+), 74 deletions(-) create mode 100644 src/solver/AllowEarlyTerminationCondition.cpp create mode 100644 src/solver/AllowEarlyTerminationCondition.h diff --git a/src/solver/AllowEarlyTerminationCondition.cpp b/src/solver/AllowEarlyTerminationCondition.cpp new file mode 100644 index 000000000..d58fd1903 --- /dev/null +++ b/src/solver/AllowEarlyTerminationCondition.cpp @@ -0,0 +1,54 @@ +#include "AllowEarlyTerminationCondition.h" +#include "src/utility/vector.h" + +namespace storm { + namespace solver { + + template + TerminateAfterFilteredSumPassesThresholdValue::TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateIfAbove) : + terminationThreshold(threshold), filter(filter), terminateIfAboveThreshold(terminateIfAbove) + { + // Intentionally left empty. + } + + template + bool TerminateAfterFilteredSumPassesThresholdValue::terminateNow(const std::vector& currentValues) const { + assert(currentValues.size() >= filter.size()); + ValueType currentThreshold = storm::utility::vector::sum_if(currentValues, filter); + + if(this->terminateIfAboveThreshold) { + return currentThreshold >= this->terminationThreshold; + } else { + return currentThreshold <= this->terminationThreshold; + } + + } + + template + TerminateAfterFilteredExtremumPassesThresholdValue::TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateIfAbove, bool useMinimum) : + terminationThreshold(threshold), filter(filter), terminateIfAboveThreshold(terminateIfAbove), useMinimumAsExtremum(useMinimum) + { + // Intentionally left empty. + } + + template + bool TerminateAfterFilteredExtremumPassesThresholdValue::terminateNow(const std::vector& currentValues) const { + assert(currentValues.size() >= filter.size()); + + ValueType initVal = terminateIfAboveThreshold ? terminationThreshold - 1 : terminationThreshold + 1; + ValueType currentThreshold = useMinimumAsExtremum ? storm::utility::vector::max_if(currentValues, filter, initVal) : storm::utility::vector::max_if(currentValues, filter, initVal); + + if(this->terminateIfAboveThreshold) { + return currentThreshold >= this->terminationThreshold; + } else { + return currentThreshold <= this->terminationThreshold; + } + + } + + + template class TerminateAfterFilteredExtremumPassesThresholdValue; + template class TerminateAfterFilteredSumPassesThresholdValue; + + } +} diff --git a/src/solver/AllowEarlyTerminationCondition.h b/src/solver/AllowEarlyTerminationCondition.h new file mode 100644 index 000000000..e2e3000b4 --- /dev/null +++ b/src/solver/AllowEarlyTerminationCondition.h @@ -0,0 +1,54 @@ +#ifndef ALLOWEARLYTERMINATIONCONDITION_H +#define ALLOWEARLYTERMINATIONCONDITION_H + +#include +#include "src/storage/BitVector.h" + + +namespace storm { + namespace solver { + template + class AllowEarlyTerminationCondition { + public: + virtual bool terminateNow(std::vector const& currentValues) const = 0; + }; + + template + class NoEarlyTerminationCondition : public AllowEarlyTerminationCondition { + public: + bool terminateNow(std::vector const& currentValues) const { return false; } + }; + + template + class TerminateAfterFilteredSumPassesThresholdValue : public AllowEarlyTerminationCondition { + public: + TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateAbove); + bool terminateNow(std::vector const& currentValues) const; + + protected: + ValueType terminationThreshold; + storm::storage::BitVector filter; + bool terminateIfAboveThreshold; + }; + + template + class TerminateAfterFilteredExtremumPassesThresholdValue : public AllowEarlyTerminationCondition{ + public: + TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateAbove, bool useMinimum); + bool terminateNow(std::vector const& currentValue) const; + + protected: + ValueType terminationThreshold; + storm::storage::BitVector filter; + bool terminateIfAboveThreshold; + bool useMinimumAsExtremum; + }; + } +} + + + + + +#endif /* ALLOWEARLYTERMINATIONCONDITION_H */ + diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp index b4357b6d4..11f5171c2 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp @@ -53,7 +53,7 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. - while (!converged && iterations < this->maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) { // Compute x' = A*x + b. gmm::mult(*gmmxxMatrix, *currentX, *multiplyResult); gmm::add(b, *multiplyResult); @@ -119,7 +119,7 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. - while (!converged && iterations < this->maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) { // Take the sub-matrix according to the current choices storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->policy, true); submatrix.convertToEquationSystem(); diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index 680ee7ee0..f0c2e4869 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -19,6 +19,10 @@ namespace storm { } } + void AbstractMinMaxLinearEquationSolver::setPolicyTracking(bool setToTrue) { + trackPolicy = setToTrue; + } + std::vector AbstractMinMaxLinearEquationSolver::getPolicy() const { STORM_LOG_THROW(!useValueIteration, storm::exceptions::NotImplementedException, "Getting policies after value iteration is not yet supported!"); return policy; diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index 6e6887cd8..b5d53a68e 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -5,6 +5,7 @@ #include #include "SolverSelectionOptions.h" #include "src/storage/sparse/StateType.h" +#include "AllowEarlyTerminationCondition.h" namespace storm { namespace storage { @@ -55,7 +56,7 @@ namespace storm { protected: MinMaxLinearEquationSolver(storm::storage::SparseMatrix const& matrix, double precision, bool relativeError, uint_fast64_t maxNrIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) : AbstractMinMaxLinearEquationSolver(precision, relativeError, maxNrIterations, trackPolicy, prefTech), - A(matrix) { + A(matrix), earlyTermination(new NoEarlyTerminationCondition()) { // Intentionally left empty. } @@ -101,7 +102,13 @@ namespace storm { */ virtual void performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; + + void setEarlyTerminationCondition(std::unique_ptr> v) { + earlyTermination = std::move(v); + } + protected: + std::unique_ptr> earlyTermination; storm::storage::SparseMatrix const& A; }; diff --git a/src/solver/NativeMinMaxLinearEquationSolver.cpp b/src/solver/NativeMinMaxLinearEquationSolver.cpp index 87ee3b043..4ac37ac3e 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.cpp +++ b/src/solver/NativeMinMaxLinearEquationSolver.cpp @@ -53,7 +53,7 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the // user-specified maximum number of iterations. - while (!converged && iterations < this->maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) { // Compute x' = A*x + b. this->A.multiplyWithVector(*currentX, *multiplyResult); storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult); @@ -121,7 +121,7 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. - while (!converged && iterations < this->maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) { // Take the sub-matrix according to the current choices storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->policy, true); submatrix.convertToEquationSystem(); diff --git a/src/solver/SolverSelectionOptions.h b/src/solver/SolverSelectionOptions.h index cfba09a15..51f448644 100644 --- a/src/solver/SolverSelectionOptions.h +++ b/src/solver/SolverSelectionOptions.h @@ -11,7 +11,8 @@ namespace storm { ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk) - ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx) + ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx, Topological) + } } diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 66927c131..05d5bf479 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -81,30 +81,56 @@ namespace storm { } template - std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - storm::solver::EquationSolverType equationSolver = storm::settings::generalSettings().getEquationSolver(); - switch (equationSolver) { - case storm::solver::EquationSolverType::Gmmxx: return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); - case storm::solver::EquationSolverType::Native: return std::unique_ptr>(new storm::solver::NativeMinMaxLinearEquationSolver(matrix)); - default: return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); - } + MinMaxLinearEquationSolverFactory::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection solver) + { + setSolverType(solver); + prefTech = storm::solver::MinMaxTechniqueSelection::FROMSETTINGS; } - + template - std::unique_ptr> GmmxxMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); + void MinMaxLinearEquationSolverFactory::setSolverType(storm::solver::EquationSolverTypeSelection solverTypeSel) { + if(solverTypeSel == storm::solver::EquationSolverTypeSelection::FROMSETTINGS) { + this->solverType = storm::settings::generalSettings().getEquationSolver(); + } else { + this->solverType = storm::solver::convert(solverTypeSel); + } + } - template - std::unique_ptr> NativeMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::unique_ptr>(new storm::solver::NativeMinMaxLinearEquationSolver(matrix)); - } + void MinMaxLinearEquationSolverFactory::setPreferredTechnique(storm::solver::MinMaxTechniqueSelection preferredTech) { + this->prefTech = preferredTech; + } + template - std::unique_ptr> TopologicalMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::unique_ptr>(new storm::solver::TopologicalMinMaxLinearEquationSolver(matrix)); + std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix, bool trackPolicy) const { + + std::unique_ptr> p1; + + switch (solverType) { + case storm::solver::EquationSolverType::Gmmxx: + { + p1.reset(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix, this->prefTech)); + break; + } + case storm::solver::EquationSolverType::Native: + { + p1.reset(new storm::solver::NativeMinMaxLinearEquationSolver(matrix, this->prefTech)); + break; + } + case storm::solver::EquationSolverType::Topological: + { + STORM_LOG_THROW(prefTech == storm::solver::MinMaxTechniqueSelection::PolicyIteration, storm::exceptions::NotImplementedException, "Policy iteration for topological solver is not supported."); + p1.reset(new storm::solver::TopologicalMinMaxLinearEquationSolver(matrix)); + break; + } + } + p1->setPolicyTracking(trackPolicy); + return p1; + } + std::unique_ptr LpSolverFactory::create(std::string const& name) const { storm::solver::LpSolverType lpSolver = storm::settings::generalSettings().getLpSolver(); switch (lpSolver) { @@ -134,9 +160,7 @@ namespace storm { template class GmmxxLinearEquationSolverFactory; template class NativeLinearEquationSolverFactory; template class MinMaxLinearEquationSolverFactory; - template class GmmxxMinMaxLinearEquationSolverFactory; - template class NativeMinMaxLinearEquationSolverFactory; - template class TopologicalMinMaxLinearEquationSolverFactory; + } } } \ No newline at end of file diff --git a/src/utility/solver.h b/src/utility/solver.h index 58a7d1018..bcece2fb5 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -7,7 +7,7 @@ #include "src/solver/LinearEquationSolver.h" #include "src/solver/NativeLinearEquationSolver.h" #include "src/storage/dd/DdType.h" -#include "src/utility/ExtendSettingEnumWithSelectionField.h" +#include "src/solver/SolverSelectionOptions.h" namespace storm { namespace solver { @@ -80,30 +80,22 @@ namespace storm { template class MinMaxLinearEquationSolverFactory { public: + MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection solverType = storm::solver::EquationSolverTypeSelection::FROMSETTINGS); /*! * Creates a new nondeterministic linear equation solver instance with the given matrix. */ - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const; - }; - - template - class NativeMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory { - public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - }; - - template - class GmmxxMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory { - public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - }; - - template - class TopologicalMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory { - public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; + virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix, bool trackPolicy = false) const; + void setSolverType(storm::solver::EquationSolverTypeSelection solverType); + void setPreferredTechnique(storm::solver::MinMaxTechniqueSelection); + + protected: + /// The type of solver which should be created. + storm::solver::EquationSolverType solverType; + /// The preferred technique to be used by the solver. + /// Notice that we save the selection enum here, which allows different solvers to use different techniques. + storm::solver::MinMaxTechniqueSelection prefTech; }; - + class LpSolverFactory { public: /*! diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index e1808f717..c148a92d9 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -41,7 +41,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> mdp = model->as>(); - storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -138,7 +138,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> mdp = model->as>(); - storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index c829a94b6..39faff058 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -28,7 +28,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -92,7 +92,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); @@ -114,7 +114,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); @@ -144,7 +144,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(3172ull, mdp->getNumberOfStates()); ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index d0f752f0c..af1e54175 100644 --- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -40,8 +40,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> mdp = model->as>(); - storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - + storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(*formula); @@ -137,7 +136,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> mdp = model->as>(); - storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); diff --git a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index 14622dae2..61b5bf654 100644 --- a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -27,7 +27,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -91,7 +91,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); @@ -113,7 +113,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); @@ -143,7 +143,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(3172ull, mdp->getNumberOfStates()); ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); @@ -207,7 +207,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -239,7 +239,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -280,7 +280,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -366,7 +366,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -488,7 +488,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index f741eabc0..e2e563cc6 100644 --- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -26,7 +26,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -87,7 +87,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { // ------------- state rewards -------------- std::shared_ptr> stateRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "")->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); @@ -112,7 +112,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { // -------------------------------- state and transition reward ------------------------ std::shared_ptr> stateAndTransitionRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew")->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); @@ -143,7 +143,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(mdp->getNumberOfStates(), 3172ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull); - storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); diff --git a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp index 6c659e7b7..bc6642e7c 100644 --- a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp @@ -25,6 +25,35 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptions) { ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::gmmxxEquationSolverSettings().getPrecision()); } +// TODO add better tests here. +TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTermination) { + storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); + ASSERT_NO_THROW(builder.newRowGroup(0)); + ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); + + storm::storage::SparseMatrix A; + ASSERT_NO_THROW(A = builder.build(2)); + + std::vector x(1); + std::vector b = {0.099, 0.5}; + + double bound = 0.8; + storm::solver::GmmxxMinMaxLinearEquationSolver solver(A); + solver.setEarlyTerminationCondition(std::unique_ptr>(new storm::solver::TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector(1, true), bound, true, true))); + ASSERT_NO_THROW(solver.solveEquationSystem(true, x, b)); + ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + ASSERT_NO_THROW(solver.solveEquationSystem(false, x, b)); + ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + bound = 0.6; + solver.setEarlyTerminationCondition(std::unique_ptr>(new storm::solver::TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector(1, true), bound, true, true))); + + ASSERT_NO_THROW(solver.solveEquationSystem(false, x, b)); + ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::gmmxxEquationSolverSettings().getPrecision()); + +} + TEST(GmmxxMinMaxLinearEquationSolver, MatrixVectorMultiplication) { storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); ASSERT_NO_THROW(builder.newRowGroup(0)); diff --git a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 9d14e2782..33f70d595 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -24,7 +24,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); @@ -82,7 +82,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); diff --git a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index 2d572d5f1..5bf41d01d 100644 --- a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -25,7 +25,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); @@ -83,7 +83,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); diff --git a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index 5b63a8ddd..2d0eb8399 100644 --- a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -20,7 +20,7 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLea ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); @@ -67,7 +67,7 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");