From 72234e96b271fa1097612c4309ceaea0d5527e30 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 30 Aug 2017 18:13:47 +0200 Subject: [PATCH] started on requirements for MinMax solvers --- .../IterativeMinMaxLinearEquationSolver.cpp | 18 ++-- .../IterativeMinMaxLinearEquationSolver.h | 9 +- .../solver/LpMinMaxLinearEquationSolver.cpp | 19 ++-- .../solver/LpMinMaxLinearEquationSolver.h | 11 +-- .../solver/MinMaxLinearEquationSolver.cpp | 67 +++++++++------ src/storm/solver/MinMaxLinearEquationSolver.h | 86 +++++++++++++------ .../StandardMinMaxLinearEquationSolver.cpp | 49 +++++------ .../StandardMinMaxLinearEquationSolver.h | 14 +-- .../TopologicalMinMaxLinearEquationSolver.cpp | 67 +++++++++------ .../TopologicalMinMaxLinearEquationSolver.h | 14 ++- 10 files changed, 203 insertions(+), 151 deletions(-) diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index f4c8a0f2f..4815fc8a4 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -75,6 +75,11 @@ namespace storm { return relative; } + template + IterativeMinMaxLinearEquationSolver::IterativeMinMaxLinearEquationSolver(std::unique_ptr>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings const& settings) : StandardMinMaxLinearEquationSolver(std::move(linearEquationSolverFactory)), settings(settings) { + // Intentionally left empty + } + template IterativeMinMaxLinearEquationSolver::IterativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings const& settings) : StandardMinMaxLinearEquationSolver(A, std::move(linearEquationSolverFactory)), settings(settings) { // Intentionally left empty. @@ -459,19 +464,10 @@ namespace storm { } template - std::unique_ptr> IterativeMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized."); - - std::unique_ptr> result = std::make_unique>(std::move(matrix), this->linearEquationSolverFactory->clone(), settings); - result->setTrackScheduler(this->isTrackSchedulerSet()); - return result; - } - - template - std::unique_ptr> IterativeMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { + std::unique_ptr> IterativeMinMaxLinearEquationSolverFactory::internalCreate() const { STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized."); - std::unique_ptr> result = std::make_unique>(std::move(matrix), this->linearEquationSolverFactory->clone(), settings); + std::unique_ptr> result = std::make_unique>(this->linearEquationSolverFactory->clone(), settings); result->setTrackScheduler(this->isTrackSchedulerSet()); return result; } diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index 23d34cd7c..dc5cc656a 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -36,7 +36,7 @@ namespace storm { template class IterativeMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver { public: - IterativeMinMaxLinearEquationSolver() = default; + IterativeMinMaxLinearEquationSolver(std::unique_ptr>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings const& settings = IterativeMinMaxLinearEquationSolverSettings()); IterativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings const& settings = IterativeMinMaxLinearEquationSolverSettings()); IterativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings const& settings = IterativeMinMaxLinearEquationSolverSettings()); @@ -81,18 +81,17 @@ namespace storm { IterativeMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false); IterativeMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false); - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; - IterativeMinMaxLinearEquationSolverSettings& getSettings(); IterativeMinMaxLinearEquationSolverSettings const& getSettings() const; virtual void setMinMaxMethod(MinMaxMethodSelection const& newMethod) override; virtual void setMinMaxMethod(MinMaxMethod const& newMethod) override; + + protected: + virtual std::unique_ptr> internalCreate() const override; private: IterativeMinMaxLinearEquationSolverSettings settings; - }; } } diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp index 9b52a1fa9..45c76e029 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -9,6 +9,11 @@ namespace storm { namespace solver { + template + LpMinMaxLinearEquationSolver::LpMinMaxLinearEquationSolver(std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver(std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) { + // Intentionally left empty. + } + template LpMinMaxLinearEquationSolver::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver(A, std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) { // Intentionally left empty. @@ -119,21 +124,11 @@ namespace storm { } template - std::unique_ptr> LpMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized."); + std::unique_ptr> LpMinMaxLinearEquationSolverFactory::internalCreate() const { STORM_LOG_ASSERT(this->lpSolverFactory, "Lp solver factory not initialized."); - - std::unique_ptr> result = std::make_unique>(std::move(matrix), this->linearEquationSolverFactory->clone(), this->lpSolverFactory->clone()); - result->setTrackScheduler(this->isTrackSchedulerSet()); - return result; - } - - template - std::unique_ptr> LpMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized."); - STORM_LOG_ASSERT(this->lpSolverFactory, "Lp solver factory not initialized."); - std::unique_ptr> result = std::make_unique>(std::move(matrix), this->linearEquationSolverFactory->clone(), this->lpSolverFactory->clone()); + std::unique_ptr> result = std::make_unique>(this->linearEquationSolverFactory->clone(), this->lpSolverFactory->clone()); result->setTrackScheduler(this->isTrackSchedulerSet()); return result; } diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.h b/src/storm/solver/LpMinMaxLinearEquationSolver.h index 84d744c39..5491e7ca2 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.h +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.h @@ -10,7 +10,7 @@ namespace storm { template class LpMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver { public: - LpMinMaxLinearEquationSolver() = default; + LpMinMaxLinearEquationSolver(std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory); LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory); LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory); @@ -29,12 +29,13 @@ namespace storm { LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& lpSolverFactory, bool trackScheduler = false); LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory, bool trackScheduler = false); - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; - virtual void setMinMaxMethod(MinMaxMethodSelection const& newMethod) override; virtual void setMinMaxMethod(MinMaxMethod const& newMethod) override; - + + protected: + virtual std::unique_ptr> internalCreate() const override; + std::unique_ptr> createLpEquationSolverFactory() const; + private: std::unique_ptr> lpSolverFactory; }; diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 0ce28bd2a..872f7c03b 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -19,7 +19,7 @@ namespace storm { namespace solver { template - MinMaxLinearEquationSolver::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), cachingEnabled(false) { + MinMaxLinearEquationSolver::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), cachingEnabled(false), requirementsChecked(false) { // Intentionally left empty. } @@ -132,13 +132,23 @@ namespace storm { } template - MinMaxLinearEquationSolverFactory::MinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : trackScheduler(trackScheduler) { - setMinMaxMethod(method); + std::vector MinMaxLinearEquationSolver::getRequirements() const { + return std::vector(); } template - std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return this->create(matrix); + void MinMaxLinearEquationSolver::setRequirementsChecked(bool value) { + this->requirementsChecked = value; + } + + template + bool MinMaxLinearEquationSolver::getRequirementsChecked() const { + return this->requirementsChecked; + } + + template + MinMaxLinearEquationSolverFactory::MinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : trackScheduler(trackScheduler) { + setMinMaxMethod(method); } template @@ -182,35 +192,45 @@ namespace storm { MinMaxMethod const& MinMaxLinearEquationSolverFactory::getMinMaxMethod() const { return method; } - + template - GeneralMinMaxLinearEquationSolverFactory::GeneralMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : MinMaxLinearEquationSolverFactory(method, trackScheduler) { - // Intentionally left empty. + std::vector MinMaxLinearEquationSolverFactory::getRequirements() const { + // Create dummy solver and ask it for requirements. + std::unique_ptr> solver = this->internalCreate(); + return solver->getRequirements(); } template - std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return selectSolver(matrix); + std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { + std::unique_ptr> solver = this->internalCreate(); + solver->setMatrix(matrix); + return solver; } template - std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return selectSolver(std::move(matrix)); + std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { + std::unique_ptr> solver = this->internalCreate(); + solver->setMatrix(std::move(matrix)); + return solver; } template - template - std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { + GeneralMinMaxLinearEquationSolverFactory::GeneralMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : MinMaxLinearEquationSolverFactory(method, trackScheduler) { + // Intentionally left empty. + } + + template + std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::internalCreate() const { std::unique_ptr> result; auto method = this->getMinMaxMethod(); if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic) { IterativeMinMaxLinearEquationSolverSettings iterativeSolverSettings; iterativeSolverSettings.setSolutionMethod(method); - result = std::make_unique>(std::forward(matrix), std::make_unique>(), iterativeSolverSettings); + result = std::make_unique>(std::make_unique>(), iterativeSolverSettings); } else if (method == MinMaxMethod::Topological) { - result = std::make_unique>(std::forward(matrix)); + result = std::make_unique>(); } else if (method == MinMaxMethod::LinearProgramming) { - result = std::make_unique>(std::forward(matrix), std::make_unique>(), std::make_unique>()); + result = std::make_unique>(std::make_unique>(), std::make_unique>()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); } @@ -218,24 +238,23 @@ namespace storm { return result; } -#ifdef STORM_HAVE_CARL template<> - template - std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { + std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::internalCreate() const { std::unique_ptr> result; auto method = this->getMinMaxMethod(); if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic) { IterativeMinMaxLinearEquationSolverSettings iterativeSolverSettings; iterativeSolverSettings.setSolutionMethod(method); - result = std::make_unique>(std::forward(matrix), std::make_unique>(), iterativeSolverSettings); + result = std::make_unique>(std::make_unique>(), iterativeSolverSettings); } else if (method == MinMaxMethod::LinearProgramming) { - result = std::make_unique>(std::forward(matrix), std::make_unique>(), std::make_unique>()); + result = std::make_unique>(std::make_unique>(), std::make_unique>()); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The selected method is not available for this data type."); + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); } + result->setTrackScheduler(this->isTrackSchedulerSet()); return result; } -#endif + template class MinMaxLinearEquationSolver; template class MinMaxLinearEquationSolver; diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 3b7574abe..b00c7f155 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -23,6 +23,14 @@ namespace storm { namespace solver { + enum class MinMaxLinearEquationSolverRequirement { + ValidSchedulerHint, + ValidValueHint, + NoEndComponents, + GlobalUpperBound, + GlobalLowerBound + }; + /*! * A class representing the interface that all min-max linear equation solvers shall implement. */ @@ -30,10 +38,13 @@ namespace storm { class MinMaxLinearEquationSolver : public AbstractEquationSolver { protected: MinMaxLinearEquationSolver(OptimizationDirectionSetting direction = OptimizationDirectionSetting::Unset); - + public: virtual ~MinMaxLinearEquationSolver(); - + + virtual void setMatrix(storm::storage::SparseMatrix const& matrix) = 0; + virtual void setMatrix(storm::storage::SparseMatrix&& matrix) = 0; + /*! * Solves the equation system x = min/max(A*x + b) given by the parameters. Note that the matrix A has * to be given upon construction time of the solver object. @@ -78,33 +89,33 @@ namespace storm { * optimization direction is used. Note: this method can only be called after setting the optimization direction. */ virtual void repeatedMultiply(std::vector& x, std::vector* b , uint_fast64_t n) const; - + /*! * Sets an optimization direction to use for calls to methods that do not explicitly provide one. */ void setOptimizationDirection(OptimizationDirection direction); - + /*! * Unsets the optimization direction to use for calls to methods that do not explicitly provide one. */ void unsetOptimizationDirection(); - + /*! * Sets whether schedulers are generated when solving equation systems. If the argument is false, the currently * stored scheduler (if any) is deleted. */ void setTrackScheduler(bool trackScheduler = true); - + /*! * Retrieves whether this solver is set to generate schedulers. */ bool isTrackSchedulerSet() const; - + /*! * Retrieves whether the solver generated a scheduler. */ bool hasScheduler() const; - + /*! * Retrieves the generated scheduler. Note: it is only legal to call this function if a scheduler was generated. */ @@ -114,7 +125,7 @@ namespace storm { * Retrieves the generated (deterministic) choices of the optimal scheduler. Note: it is only legal to call this function if a scheduler was generated. */ std::vector const& getSchedulerChoices() const; - + /*! * Sets whether some of the generated data during solver calls should be cached. * This possibly decreases the runtime of subsequent calls but also increases memory consumption. @@ -125,12 +136,12 @@ namespace storm { * Retrieves whether some of the generated data during solver calls should be cached. */ bool isCachingEnabled() const; - + /* * Clears the currently cached data that has been stored during previous calls of the solver. */ virtual void clearCache() const; - + /*! * Sets a lower bound for the solution that can potentially used by the solver. */ @@ -154,15 +165,31 @@ namespace storm { /*! * Returns true iff a scheduler hint was defined */ - bool hasSchedulerHint() const; - + bool hasSchedulerHint() const; + + /*! + * Retrieves the requirements of this solver for solving equations with the current settings. + */ + virtual std::vector getRequirements() const; + + /*! + * Notifies the solver that the requirements for solving equations have been checked. If this has not been + * done before solving equations, the solver might issue a warning, perform the checks itself or even fail. + */ + void setRequirementsChecked(bool value = true); + + /*! + * Retrieves whether the solver is aware that the requirements were checked. + */ + bool getRequirementsChecked() const; + protected: /// The optimization direction to use for calls to functions that do not provide it explicitly. Can also be unset. OptimizationDirectionSetting direction; - + /// Whether we generate a scheduler during solving. bool trackScheduler; - + /// The scheduler choices that induce the optimal values (if they could be successfully generated). mutable boost::optional> schedulerChoices; @@ -179,16 +206,18 @@ namespace storm { /// Whether some of the generated data during solver calls should be cached. bool cachingEnabled; + /// A flag storing whether the requirements of the solver were checked. + bool requirementsChecked; }; - + template class MinMaxLinearEquationSolverFactory { public: MinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false); - - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const = 0; + + virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const; virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const; - + void setTrackScheduler(bool value); bool isTrackSchedulerSet() const; @@ -196,23 +225,24 @@ namespace storm { virtual void setMinMaxMethod(MinMaxMethod const& newMethod); MinMaxMethod const& getMinMaxMethod() const; - + + std::vector getRequirements() const; + + protected: + virtual std::unique_ptr> internalCreate() const = 0; + private: bool trackScheduler; MinMaxMethod method; }; - + template class GeneralMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory { public: GeneralMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false); - - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; - - private: - template - std::unique_ptr> selectSolver(MatrixType&& matrix) const; + + protected: + virtual std::unique_ptr> internalCreate() const override; }; } // namespace solver diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index 5fedfced4..ab879a175 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -15,7 +15,7 @@ namespace storm { namespace solver { template - StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver() : A(nullptr) { + StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), A(nullptr) { // Intentionally left empty. } @@ -29,6 +29,18 @@ namespace storm { // Intentionally left empty. } + template + void StandardMinMaxLinearEquationSolver::setMatrix(storm::storage::SparseMatrix const& matrix) { + this->localA = nullptr; + this->A = &matrix; + } + + template + void StandardMinMaxLinearEquationSolver::setMatrix(storm::storage::SparseMatrix&& matrix) { + this->localA = std::make_unique>(std::move(matrix)); + this->A = this->localA.get(); + } + template void StandardMinMaxLinearEquationSolver::repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const { if (!linEqSolverA) { @@ -80,46 +92,25 @@ namespace storm { case EquationSolverType::Elimination: linearEquationSolverFactory = std::make_unique>(); break; } } - -#ifdef STORM_HAVE_CARL + template<> StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, MinMaxMethodSelection const& method, bool trackScheduler) : MinMaxLinearEquationSolverFactory(method, trackScheduler) { switch (solverType) { - case EquationSolverType::Eigen: linearEquationSolverFactory = std::make_unique>(); break; - case EquationSolverType::Elimination: linearEquationSolverFactory = std::make_unique>(); break; + case EquationSolverType::Eigen: linearEquationSolverFactory = std::make_unique>(); break; + case EquationSolverType::Elimination: linearEquationSolverFactory = std::make_unique>(); break; default: - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot create the requested solver for this data type."); + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported equation solver for this data type."); } } -#endif - - template - std::unique_ptr> StandardMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - STORM_LOG_ASSERT(linearEquationSolverFactory, "Linear equation solver factory not initialized."); - - std::unique_ptr> result; - auto method = this->getMinMaxMethod(); - if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic) { - IterativeMinMaxLinearEquationSolverSettings iterativeSolverSettings; - iterativeSolverSettings.setSolutionMethod(method); - result = std::make_unique>(matrix, linearEquationSolverFactory->clone(), iterativeSolverSettings); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); - } - result->setTrackScheduler(this->isTrackSchedulerSet()); - return result; - } - + template - std::unique_ptr> StandardMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - STORM_LOG_ASSERT(linearEquationSolverFactory, "Linear equation solver factory not initialized."); - + std::unique_ptr> StandardMinMaxLinearEquationSolverFactory::internalCreate() const { std::unique_ptr> result; auto method = this->getMinMaxMethod(); if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic) { IterativeMinMaxLinearEquationSolverSettings iterativeSolverSettings; iterativeSolverSettings.setSolutionMethod(method); - result = std::make_unique>(std::move(matrix), linearEquationSolverFactory->clone(), iterativeSolverSettings); + result = std::make_unique>(this->linearEquationSolverFactory->clone(), iterativeSolverSettings); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); } diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.h b/src/storm/solver/StandardMinMaxLinearEquationSolver.h index b122489c8..765e24888 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.h +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.h @@ -9,11 +9,13 @@ namespace storm { template class StandardMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver { public: - StandardMinMaxLinearEquationSolver(); - + StandardMinMaxLinearEquationSolver(std::unique_ptr>&& linearEquationSolverFactory); StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory); StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory); + virtual void setMatrix(storm::storage::SparseMatrix const& matrix) override; + virtual void setMatrix(storm::storage::SparseMatrix&& matrix) override; + virtual ~StandardMinMaxLinearEquationSolver() = default; virtual void repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const override; @@ -46,11 +48,13 @@ namespace storm { StandardMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false); StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false); - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; - protected: + virtual std::unique_ptr> internalCreate() const override; + std::unique_ptr> linearEquationSolverFactory; + + private: + void createLinearEquationSolverFactory() const; }; template diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index f659620e9..f60fce272 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -23,15 +23,31 @@ namespace storm { namespace solver { template - TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) - { - // Get the settings object to customize solving. - this->enableCuda = storm::settings::getModule().isCudaSet(); + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { + // Get the settings object to customize solving. + this->enableCuda = storm::settings::getModule().isCudaSet(); #ifdef STORM_HAVE_CUDA - STORM_LOG_INFO_COND(this->enableCuda, "Option CUDA was not set, but the topological value iteration solver will use it anyways."); + STORM_LOG_INFO_COND(this->enableCuda, "Option CUDA was not set, but the topological value iteration solver will use it anyways."); #endif } - + + template + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : TopologicalMinMaxLinearEquationSolver(precision, maximalNumberOfIterations, relative) { + this->setMatrix(A); + } + + template + void TopologicalMinMaxLinearEquationSolver::setMatrix(storm::storage::SparseMatrix const& matrix) { + this->localA = nullptr; + this->A = &matrix; + } + + template + void TopologicalMinMaxLinearEquationSolver::setMatrix(storm::storage::SparseMatrix&& matrix) { + this->localA = std::make_unique>(std::move(matrix)); + this->A = this->localA.get(); + } + template bool TopologicalMinMaxLinearEquationSolver::solveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b) const { @@ -42,7 +58,7 @@ namespace storm { #endif if (__FORCE_FLOAT_CALCULATION && std::is_same::value) { // FIXME: This actually allocates quite some storage, because of this conversion, is it really necessary? - storm::storage::SparseMatrix newA = this->A.template toValueType(); + storm::storage::SparseMatrix newA = this->A->template toValueType(); TopologicalMinMaxLinearEquationSolver newSolver(newA, this->precision, this->maximalNumberOfIterations, this->relative); @@ -67,12 +83,12 @@ namespace storm { } // Now, we need to determine the SCCs of the MDP and perform a topological sort. - std::vector const& nondeterministicChoiceIndices = this->A.getRowGroupIndices(); + std::vector const& nondeterministicChoiceIndices = this->A->getRowGroupIndices(); // Check if the decomposition is necessary #ifdef STORM_HAVE_CUDA #define __USE_CUDAFORSTORM_OPT true - size_t const gpuSizeOfCompleteSystem = basicValueIteration_mvReduce_uint64_double_calculateMemorySize(static_cast(A.getRowCount()), nondeterministicChoiceIndices.size(), static_cast(A.getEntryCount())); + size_t const gpuSizeOfCompleteSystem = basicValueIteration_mvReduce_uint64_double_calculateMemorySize(static_cast(A->getRowCount()), nondeterministicChoiceIndices.size(), static_cast(A->getEntryCount())); size_t const cudaFreeMemory = static_cast(getFreeCudaMemory() * 0.95); #else #define __USE_CUDAFORSTORM_OPT false @@ -90,9 +106,9 @@ namespace storm { bool result = false; size_t globalIterations = 0; if (dir == OptimizationDirection::Minimize) { - result = __basicValueIteration_mvReduce_minimize(this->maximalNumberOfIterations, this->precision, this->relative, A.rowIndications, A.columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations); + result = __basicValueIteration_mvReduce_minimize(this->maximalNumberOfIterations, this->precision, this->relative, A->rowIndications, A->columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations); } else { - result = __basicValueIteration_mvReduce_maximize(this->maximalNumberOfIterations, this->precision, this->relative, A.rowIndications, A.columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations); + result = __basicValueIteration_mvReduce_maximize(this->maximalNumberOfIterations, this->precision, this->relative, A->rowIndications, A->columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations); } STORM_LOG_INFO("Executed " << globalIterations << " of max. " << maximalNumberOfIterations << " Iterations on GPU."); @@ -116,16 +132,16 @@ namespace storm { throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of storm does not support CUDA acceleration. Internal Error!"; #endif } else { - storm::storage::BitVector fullSystem(this->A.getRowGroupCount(), true); - storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(this->A, fullSystem, false, false); + storm::storage::BitVector fullSystem(this->A->getRowGroupCount(), true); + storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(*this->A, fullSystem, false, false); STORM_LOG_THROW(sccDecomposition.size() > 0, storm::exceptions::IllegalArgumentException, "Can not solve given equation system as the SCC decomposition returned no SCCs."); - storm::storage::SparseMatrix stronglyConnectedComponentsDependencyGraph = sccDecomposition.extractPartitionDependencyGraph(this->A); + storm::storage::SparseMatrix stronglyConnectedComponentsDependencyGraph = sccDecomposition.extractPartitionDependencyGraph(*this->A); std::vector topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); // Calculate the optimal distribution of sccs - std::vector> optimalSccs = this->getOptimalGroupingFromTopologicalSccDecomposition(sccDecomposition, topologicalSort, this->A); + std::vector> optimalSccs = this->getOptimalGroupingFromTopologicalSccDecomposition(sccDecomposition, topologicalSort, *this->A); STORM_LOG_INFO("Optimized SCC Decomposition, originally " << topologicalSort.size() << " SCCs, optimized to " << optimalSccs.size() << " SCCs."); std::vector* currentX = nullptr; @@ -142,8 +158,8 @@ namespace storm { storm::storage::StateBlock const& scc = sccIndexIt->second; // Generate a sub matrix - storm::storage::BitVector subMatrixIndices(this->A.getColumnCount(), scc.cbegin(), scc.cend()); - storm::storage::SparseMatrix sccSubmatrix = this->A.getSubmatrix(true, subMatrixIndices, subMatrixIndices); + storm::storage::BitVector subMatrixIndices(this->A->getColumnCount(), scc.cbegin(), scc.cend()); + storm::storage::SparseMatrix sccSubmatrix = this->A->getSubmatrix(true, subMatrixIndices, subMatrixIndices); std::vector sccSubB(sccSubmatrix.getRowCount()); storm::utility::vector::selectVectorValues(sccSubB, subMatrixIndices, nondeterministicChoiceIndices, b); std::vector sccSubX(sccSubmatrix.getColumnCount()); @@ -167,7 +183,7 @@ namespace storm { sccSubNondeterministicChoiceIndices.at(outerIndex + 1) = sccSubNondeterministicChoiceIndices.at(outerIndex) + (nondeterministicChoiceIndices[state + 1] - nondeterministicChoiceIndices[state]); for (auto rowGroupIt = nondeterministicChoiceIndices[state]; rowGroupIt != nondeterministicChoiceIndices[state + 1]; ++rowGroupIt) { - typename storm::storage::SparseMatrix::const_rows row = this->A.getRow(rowGroupIt); + typename storm::storage::SparseMatrix::const_rows row = this->A->getRow(rowGroupIt); for (auto rowIt = row.begin(); rowIt != row.end(); ++rowIt) { if (!subMatrixIndices.get(rowIt->getColumn())) { // This is an outgoing transition of a state in the SCC to a state not included in the SCC @@ -439,11 +455,11 @@ namespace storm { template void TopologicalMinMaxLinearEquationSolver::repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const { - std::unique_ptr> multiplyResult = std::make_unique>(this->A.getRowCount()); + std::unique_ptr> multiplyResult = std::make_unique>(this->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) { - this->A.multiplyWithVector(x, *multiplyResult); + this->A->multiplyWithVector(x, *multiplyResult); // Add b if it is non-null. if (b != nullptr) { @@ -452,7 +468,7 @@ namespace storm { // 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. - storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, this->A.getRowGroupIndices()); + storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, this->A->getRowGroupIndices()); } } @@ -462,15 +478,10 @@ namespace storm { } template - std::unique_ptr> TopologicalMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::make_unique>(matrix); + std::unique_ptr> TopologicalMinMaxLinearEquationSolverFactory::internalCreate() const { + return std::make_unique>(); } - template - std::unique_ptr> TopologicalMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { - return std::make_unique>(std::move(matrix)); - } - // Explicitly instantiate the solver. template class TopologicalMinMaxLinearEquationSolver; diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h index fcbdcf988..2488ead3f 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h @@ -24,6 +24,8 @@ namespace storm { template class TopologicalMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver { public: + TopologicalMinMaxLinearEquationSolver(double precision = 1e-6, uint_fast64_t maximalNumberOfIterations = 20000, bool relative = true); + /*! * Constructs a min-max linear equation solver with parameters being set according to the settings * object. @@ -31,7 +33,10 @@ namespace storm { * @param A The matrix defining the coefficients of the linear equation system. */ TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision = 1e-6, uint_fast64_t maximalNumberOfIterations = 20000, bool relative = true); - + + virtual void setMatrix(storm::storage::SparseMatrix const& matrix) override; + virtual void setMatrix(storm::storage::SparseMatrix&& matrix) override; + virtual bool solveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b) const override; virtual void repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const override; @@ -40,7 +45,8 @@ namespace storm { bool getRelative() const; private: - storm::storage::SparseMatrix const& A; + storm::storage::SparseMatrix const* A; + std::unique_ptr> localA; double precision; uint_fast64_t maximalNumberOfIterations; bool relative; @@ -144,8 +150,8 @@ namespace storm { public: TopologicalMinMaxLinearEquationSolverFactory(bool trackScheduler = false); - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; + protected: + virtual std::unique_ptr> internalCreate() const override; }; } // namespace solver