From e6597b35a62088fc4c2edf31d5f678411117719b Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 25 Feb 2020 17:19:09 +0100 Subject: [PATCH] OVI: Added a few settings to tweak ovi --- src/storm/environment/SubEnvironment.cpp | 4 +- .../solver/OviSolverEnvironment.cpp | 33 +++++++++++++++ .../environment/solver/OviSolverEnvironment.h | 25 +++++++++++ .../environment/solver/SolverEnvironment.cpp | 9 ++++ .../environment/solver/SolverEnvironment.h | 4 ++ src/storm/settings/SettingsManager.cpp | 2 + .../settings/modules/OviSolverSettings.cpp | 42 +++++++++++++++++++ .../settings/modules/OviSolverSettings.h | 36 ++++++++++++++++ .../IterativeMinMaxLinearEquationSolver.cpp | 38 +++++++++++++---- 9 files changed, 184 insertions(+), 9 deletions(-) create mode 100644 src/storm/environment/solver/OviSolverEnvironment.cpp create mode 100644 src/storm/environment/solver/OviSolverEnvironment.h create mode 100644 src/storm/settings/modules/OviSolverSettings.cpp create mode 100644 src/storm/settings/modules/OviSolverSettings.h diff --git a/src/storm/environment/SubEnvironment.cpp b/src/storm/environment/SubEnvironment.cpp index c42e21c93..feabd5e46 100644 --- a/src/storm/environment/SubEnvironment.cpp +++ b/src/storm/environment/SubEnvironment.cpp @@ -6,12 +6,13 @@ #include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/EigenSolverEnvironment.h" +#include "storm/environment/solver/GameSolverEnvironment.h" #include "storm/environment/solver/GmmxxSolverEnvironment.h" #include "storm/environment/solver/NativeSolverEnvironment.h" #include "storm/environment/solver/LongRunAverageSolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/environment/solver/MultiplierEnvironment.h" -#include "storm/environment/solver/GameSolverEnvironment.h" +#include "storm/environment/solver/OviSolverEnvironment.h" #include "storm/environment/solver/TopologicalSolverEnvironment.h" namespace storm { @@ -67,6 +68,7 @@ namespace storm { template class SubEnvironment; template class SubEnvironment; template class SubEnvironment; + template class SubEnvironment; template class SubEnvironment; template class SubEnvironment; diff --git a/src/storm/environment/solver/OviSolverEnvironment.cpp b/src/storm/environment/solver/OviSolverEnvironment.cpp new file mode 100644 index 000000000..759b24783 --- /dev/null +++ b/src/storm/environment/solver/OviSolverEnvironment.cpp @@ -0,0 +1,33 @@ +#include "storm/environment/solver/OviSolverEnvironment.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/OviSolverSettings.h" +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" + +namespace storm { + + OviSolverEnvironment::OviSolverEnvironment() { + auto const& oviSettings = storm::settings::getModule(); + precisionUpdateFactor = storm::utility::convertNumber(oviSettings.getPrecisionUpdateFactor()); + maxVerificationIterationFactor = storm::utility::convertNumber(oviSettings.getMaxVerificationIterationFactor()); + relevantValuesForPrecisionUpdate = oviSettings.useRelevantValuesForPrecisionUpdate(); + }; + + OviSolverEnvironment::~OviSolverEnvironment() { + // Intentionally left empty + } + + storm::RationalNumber OviSolverEnvironment::getPrecisionUpdateFactor() const { + return precisionUpdateFactor; + } + + storm::RationalNumber OviSolverEnvironment::getMaxVerificationIterationFactor() const { + return maxVerificationIterationFactor; + } + + bool OviSolverEnvironment::useRelevantValuesForPrecisionUpdate() const { + return relevantValuesForPrecisionUpdate; + } + +} diff --git a/src/storm/environment/solver/OviSolverEnvironment.h b/src/storm/environment/solver/OviSolverEnvironment.h new file mode 100644 index 000000000..49ef20587 --- /dev/null +++ b/src/storm/environment/solver/OviSolverEnvironment.h @@ -0,0 +1,25 @@ +#pragma once + +#include "storm/environment/solver/SolverEnvironment.h" + +#include "storm/adapters/RationalNumberAdapter.h" + +namespace storm { + + class OviSolverEnvironment { + public: + + OviSolverEnvironment(); + ~OviSolverEnvironment(); + + storm::RationalNumber getPrecisionUpdateFactor() const; + storm::RationalNumber getMaxVerificationIterationFactor() const; + bool useRelevantValuesForPrecisionUpdate() const; + + private: + storm::RationalNumber precisionUpdateFactor; + storm::RationalNumber maxVerificationIterationFactor; + bool relevantValuesForPrecisionUpdate; + }; +} + diff --git a/src/storm/environment/solver/SolverEnvironment.cpp b/src/storm/environment/solver/SolverEnvironment.cpp index 07a02aca1..c4402903f 100644 --- a/src/storm/environment/solver/SolverEnvironment.cpp +++ b/src/storm/environment/solver/SolverEnvironment.cpp @@ -8,6 +8,7 @@ #include "storm/environment/solver/NativeSolverEnvironment.h" #include "storm/environment/solver/GameSolverEnvironment.h" #include "storm/environment/solver/TopologicalSolverEnvironment.h" +#include "storm/environment/solver/OviSolverEnvironment.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" @@ -94,6 +95,14 @@ namespace storm { return topologicalSolverEnvironment.get(); } + OviSolverEnvironment& SolverEnvironment::ovi() { + return oviSolverEnvironment.get(); + } + + OviSolverEnvironment const& SolverEnvironment::ovi() const { + return oviSolverEnvironment.get(); + } + bool SolverEnvironment::isForceSoundness() const { return forceSoundness; } diff --git a/src/storm/environment/solver/SolverEnvironment.h b/src/storm/environment/solver/SolverEnvironment.h index 26ac33fea..303a0cc79 100644 --- a/src/storm/environment/solver/SolverEnvironment.h +++ b/src/storm/environment/solver/SolverEnvironment.h @@ -19,6 +19,7 @@ namespace storm { class MultiplierEnvironment; class GameSolverEnvironment; class TopologicalSolverEnvironment; + class OviSolverEnvironment; class SolverEnvironment { public: @@ -38,6 +39,8 @@ namespace storm { MinMaxSolverEnvironment const& minMax() const; MultiplierEnvironment& multiplier(); MultiplierEnvironment const& multiplier() const; + OviSolverEnvironment const& ovi() const; + OviSolverEnvironment& ovi(); GameSolverEnvironment& game(); GameSolverEnvironment const& game() const; TopologicalSolverEnvironment& topological(); @@ -62,6 +65,7 @@ namespace storm { SubEnvironment longRunAverageSolverEnvironment; SubEnvironment minMaxSolverEnvironment; SubEnvironment multiplierEnvironment; + SubEnvironment oviSolverEnvironment; storm::solver::EquationSolverType linearEquationSolverType; bool linearEquationSolverTypeSetFromDefault; diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 8e278fecb..fcd378fe6 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -40,6 +40,7 @@ #include "storm/settings/modules/MultiplierSettings.h" #include "storm/settings/modules/TransformationSettings.h" #include "storm/settings/modules/HintSettings.h" +#include "storm/settings/modules/OviSolverSettings.h" #include "storm/utility/macros.h" #include "storm/utility/file.h" #include "storm/utility/string.h" @@ -672,6 +673,7 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); } } diff --git a/src/storm/settings/modules/OviSolverSettings.cpp b/src/storm/settings/modules/OviSolverSettings.cpp new file mode 100644 index 000000000..28614a6a6 --- /dev/null +++ b/src/storm/settings/modules/OviSolverSettings.cpp @@ -0,0 +1,42 @@ +#include "storm/settings/modules/OviSolverSettings.h" + +#include "storm/settings/Option.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/OptionBuilder.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string OviSolverSettings::moduleName = "ovi"; + 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"; + + 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()); + } + + double OviSolverSettings::getPrecisionUpdateFactor() const { + return this->getOption(precisionUpdateFactorOptionName).getArgumentByName("factor").getValueAsDouble(); + } + + double OviSolverSettings::getMaxVerificationIterationFactor() const { + return this->getOption(maxVerificationIterationFactorOptionName).getArgumentByName("factor").getValueAsDouble(); + } + + bool OviSolverSettings::useRelevantValuesForPrecisionUpdate() const { + return this->getOption(useRelevantValuesForPrecisionUpdateOptionName).getHasOptionBeenSet(); + } + + } + } +} diff --git a/src/storm/settings/modules/OviSolverSettings.h b/src/storm/settings/modules/OviSolverSettings.h new file mode 100644 index 000000000..d7fec8c91 --- /dev/null +++ b/src/storm/settings/modules/OviSolverSettings.h @@ -0,0 +1,36 @@ +#pragma once + +#include "storm-config.h" +#include "storm/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the settings for the optimistic value iteration solver. + */ + class OviSolverSettings : public ModuleSettings { + public: + + OviSolverSettings(); + + double getPrecisionUpdateFactor() const; + + double getMaxVerificationIterationFactor() const; + + bool useRelevantValuesForPrecisionUpdate() const; + + + // The name of the module. + static const std::string moduleName; + + private: + static const std::string precisionUpdateFactorOptionName; + static const std::string maxVerificationIterationFactorOptionName; + static const std::string useRelevantValuesForPrecisionUpdateOptionName; + }; + + } + } +} diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index ac0a05c47..5f024a284 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -6,6 +6,7 @@ #include "storm/utility/ConstantsComparator.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/environment/solver/OviSolverEnvironment.h" #include "storm/utility/KwekMehlhorn.h" #include "storm/utility/NumberTraits.h" @@ -366,6 +367,19 @@ namespace storm { } return result; } + + template + ValueType computeMaxRelDiff(std::vector const& allOldValues, std::vector const& allNewValues, storm::storage::BitVector const& relevantValues) { + ValueType result = storm::utility::zero(); + for (auto const& i : relevantValues) { + STORM_LOG_ASSERT(!storm::utility::isZero(allNewValues[i]) || storm::utility::isZero(allOldValues[i]), "Unexpected entry in iteration vector."); + if (!storm::utility::isZero(allNewValues[i])) { + result = storm::utility::max(result, storm::utility::abs(allNewValues[i] - allOldValues[i]) / allNewValues[i]); + } + } + return result; + } + template ValueType computeMaxRelDiff(std::vector const& allOldValues, std::vector const& allNewValues) { ValueType result = storm::utility::zero(); @@ -379,11 +393,13 @@ namespace storm { } template - ValueType updateIterationPrecision(std::vector const& currentX, std::vector const& newX, bool const& relative) { + ValueType updateIterationPrecision(storm::Environment const& env, std::vector const& currentX, std::vector const& newX, bool const& relative, boost::optional const& relevantValues) { + auto factor = storm::utility::convertNumber(env.solver().ovi().getPrecisionUpdateFactor()); + bool useRelevant = relevantValues.is_initialized() && env.solver().ovi().useRelevantValuesForPrecisionUpdate(); if (relative) { - return computeMaxRelDiff(newX, currentX) / storm::utility::convertNumber(2); + return (useRelevant ? computeMaxRelDiff(newX, currentX, relevantValues.get()) : computeMaxRelDiff(newX, currentX)) * factor; } else { - return computeMaxAbsDiff(newX, currentX) / storm::utility::convertNumber(2); + return (useRelevant ? computeMaxAbsDiff(newX, currentX, relevantValues.get()) : computeMaxAbsDiff(newX, currentX)) * factor; } } @@ -424,6 +440,11 @@ namespace storm { // Relative errors bool relative = env.solver().minMax().getRelativeTerminationCriterion(); + boost::optional relevantValues; + if (this->hasRelevantValues()) { + relevantValues = this->getRelevantValues(); + } + // x has to start with a lower bound. this->createLowerBoundsVector(x); @@ -502,7 +523,7 @@ namespace storm { std::swap(currentUpperBound, newUpperBound); if (newUpperBoundAlwaysHigher) { - iterationPrecision = updateIterationPrecision(*currentX, *newX, relative); + iterationPrecision = updateIterationPrecision(env, *currentX, *newX, relative, relevantValues); // Not all values moved up or stayed the same // If we have a single fixed point, we can safely set the new lower bound, to the wrongly guessed upper bound if (this->hasUniqueSolution()) { @@ -510,7 +531,7 @@ namespace storm { } break; } else if (valuesCrossed) { - iterationPrecision = updateIterationPrecision(*currentX, *newX, relative); + iterationPrecision = updateIterationPrecision(env, *currentX, *newX, relative, relevantValues); break; } else if (newUpperBoundAlwaysLowerEqual) { // All values moved down or stayed the same and we have a maximum difference of twice the requested precision @@ -518,7 +539,7 @@ namespace storm { // We can use max_if instead of computeMaxAbsDiff, as x is definitely a lower bound and ub is larger in all elements // Recalculate terminationPrecision if relative error requested bool reachedPrecision = true; - for (auto const& valueIndex : this->hasRelevantValues() ? this->getRelevantValues() : storm::storage::BitVector(x.size(), true)) { + for (auto const& valueIndex : relevantValues ? relevantValues.get() : storm::storage::BitVector(x.size(), true)) { ValueType absDiff = currentUpperBound[valueIndex] - (*currentX)[valueIndex]; if (relative) { if (absDiff > doublePrecision * (*currentX)[valueIndex]) { @@ -539,9 +560,10 @@ namespace storm { } } - if ((currentVerificationIterations / 10) >= lastValueIterationIterations) { + ValueType scaledIterationCount = storm::utility::convertNumber(currentVerificationIterations) * storm::utility::convertNumber(env.solver().ovi().getMaxVerificationIterationFactor()); + if (scaledIterationCount >= storm::utility::convertNumber(lastValueIterationIterations)) { cancelGuess = true; - iterationPrecision = updateIterationPrecision(*currentX, *newX, relative); + iterationPrecision = updateIterationPrecision(env, *currentX, *newX, relative, relevantValues); } ++overallIterations;