diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index 1adb29b38..4cfe6c012 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -175,7 +175,7 @@ namespace storm { newUpperBoundAlwaysLowerEqual = false; } } - if (newUpperBoundAlwaysHigherEqual & !newUpperBoundAlwaysLowerEqual) { + if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { // All values moved up or stayed the same (but are not the same) // That means the guess for an upper bound is actually a lower bound iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); @@ -183,7 +183,7 @@ namespace storm { // Set lowerX to the upper bound candidate std::swap(lowerX, upperX); break; - } else if (newUpperBoundAlwaysLowerEqual) { + } else if (newUpperBoundAlwaysLowerEqual &! newUpperBoundAlwaysHigherEqual) { // All values moved down or stayed the same and we have a maximum difference of twice the requested precision // We can safely use twice the requested precision, as we calculate the center of both vectors bool reachedPrecision; @@ -199,6 +199,9 @@ namespace storm { // From now on, we keep updating both bounds intervalIterationNeeded = true; } + } else if (newUpperBoundAlwaysHigherEqual && newUpperBoundAlwaysLowerEqual) { + // All values stayed the same. For safety we guess above this value again and check, if all values move down + break; } // At this point, the old upper bounds (auxVector) are not needed anymore.