diff --git a/src/storm/environment/solver/OviSolverEnvironment.cpp b/src/storm/environment/solver/OviSolverEnvironment.cpp index 759b24783..91c8e5c1a 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.cpp +++ b/src/storm/environment/solver/OviSolverEnvironment.cpp @@ -12,7 +12,8 @@ namespace storm { precisionUpdateFactor = storm::utility::convertNumber(oviSettings.getPrecisionUpdateFactor()); maxVerificationIterationFactor = storm::utility::convertNumber(oviSettings.getMaxVerificationIterationFactor()); relevantValuesForPrecisionUpdate = oviSettings.useRelevantValuesForPrecisionUpdate(); - }; + upperBoundGuessingFactor = storm::utility::convertNumber(oviSettings.getUpperBoundGuessingFactor()); + } OviSolverEnvironment::~OviSolverEnvironment() { // Intentionally left empty @@ -29,5 +30,9 @@ namespace storm { bool OviSolverEnvironment::useRelevantValuesForPrecisionUpdate() const { return relevantValuesForPrecisionUpdate; } + + storm::RationalNumber OviSolverEnvironment::getUpperBoundGuessingFactor() const { + return maxVerificationIterationFactor; + } } diff --git a/src/storm/environment/solver/OviSolverEnvironment.h b/src/storm/environment/solver/OviSolverEnvironment.h index 49ef20587..92897deb2 100644 --- a/src/storm/environment/solver/OviSolverEnvironment.h +++ b/src/storm/environment/solver/OviSolverEnvironment.h @@ -15,11 +15,13 @@ namespace storm { storm::RationalNumber getPrecisionUpdateFactor() const; storm::RationalNumber getMaxVerificationIterationFactor() const; bool useRelevantValuesForPrecisionUpdate() const; + storm::RationalNumber getUpperBoundGuessingFactor() const; private: storm::RationalNumber precisionUpdateFactor; storm::RationalNumber maxVerificationIterationFactor; bool relevantValuesForPrecisionUpdate; + storm::RationalNumber upperBoundGuessingFactor; }; } diff --git a/src/storm/settings/modules/OviSolverSettings.cpp b/src/storm/settings/modules/OviSolverSettings.cpp index 28614a6a6..104190ba7 100644 --- a/src/storm/settings/modules/OviSolverSettings.cpp +++ b/src/storm/settings/modules/OviSolverSettings.cpp @@ -15,14 +15,17 @@ namespace storm { const std::string OviSolverSettings::precisionUpdateFactorOptionName = "precision-update-factor"; 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"; 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.5).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); 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, 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()); } double OviSolverSettings::getPrecisionUpdateFactor() const { @@ -36,6 +39,10 @@ namespace storm { bool OviSolverSettings::useRelevantValuesForPrecisionUpdate() const { return this->getOption(useRelevantValuesForPrecisionUpdateOptionName).getHasOptionBeenSet(); } + + double OviSolverSettings::getUpperBoundGuessingFactor() const { + return this->getOption(upperBoundGuessingFactorOptionName).getArgumentByName("factor").getValueAsDouble(); + } } } diff --git a/src/storm/settings/modules/OviSolverSettings.h b/src/storm/settings/modules/OviSolverSettings.h index d7fec8c91..1528d7769 100644 --- a/src/storm/settings/modules/OviSolverSettings.h +++ b/src/storm/settings/modules/OviSolverSettings.h @@ -20,6 +20,8 @@ namespace storm { double getMaxVerificationIterationFactor() const; bool useRelevantValuesForPrecisionUpdate() const; + + double getUpperBoundGuessingFactor() const; // The name of the module. @@ -29,6 +31,7 @@ namespace storm { static const std::string precisionUpdateFactorOptionName; static const std::string maxVerificationIterationFactorOptionName; static const std::string useRelevantValuesForPrecisionUpdateOptionName; + static const std::string upperBoundGuessingFactorOptionName; }; }