diff --git a/src/storm/environment/solver/OviSolverEnvironment.cpp b/src/storm/environment/solver/OviSolverEnvironment.cpp index a5007aa78..fe6a21a12 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.cpp +++ b/src/storm/environment/solver/OviSolverEnvironment.cpp @@ -14,6 +14,7 @@ namespace storm { relevantValuesForPrecisionUpdate = oviSettings.useRelevantValuesForPrecisionUpdate(); upperBoundGuessingFactor = storm::utility::convertNumber(oviSettings.getUpperBoundGuessingFactor()); upperBoundOnlyIterations = oviSettings.getUpperBoundOnlyIterations(); + noTerminationGuaranteeMinimumMethod = oviSettings.useNoTerminationGuaranteeMinimumMethod(); } OviSolverEnvironment::~OviSolverEnvironment() { @@ -33,11 +34,15 @@ namespace storm { } storm::RationalNumber OviSolverEnvironment::getUpperBoundGuessingFactor() const { - return maxVerificationIterationFactor; + return upperBoundGuessingFactor; } uint64_t OviSolverEnvironment::getUpperBoundOnlyIterations() const { return upperBoundOnlyIterations; } + + bool OviSolverEnvironment::useNoTerminationGuaranteeMinimumMethod() const { + return noTerminationGuaranteeMinimumMethod; + } } diff --git a/src/storm/environment/solver/OviSolverEnvironment.h b/src/storm/environment/solver/OviSolverEnvironment.h index 74a99e518..0875bad9a 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.h +++ b/src/storm/environment/solver/OviSolverEnvironment.h @@ -17,6 +17,7 @@ namespace storm { bool useRelevantValuesForPrecisionUpdate() const; storm::RationalNumber getUpperBoundGuessingFactor() const; uint64_t getUpperBoundOnlyIterations() const; + bool useNoTerminationGuaranteeMinimumMethod() const; private: storm::RationalNumber precisionUpdateFactor; @@ -24,6 +25,7 @@ namespace storm { bool relevantValuesForPrecisionUpdate; storm::RationalNumber upperBoundGuessingFactor; uint64_t upperBoundOnlyIterations; + bool noTerminationGuaranteeMinimumMethod; }; } diff --git a/src/storm/settings/modules/OviSolverSettings.cpp b/src/storm/settings/modules/OviSolverSettings.cpp index c617db06f..46cc82f36 100644 --- a/src/storm/settings/modules/OviSolverSettings.cpp +++ b/src/storm/settings/modules/OviSolverSettings.cpp @@ -17,7 +17,8 @@ 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::useNoTerminationGuaranteeMinimumMethodOptionName = "no-termination-guarantee"; + OviSolverSettings::OviSolverSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, precisionUpdateFactorOptionName, false, "Sets with which factor the precision of the inner value iteration is updated.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor", "The factor.").setDefaultValueDouble(0.4).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); @@ -29,6 +30,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, upperBoundGuessingFactorOptionName, false, "Sets with which factor the precision is multiplied to guess the upper bound.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor", "The factor.").setDefaultValueDouble(1.0).addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); 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, 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 { @@ -50,6 +53,10 @@ namespace storm { uint64_t OviSolverSettings::getUpperBoundOnlyIterations() const { return this->getOption(upperBoundOnlyIterationsOptionName).getArgumentByName("iter").getValueAsInteger(); } + + 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 21884169d..70c1c4f0f 100644 --- a/src/storm/settings/modules/OviSolverSettings.h +++ b/src/storm/settings/modules/OviSolverSettings.h @@ -24,7 +24,8 @@ namespace storm { double getUpperBoundGuessingFactor() const; uint64_t getUpperBoundOnlyIterations() const; - + + bool useNoTerminationGuaranteeMinimumMethod() const; // The name of the module. static const std::string moduleName; @@ -35,6 +36,7 @@ namespace storm { static const std::string useRelevantValuesForPrecisionUpdateOptionName; static const std::string upperBoundGuessingFactorOptionName; static const std::string upperBoundOnlyIterationsOptionName; + static const std::string useNoTerminationGuaranteeMinimumMethodOptionName; }; } diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index 2869540d6..22cad53fc 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -82,7 +82,7 @@ namespace storm { void guessUpperBoundAbsolute(std::vector const& x, std::vector &target, ValueType const& precision) { storm::utility::vector::applyPointwise(x, target, [&precision] (ValueType const& argument) -> ValueType { return argument + precision; }); } - + } @@ -122,6 +122,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 @@ -137,54 +139,86 @@ 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); } 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, auxVector contains the old values for the upper bound whereas upperX contains the new ones. - + // 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 ((*auxVector)[i] > (*upperX)[i]) { - newUpperBoundAlwaysHigherEqual = false; - } else if ((*auxVector)[i] != (*upperX)[i]) { - newUpperBoundAlwaysLowerEqual = false; + if(noTerminationGuarantee) { + 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]) { + newUpperBoundAlwaysHigherEqual = false; + cancelOuterScan = true; + break; + } + ++i; + } + } + } + } + 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]); + } } } - if (newUpperBoundAlwaysHigherEqual & !newUpperBoundAlwaysLowerEqual) { - // All values moved up or stayed the same (but are not the same) + + 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) { + } 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; @@ -202,19 +236,19 @@ namespace storm { } } // 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) { @@ -223,7 +257,7 @@ namespace storm { break; } } - + if (cancelGuess || valuesCrossed) { // A new guess is needed. iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues);