From a8c6c62275ed0ff5edb40a78a34cfe0510db400f Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 10 Oct 2017 20:22:00 +0200 Subject: [PATCH] rational search working for symbolic MDPs --- .../SymbolicMinMaxLinearEquationSolver.cpp | 39 +++++++++++-------- .../SymbolicMinMaxLinearEquationSolver.h | 3 ++ 2 files changed, 25 insertions(+), 17 deletions(-) diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index 44ba169c6..bee9c20c6 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -13,6 +13,7 @@ #include "storm/utility/dd.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidSettingsException.h" +#include "storm/exceptions/PrecisionExceededException.h" namespace storm { namespace solver { @@ -82,7 +83,7 @@ namespace storm { } template - SymbolicMinMaxLinearEquationSolver::SymbolicMinMaxLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs, std::unique_ptr>&& linearEquationSolverFactory, SymbolicMinMaxLinearEquationSolverSettings const& settings) : A(A), allRows(allRows), illegalMaskAdd(illegalMask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), settings(settings), requirementsChecked(false) { + SymbolicMinMaxLinearEquationSolver::SymbolicMinMaxLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs, std::unique_ptr>&& linearEquationSolverFactory, SymbolicMinMaxLinearEquationSolverSettings const& settings) : A(A), allRows(allRows), illegalMask(illegalMask), illegalMaskAdd(illegalMask.ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), settings(settings), requirementsChecked(false) { // Intentionally left empty. } @@ -111,7 +112,7 @@ namespace storm { // Value iteration loop. SolverStatus status = SolverStatus::InProgress; - while (status == SolverStatus::Converged && iterations < this->settings.getMaximalNumberOfIterations()) { + while (status == SolverStatus::InProgress && iterations < this->settings.getMaximalNumberOfIterations()) { // Compute tmp = A * x + b storm::dd::Add localXAsColumn = localX.swapVariables(this->rowColumnMetaVariablePairs); storm::dd::Add tmp = this->A.multiplyMatrix(localXAsColumn, this->columnMetaVariables); @@ -164,7 +165,7 @@ namespace storm { storm::dd::Add sharpenedX; for (uint64_t p = 1; p < precision; ++p) { - storm::dd::Add sharpenedX = x.sharpenKwekMehlhorn(precision); + sharpenedX = x.sharpenKwekMehlhorn(precision); isSolution = rationalSolver.isSolution(dir, sharpenedX, rationalB); if (isSolution) { @@ -200,7 +201,7 @@ namespace storm { uint64_t p = storm::utility::convertNumber(storm::utility::ceil(storm::utility::log10(storm::utility::one() / precision))); bool isSolution = false; - storm::dd::Add sharpenedX = sharpen(dir, p, rationalSolver, viResult.values, rationalB, isSolution); + sharpenedX = sharpen(dir, p, rationalSolver, viResult.values, rationalB, isSolution); if (isSolution) { status = SolverStatus::Converged; @@ -218,7 +219,7 @@ namespace storm { } else { STORM_LOG_WARN("Iterative solver (rational search) did not converge in " << overallIterations << " iterations."); } - + return sharpenedX; } @@ -226,12 +227,7 @@ namespace storm { template typename std::enable_if::value && storm::NumberTraits::IsExact, storm::dd::Add>::type SymbolicMinMaxLinearEquationSolver::solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const { - storm::dd::Add rationalX = x.template toValueType(); - storm::dd::Add rationalB = b.template toValueType(); - SymbolicMinMaxLinearEquationSolver rationalSolver; - - storm::dd::Add rationalResult = solveEquationsRationalSearchHelper(dir, *this, *this, rationalX, rationalB, x, b); - return rationalResult.template toValueType(); + return solveEquationsRationalSearchHelper(dir, *this, *this, x, b, x, b); } template @@ -240,7 +236,7 @@ namespace storm { storm::dd::Add rationalX = x.template toValueType(); storm::dd::Add rationalB = b.template toValueType(); - SymbolicMinMaxLinearEquationSolver rationalSolver; + SymbolicMinMaxLinearEquationSolver rationalSolver(this->A.template toValueType(), this->allRows, this->illegalMask, this->rowMetaVariables, this->columnMetaVariables, this->choiceVariables, this->rowColumnMetaVariablePairs, std::make_unique>()); storm::dd::Add rationalResult = solveEquationsRationalSearchHelper(dir, rationalSolver, *this, rationalX, rationalB, x, b); return rationalResult.template toValueType(); @@ -250,11 +246,20 @@ namespace storm { template typename std::enable_if::value, storm::dd::Add>::type SymbolicMinMaxLinearEquationSolver::solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const { - storm::dd::Add impreciseX = x.template toValueType(); - storm::dd::Add impreciseB = b.template toValueType(); - SymbolicMinMaxLinearEquationSolver impreciseSolver; - - storm::dd::Add rationalResult = solveEquationsRationalSearchHelper(dir, *this, impreciseSolver, x, b, impreciseX, impreciseB); + // First try to find a solution using the imprecise value type. + storm::dd::Add rationalResult; + try { + storm::dd::Add impreciseX = x.template toValueType(); + storm::dd::Add impreciseB = b.template toValueType(); + SymbolicMinMaxLinearEquationSolver impreciseSolver(this->A.template toValueType(), this->allRows, this->illegalMask, this->rowMetaVariables, this->columnMetaVariables, this->choiceVariables, this->rowColumnMetaVariablePairs, std::make_unique>()); + + rationalResult = solveEquationsRationalSearchHelper(dir, *this, impreciseSolver, x, b, impreciseX, impreciseB); + } catch (storm::exceptions::PrecisionExceededException const& e) { + STORM_LOG_WARN("Precision of value type was exceeded, trying to recover by switching to rational arithmetic."); + + // Fall back to precise value type if the precision of the imprecise value type was exceeded. + rationalResult = solveEquationsRationalSearchHelper(dir, *this, *this, x, b, x, b); + } return rationalResult.template toValueType(); } diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h index 684c0f67d..408faf21e 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h @@ -186,6 +186,9 @@ namespace storm { // A BDD characterizing all rows of the equation system. storm::dd::Bdd allRows; + // A BDD characterizing the illegal choices. + storm::dd::Bdd illegalMask; + // An ADD characterizing the illegal choices. storm::dd::Add illegalMaskAdd;