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<LongRunAverageSolverEnvironment>;
template class SubEnvironment<MinMaxSolverEnvironment>;
template class SubEnvironment<MultiplierEnvironment>;
+ template class SubEnvironment<OviSolverEnvironment>;
template class SubEnvironment<GameSolverEnvironment>;
template class SubEnvironment<TopologicalSolverEnvironment>;
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<storm::settings::modules::OviSolverSettings>();
+ precisionUpdateFactor = storm::utility::convertNumber<storm::RationalNumber>(oviSettings.getPrecisionUpdateFactor());
+ maxVerificationIterationFactor = storm::utility::convertNumber<storm::RationalNumber>(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> longRunAverageSolverEnvironment;
SubEnvironment<MinMaxSolverEnvironment> minMaxSolverEnvironment;
SubEnvironment<MultiplierEnvironment> multiplierEnvironment;
+ SubEnvironment<OviSolverEnvironment> 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::modules::MultiplierSettings>();
storm::settings::addModule<storm::settings::modules::TransformationSettings>();
storm::settings::addModule<storm::settings::modules::HintSettings>();
+ storm::settings::addModule<storm::settings::modules::OviSolverSettings>();
}
}
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<typename ValueType>
+ ValueType computeMaxRelDiff(std::vector<ValueType> const& allOldValues, std::vector<ValueType> const& allNewValues, storm::storage::BitVector const& relevantValues) {
+ ValueType result = storm::utility::zero<ValueType>();
+ 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<ValueType>(result, storm::utility::abs<ValueType>(allNewValues[i] - allOldValues[i]) / allNewValues[i]);
+ }
+ }
+ return result;
+ }
+
template<typename ValueType>
ValueType computeMaxRelDiff(std::vector<ValueType> const& allOldValues, std::vector<ValueType> const& allNewValues) {
ValueType result = storm::utility::zero<ValueType>();
@@ -379,11 +393,13 @@ namespace storm {
}
template<typename ValueType>
- ValueType updateIterationPrecision(std::vector<ValueType> const& currentX, std::vector<ValueType> const& newX, bool const& relative) {
+ ValueType updateIterationPrecision(storm::Environment const& env, std::vector<ValueType> const& currentX, std::vector<ValueType> const& newX, bool const& relative, boost::optional<storm::storage::BitVector> const& relevantValues) {
+ auto factor = storm::utility::convertNumber<ValueType>(env.solver().ovi().getPrecisionUpdateFactor());
+ bool useRelevant = relevantValues.is_initialized() && env.solver().ovi().useRelevantValuesForPrecisionUpdate();
if (relative) {
- return computeMaxRelDiff(newX, currentX) / storm::utility::convertNumber<ValueType>(2);
+ return (useRelevant ? computeMaxRelDiff(newX, currentX, relevantValues.get()) : computeMaxRelDiff(newX, currentX)) * factor;
} else {
- return computeMaxAbsDiff(newX, currentX) / storm::utility::convertNumber<ValueType>(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<storm::storage::BitVector> 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<ValueType>(currentVerificationIterations) * storm::utility::convertNumber<ValueType>(env.solver().ovi().getMaxVerificationIterationFactor());
+ if (scaledIterationCount >= storm::utility::convertNumber<ValueType>(lastValueIterationIterations)) {
cancelGuess = true;
- iterationPrecision = updateIterationPrecision(*currentX, *newX, relative);
+ iterationPrecision = updateIterationPrecision(env, *currentX, *newX, relative, relevantValues);
}
++overallIterations;