From 3571f0ddcada672ef3bab7ed264f4ec9775059b4 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 25 Oct 2017 19:48:17 +0200 Subject: [PATCH] Respected that the solution is unique when doing value iteration --- src/storm/solver/AbstractEquationSolver.cpp | 22 ++++++++--------- src/storm/solver/AbstractEquationSolver.h | 1 + .../IterativeMinMaxLinearEquationSolver.cpp | 24 ++++++++++++------- .../SymbolicMinMaxLinearEquationSolver.cpp | 12 ++++++---- 4 files changed, 35 insertions(+), 24 deletions(-) diff --git a/src/storm/solver/AbstractEquationSolver.cpp b/src/storm/solver/AbstractEquationSolver.cpp index afbec8ac7..c7fe0bd01 100644 --- a/src/storm/solver/AbstractEquationSolver.cpp +++ b/src/storm/solver/AbstractEquationSolver.cpp @@ -168,6 +168,16 @@ namespace storm { } } + template + void AbstractEquationSolver::createUpperBoundsVector(std::vector& upperBoundsVector) const { + STORM_LOG_ASSERT(this->hasUpperBound(), "Expecting upper bound(s)."); + if (this->hasUpperBound(BoundType::Global)) { + upperBoundsVector.assign(upperBoundsVector.size(), this->getUpperBound()); + } else { + upperBoundsVector.assign(this->getUpperBounds().begin(), this->getUpperBounds().end()); + } + } + template void AbstractEquationSolver::createUpperBoundsVector(std::unique_ptr>& upperBoundsVector, uint64_t length) const { STORM_LOG_ASSERT(this->hasUpperBound(), "Expecting upper bound(s)."); @@ -179,17 +189,7 @@ namespace storm { upperBoundsVector = std::make_unique>(length, this->getUpperBound()); } } else { - if (this->hasUpperBound(BoundType::Global)) { - for (auto& e : *upperBoundsVector) { - e = this->getUpperBound(); - } - } else { - auto upperBoundsIt = this->getUpperBounds().begin(); - for (auto& e : *upperBoundsVector) { - e = *upperBoundsIt; - ++upperBoundsIt; - } - } + createUpperBoundsVector(*upperBoundsVector); } } diff --git a/src/storm/solver/AbstractEquationSolver.h b/src/storm/solver/AbstractEquationSolver.h index 22e9d0f56..98f6895f4 100644 --- a/src/storm/solver/AbstractEquationSolver.h +++ b/src/storm/solver/AbstractEquationSolver.h @@ -160,6 +160,7 @@ namespace storm { TerminationCondition const& getTerminationCondition() const; std::unique_ptr> const& getTerminationConditionPointer() const; + void createUpperBoundsVector(std::vector& upperBoundsVector) const; void createUpperBoundsVector(std::unique_ptr>& upperBoundsVector, uint64_t length) const; void createLowerBoundsVector(std::vector& lowerBoundsVector) const; diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index eb6a970b9..1aa038ebd 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -367,9 +367,8 @@ namespace storm { auxiliaryRowGroupVector = std::make_unique>(this->A->getRowGroupCount()); } - // By default, the guarantee that we can provide is that our solution is always less-or-equal than the - // actual solution. - SolverGuarantee guarantee = SolverGuarantee::LessOrEqual; + // By default, we can not provide any guarantee + SolverGuarantee guarantee = SolverGuarantee::None; if (this->hasInitialScheduler()) { // Resolve the nondeterminism according to the initial scheduler. @@ -391,14 +390,21 @@ namespace storm { } submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector); - // If we were given an initial scheduler and are in fact minimizing, our current solution becomes - // always greater-or-equal than the actual solution. - if (dir == storm::OptimizationDirection::Minimize) { + // 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. + if (dir == storm::OptimizationDirection::Maximize) { + guarantee = SolverGuarantee::LessOrEqual; + } else { + guarantee = SolverGuarantee::GreaterOrEqual; + } + } else if (!this->hasUniqueSolution()) { + if (dir == storm::OptimizationDirection::Maximize) { + this->createLowerBoundsVector(x); + guarantee = SolverGuarantee::LessOrEqual; + } else { + this->createUpperBoundsVector(x); guarantee = SolverGuarantee::GreaterOrEqual; } - } else { - // If no initial scheduler is given, we start from the lower bound. - this->createLowerBoundsVector(x); } std::vector* newX = auxiliaryRowGroupVector.get(); diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index a5845d556..5036ce5ea 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -280,11 +280,15 @@ namespace storm { // Set up the environment. storm::dd::Add localX; - // If we were given an initial scheduler, we take its solution as the starting point. - if (this->hasInitialScheduler()) { - localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b); + if (this->hasUniqueSolution()) { + localX = x; } else { - localX = this->getLowerBoundsVector(); + // If we were given an initial scheduler, we take its solution as the starting point. + if (this->hasInitialScheduler()) { + localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b); + } else { + localX = this->getLowerBoundsVector(); + } } ValueIterationResult viResult = performValueIteration(dir, localX, b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->settings.getMaximalNumberOfIterations());