From 169f9201b23b8a35958e1457cd2016dc0d8399e1 Mon Sep 17 00:00:00 2001 From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de> Date: Fri, 4 Sep 2020 10:45:16 +0200 Subject: [PATCH] ovi: Fixed heuristic for canceling a guess. --- src/storm/settings/modules/OviSolverSettings.cpp | 2 +- src/storm/solver/helper/OptimisticValueIterationHelper.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/settings/modules/OviSolverSettings.cpp b/src/storm/settings/modules/OviSolverSettings.cpp index 931aa1af8..bc474b798 100644 --- a/src/storm/settings/modules/OviSolverSettings.cpp +++ b/src/storm/settings/modules/OviSolverSettings.cpp @@ -25,7 +25,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, useRelevantValuesForPrecisionUpdateOptionName, false, "Sets whether the precision of the inner value iteration is only based on the relevant values (i.e. initial states).").setIsAdvanced().build()); - this->addOption(storm::settings::OptionBuilder(moduleName, maxVerificationIterationFactorOptionName, false, "Controls how many verification iterations are performed before guessing a new upper bound.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor", "The factor.").setDefaultValueDouble(0.1).addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, maxVerificationIterationFactorOptionName, false, "Controls how many verification iterations are performed before guessing a new 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, 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()); diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp index a9f8c663f..076782e40 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp @@ -363,7 +363,7 @@ namespace storm { // Check whether we tried this guess for too long ValueType scaledIterationCount = storm::utility::convertNumber<ValueType>(currentVerificationIterations) * storm::utility::convertNumber<ValueType>(env.solver().ovi().getMaxVerificationIterationFactor()); - if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber<ValueType>(lastValueIterationIterations)) { + if (!intervalIterationNeeded && scaledIterationCount * iterationPrecision >= storm::utility::one<ValueType>()) { cancelGuess = true; // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision) }