diff --git a/src/storm/environment/solver/SolverEnvironment.cpp b/src/storm/environment/solver/SolverEnvironment.cpp index 6e0eb49c0..b9635757c 100644 --- a/src/storm/environment/solver/SolverEnvironment.cpp +++ b/src/storm/environment/solver/SolverEnvironment.cpp @@ -13,6 +13,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/InvalidEnvironmentException.h" +#include "storm/exceptions/UnexpectedException.h" namespace storm { @@ -87,8 +88,8 @@ namespace storm { return linearEquationSolverType; } - void SolverEnvironment::setLinearEquationSolverType(storm::solver::EquationSolverType const& value) { - linearEquationSolverTypeSetFromDefault = false; + void SolverEnvironment::setLinearEquationSolverType(storm::solver::EquationSolverType const& value, bool assumeSetFromDefault) { + linearEquationSolverTypeSetFromDefault = assumeSetFromDefault; linearEquationSolverType = value; } @@ -96,46 +97,49 @@ namespace storm { return linearEquationSolverTypeSetFromDefault; } - boost::optional SolverEnvironment::getPrecisionOfCurrentLinearEquationSolver() const { - switch (getLinearEquationSolverType()) { + std::pair, boost::optional> SolverEnvironment::getPrecisionOfLinearEquationSolver(storm::solver::EquationSolverType const& solverType) const { + std::pair, boost::optional> result; + switch (solverType) { case storm::solver::EquationSolverType::Gmmxx: - return gmmxx().getPrecision(); + result.first = gmmxx().getPrecision(); + break; case storm::solver::EquationSolverType::Eigen: - return eigen().getPrecision(); + result.first = eigen().getPrecision(); + break; case storm::solver::EquationSolverType::Native: - return native().getPrecision(); + result.first = native().getPrecision(); + result.second = native().getRelativeTerminationCriterion(); + break; case storm::solver::EquationSolverType::Elimination: - return boost::none; + break; + case storm::solver::EquationSolverType::Topological: + result = getPrecisionOfLinearEquationSolver(topological().getUnderlyingSolverType()); + break; default: - STORM_LOG_ASSERT(false, "The selected solver type is unknown."); + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The selected solver type is unknown."); } + return result; } - void SolverEnvironment::setLinearEquationSolverPrecision(storm::RationalNumber const& value) { + void SolverEnvironment::setLinearEquationSolverPrecision(boost::optional const& newPrecision, boost::optional const& relativePrecision) { + // Assert that each solver type is handled in this method. STORM_LOG_ASSERT(getLinearEquationSolverType() == storm::solver::EquationSolverType::Native || getLinearEquationSolverType() == storm::solver::EquationSolverType::Gmmxx || getLinearEquationSolverType() == storm::solver::EquationSolverType::Eigen || getLinearEquationSolverType() == storm::solver::EquationSolverType::Elimination || getLinearEquationSolverType() == storm::solver::EquationSolverType::Topological, "The current solver type is not respected in this method."); - native().setPrecision(value); - gmmxx().setPrecision(value); - eigen().setPrecision(value); - // Elimination and Topological solver do not have a precision - } - - void SolverEnvironment::setLinearEquationSolverRelativeTerminationCriterion(bool value) { - STORM_LOG_ASSERT(getLinearEquationSolverType() == storm::solver::EquationSolverType::Native || - getLinearEquationSolverType() == storm::solver::EquationSolverType::Gmmxx || - getLinearEquationSolverType() == storm::solver::EquationSolverType::Eigen || - getLinearEquationSolverType() == storm::solver::EquationSolverType::Elimination || - getLinearEquationSolverType() == storm::solver::EquationSolverType::Topological, - "The current solver type is not respected in this method."); - native().setRelativeTerminationCriterion(value); - // Elimination, gmm, eigen, and topological solver do not have an option for relative termination criterion + if (newPrecision) { + native().setPrecision(newPrecision.get()); + gmmxx().setPrecision(newPrecision.get()); + eigen().setPrecision(newPrecision.get()); + // Elimination and Topological solver do not have a precision + } + if (relativePrecision) { + native().setRelativeTerminationCriterion(relativePrecision.get()); + // gmm, eigen, elimination, and topological solvers do not have a precision + } } - - } diff --git a/src/storm/environment/solver/SolverEnvironment.h b/src/storm/environment/solver/SolverEnvironment.h index 7f3260291..614fd1d02 100644 --- a/src/storm/environment/solver/SolverEnvironment.h +++ b/src/storm/environment/solver/SolverEnvironment.h @@ -41,12 +41,11 @@ namespace storm { void setForceSoundness(bool value); storm::solver::EquationSolverType const& getLinearEquationSolverType() const; - void setLinearEquationSolverType(storm::solver::EquationSolverType const& value); + void setLinearEquationSolverType(storm::solver::EquationSolverType const& value, bool assumeSetFromDefault = false); bool isLinearEquationSolverTypeSetFromDefaultValue() const; - - boost::optional getPrecisionOfCurrentLinearEquationSolver() const; - void setLinearEquationSolverPrecision(storm::RationalNumber const& value); - void setLinearEquationSolverRelativeTerminationCriterion(bool value); + + std::pair, boost::optional> getPrecisionOfLinearEquationSolver(storm::solver::EquationSolverType const& solverType) const; + void setLinearEquationSolverPrecision(boost::optional const& newPrecision, boost::optional const& relativePrecision = boost::none); private: SubEnvironment eigenSolverEnvironment; diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index fb71fa43f..059cdb5a8 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -114,19 +114,32 @@ namespace storm { // The solver that we will use throughout the procedure. std::unique_ptr> solver; // The linear equation solver should be at least as precise as this solver - std::unique_ptr environmentOfSolver; - boost::optional precOfSolver = env.solver().getPrecisionOfCurrentLinearEquationSolver(); - if (!storm::NumberTraits::IsExact && precOfSolver && precOfSolver.get() > env.solver().minMax().getPrecision()) { - environmentOfSolver = std::make_unique(env); - environmentOfSolver->solver().setLinearEquationSolverPrecision(env.solver().minMax().getPrecision()); + std::unique_ptr environmentOfSolverStorage; + auto precOfSolver = env.solver().getPrecisionOfLinearEquationSolver(env.solver().getLinearEquationSolverType()); + if (!storm::NumberTraits::IsExact) { + bool changePrecision = precOfSolver.first && precOfSolver.first.get() > env.solver().minMax().getPrecision(); + bool changeRelative = precOfSolver.second && !precOfSolver.second.get() && env.solver().minMax().getRelativeTerminationCriterion(); + if (changePrecision || changeRelative) { + environmentOfSolverStorage = std::make_unique(env); + boost::optional newPrecision; + boost::optional newRelative; + if (changePrecision) { + newPrecision = env.solver().minMax().getPrecision(); + } + if (changeRelative) { + newRelative = true; + } + environmentOfSolverStorage->solver().setLinearEquationSolverPrecision(newPrecision, newRelative); + } } - + storm::Environment const& environmentOfSolver = environmentOfSolverStorage ? *environmentOfSolverStorage : env; + SolverStatus status = SolverStatus::InProgress; uint64_t iterations = 0; this->startMeasureProgress(); do { // Solve the equation system for the 'DTMC'. - solveInducedEquationSystem(environmentOfSolver ? *environmentOfSolver : env, solver, scheduler, x, subB, b); + solveInducedEquationSystem(environmentOfSolver, solver, scheduler, x, subB, b); // Go through the multiplication result and see whether we can improve any of the choices. bool schedulerImproved = false; @@ -311,14 +324,27 @@ namespace storm { // Solve the equation system induced by the initial scheduler. std::unique_ptr> linEqSolver; // The linear equation solver should be at least as precise as this solver - std::unique_ptr environmentOfSolver; - boost::optional precOfSolver = env.solver().getPrecisionOfCurrentLinearEquationSolver(); - if (!storm::NumberTraits::IsExact && precOfSolver && precOfSolver.get() > env.solver().minMax().getPrecision()) { - environmentOfSolver = std::make_unique(env); - environmentOfSolver->solver().setLinearEquationSolverPrecision(env.solver().minMax().getPrecision()); + std::unique_ptr environmentOfSolverStorage; + auto precOfSolver = env.solver().getPrecisionOfLinearEquationSolver(env.solver().getLinearEquationSolverType()); + if (!storm::NumberTraits::IsExact) { + bool changePrecision = precOfSolver.first && precOfSolver.first.get() > env.solver().minMax().getPrecision(); + bool changeRelative = precOfSolver.second && !precOfSolver.second.get() && env.solver().minMax().getRelativeTerminationCriterion(); + if (changePrecision || changeRelative) { + environmentOfSolverStorage = std::make_unique(env); + boost::optional newPrecision; + boost::optional newRelative; + if (changePrecision) { + newPrecision = env.solver().minMax().getPrecision(); + } + if (changeRelative) { + newRelative = true; + } + environmentOfSolverStorage->solver().setLinearEquationSolverPrecision(newPrecision, newRelative); + } } + storm::Environment const& environmentOfSolver = environmentOfSolverStorage ? *environmentOfSolverStorage : env; - solveInducedEquationSystem(environmentOfSolver ? *environmentOfSolver : env, linEqSolver, this->getInitialScheduler(), x, *auxiliaryRowGroupVector, b); + solveInducedEquationSystem(environmentOfSolver, linEqSolver, this->getInitialScheduler(), x, *auxiliaryRowGroupVector, b); // If we were given an initial scheduler and are maximizing (minimizing), our current solution becomes // always less-or-equal (greater-or-equal) than the actual solution. guarantee = maximize(dir) ? SolverGuarantee::LessOrEqual : SolverGuarantee::GreaterOrEqual; diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp index 26d4cc3d0..bd1024a86 100644 --- a/src/storm/solver/StandardGameSolver.cpp +++ b/src/storm/solver/StandardGameSolver.cpp @@ -76,13 +76,34 @@ namespace storm { uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); + // The linear equation solver should be at least as precise as this solver + std::unique_ptr environmentOfSolverStorage; + auto precOfSolver = env.solver().getPrecisionOfLinearEquationSolver(env.solver().getLinearEquationSolverType()); + if (!storm::NumberTraits::IsExact) { + bool changePrecision = precOfSolver.first && precOfSolver.first.get() > env.solver().game().getPrecision(); + bool changeRelative = precOfSolver.second && !precOfSolver.second.get() && env.solver().game().getRelativeTerminationCriterion(); + if (changePrecision || changeRelative) { + environmentOfSolverStorage = std::make_unique(env); + boost::optional newPrecision; + boost::optional newRelative; + if (changePrecision) { + newPrecision = env.solver().game().getPrecision(); + } + if (changeRelative) { + newRelative = true; + } + environmentOfSolverStorage->solver().setLinearEquationSolverPrecision(newPrecision, newRelative); + } + } + storm::Environment const& environmentOfSolver = environmentOfSolverStorage ? *environmentOfSolverStorage : env; + // Solve the equation system induced by the two schedulers. storm::storage::SparseMatrix submatrix; getInducedMatrixVector(x, b, player1Choices, player2Choices, submatrix, subB); - if (this->linearEquationSolverFactory->getEquationProblemFormat(env) == LinearEquationSolverProblemFormat::EquationSystem) { + if (this->linearEquationSolverFactory->getEquationProblemFormat(environmentOfSolver) == LinearEquationSolverProblemFormat::EquationSystem) { submatrix.convertToEquationSystem(); } - auto submatrixSolver = linearEquationSolverFactory->create(env, std::move(submatrix)); + auto submatrixSolver = linearEquationSolverFactory->create(environmentOfSolver, std::move(submatrix)); if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); } if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); } submatrixSolver->setCachingEnabled(true); @@ -92,7 +113,7 @@ namespace storm { do { // Solve the equation system for the 'DTMC'. // FIXME: we need to remove the 0- and 1- states to make the solution unique. - submatrixSolver->solveEquations(env, x, subB); + submatrixSolver->solveEquations(environmentOfSolver, x, subB); bool schedulerImproved = extractChoices(player1Dir, player2Dir, x, b, *auxiliaryP2RowGroupVector, player1Choices, player2Choices); diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index b1501fd32..b599face7 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -244,13 +244,26 @@ namespace storm { // If we were given an initial scheduler, we take its solution as the starting point. if (this->hasInitialScheduler()) { // The linear equation solver should be at least as precise as this solver - std::unique_ptr environmentOfSolver; - boost::optional precOfSolver = env.solver().getPrecisionOfCurrentLinearEquationSolver(); - if (!storm::NumberTraits::IsExact && precOfSolver && precOfSolver.get() > env.solver().minMax().getPrecision()) { - environmentOfSolver = std::make_unique(env); - environmentOfSolver->solver().setLinearEquationSolverPrecision(env.solver().minMax().getPrecision()); + std::unique_ptr environmentOfSolverStorage; + auto precOfSolver = env.solver().getPrecisionOfLinearEquationSolver(env.solver().getLinearEquationSolverType()); + if (!storm::NumberTraits::IsExact) { + bool changePrecision = precOfSolver.first && precOfSolver.first.get() > env.solver().minMax().getPrecision(); + bool changeRelative = precOfSolver.second && !precOfSolver.second.get() && env.solver().minMax().getRelativeTerminationCriterion(); + if (changePrecision || changeRelative) { + environmentOfSolverStorage = std::make_unique(env); + boost::optional newPrecision; + boost::optional newRelative; + if (changePrecision) { + newPrecision = env.solver().minMax().getPrecision(); + } + if (changeRelative) { + newRelative = true; + } + environmentOfSolverStorage->solver().setLinearEquationSolverPrecision(newPrecision, newRelative); + } } - localX = solveEquationsWithScheduler(environmentOfSolver ? *environmentOfSolver : env, this->getInitialScheduler(), x, b); + storm::Environment const& environmentOfSolver = environmentOfSolverStorage ? *environmentOfSolverStorage : env; + localX = solveEquationsWithScheduler(environmentOfSolver, this->getInitialScheduler(), x, b); } else { localX = this->getLowerBoundsVector(); } @@ -311,20 +324,33 @@ namespace storm { // Initialize linear equation solver. // It should be at least as precise as this solver. - std::unique_ptr environmentOfSolver; - boost::optional precOfSolver = env.solver().getPrecisionOfCurrentLinearEquationSolver(); - if (!storm::NumberTraits::IsExact && precOfSolver && precOfSolver.get() > env.solver().minMax().getPrecision()) { - environmentOfSolver = std::make_unique(env); - environmentOfSolver->solver().setLinearEquationSolverPrecision(env.solver().minMax().getPrecision()); + std::unique_ptr environmentOfSolverStorage; + auto precOfSolver = env.solver().getPrecisionOfLinearEquationSolver(env.solver().getLinearEquationSolverType()); + if (!storm::NumberTraits::IsExact) { + bool changePrecision = precOfSolver.first && precOfSolver.first.get() > env.solver().minMax().getPrecision(); + bool changeRelative = precOfSolver.second && !precOfSolver.second.get() && env.solver().minMax().getRelativeTerminationCriterion(); + if (changePrecision || changeRelative) { + environmentOfSolverStorage = std::make_unique(env); + boost::optional newPrecision; + boost::optional newRelative; + if (changePrecision) { + newPrecision = env.solver().minMax().getPrecision(); + } + if (changeRelative) { + newRelative = true; + } + environmentOfSolverStorage->solver().setLinearEquationSolverPrecision(newPrecision, newRelative); + } } + storm::Environment const& environmentOfSolver = environmentOfSolverStorage ? *environmentOfSolverStorage : env; - std::unique_ptr> linearEquationSolver = linearEquationSolverFactory->create(environmentOfSolver ? *environmentOfSolver : env, this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs); + std::unique_ptr> linearEquationSolver = linearEquationSolverFactory->create(environmentOfSolver, this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs); this->forwardBounds(*linearEquationSolver); // Iteratively solve and improve the scheduler. uint64_t maxIter = env.solver().minMax().getMaximalNumberOfIterations(); while (!converged && iterations < maxIter) { - storm::dd::Add schedulerX = solveEquationsWithScheduler(environmentOfSolver ? *environmentOfSolver : env, *linearEquationSolver, scheduler, currentSolution, b, diagonal); + storm::dd::Add schedulerX = solveEquationsWithScheduler(environmentOfSolver, *linearEquationSolver, scheduler, currentSolution, b, diagonal); // Policy improvement step. storm::dd::Add choiceValues = this->A.multiplyMatrix(schedulerX.swapVariables(this->rowColumnMetaVariablePairs), this->columnMetaVariables) + b;