diff --git a/src/storm/environment/solver/OviSolverEnvironment.cpp b/src/storm/environment/solver/OviSolverEnvironment.cpp index dba37846e..fe6a21a12 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.cpp +++ b/src/storm/environment/solver/OviSolverEnvironment.cpp @@ -14,7 +14,7 @@ namespace storm { relevantValuesForPrecisionUpdate = oviSettings.useRelevantValuesForPrecisionUpdate(); upperBoundGuessingFactor = storm::utility::convertNumber(oviSettings.getUpperBoundGuessingFactor()); upperBoundOnlyIterations = oviSettings.getUpperBoundOnlyIterations(); - terminationGuaranteedMinimumMethod = oviSettings.useTerminationGuaranteedMinimumMethod(); + noTerminationGuaranteeMinimumMethod = oviSettings.useNoTerminationGuaranteeMinimumMethod(); } OviSolverEnvironment::~OviSolverEnvironment() { @@ -41,8 +41,8 @@ namespace storm { return upperBoundOnlyIterations; } - bool OviSolverEnvironment::useTerminationGuaranteedMinimumMethod() const { - return terminationGuaranteedMinimumMethod; + bool OviSolverEnvironment::useNoTerminationGuaranteeMinimumMethod() const { + return noTerminationGuaranteeMinimumMethod; } } diff --git a/src/storm/environment/solver/OviSolverEnvironment.h b/src/storm/environment/solver/OviSolverEnvironment.h index f75985924..0875bad9a 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.h +++ b/src/storm/environment/solver/OviSolverEnvironment.h @@ -17,7 +17,7 @@ namespace storm { bool useRelevantValuesForPrecisionUpdate() const; storm::RationalNumber getUpperBoundGuessingFactor() const; uint64_t getUpperBoundOnlyIterations() const; - bool useTerminationGuaranteedMinimumMethod() const; + bool useNoTerminationGuaranteeMinimumMethod() const; private: storm::RationalNumber precisionUpdateFactor; @@ -25,7 +25,7 @@ namespace storm { bool relevantValuesForPrecisionUpdate; storm::RationalNumber upperBoundGuessingFactor; uint64_t upperBoundOnlyIterations; - bool terminationGuaranteedMinimumMethod; + bool noTerminationGuaranteeMinimumMethod; }; } diff --git a/src/storm/settings/modules/OviSolverSettings.cpp b/src/storm/settings/modules/OviSolverSettings.cpp index 7c34b69dc..46cc82f36 100644 --- a/src/storm/settings/modules/OviSolverSettings.cpp +++ b/src/storm/settings/modules/OviSolverSettings.cpp @@ -17,7 +17,7 @@ namespace storm { const std::string OviSolverSettings::useRelevantValuesForPrecisionUpdateOptionName = "use-relevant-values"; const std::string OviSolverSettings::upperBoundGuessingFactorOptionName = "upper-bound-factor"; const std::string OviSolverSettings::upperBoundOnlyIterationsOptionName = "check-upper-only-iter"; - const std::string OviSolverSettings::useTerminationGuaranteedMinimumMethodOptionName = "termination-guarantee"; + const std::string OviSolverSettings::useNoTerminationGuaranteeMinimumMethodOptionName = "no-termination-guarantee"; OviSolverSettings::OviSolverSettings() : ModuleSettings(moduleName) { @@ -31,7 +31,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, upperBoundOnlyIterationsOptionName, false, "Sets the max. iterations OVI will only iterate over the upper bound.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createIntegerArgument("iter", "The iterations.").setDefaultValueInteger(20000).addValidatorInteger(ArgumentValidatorFactory::createIntegerGreaterValidator(0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, useTerminationGuaranteedMinimumMethodOptionName, false, "Sets whether to perform calculations on element-wise minimum of iterated and old upper bound.").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, useNoTerminationGuaranteeMinimumMethodOptionName, false, "Sets whether to perform element-wise minimum of iterated and old upper bound. If this option is set, that will be skipped, slightly increasing performance but giving no termination guarantee.").setShortName("ntg").setIsAdvanced().build()); } double OviSolverSettings::getPrecisionUpdateFactor() const { @@ -54,8 +54,8 @@ namespace storm { return this->getOption(upperBoundOnlyIterationsOptionName).getArgumentByName("iter").getValueAsInteger(); } - bool OviSolverSettings::useTerminationGuaranteedMinimumMethod() const { - return this->getOption(useTerminationGuaranteedMinimumMethodOptionName).getHasOptionBeenSet(); + bool OviSolverSettings::useNoTerminationGuaranteeMinimumMethod() const { + return this->getOption(useNoTerminationGuaranteeMinimumMethodOptionName).getHasOptionBeenSet(); } } diff --git a/src/storm/settings/modules/OviSolverSettings.h b/src/storm/settings/modules/OviSolverSettings.h index 2e5934350..70c1c4f0f 100644 --- a/src/storm/settings/modules/OviSolverSettings.h +++ b/src/storm/settings/modules/OviSolverSettings.h @@ -25,7 +25,7 @@ namespace storm { uint64_t getUpperBoundOnlyIterations() const; - bool useTerminationGuaranteedMinimumMethod() const; + bool useNoTerminationGuaranteeMinimumMethod() const; // The name of the module. static const std::string moduleName; @@ -36,7 +36,7 @@ namespace storm { static const std::string useRelevantValuesForPrecisionUpdateOptionName; static const std::string upperBoundGuessingFactorOptionName; static const std::string upperBoundOnlyIterationsOptionName; - static const std::string useTerminationGuaranteedMinimumMethodOptionName; + static const std::string useNoTerminationGuaranteeMinimumMethodOptionName; }; } diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index 5d9dc8b34..8bb6a3cca 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -121,6 +121,8 @@ namespace storm { ValueType two = storm::utility::convertNumber(2.0); // Relative errors bool relative = env.solver().minMax().getRelativeTerminationCriterion(); + // Use no termination guaranteed upper bound iteration method + bool noTerminationGuarantee = env.solver().ovi().useNoTerminationGuaranteeMinimumMethod(); // Goal precision ValueType precision = storm::utility::convertNumber(env.solver().minMax().getPrecision()); // Desired max difference between upperX and lowerX @@ -135,142 +137,40 @@ namespace storm { SolverStatus status = SolverStatus::InProgress; - if(env.solver().ovi().useTerminationGuaranteedMinimumMethod()) { - while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + 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; + // 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); - } - - 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 (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; - } - } - } - } - } - } - 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 (result.status != SolverStatus::Converged) { - status = result.status; + if (relative) { + oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler); } else { - bool intervalIterationNeeded = false; - currentVerificationIterations = 0; - - if (relative) { - oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler); - } 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 + oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision); + } - // Upper bound iteration - singleIterationCallback(upperX, auxVector, overallIterations); + bool cancelGuess = false; + while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + ++overallIterations; + ++currentVerificationIterations; + // Perform value iteration stepwise for lower bound and guessed upper bound - // At this point,h auxVector contains the old values for the upper bound whereas upperX contains the new ones. + // 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; + // Compare the new upper bound candidate with the old one + bool newUpperBoundAlwaysHigherEqual = true; + bool newUpperBoundAlwaysLowerEqual = true; + if(noTerminationGuarantee) { bool cancelOuterScan = false; for (uint64_t i = 0; i < upperX->size() &! cancelOuterScan; ++i) { if ((*upperX)[i] < (*auxVector)[i]) { @@ -288,8 +188,8 @@ namespace storm { newUpperBoundAlwaysLowerEqual = false; ++i; while (i < upperX->size()) { - if ((*upperX)[i] > (*auxVector)[i]) { - newUpperBoundAlwaysLowerEqual = false; + if ((*upperX)[i] < (*auxVector)[i]) { + newUpperBoundAlwaysHigherEqual = false; cancelOuterScan = true; break; } @@ -297,61 +197,71 @@ namespace storm { } } } - - 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; + } + else { + 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]); } } - // 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) + 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. - // 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 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) + } - // 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; - } - } + // 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. - if (cancelGuess || valuesCrossed) { - // A new guess is needed. - iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues); + // 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; + } } } }