diff --git a/src/storm/environment/solver/OviSolverEnvironment.cpp b/src/storm/environment/solver/OviSolverEnvironment.cpp index a5007aa78..f1e8e1b5b 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(); + useTerminationGuaranteedMinimumMethod = oviSettings.getUseTerminationGuaranteedMinimumMethod(); } OviSolverEnvironment::~OviSolverEnvironment() { @@ -39,5 +40,9 @@ namespace storm { uint64_t OviSolverEnvironment::getUpperBoundOnlyIterations() const { return upperBoundOnlyIterations; } + + bool OviSolverEnvironment::getUseTerminationGuaranteedMinimumMethod() const { + return useTerminationGuaranteedMinimumMethod; + } } diff --git a/src/storm/environment/solver/OviSolverEnvironment.h b/src/storm/environment/solver/OviSolverEnvironment.h index 74a99e518..7b0fa4d8e 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 getUseTerminationGuaranteedMinimumMethod() const; private: storm::RationalNumber precisionUpdateFactor; @@ -24,6 +25,7 @@ namespace storm { bool relevantValuesForPrecisionUpdate; storm::RationalNumber upperBoundGuessingFactor; uint64_t upperBoundOnlyIterations; + bool useTerminationGuaranteedMinimumMethod; }; } diff --git a/src/storm/settings/modules/OviSolverSettings.cpp b/src/storm/settings/modules/OviSolverSettings.cpp index c617db06f..8f117365c 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::useTerminationGuaranteedMinimumMethodOptionName = "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, useTerminationGuaranteedMinimumMethodOptionName, false, "Sets whether to perform calculations on element-wise minimum of iterated and old upper bound.").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::getUseTerminationGuaranteedMinimumMethod() const { + return this->getOption(useTerminationGuaranteedMinimumMethodOptionName).getHasOptionBeenSet(); + } } } diff --git a/src/storm/settings/modules/OviSolverSettings.h b/src/storm/settings/modules/OviSolverSettings.h index 21884169d..718a646d5 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 getUseTerminationGuaranteedMinimumMethod() 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 useTerminationGuaranteedMinimumMethodOptionName; }; } diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h index 0d905d632..5ebd9c14e 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.h +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h @@ -163,16 +163,17 @@ namespace storm { // 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]) { + if ((*upperX)[i] < (*auxVector)[i]) { + newUpperBoundAlwaysHigherEqual = false; + } else if ((*upperX)[i] != (*auxVector)[i]) { newUpperBoundAlwaysLowerEqual = false; + //std::swap((*upperX)[i], (*auxVector)[i]); } } if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) {