From 39549f6ebd0c8a999c7def233e906f3bf29b3f04 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sat, 29 Jul 2017 21:21:20 +0200 Subject: [PATCH] Moved some functionality of StandardMinMaxSolver into a subclass --- ...SparseDtmcParameterLiftingModelChecker.cpp | 9 +- .../IterativeMinMaxLinearEquationSolver.cpp | 511 ++++++++++++++++++ .../IterativeMinMaxLinearEquationSolver.h | 96 ++++ .../solver/MinMaxLinearEquationSolver.cpp | 39 +- src/storm/solver/MinMaxLinearEquationSolver.h | 10 +- .../StandardMinMaxLinearEquationSolver.cpp | 482 ++--------------- .../StandardMinMaxLinearEquationSolver.h | 80 +-- .../TopologicalMinMaxLinearEquationSolver.cpp | 2 +- .../GmmxxMdpPrctlModelCheckerTest.cpp | 3 +- .../GmmxxMinMaxLinearEquationSolverTest.cpp | 3 +- .../NativeMinMaxLinearEquationSolverTest.cpp | 3 +- 11 files changed, 697 insertions(+), 541 deletions(-) create mode 100644 src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp create mode 100644 src/storm/solver/IterativeMinMaxLinearEquationSolver.h diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 155b13dec..3d8d18f8b 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -222,14 +222,11 @@ namespace storm { parameterLifter->specifyRegion(region, dirForParameters); // Set up the solver - auto solver = solverFactory->create(parameterLifter->getMatrix()); - if (storm::NumberTraits::IsExact && dynamic_cast*>(solver.get())) { + if (storm::NumberTraits::IsExact && solverFactory->getMinMaxMethod() == storm::solver::MinMaxMethod::ValueIteration) { STORM_LOG_INFO("Parameter Lifting: Setting solution method for exact MinMaxSolver to policy iteration"); - auto* standardSolver = dynamic_cast*>(solver.get()); - auto settings = standardSolver->getSettings(); - settings.setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration); - standardSolver->setSettings(settings); + solverFactory->setMinMaxMethod(storm::solver::MinMaxMethod::PolicyIteration); } + auto solver = solverFactory->create(parameterLifter->getMatrix()); if (lowerResultBound) solver->setLowerBound(lowerResultBound.get()); if (upperResultBound) solver->setUpperBound(upperResultBound.get()); if (!stepBound) solver->setTrackScheduler(true); diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp new file mode 100644 index 000000000..d03e356ac --- /dev/null +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -0,0 +1,511 @@ +#include "storm/solver/IterativeMinMaxLinearEquationSolver.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/MinMaxEquationSolverSettings.h" + +#include "storm/utility/vector.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidSettingsException.h" +#include "storm/exceptions/InvalidStateException.h" + +namespace storm { + namespace solver { + + template + IterativeMinMaxLinearEquationSolverSettings::IterativeMinMaxLinearEquationSolverSettings() { + // Get the settings object to customize linear solving. + storm::settings::modules::MinMaxEquationSolverSettings const& settings = storm::settings::getModule(); + + maximalNumberOfIterations = settings.getMaximalIterationCount(); + precision = storm::utility::convertNumber(settings.getPrecision()); + relative = settings.getConvergenceCriterion() == storm::settings::modules::MinMaxEquationSolverSettings::ConvergenceCriterion::Relative; + + setSolutionMethod(settings.getMinMaxEquationSolvingMethod()); + + } + + template + void IterativeMinMaxLinearEquationSolverSettings::setSolutionMethod(SolutionMethod const& solutionMethod) { + this->solutionMethod = solutionMethod; + } + + template + void IterativeMinMaxLinearEquationSolverSettings::setSolutionMethod(MinMaxMethod const& solutionMethod) { + switch (solutionMethod) { + case MinMaxMethod::ValueIteration: this->solutionMethod = SolutionMethod::ValueIteration; break; + case MinMaxMethod::PolicyIteration: this->solutionMethod = SolutionMethod::PolicyIteration; break; + case MinMaxMethod::Acyclic: this->solutionMethod = SolutionMethod::Acyclic; break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique for iterative MinMax linear equation solver."); + } + } + + template + void IterativeMinMaxLinearEquationSolverSettings::setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations) { + this->maximalNumberOfIterations = maximalNumberOfIterations; + } + + template + void IterativeMinMaxLinearEquationSolverSettings::setRelativeTerminationCriterion(bool value) { + this->relative = value; + } + + template + void IterativeMinMaxLinearEquationSolverSettings::setPrecision(ValueType precision) { + this->precision = precision; + } + + template + typename IterativeMinMaxLinearEquationSolverSettings::SolutionMethod const& IterativeMinMaxLinearEquationSolverSettings::getSolutionMethod() const { + return solutionMethod; + } + + template + uint64_t IterativeMinMaxLinearEquationSolverSettings::getMaximalNumberOfIterations() const { + return maximalNumberOfIterations; + } + + template + ValueType IterativeMinMaxLinearEquationSolverSettings::getPrecision() const { + return precision; + } + + template + bool IterativeMinMaxLinearEquationSolverSettings::getRelativeTerminationCriterion() const { + return relative; + } + + 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. + } + + template + IterativeMinMaxLinearEquationSolver::IterativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings const& settings) : StandardMinMaxLinearEquationSolver(std::move(A), std::move(linearEquationSolverFactory)), settings(settings) { + // Intentionally left empty. + } + + template + bool IterativeMinMaxLinearEquationSolver::solveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b) const { + switch (this->getSettings().getSolutionMethod()) { + case IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration: + return solveEquationsValueIteration(dir, x, b); + case IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration: + return solveEquationsPolicyIteration(dir, x, b); + case IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::Acyclic: + return solveEquationsAcyclic(dir, x, b); + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "This solver does not implement the selected solution method"); + } + return false; + } + + template + bool IterativeMinMaxLinearEquationSolver::solveEquationsPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const { + // Create the initial scheduler. + std::vector scheduler = this->hasSchedulerHint() ? this->choicesHint.get() : std::vector(this->A.getRowGroupCount()); + + // Get a vector for storing the right-hand side of the inner equation system. + if(!auxiliaryRowGroupVector) { + auxiliaryRowGroupVector = std::make_unique>(this->A.getRowGroupCount()); + } + std::vector& subB = *auxiliaryRowGroupVector; + + // Resolve the nondeterminism according to the current scheduler. + storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(scheduler, true); + submatrix.convertToEquationSystem(); + storm::utility::vector::selectVectorValues(subB, scheduler, this->A.getRowGroupIndices(), b); + + // Create a solver that we will use throughout the procedure. We will modify the matrix in each iteration. + auto solver = this->linearEquationSolverFactory->create(std::move(submatrix)); + if (this->lowerBound) { + solver->setLowerBound(this->lowerBound.get()); + } + if (this->upperBound) { + solver->setUpperBound(this->upperBound.get()); + } + solver->setCachingEnabled(true); + + Status status = Status::InProgress; + uint64_t iterations = 0; + do { + // Solve the equation system for the 'DTMC'. + // FIXME: we need to remove the 0- and 1- states to make the solution unique. + // HOWEVER: if we start with a valid scheduler, then we will never get an illegal one, because staying + // within illegal MECs will never strictly improve the value. Is this true? + solver->solveEquations(x, subB); + + // Go through the multiplication result and see whether we can improve any of the choices. + bool schedulerImproved = false; + for (uint_fast64_t group = 0; group < this->A.getRowGroupCount(); ++group) { + uint_fast64_t currentChoice = scheduler[group]; + for (uint_fast64_t choice = this->A.getRowGroupIndices()[group]; choice < this->A.getRowGroupIndices()[group + 1]; ++choice) { + // If the choice is the currently selected one, we can skip it. + if (choice - this->A.getRowGroupIndices()[group] == currentChoice) { + continue; + } + + // Create the value of the choice. + ValueType choiceValue = storm::utility::zero(); + for (auto const& entry : this->A.getRow(choice)) { + choiceValue += entry.getValue() * x[entry.getColumn()]; + } + choiceValue += b[choice]; + + // If the value is strictly better than the solution of the inner system, we need to improve the scheduler. + // TODO: If the underlying solver is not precise, this might run forever (i.e. when a state has two choices where the (exact) values are equal). + // only changing the scheduler if the values are not equal (modulo precision) would make this unsound. + if (valueImproved(dir, x[group], choiceValue)) { + schedulerImproved = true; + scheduler[group] = choice - this->A.getRowGroupIndices()[group]; + x[group] = std::move(choiceValue); + } + } + } + + // If the scheduler did not improve, we are done. + if (!schedulerImproved) { + status = Status::Converged; + } else { + // Update the scheduler and the solver. + submatrix = this->A.selectRowsFromRowGroups(scheduler, true); + submatrix.convertToEquationSystem(); + storm::utility::vector::selectVectorValues(subB, scheduler, this->A.getRowGroupIndices(), b); + solver->setMatrix(std::move(submatrix)); + } + + // Update environment variables. + ++iterations; + status = updateStatusIfNotConverged(status, x, iterations); + } while (status == Status::InProgress); + + reportStatus(status, iterations); + + // If requested, we store the scheduler for retrieval. + if (this->isTrackSchedulerSet()) { + this->schedulerChoices = std::move(scheduler); + } + + if(!this->isCachingEnabled()) { + clearCache(); + } + + return status == Status::Converged || status == Status::TerminatedEarly; + } + + template + bool IterativeMinMaxLinearEquationSolver::valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const { + if (dir == OptimizationDirection::Minimize) { + return value2 < value1; + } else { + return value2 > value1; + } + } + + template + ValueType IterativeMinMaxLinearEquationSolver::getPrecision() const { + return this->getSettings().getPrecision(); + } + + template + bool IterativeMinMaxLinearEquationSolver::getRelative() const { + return this->getSettings().getRelativeTerminationCriterion(); + } + + template + bool IterativeMinMaxLinearEquationSolver::solveEquationsValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const { + if(!this->linEqSolverA) { + this->linEqSolverA = this->linearEquationSolverFactory->create(this->A); + this->linEqSolverA->setCachingEnabled(true); + } + + if (!this->auxiliaryRowVector) { + this->auxiliaryRowVector = std::make_unique>(this->A.getRowCount()); + } + std::vector& multiplyResult = *this->auxiliaryRowVector; + + if (!auxiliaryRowGroupVector) { + auxiliaryRowGroupVector = std::make_unique>(this->A.getRowGroupCount()); + } + + if (this->hasSchedulerHint()) { + // Resolve the nondeterminism according to the scheduler hint + storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->choicesHint.get(), true); + submatrix.convertToEquationSystem(); + storm::utility::vector::selectVectorValues(*auxiliaryRowGroupVector, this->choicesHint.get(), this->A.getRowGroupIndices(), b); + + // Solve the resulting equation system. + // Note that the linEqSolver might consider a slightly different interpretation of "equalModuloPrecision". Hence, we iteratively increase its precision. + auto submatrixSolver = this->linearEquationSolverFactory->create(std::move(submatrix)); + submatrixSolver->setCachingEnabled(true); + if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); } + if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); } + submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector); + } + + std::vector* newX = auxiliaryRowGroupVector.get(); + + std::vector* currentX = &x; + + // Proceed with the iterations as long as the method did not converge or reach the maximum number of iterations. + uint64_t iterations = 0; + + Status status = Status::InProgress; + while (status == Status::InProgress) { + // Compute x' = A*x + b. + this->linEqSolverA->multiply(*currentX, &b, multiplyResult); + + // Reduce the vector x' by applying min/max for all non-deterministic choices. + storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, *newX, this->A.getRowGroupIndices()); + + // Determine whether the method converged. + if (storm::utility::vector::equalModuloPrecision(*currentX, *newX, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion())) { + status = Status::Converged; + } + + // Update environment variables. + std::swap(currentX, newX); + ++iterations; + status = updateStatusIfNotConverged(status, *currentX, iterations); + } + + reportStatus(status, iterations); + + // 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 (currentX == auxiliaryRowGroupVector.get()) { + std::swap(x, *currentX); + } + + // If requested, we store the scheduler for retrieval. + if (this->isTrackSchedulerSet()) { + // Due to a custom termination condition, it may be the case that no iterations are performed. In this + // case we need to compute x'= A*x+b once. + if (iterations==0) { + this->linEqSolverA->multiply(x, &b, multiplyResult); + } + this->schedulerChoices = std::vector(this->A.getRowGroupCount()); + // Reduce the multiplyResult and keep track of the choices made + storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A.getRowGroupIndices(), &this->schedulerChoices.get()); + } + + if (!this->isCachingEnabled()) { + clearCache(); + } + + return status == Status::Converged || status == Status::TerminatedEarly; + } + + template + bool IterativeMinMaxLinearEquationSolver::solveEquationsAcyclic(OptimizationDirection dir, std::vector& x, std::vector const& b) const { + uint64_t numGroups = this->A.getRowGroupCount(); + + // Allocate memory for the scheduler (if required) + if (this->isTrackSchedulerSet()) { + if (this->schedulerChoices) { + this->schedulerChoices->resize(numGroups); + } else { + this->schedulerChoices = std::vector(numGroups); + } + } + + // We now compute a topological sort of the row groups. + // If caching is enabled, it might be possible to obtain this sort from the cache. + if (this->isCachingEnabled()) { + if (rowGroupOrdering) { + for (auto const& group : *rowGroupOrdering) { + computeOptimalValueForRowGroup(group, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[group] : nullptr); + } + return true; + } else { + rowGroupOrdering = std::make_unique>(); + rowGroupOrdering->reserve(numGroups); + } + } + + auto transposedMatrix = this->A.transpose(true); + + // We store the groups that have already been processed, i.e., the groups for which x[group] was already set to the correct value. + storm::storage::BitVector processedGroups(numGroups, false); + // Furthermore, we keep track of all candidate groups for which we still need to check whether this group can be processed now. + // A group can be processed if all successors have already been processed. + // Notice that the BitVector candidates is considered in a reversed way, i.e., group i is a candidate iff candidates.get(numGroups - i - 1) is true. + // This is due to the observation that groups with higher indices usually need to be processed earlier. + storm::storage::BitVector candidates(numGroups, true); + uint64_t candidate = numGroups - 1; + for (uint64_t numCandidates = candidates.size(); numCandidates > 0; --numCandidates) { + candidates.set(numGroups - candidate - 1, false); + + // Check if the candidate row group has an unprocessed successor + bool hasUnprocessedSuccessor = false; + for (auto const& entry : this->A.getRowGroup(candidate)) { + if (!processedGroups.get(entry.getColumn())) { + hasUnprocessedSuccessor = true; + break; + } + } + + uint64_t nextCandidate = numGroups - candidates.getNextSetIndex(numGroups - candidate - 1 + 1) - 1; + + if (!hasUnprocessedSuccessor) { + // This candidate can be processed. + processedGroups.set(candidate); + computeOptimalValueForRowGroup(candidate, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[candidate] : nullptr); + if (this->isCachingEnabled()) { + rowGroupOrdering->push_back(candidate); + } + + // Add new candidates + for (auto const& predecessorEntry : transposedMatrix.getRow(candidate)) { + uint64_t predecessor = predecessorEntry.getColumn(); + if (!candidates.get(numGroups - predecessor - 1)) { + candidates.set(numGroups - predecessor - 1, true); + nextCandidate = std::max(nextCandidate, predecessor); + ++numCandidates; + } + } + } + candidate = nextCandidate; + } + + assert(candidates.empty()); + STORM_LOG_THROW(processedGroups.full(), storm::exceptions::InvalidOperationException, "The MinMax equation system is not acyclic."); + return true; + } + + template + void IterativeMinMaxLinearEquationSolver::computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector& x, std::vector const& b, uint_fast64_t* choice) const { + uint64_t row = this->A.getRowGroupIndices()[group]; + uint64_t groupEnd = this->A.getRowGroupIndices()[group + 1]; + assert(row != groupEnd); + + auto bIt = b.begin() + row; + ValueType& xi = x[group]; + xi = this->A.multiplyRowWithVector(row, x) + *bIt; + uint64_t optimalRow = row; + + for (++row, ++bIt; row < groupEnd; ++row, ++bIt) { + ValueType choiceVal = this->A.multiplyRowWithVector(row, x) + *bIt; + if (minimize(dir)) { + if (choiceVal < xi) { + xi = choiceVal; + optimalRow = row; + } + } else { + if (choiceVal > xi) { + xi = choiceVal; + optimalRow = row; + } + } + } + if (choice != nullptr) { + *choice = optimalRow - this->A.getRowGroupIndices()[group]; + } + } + + template + typename IterativeMinMaxLinearEquationSolver::Status IterativeMinMaxLinearEquationSolver::updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations) const { + if (status != Status::Converged) { + if (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x)) { + status = Status::TerminatedEarly; + } else if (iterations >= this->getSettings().getMaximalNumberOfIterations()) { + status = Status::MaximalIterationsExceeded; + } + } + return status; + } + + template + void IterativeMinMaxLinearEquationSolver::reportStatus(Status status, uint64_t iterations) const { + switch (status) { + case Status::Converged: STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations."); break; + case Status::TerminatedEarly: STORM_LOG_INFO("Iterative solver terminated early after " << iterations << " iterations."); break; + case Status::MaximalIterationsExceeded: STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations."); break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Iterative solver terminated unexpectedly."); + } + } + + template + IterativeMinMaxLinearEquationSolverSettings const& IterativeMinMaxLinearEquationSolver::getSettings() const { + return settings; + } + + template + void IterativeMinMaxLinearEquationSolver::setSettings(IterativeMinMaxLinearEquationSolverSettings const& newSettings) { + settings = newSettings; + } + + template + void IterativeMinMaxLinearEquationSolver::clearCache() const { + auxiliaryRowGroupVector.reset(); + rowGroupOrdering.reset(); + StandardMinMaxLinearEquationSolver::clearCache(); + } + + template + IterativeMinMaxLinearEquationSolverFactory::IterativeMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(method, trackScheduler) { + settings.setSolutionMethod(this->getMinMaxMethod()); + } + + template + IterativeMinMaxLinearEquationSolverFactory::IterativeMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, MinMaxMethodSelection const& method, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(std::move(linearEquationSolverFactory), method, trackScheduler) { + settings.setSolutionMethod(this->getMinMaxMethod()); + } + + template + IterativeMinMaxLinearEquationSolverFactory::IterativeMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, MinMaxMethodSelection const& method, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(solverType, method, trackScheduler) { + settings.setSolutionMethod(this->getMinMaxMethod()); + } + + 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 { + 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 + IterativeMinMaxLinearEquationSolverSettings& IterativeMinMaxLinearEquationSolverFactory::getSettings() { + return settings; + } + + template + IterativeMinMaxLinearEquationSolverSettings const& IterativeMinMaxLinearEquationSolverFactory::getSettings() const { + return settings; + } + + template + void IterativeMinMaxLinearEquationSolverFactory::setMinMaxMethod(MinMaxMethodSelection const& newMethod) { + MinMaxLinearEquationSolverFactory::setMinMaxMethod(newMethod); + settings.setSolutionMethod(this->getMinMaxMethod()); + } + + template + void IterativeMinMaxLinearEquationSolverFactory::setMinMaxMethod(MinMaxMethod const& newMethod) { + MinMaxLinearEquationSolverFactory::setMinMaxMethod(newMethod); + settings.setSolutionMethod(this->getMinMaxMethod()); + } + + template class IterativeMinMaxLinearEquationSolverSettings; + template class IterativeMinMaxLinearEquationSolver; + template class IterativeMinMaxLinearEquationSolverFactory; + +#ifdef STORM_HAVE_CARL + template class IterativeMinMaxLinearEquationSolverSettings; + template class IterativeMinMaxLinearEquationSolver; + template class IterativeMinMaxLinearEquationSolverFactory; +#endif + } +} diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h new file mode 100644 index 000000000..3d4f06156 --- /dev/null +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -0,0 +1,96 @@ +#pragma once + +#include "storm/solver/LinearEquationSolver.h" +#include "storm/solver/StandardMinMaxLinearEquationSolver.h" + +namespace storm { + namespace solver { + + template + class IterativeMinMaxLinearEquationSolverSettings { + public: + IterativeMinMaxLinearEquationSolverSettings(); + + enum class SolutionMethod { + ValueIteration, PolicyIteration, Acyclic + }; + + void setSolutionMethod(SolutionMethod const& solutionMethod); + void setSolutionMethod(MinMaxMethod const& solutionMethod); + void setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations); + void setRelativeTerminationCriterion(bool value); + void setPrecision(ValueType precision); + + SolutionMethod const& getSolutionMethod() const; + uint64_t getMaximalNumberOfIterations() const; + ValueType getPrecision() const; + bool getRelativeTerminationCriterion() const; + + private: + SolutionMethod solutionMethod; + uint64_t maximalNumberOfIterations; + ValueType precision; + bool relative; + }; + + template + class IterativeMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver { + public: + 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()); + + virtual bool solveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b) const override; + + IterativeMinMaxLinearEquationSolverSettings const& getSettings() const; + void setSettings(IterativeMinMaxLinearEquationSolverSettings const& newSettings); + + virtual void clearCache() const override; + + virtual ValueType getPrecision() const override; + virtual bool getRelative() const override; + private: + bool solveEquationsPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const; + bool solveEquationsValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const; + bool solveEquationsAcyclic(OptimizationDirection dir, std::vector& x, std::vector const& b) const; + + bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const; + + void computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector& x, std::vector const& b, uint_fast64_t* choice = nullptr) const; + + enum class Status { + Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress + }; + + // possibly cached data + mutable std::unique_ptr> auxiliaryRowGroupVector; // A.rowGroupCount() entries + mutable std::unique_ptr> rowGroupOrdering; // A.rowGroupCount() entries + + Status updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations) const; + void reportStatus(Status status, uint64_t iterations) const; + + /// The settings of this solver. + IterativeMinMaxLinearEquationSolverSettings settings; + }; + + template + class IterativeMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory { + public: + IterativeMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false); + 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; + + private: + IterativeMinMaxLinearEquationSolverSettings settings; + + }; + } +} diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 4bdb08f3e..1c6f8dc65 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -3,7 +3,7 @@ #include #include "storm/solver/LinearEquationSolver.h" -#include "storm/solver/StandardMinMaxLinearEquationSolver.h" +#include "storm/solver/IterativeMinMaxLinearEquationSolver.h" #include "storm/solver/TopologicalMinMaxLinearEquationSolver.h" #include "storm/settings/SettingsManager.h" @@ -131,8 +131,8 @@ namespace storm { } template - MinMaxLinearEquationSolverFactory::MinMaxLinearEquationSolverFactory(bool trackScheduler) : trackScheduler(trackScheduler) { - // Intentionally left empty. + MinMaxLinearEquationSolverFactory::MinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : trackScheduler(trackScheduler) { + setMinMaxMethod(method); } template @@ -151,7 +151,26 @@ namespace storm { } template - GeneralMinMaxLinearEquationSolverFactory::GeneralMinMaxLinearEquationSolverFactory(bool trackScheduler) : MinMaxLinearEquationSolverFactory(trackScheduler) { + void MinMaxLinearEquationSolverFactory::setMinMaxMethod(MinMaxMethodSelection const& newMethod) { + if (newMethod == MinMaxMethodSelection::FROMSETTINGS) { + setMinMaxMethod(storm::settings::getModule().getMinMaxEquationSolvingMethod()); + } else { + setMinMaxMethod(convert(newMethod)); + } + } + + template + void MinMaxLinearEquationSolverFactory::setMinMaxMethod(MinMaxMethod const& newMethod) { + method = newMethod; + } + + template + MinMaxMethod const& MinMaxLinearEquationSolverFactory::getMinMaxMethod() const { + return method; + } + + template + GeneralMinMaxLinearEquationSolverFactory::GeneralMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : MinMaxLinearEquationSolverFactory(method, trackScheduler) { // Intentionally left empty. } @@ -169,9 +188,11 @@ namespace storm { template std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { std::unique_ptr> result; - auto method = storm::settings::getModule().getMinMaxEquationSolvingMethod(); + auto method = this->getMinMaxMethod(); if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic) { - result = std::make_unique>(std::forward(matrix), std::make_unique>()); + IterativeMinMaxLinearEquationSolverSettings iterativeSolverSettings; + iterativeSolverSettings.setSolutionMethod(method); + result = std::make_unique>(std::forward(matrix), std::make_unique>(), iterativeSolverSettings); } else if (method == MinMaxMethod::Topological) { result = std::make_unique>(std::forward(matrix)); } else { @@ -186,9 +207,11 @@ namespace storm { template std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { std::unique_ptr> result; - auto method = storm::settings::getModule().getMinMaxEquationSolvingMethod(); + auto method = this->getMinMaxMethod(); STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic, storm::exceptions::InvalidSettingsException, "For this data type only value iteration, policy iteration, and acyclic value iteration are available."); - return std::make_unique>(std::forward(matrix), std::make_unique>()); + IterativeMinMaxLinearEquationSolverSettings iterativeSolverSettings; + iterativeSolverSettings.setSolutionMethod(method); + return std::make_unique>(std::forward(matrix), std::make_unique>(), iterativeSolverSettings); } #endif template class MinMaxLinearEquationSolver; diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 1b869d165..7b4aa18a1 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -196,22 +196,28 @@ namespace storm { template class MinMaxLinearEquationSolverFactory { public: - MinMaxLinearEquationSolverFactory(bool trackScheduler = false); + 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&& matrix) const; void setTrackScheduler(bool value); bool isTrackSchedulerSet() const; + + virtual void setMinMaxMethod(MinMaxMethodSelection const& newMethod); + virtual void setMinMaxMethod(MinMaxMethod const& newMethod); + + MinMaxMethod const& getMinMaxMethod() const; private: bool trackScheduler; + MinMaxMethod method; }; template class GeneralMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory { public: - GeneralMinMaxLinearEquationSolverFactory(bool trackScheduler = false); + 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; diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index 627dcd131..6b0f140ce 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -1,8 +1,6 @@ #include "storm/solver/StandardMinMaxLinearEquationSolver.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/MinMaxEquationSolverSettings.h" - +#include "storm/solver/IterativeMinMaxLinearEquationSolver.h" #include "storm/solver/GmmxxLinearEquationSolver.h" #include "storm/solver/EigenLinearEquationSolver.h" #include "storm/solver/NativeLinearEquationSolver.h" @@ -17,395 +15,18 @@ namespace storm { namespace solver { template - StandardMinMaxLinearEquationSolverSettings::StandardMinMaxLinearEquationSolverSettings() { - // Get the settings object to customize linear solving. - storm::settings::modules::MinMaxEquationSolverSettings const& settings = storm::settings::getModule(); - - maximalNumberOfIterations = settings.getMaximalIterationCount(); - precision = storm::utility::convertNumber(settings.getPrecision()); - relative = settings.getConvergenceCriterion() == storm::settings::modules::MinMaxEquationSolverSettings::ConvergenceCriterion::Relative; - - auto method = settings.getMinMaxEquationSolvingMethod(); - switch (method) { - case MinMaxMethod::ValueIteration: this->solutionMethod = SolutionMethod::ValueIteration; break; - case MinMaxMethod::PolicyIteration: this->solutionMethod = SolutionMethod::PolicyIteration; break; - case MinMaxMethod::Acyclic: this->solutionMethod = SolutionMethod::Acyclic; break; - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); - } - } - - template - void StandardMinMaxLinearEquationSolverSettings::setSolutionMethod(SolutionMethod const& solutionMethod) { - this->solutionMethod = solutionMethod; - } - - template - void StandardMinMaxLinearEquationSolverSettings::setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations) { - this->maximalNumberOfIterations = maximalNumberOfIterations; - } - - template - void StandardMinMaxLinearEquationSolverSettings::setRelativeTerminationCriterion(bool value) { - this->relative = value; - } - - template - void StandardMinMaxLinearEquationSolverSettings::setPrecision(ValueType precision) { - this->precision = precision; - } - - template - typename StandardMinMaxLinearEquationSolverSettings::SolutionMethod const& StandardMinMaxLinearEquationSolverSettings::getSolutionMethod() const { - return solutionMethod; - } - - template - uint64_t StandardMinMaxLinearEquationSolverSettings::getMaximalNumberOfIterations() const { - return maximalNumberOfIterations; - } - - template - ValueType StandardMinMaxLinearEquationSolverSettings::getPrecision() const { - return precision; - } - - template - bool StandardMinMaxLinearEquationSolverSettings::getRelativeTerminationCriterion() const { - return relative; - } - - template - StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings const& settings) : settings(settings), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(nullptr), A(A) { + StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(nullptr), A(A) { // Intentionally left empty. } template - StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings const& settings) : settings(settings), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(std::make_unique>(std::move(A))), A(*localA) { + StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(std::make_unique>(std::move(A))), A(*localA) { // Intentionally left empty. } - template - bool StandardMinMaxLinearEquationSolver::solveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b) const { - switch (this->getSettings().getSolutionMethod()) { - case StandardMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration: - return solveEquationsValueIteration(dir, x, b); - case StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration: - return solveEquationsPolicyIteration(dir, x, b); - case StandardMinMaxLinearEquationSolverSettings::SolutionMethod::Acyclic: - return solveEquationsAcyclic(dir, x, b); - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "This solver does not implement the selected solution method"); - } - return false; - } - - template - bool StandardMinMaxLinearEquationSolver::solveEquationsPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const { - // Create the initial scheduler. - std::vector scheduler = this->hasSchedulerHint() ? this->choicesHint.get() : std::vector(this->A.getRowGroupCount()); - - // Get a vector for storing the right-hand side of the inner equation system. - if(!auxiliaryRowGroupVector) { - auxiliaryRowGroupVector = std::make_unique>(this->A.getRowGroupCount()); - } - std::vector& subB = *auxiliaryRowGroupVector; - - // Resolve the nondeterminism according to the current scheduler. - storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(scheduler, true); - submatrix.convertToEquationSystem(); - storm::utility::vector::selectVectorValues(subB, scheduler, this->A.getRowGroupIndices(), b); - - // Create a solver that we will use throughout the procedure. We will modify the matrix in each iteration. - auto solver = linearEquationSolverFactory->create(std::move(submatrix)); - if (this->lowerBound) { - solver->setLowerBound(this->lowerBound.get()); - } - if (this->upperBound) { - solver->setUpperBound(this->upperBound.get()); - } - solver->setCachingEnabled(true); - - Status status = Status::InProgress; - uint64_t iterations = 0; - do { - // Solve the equation system for the 'DTMC'. - // FIXME: we need to remove the 0- and 1- states to make the solution unique. - // HOWEVER: if we start with a valid scheduler, then we will never get an illegal one, because staying - // within illegal MECs will never strictly improve the value. Is this true? - solver->solveEquations(x, subB); - - // Go through the multiplication result and see whether we can improve any of the choices. - bool schedulerImproved = false; - for (uint_fast64_t group = 0; group < this->A.getRowGroupCount(); ++group) { - uint_fast64_t currentChoice = scheduler[group]; - for (uint_fast64_t choice = this->A.getRowGroupIndices()[group]; choice < this->A.getRowGroupIndices()[group + 1]; ++choice) { - // If the choice is the currently selected one, we can skip it. - if (choice - this->A.getRowGroupIndices()[group] == currentChoice) { - continue; - } - - // Create the value of the choice. - ValueType choiceValue = storm::utility::zero(); - for (auto const& entry : this->A.getRow(choice)) { - choiceValue += entry.getValue() * x[entry.getColumn()]; - } - choiceValue += b[choice]; - - // If the value is strictly better than the solution of the inner system, we need to improve the scheduler. - // TODO: If the underlying solver is not precise, this might run forever (i.e. when a state has two choices where the (exact) values are equal). - // only changing the scheduler if the values are not equal (modulo precision) would make this unsound. - if (valueImproved(dir, x[group], choiceValue)) { - schedulerImproved = true; - scheduler[group] = choice - this->A.getRowGroupIndices()[group]; - x[group] = std::move(choiceValue); - } - } - } - - // If the scheduler did not improve, we are done. - if (!schedulerImproved) { - status = Status::Converged; - } else { - // Update the scheduler and the solver. - submatrix = this->A.selectRowsFromRowGroups(scheduler, true); - submatrix.convertToEquationSystem(); - storm::utility::vector::selectVectorValues(subB, scheduler, this->A.getRowGroupIndices(), b); - solver->setMatrix(std::move(submatrix)); - } - - // Update environment variables. - ++iterations; - status = updateStatusIfNotConverged(status, x, iterations); - } while (status == Status::InProgress); - - reportStatus(status, iterations); - - // If requested, we store the scheduler for retrieval. - if (this->isTrackSchedulerSet()) { - this->schedulerChoices = std::move(scheduler); - } - - if(!this->isCachingEnabled()) { - clearCache(); - } - - return status == Status::Converged || status == Status::TerminatedEarly; - } - - template - bool StandardMinMaxLinearEquationSolver::valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const { - if (dir == OptimizationDirection::Minimize) { - return value2 < value1; - } else { - return value2 > value1; - } - } - - template - ValueType StandardMinMaxLinearEquationSolver::getPrecision() const { - return this->getSettings().getPrecision(); - } - - template - bool StandardMinMaxLinearEquationSolver::getRelative() const { - return this->getSettings().getRelativeTerminationCriterion(); - } - - template - bool StandardMinMaxLinearEquationSolver::solveEquationsValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const { - if(!linEqSolverA) { - linEqSolverA = linearEquationSolverFactory->create(A); - linEqSolverA->setCachingEnabled(true); - } - - if (!auxiliaryRowVector) { - auxiliaryRowVector = std::make_unique>(A.getRowCount()); - } - std::vector& multiplyResult = *auxiliaryRowVector; - - if (!auxiliaryRowGroupVector) { - auxiliaryRowGroupVector = std::make_unique>(A.getRowGroupCount()); - } - - if (this->hasSchedulerHint()) { - // Resolve the nondeterminism according to the scheduler hint - storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->choicesHint.get(), true); - submatrix.convertToEquationSystem(); - storm::utility::vector::selectVectorValues(*auxiliaryRowGroupVector, this->choicesHint.get(), this->A.getRowGroupIndices(), b); - - // Solve the resulting equation system. - // Note that the linEqSolver might consider a slightly different interpretation of "equalModuloPrecision". Hence, we iteratively increase its precision. - auto submatrixSolver = linearEquationSolverFactory->create(std::move(submatrix)); - submatrixSolver->setCachingEnabled(true); - if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); } - if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); } - submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector); - } - - std::vector* newX = auxiliaryRowGroupVector.get(); - - std::vector* currentX = &x; - - // Proceed with the iterations as long as the method did not converge or reach the maximum number of iterations. - uint64_t iterations = 0; - - Status status = Status::InProgress; - while (status == Status::InProgress) { - // Compute x' = A*x + b. - linEqSolverA->multiply(*currentX, &b, multiplyResult); - - // Reduce the vector x' by applying min/max for all non-deterministic choices. - storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, *newX, this->A.getRowGroupIndices()); - - // Determine whether the method converged. - if (storm::utility::vector::equalModuloPrecision(*currentX, *newX, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion())) { - status = Status::Converged; - } - - // Update environment variables. - std::swap(currentX, newX); - ++iterations; - status = updateStatusIfNotConverged(status, *currentX, iterations); - } - - reportStatus(status, iterations); - - // 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 (currentX == auxiliaryRowGroupVector.get()) { - std::swap(x, *currentX); - } - - // If requested, we store the scheduler for retrieval. - if (this->isTrackSchedulerSet()) { - // Due to a custom termination condition, it may be the case that no iterations are performed. In this - // case we need to compute x'= A*x+b once. - if (iterations==0) { - linEqSolverA->multiply(x, &b, multiplyResult); - } - this->schedulerChoices = std::vector(this->A.getRowGroupCount()); - // Reduce the multiplyResult and keep track of the choices made - storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A.getRowGroupIndices(), &this->schedulerChoices.get()); - } - - if (!this->isCachingEnabled()) { - clearCache(); - } - - return status == Status::Converged || status == Status::TerminatedEarly; - } - - template - bool StandardMinMaxLinearEquationSolver::solveEquationsAcyclic(OptimizationDirection dir, std::vector& x, std::vector const& b) const { - uint64_t numGroups = this->A.getRowGroupCount(); - - // Allocate memory for the scheduler (if required) - if (this->isTrackSchedulerSet()) { - if (this->schedulerChoices) { - this->schedulerChoices->resize(numGroups); - } else { - this->schedulerChoices = std::vector(numGroups); - } - } - - // We now compute a topological sort of the row groups. - // If caching is enabled, it might be possible to obtain this sort from the cache. - if (this->isCachingEnabled()) { - if (rowGroupOrdering) { - for (auto const& group : *rowGroupOrdering) { - computeOptimalValueForRowGroup(group, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[group] : nullptr); - } - return true; - } else { - rowGroupOrdering = std::make_unique>(); - rowGroupOrdering->reserve(numGroups); - } - } - - auto transposedMatrix = this->A.transpose(true); - - // We store the groups that have already been processed, i.e., the groups for which x[group] was already set to the correct value. - storm::storage::BitVector processedGroups(numGroups, false); - // Furthermore, we keep track of all candidate groups for which we still need to check whether this group can be processed now. - // A group can be processed if all successors have already been processed. - // Notice that the BitVector candidates is considered in a reversed way, i.e., group i is a candidate iff candidates.get(numGroups - i - 1) is true. - // This is due to the observation that groups with higher indices usually need to be processed earlier. - storm::storage::BitVector candidates(numGroups, true); - uint64_t candidate = numGroups - 1; - for (uint64_t numCandidates = candidates.size(); numCandidates > 0; --numCandidates) { - candidates.set(numGroups - candidate - 1, false); - - // Check if the candidate row group has an unprocessed successor - bool hasUnprocessedSuccessor = false; - for (auto const& entry : this->A.getRowGroup(candidate)) { - if (!processedGroups.get(entry.getColumn())) { - hasUnprocessedSuccessor = true; - break; - } - } - - uint64_t nextCandidate = numGroups - candidates.getNextSetIndex(numGroups - candidate - 1 + 1) - 1; - - if (!hasUnprocessedSuccessor) { - // This candidate can be processed. - processedGroups.set(candidate); - computeOptimalValueForRowGroup(candidate, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[candidate] : nullptr); - if (this->isCachingEnabled()) { - rowGroupOrdering->push_back(candidate); - } - - // Add new candidates - for (auto const& predecessorEntry : transposedMatrix.getRow(candidate)) { - uint64_t predecessor = predecessorEntry.getColumn(); - if (!candidates.get(numGroups - predecessor - 1)) { - candidates.set(numGroups - predecessor - 1, true); - nextCandidate = std::max(nextCandidate, predecessor); - ++numCandidates; - } - } - } - candidate = nextCandidate; - } - - assert(candidates.empty()); - STORM_LOG_THROW(processedGroups.full(), storm::exceptions::InvalidOperationException, "The MinMax equation system is not acyclic."); - return true; - } - - template - void StandardMinMaxLinearEquationSolver::computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector& x, std::vector const& b, uint_fast64_t* choice) const { - uint64_t row = this->A.getRowGroupIndices()[group]; - uint64_t groupEnd = this->A.getRowGroupIndices()[group + 1]; - assert(row != groupEnd); - - auto bIt = b.begin() + row; - ValueType& xi = x[group]; - xi = this->A.multiplyRowWithVector(row, x) + *bIt; - uint64_t optimalRow = row; - - for (++row, ++bIt; row < groupEnd; ++row, ++bIt) { - ValueType choiceVal = this->A.multiplyRowWithVector(row, x) + *bIt; - if (minimize(dir)) { - if (choiceVal < xi) { - xi = choiceVal; - optimalRow = row; - } - } else { - if (choiceVal > xi) { - xi = choiceVal; - optimalRow = row; - } - } - } - if (choice != nullptr) { - *choice = optimalRow - this->A.getRowGroupIndices()[group]; - } - } - template void StandardMinMaxLinearEquationSolver::repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const { - if(!linEqSolverA) { + if (!linEqSolverA) { linEqSolverA = linearEquationSolverFactory->create(A); linEqSolverA->setCachingEnabled(true); } @@ -423,65 +44,30 @@ namespace storm { storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A.getRowGroupIndices()); } - if(!this->isCachingEnabled()) { + if (!this->isCachingEnabled()) { clearCache(); } } - template - typename StandardMinMaxLinearEquationSolver::Status StandardMinMaxLinearEquationSolver::updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations) const { - if (status != Status::Converged) { - if (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x)) { - status = Status::TerminatedEarly; - } else if (iterations >= this->getSettings().getMaximalNumberOfIterations()) { - status = Status::MaximalIterationsExceeded; - } - } - return status; - } - - template - void StandardMinMaxLinearEquationSolver::reportStatus(Status status, uint64_t iterations) const { - switch (status) { - case Status::Converged: STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations."); break; - case Status::TerminatedEarly: STORM_LOG_INFO("Iterative solver terminated early after " << iterations << " iterations."); break; - case Status::MaximalIterationsExceeded: STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations."); break; - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Iterative solver terminated unexpectedly."); - } - } - - template - StandardMinMaxLinearEquationSolverSettings const& StandardMinMaxLinearEquationSolver::getSettings() const { - return settings; - } - - template - void StandardMinMaxLinearEquationSolver::setSettings(StandardMinMaxLinearEquationSolverSettings const& newSettings) { - settings = newSettings; - } - template void StandardMinMaxLinearEquationSolver::clearCache() const { linEqSolverA.reset(); auxiliaryRowVector.reset(); - auxiliaryRowGroupVector.reset(); - rowGroupOrdering.reset(); MinMaxLinearEquationSolver::clearCache(); } template - StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(bool trackScheduler) : MinMaxLinearEquationSolverFactory(trackScheduler), linearEquationSolverFactory(nullptr) { + StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : MinMaxLinearEquationSolverFactory(method, trackScheduler), linearEquationSolverFactory(std::make_unique>()) { // Intentionally left empty. } template - StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, bool trackScheduler) : MinMaxLinearEquationSolverFactory(trackScheduler), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, MinMaxMethodSelection const& method, bool trackScheduler) : MinMaxLinearEquationSolverFactory(method, trackScheduler), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } template - StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, bool trackScheduler) : MinMaxLinearEquationSolverFactory(trackScheduler) { + StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, MinMaxMethodSelection const& method, bool trackScheduler) : MinMaxLinearEquationSolverFactory(method, trackScheduler) { switch (solverType) { case EquationSolverType::Gmmxx: linearEquationSolverFactory = std::make_unique>(); break; case EquationSolverType::Eigen: linearEquationSolverFactory = std::make_unique>(); break; @@ -492,7 +78,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, bool trackScheduler) : MinMaxLinearEquationSolverFactory(trackScheduler) { + 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; @@ -504,63 +90,58 @@ namespace storm { 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; - if (linearEquationSolverFactory) { - result = std::make_unique>(matrix, linearEquationSolverFactory->clone(), settings); + 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 { - result = std::make_unique>(matrix, std::make_unique>(), settings); - } - if (this->isTrackSchedulerSet()) { - result->setTrackScheduler(true); + 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> result; - if (linearEquationSolverFactory) { - result = std::make_unique>(std::move(matrix), linearEquationSolverFactory->clone(), settings); + 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); } else { - result = std::make_unique>(std::move(matrix), std::make_unique>(), settings); - } - if (this->isTrackSchedulerSet()) { - result->setTrackScheduler(true); + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); } + result->setTrackScheduler(this->isTrackSchedulerSet()); return result; } template - StandardMinMaxLinearEquationSolverSettings& StandardMinMaxLinearEquationSolverFactory::getSettings() { - return settings; - } - - template - StandardMinMaxLinearEquationSolverSettings const& StandardMinMaxLinearEquationSolverFactory::getSettings() const { - return settings; - } - - template - GmmxxMinMaxLinearEquationSolverFactory::GmmxxMinMaxLinearEquationSolverFactory(bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Gmmxx, trackScheduler) { + GmmxxMinMaxLinearEquationSolverFactory::GmmxxMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Gmmxx, method, trackScheduler) { // Intentionally left empty. } template - EigenMinMaxLinearEquationSolverFactory::EigenMinMaxLinearEquationSolverFactory(bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Eigen, trackScheduler) { + EigenMinMaxLinearEquationSolverFactory::EigenMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Eigen, method, trackScheduler) { // Intentionally left empty. } template - NativeMinMaxLinearEquationSolverFactory::NativeMinMaxLinearEquationSolverFactory(bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Native, trackScheduler) { + NativeMinMaxLinearEquationSolverFactory::NativeMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Native, method, trackScheduler) { // Intentionally left empty. } template - EliminationMinMaxLinearEquationSolverFactory::EliminationMinMaxLinearEquationSolverFactory(bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Elimination, trackScheduler) { + EliminationMinMaxLinearEquationSolverFactory::EliminationMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Elimination, method, trackScheduler) { // Intentionally left empty. } - template class StandardMinMaxLinearEquationSolverSettings; template class StandardMinMaxLinearEquationSolver; template class StandardMinMaxLinearEquationSolverFactory; template class GmmxxMinMaxLinearEquationSolverFactory; @@ -569,7 +150,6 @@ namespace storm { template class EliminationMinMaxLinearEquationSolverFactory; #ifdef STORM_HAVE_CARL - template class StandardMinMaxLinearEquationSolverSettings; template class StandardMinMaxLinearEquationSolver; template class StandardMinMaxLinearEquationSolverFactory; template class EigenMinMaxLinearEquationSolverFactory; diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.h b/src/storm/solver/StandardMinMaxLinearEquationSolver.h index 050ce0bde..1305f3e26 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.h +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.h @@ -6,72 +6,23 @@ namespace storm { namespace solver { - template - class StandardMinMaxLinearEquationSolverSettings { - public: - StandardMinMaxLinearEquationSolverSettings(); - - enum class SolutionMethod { - ValueIteration, PolicyIteration, Acyclic - }; - - void setSolutionMethod(SolutionMethod const& solutionMethod); - void setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations); - void setRelativeTerminationCriterion(bool value); - void setPrecision(ValueType precision); - - SolutionMethod const& getSolutionMethod() const; - uint64_t getMaximalNumberOfIterations() const; - ValueType getPrecision() const; - bool getRelativeTerminationCriterion() const; - - private: - SolutionMethod solutionMethod; - uint64_t maximalNumberOfIterations; - ValueType precision; - bool relative; - }; - template class StandardMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver { public: - StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings const& settings = StandardMinMaxLinearEquationSolverSettings()); - StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings const& settings = StandardMinMaxLinearEquationSolverSettings()); + StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory); + StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory); + + virtual ~StandardMinMaxLinearEquationSolver() = default; - 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; - StandardMinMaxLinearEquationSolverSettings const& getSettings() const; - void setSettings(StandardMinMaxLinearEquationSolverSettings const& newSettings); - virtual void clearCache() const override; - virtual ValueType getPrecision() const override; - virtual bool getRelative() const override; - private: - bool solveEquationsPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const; - bool solveEquationsValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const; - bool solveEquationsAcyclic(OptimizationDirection dir, std::vector& x, std::vector const& b) const; - - bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const; - - void computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector& x, std::vector const& b, uint_fast64_t* choice = nullptr) const; - - enum class Status { - Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress - }; + protected: // possibly cached data mutable std::unique_ptr> linEqSolverA; mutable std::unique_ptr> auxiliaryRowVector; // A.rowCount() entries - mutable std::unique_ptr> auxiliaryRowGroupVector; // A.rowGroupCount() entries - mutable std::unique_ptr> rowGroupOrdering; // A.rowGroupCount() entries - - Status updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations) const; - void reportStatus(Status status, uint64_t iterations) const; - - /// The settings of this solver. - StandardMinMaxLinearEquationSolverSettings settings; /// The factory used to obtain linear equation solvers. std::unique_ptr> linearEquationSolverFactory; @@ -89,44 +40,39 @@ namespace storm { template class StandardMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory { public: - StandardMinMaxLinearEquationSolverFactory(bool trackScheduler = false); - StandardMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, bool trackScheduler = false); - StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, bool trackScheduler = false); + StandardMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false); + 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; - StandardMinMaxLinearEquationSolverSettings& getSettings(); - StandardMinMaxLinearEquationSolverSettings const& getSettings() const; - - private: - StandardMinMaxLinearEquationSolverSettings settings; - + protected: std::unique_ptr> linearEquationSolverFactory; }; template class GmmxxMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory { public: - GmmxxMinMaxLinearEquationSolverFactory(bool trackScheduler = false); + GmmxxMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false); }; template class EigenMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory { public: - EigenMinMaxLinearEquationSolverFactory(bool trackScheduler = false); + EigenMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false); }; template class NativeMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory { public: - NativeMinMaxLinearEquationSolverFactory(bool trackScheduler = false); + NativeMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false); }; template class EliminationMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory { public: - EliminationMinMaxLinearEquationSolverFactory(bool trackScheduler = false); + EliminationMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false); }; } diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index d47bff510..e320f3497 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -458,7 +458,7 @@ namespace storm { } template - TopologicalMinMaxLinearEquationSolverFactory::TopologicalMinMaxLinearEquationSolverFactory(bool trackScheduler) : MinMaxLinearEquationSolverFactory(trackScheduler) { + TopologicalMinMaxLinearEquationSolverFactory::TopologicalMinMaxLinearEquationSolverFactory(bool trackScheduler) : MinMaxLinearEquationSolverFactory(MinMaxMethodSelection::Topological, trackScheduler) { // Intentionally left empty. } diff --git a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 8ddc74d27..3d590ef74 100644 --- a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -209,8 +209,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { EXPECT_EQ(7ull, mdp->getNumberOfChoices()); - auto solverFactory = std::make_unique>(); - solverFactory->getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration); + auto solverFactory = std::make_unique>(storm::solver::MinMaxMethodSelection::PolicyIteration); storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::move(solverFactory)); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); diff --git a/src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp index b30f329ba..da68456fe 100644 --- a/src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp +++ b/src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp @@ -109,8 +109,7 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithPolicyIteration) { std::vector x(1); std::vector b = { 0.099, 0.5 }; - auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory(); - factory.getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration); + auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory(storm::solver::MinMaxMethodSelection::PolicyIteration); auto solver = factory.create(A); ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); diff --git a/src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp index 75f0ddd23..de724e39f 100644 --- a/src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp +++ b/src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp @@ -80,8 +80,7 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithPolicyIteration) { std::vector x(1); std::vector b = { 0.099, 0.5 }; - auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory(); - factory.getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration); + auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory(storm::solver::MinMaxMethodSelection::PolicyIteration); auto solver = factory.create(A); ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b));