OVI: Fixed too early termination.

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -360,6 +360,15 @@ namespace storm {
         template<typename ValueType>
         bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsOptimisticValueIteration(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> 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<ValueType>());
+                if (this->isTrackSchedulerSet()) {
+                    this->schedulerChoices = std::vector<uint_fast64_t>(x.size(), 0);
+                }
+                return true;
+            }
+            
             if (!this->multiplierA) {
                 this->multiplierA = storm::solver::MultiplierFactory<ValueType>().create(env, *this->A);
             }

src/storm/solver/NativeLinearEquationSolver.cpp

@@ -637,6 +637,12 @@ namespace storm {
         template<typename ValueType>
         bool NativeLinearEquationSolver<ValueType>::solveEquationsOptimisticValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> 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<ValueType>());
+                return true;
+            }
+            
             if (!this->multiplier) {
                 this->multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, *this->A);
             }

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.