diff --git a/src/storm/environment/solver/OviSolverEnvironment.cpp b/src/storm/environment/solver/OviSolverEnvironment.cpp index 91c8e5c1a..a5007aa78 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.cpp +++ b/src/storm/environment/solver/OviSolverEnvironment.cpp @@ -13,6 +13,7 @@ namespace storm { maxVerificationIterationFactor = storm::utility::convertNumber(oviSettings.getMaxVerificationIterationFactor()); relevantValuesForPrecisionUpdate = oviSettings.useRelevantValuesForPrecisionUpdate(); upperBoundGuessingFactor = storm::utility::convertNumber(oviSettings.getUpperBoundGuessingFactor()); + upperBoundOnlyIterations = oviSettings.getUpperBoundOnlyIterations(); } OviSolverEnvironment::~OviSolverEnvironment() { @@ -34,5 +35,9 @@ namespace storm { storm::RationalNumber OviSolverEnvironment::getUpperBoundGuessingFactor() const { return maxVerificationIterationFactor; } + + uint64_t OviSolverEnvironment::getUpperBoundOnlyIterations() const { + return upperBoundOnlyIterations; + } } diff --git a/src/storm/environment/solver/OviSolverEnvironment.h b/src/storm/environment/solver/OviSolverEnvironment.h index 92897deb2..74a99e518 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.h +++ b/src/storm/environment/solver/OviSolverEnvironment.h @@ -16,12 +16,14 @@ namespace storm { storm::RationalNumber getMaxVerificationIterationFactor() const; bool useRelevantValuesForPrecisionUpdate() const; storm::RationalNumber getUpperBoundGuessingFactor() const; + uint64_t getUpperBoundOnlyIterations() const; private: storm::RationalNumber precisionUpdateFactor; storm::RationalNumber maxVerificationIterationFactor; bool relevantValuesForPrecisionUpdate; storm::RationalNumber upperBoundGuessingFactor; + uint64_t upperBoundOnlyIterations; }; } diff --git a/src/storm/settings/modules/OviSolverSettings.cpp b/src/storm/settings/modules/OviSolverSettings.cpp index 104190ba7..0d367a25c 100644 --- a/src/storm/settings/modules/OviSolverSettings.cpp +++ b/src/storm/settings/modules/OviSolverSettings.cpp @@ -16,6 +16,7 @@ namespace storm { const std::string OviSolverSettings::maxVerificationIterationFactorOptionName = "max-verification-iter-factor"; 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"; OviSolverSettings::OviSolverSettings() : ModuleSettings(moduleName) { @@ -26,6 +27,8 @@ namespace storm { 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, 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()); } double OviSolverSettings::getPrecisionUpdateFactor() const { @@ -43,6 +46,10 @@ namespace storm { double OviSolverSettings::getUpperBoundGuessingFactor() const { return this->getOption(upperBoundGuessingFactorOptionName).getArgumentByName("factor").getValueAsDouble(); } + + uint64_t OviSolverSettings::getUpperBoundOnlyIterations() const { + return this->getOption(upperBoundOnlyIterationsOptionName).getArgumentByName("iter").getValueAsInteger(); + } } } diff --git a/src/storm/settings/modules/OviSolverSettings.h b/src/storm/settings/modules/OviSolverSettings.h index 1528d7769..21884169d 100644 --- a/src/storm/settings/modules/OviSolverSettings.h +++ b/src/storm/settings/modules/OviSolverSettings.h @@ -22,6 +22,8 @@ namespace storm { bool useRelevantValuesForPrecisionUpdate() const; double getUpperBoundGuessingFactor() const; + + uint64_t getUpperBoundOnlyIterations() const; // The name of the module. @@ -32,6 +34,7 @@ namespace storm { static const std::string maxVerificationIterationFactorOptionName; static const std::string useRelevantValuesForPrecisionUpdateOptionName; static const std::string upperBoundGuessingFactorOptionName; + static const std::string upperBoundOnlyIterationsOptionName; }; }