diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index 5ebd9c14e..5d9dc8b34 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -135,99 +135,222 @@ namespace storm { SolverStatus status = SolverStatus::InProgress; - while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { - - // Perform value iteration until convergence - ++valueIterationInvocations; - auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations); - lastValueIterationIterations = result.iterations; - overallIterations += result.iterations; - - if (result.status != SolverStatus::Converged) { - status = result.status; - } else { - bool intervalIterationNeeded = false; - currentVerificationIterations = 0; - - if (relative) { - oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler); + if(env.solver().ovi().useTerminationGuaranteedMinimumMethod()) { + while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + + // Perform value iteration until convergence + ++valueIterationInvocations; + auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations); + lastValueIterationIterations = result.iterations; + overallIterations += result.iterations; + + if (result.status != SolverStatus::Converged) { + status = result.status; } else { - oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision); - } - - bool cancelGuess = false; - while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { - ++overallIterations; - ++currentVerificationIterations; - // Perform value iteration stepwise for lower bound and guessed upper bound - - // Upper bound iteration - singleIterationCallback(upperX, auxVector, overallIterations); - // At this point,h auxVector contains the old values for the upper bound whereas upperX contains the new ones. - - // Compare the new upper bound candidate with the old one - bool newUpperBoundAlwaysHigherEqual = true; - bool newUpperBoundAlwaysLowerEqual = true; - for (uint64_t i = 0; i < upperX->size(); ++i) { - if ((*upperX)[i] < (*auxVector)[i]) { - newUpperBoundAlwaysHigherEqual = false; - } else if ((*upperX)[i] != (*auxVector)[i]) { - newUpperBoundAlwaysLowerEqual = false; - //std::swap((*upperX)[i], (*auxVector)[i]); - } + bool intervalIterationNeeded = false; + currentVerificationIterations = 0; + + if (relative) { + oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler); + } else { + oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision); } - if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { - // All values moved up or stayed the same - // That means the guess for an upper bound is actually a lower bound - iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); - // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound - // Set lowerX to the upper bound candidate - std::swap(lowerX, upperX); - break; - } 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; - if (relevantValues) { - reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative); - } else { - reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative); + + bool cancelGuess = false; + while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + ++overallIterations; + ++currentVerificationIterations; + // Perform value iteration stepwise for lower bound and guessed upper bound + + // Upper bound iteration + singleIterationCallback(upperX, auxVector, overallIterations); + // At this point,h auxVector contains the old values for the upper bound whereas upperX contains the new ones. + + // Compare the new upper bound candidate with the old one + bool newUpperBoundAlwaysHigherEqual = true; + bool newUpperBoundAlwaysLowerEqual = true; + for (uint64_t i = 0; i < upperX->size(); ++i) { + if ((*upperX)[i] < (*auxVector)[i]) { + newUpperBoundAlwaysHigherEqual = false; + } else if ((*upperX)[i] != (*auxVector)[i]) { + newUpperBoundAlwaysLowerEqual = false; + std::swap((*upperX)[i], (*auxVector)[i]); + } } - if (reachedPrecision) { - status = SolverStatus::Converged; + + if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { + // All values moved up or stayed the same + // That means the guess for an upper bound is actually a lower bound + iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); + // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound + // Set lowerX to the upper bound candidate + std::swap(lowerX, upperX); break; - } else { - // From now on, we keep updating both bounds - intervalIterationNeeded = true; + } 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; + if (relevantValues) { + reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative); + } else { + reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative); + } + if (reachedPrecision) { + status = SolverStatus::Converged; + break; + } else { + // From now on, we keep updating both bounds + intervalIterationNeeded = true; + } + } + // At this point, the old upper bounds (auxVector) are not needed anymore. + + // Check whether we tried this guess for too long + ValueType scaledIterationCount = storm::utility::convertNumber(currentVerificationIterations) * storm::utility::convertNumber(env.solver().ovi().getMaxVerificationIterationFactor()); + if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber(lastValueIterationIterations)) { + cancelGuess = true; + // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision) + } + + // Lower bound iteration (only if needed) + if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) { + singleIterationCallback(lowerX, auxVector, overallIterations); + // At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones. + + // Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound. + bool valuesCrossed = false; + for (uint64_t i = 0; i < lowerX->size(); ++i) { + if ((*upperX)[i] < (*lowerX)[i]) { + valuesCrossed = true; + break; + } + } + + if (cancelGuess || valuesCrossed) { + // A new guess is needed. + iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues); + break; + } } } - // At this point, the old upper bounds (auxVector) are not needed anymore. - - // Check whether we tried this guess for too long - ValueType scaledIterationCount = storm::utility::convertNumber(currentVerificationIterations) * storm::utility::convertNumber(env.solver().ovi().getMaxVerificationIterationFactor()); - if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber(lastValueIterationIterations)) { - cancelGuess = true; - // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision) + } + } + } + else { + while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + + // Perform value iteration until convergence + ++valueIterationInvocations; + auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations); + lastValueIterationIterations = result.iterations; + overallIterations += result.iterations; + + if (result.status != SolverStatus::Converged) { + status = result.status; + } else { + bool intervalIterationNeeded = false; + currentVerificationIterations = 0; + + if (relative) { + oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler); + } else { + oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision); } - - // Lower bound iteration (only if needed) - if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) { - singleIterationCallback(lowerX, auxVector, overallIterations); - // At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones. - - // Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound. - bool valuesCrossed = false; - for (uint64_t i = 0; i < lowerX->size(); ++i) { - if ((*upperX)[i] < (*lowerX)[i]) { - valuesCrossed = true; - break; + + bool cancelGuess = false; + while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + ++overallIterations; + ++currentVerificationIterations; + // Perform value iteration stepwise for lower bound and guessed upper bound + + // Upper bound iteration + singleIterationCallback(upperX, auxVector, overallIterations); + + // At this point,h auxVector contains the old values for the upper bound whereas upperX contains the new ones. + + // Compare the new upper bound candidate with the old one + bool newUpperBoundAlwaysHigherEqual = true; + bool newUpperBoundAlwaysLowerEqual = true; + bool cancelOuterScan = false; + for (uint64_t i = 0; i < upperX->size() &! cancelOuterScan; ++i) { + if ((*upperX)[i] < (*auxVector)[i]) { + newUpperBoundAlwaysHigherEqual = false; + ++i; + while (i < upperX->size()) { + if ((*upperX)[i] > (*auxVector)[i]) { + newUpperBoundAlwaysLowerEqual = false; + cancelOuterScan = true; + break; + } + ++i; + } + } else if ((*upperX)[i] != (*auxVector)[i]) { + newUpperBoundAlwaysLowerEqual = false; + ++i; + while (i < upperX->size()) { + if ((*upperX)[i] > (*auxVector)[i]) { + newUpperBoundAlwaysLowerEqual = false; + cancelOuterScan = true; + break; + } + ++i; + } } } - - if (cancelGuess || valuesCrossed) { - // A new guess is needed. - iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues); + + if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { + // All values moved up or stayed the same + // That means the guess for an upper bound is actually a lower bound + iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); + // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound + // Set lowerX to the upper bound candidate + std::swap(lowerX, upperX); break; + } 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; + if (relevantValues) { + reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative); + } else { + reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative); + } + if (reachedPrecision) { + status = SolverStatus::Converged; + break; + } else { + // From now on, we keep updating both bounds + intervalIterationNeeded = true; + } + } + // At this point, the old upper bounds (auxVector) are not needed anymore. + + // Check whether we tried this guess for too long + ValueType scaledIterationCount = storm::utility::convertNumber(currentVerificationIterations) * storm::utility::convertNumber(env.solver().ovi().getMaxVerificationIterationFactor()); + if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber(lastValueIterationIterations)) { + cancelGuess = true; + // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision) + } + + // Lower bound iteration (only if needed) + if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) { + singleIterationCallback(lowerX, auxVector, overallIterations); + // At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones. + + // Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound. + bool valuesCrossed = false; + for (uint64_t i = 0; i < lowerX->size(); ++i) { + if ((*upperX)[i] < (*lowerX)[i]) { + valuesCrossed = true; + break; + } + } + + if (cancelGuess || valuesCrossed) { + // A new guess is needed. + iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues); + break; + } } } }