Browse Source

OVI: Add upper bound guessing scaler factor option

main
Jan Erik Karuc 5 years ago
parent
commit
6ecee7e371
  1. 7
      src/storm/environment/solver/OviSolverEnvironment.cpp
  2. 2
      src/storm/environment/solver/OviSolverEnvironment.h
  3. 9
      src/storm/settings/modules/OviSolverSettings.cpp
  4. 3
      src/storm/settings/modules/OviSolverSettings.h

7
src/storm/environment/solver/OviSolverEnvironment.cpp

@ -12,7 +12,8 @@ namespace storm {
precisionUpdateFactor = storm::utility::convertNumber<storm::RationalNumber>(oviSettings.getPrecisionUpdateFactor());
maxVerificationIterationFactor = storm::utility::convertNumber<storm::RationalNumber>(oviSettings.getMaxVerificationIterationFactor());
relevantValuesForPrecisionUpdate = oviSettings.useRelevantValuesForPrecisionUpdate();
};
upperBoundGuessingFactor = storm::utility::convertNumber<storm::RationalNumber>(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;
}
}

2
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;
};
}

9
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();
}
}
}

3
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;
};
}

Loading…
Cancel
Save