diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 90837a6b3..4f74b143e 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -360,6 +360,15 @@ namespace storm { template bool IterativeMinMaxLinearEquationSolver::solveEquationsOptimisticValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { + if (!storm::utility::vector::hasNonZeroEntry(b)) { + // If all entries are zero, OVI might run in an endless loop. However, the result is easy in this case. + x.assign(x.size(), storm::utility::zero()); + if (this->isTrackSchedulerSet()) { + this->schedulerChoices = std::vector(x.size(), 0); + } + return true; + } + if (!this->multiplierA) { this->multiplierA = storm::solver::MultiplierFactory().create(env, *this->A); } diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index f06e1f311..a27988ba6 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -637,6 +637,12 @@ namespace storm { template bool NativeLinearEquationSolver::solveEquationsOptimisticValueIteration(Environment const& env, std::vector& x, std::vector const& b) const { + if (!storm::utility::vector::hasNonZeroEntry(b)) { + // If all entries are zero, OVI might run in an endless loop. However, the result is easy in this case. + x.assign(x.size(), storm::utility::zero()); + return true; + } + if (!this->multiplier) { this->multiplier = storm::solver::MultiplierFactory().create(env, *this->A); } diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index fb646ce76..5542eb473 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -223,11 +223,14 @@ namespace storm { // From now on, we keep updating both bounds intervalIterationNeeded = true; } - } else if (newUpperBoundAlwaysHigherEqual && newUpperBoundAlwaysLowerEqual) { + // The following case below covers that bouth vectors (old and new) are equal. + // Theoretically, this means that the precise fixpoint has been reached. However, numerical instabilities can be tricky and this detection might be incorrect (see the haddad-monmege model). + // We therefore disable it. It is very unlikely that we guessed the right fixpoint anyway. + //} else if (newUpperBoundAlwaysHigherEqual && newUpperBoundAlwaysLowerEqual) { // In this case, the guessed upper bound is the precise fixpoint - status = SolverStatus::Converged; - std::swap(lowerX, auxVector); - break; + // status = SolverStatus::Converged; + // std::swap(lowerX, auxVector); + // break; } // At this point, the old upper bounds (auxVector) are not needed anymore.