diff --git a/src/storm/environment/solver/MinMaxSolverEnvironment.cpp b/src/storm/environment/solver/MinMaxSolverEnvironment.cpp index 83ff18826..d9e43c2e2 100644 --- a/src/storm/environment/solver/MinMaxSolverEnvironment.cpp +++ b/src/storm/environment/solver/MinMaxSolverEnvironment.cpp @@ -18,6 +18,7 @@ namespace storm { STORM_LOG_ASSERT(considerRelativeTerminationCriterion || minMaxSettings.getConvergenceCriterion() == storm::settings::modules::MinMaxEquationSolverSettings::ConvergenceCriterion::Absolute, "Unknown convergence criterion"); multiplicationStyle = minMaxSettings.getValueIterationMultiplicationStyle(); forceBounds = minMaxSettings.isForceBoundsSet(); + symmetricUpdates = minMaxSettings.isForceIntervalIterationSymmetricUpdatesSet(); qviRestartThreshold = minMaxSettings.getQviRestartThreshold(); qviRestartMaxIterations = minMaxSettings.getQviRestartMaxIterations(); } @@ -78,6 +79,14 @@ namespace storm { void MinMaxSolverEnvironment::setForceBounds(bool value) { forceBounds = value; } + + bool MinMaxSolverEnvironment::isSymmetricUpdatesSet() const { + return symmetricUpdates; + } + + void MinMaxSolverEnvironment::setSymmetricUpdates(bool value) { + symmetricUpdates = value; + } storm::RationalNumber MinMaxSolverEnvironment::getQviRestartThreshold() const { return qviRestartThreshold; diff --git a/src/storm/environment/solver/MinMaxSolverEnvironment.h b/src/storm/environment/solver/MinMaxSolverEnvironment.h index f7e0a24b1..6196942a1 100644 --- a/src/storm/environment/solver/MinMaxSolverEnvironment.h +++ b/src/storm/environment/solver/MinMaxSolverEnvironment.h @@ -27,6 +27,8 @@ namespace storm { void setMultiplicationStyle(storm::solver::MultiplicationStyle value); bool isForceBoundsSet() const; void setForceBounds(bool value); + bool isSymmetricUpdatesSet() const; + void setSymmetricUpdates(bool value); storm::RationalNumber getQviRestartThreshold() const; void setQviRestartThreshold(storm::RationalNumber value); uint64_t getQviRestartMaxIterations() const; @@ -40,6 +42,7 @@ namespace storm { bool considerRelativeTerminationCriterion; storm::solver::MultiplicationStyle multiplicationStyle; bool forceBounds; + bool symmetricUpdates; storm::RationalNumber qviRestartThreshold; uint64_t qviRestartMaxIterations; }; diff --git a/src/storm/environment/solver/NativeSolverEnvironment.cpp b/src/storm/environment/solver/NativeSolverEnvironment.cpp index b11b906df..722fed3d1 100644 --- a/src/storm/environment/solver/NativeSolverEnvironment.cpp +++ b/src/storm/environment/solver/NativeSolverEnvironment.cpp @@ -19,6 +19,8 @@ namespace storm { powerMethodMultiplicationStyle = nativeSettings.getPowerMethodMultiplicationStyle(); sorOmega = storm::utility::convertNumber(nativeSettings.getOmega()); forceBounds = nativeSettings.isForceBoundsSet(); + symmetricUpdates = nativeSettings.isForcePowerMethodSymmetricUpdatesSet(); + } NativeSolverEnvironment::~NativeSolverEnvironment() { @@ -86,5 +88,12 @@ namespace storm { forceBounds = value; } + bool NativeSolverEnvironment::isSymmetricUpdatesSet() const { + return symmetricUpdates; + } + void NativeSolverEnvironment::setSymmetricUpdates(bool value) { + symmetricUpdates = value; + } + } diff --git a/src/storm/environment/solver/NativeSolverEnvironment.h b/src/storm/environment/solver/NativeSolverEnvironment.h index 675b553b0..b3c9ce457 100644 --- a/src/storm/environment/solver/NativeSolverEnvironment.h +++ b/src/storm/environment/solver/NativeSolverEnvironment.h @@ -29,6 +29,8 @@ namespace storm { void setSorOmega(storm::RationalNumber const& value); bool isForceBoundsSet() const; void setForceBounds(bool value); + bool isSymmetricUpdatesSet() const; + void setSymmetricUpdates(bool value); private: storm::solver::NativeLinearEquationSolverMethod method; @@ -39,6 +41,7 @@ namespace storm { storm::solver::MultiplicationStyle powerMethodMultiplicationStyle; storm::RationalNumber sorOmega; bool forceBounds; + bool symmetricUpdates; }; } diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp index c0728c579..f918fe112 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp @@ -19,6 +19,7 @@ namespace storm { const std::string MinMaxEquationSolverSettings::absoluteOptionName = "absolute"; const std::string MinMaxEquationSolverSettings::lraMethodOptionName = "lramethod"; const std::string MinMaxEquationSolverSettings::valueIterationMultiplicationStyleOptionName = "vimult"; + const std::string MinMaxEquationSolverSettings::intervalIterationSymmetricUpdatesOptionName = "symmetricupdates"; const std::string MinMaxEquationSolverSettings::forceBoundsOptionName = "forcebounds"; const std::string MinMaxEquationSolverSettings::quickValueIterationRestartOptionName = "qvirestart"; @@ -41,6 +42,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, valueIterationMultiplicationStyleOptionName, false, "Sets which method multiplication style to prefer for value iteration.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a multiplication style.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(multiplicationStyles)).setDefaultValueString("gaussseidel").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, intervalIterationSymmetricUpdatesOptionName, false, "If set, interval iteration performs an update on both, lower and upper bound in each iteration").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, forceBoundsOptionName, false, "If set, minmax solver always require that a priori bounds for the solution are computed.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, quickValueIterationRestartOptionName, false, "Controls when a restart of quick value iteration is triggered.") @@ -118,6 +121,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown multiplication style '" << multiplicationStyleString << "'."); } + bool MinMaxEquationSolverSettings::isForceIntervalIterationSymmetricUpdatesSet() const { + return this->getOption(intervalIterationSymmetricUpdatesOptionName).getHasOptionBeenSet(); + } + bool MinMaxEquationSolverSettings::isForceBoundsSet() const { return this->getOption(forceBoundsOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.h b/src/storm/settings/modules/MinMaxEquationSolverSettings.h index eeb60be4e..02be37d00 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.h +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.h @@ -97,6 +97,11 @@ namespace storm { */ storm::solver::MultiplicationStyle getValueIterationMultiplicationStyle() const; + /*! + * Retrievew whether updates in interval iteration have to be made symmetrically + */ + bool isForceIntervalIterationSymmetricUpdatesSet() const; + /*! * Retrieves whether the force bounds option has been set. */ @@ -123,6 +128,7 @@ namespace storm { static const std::string absoluteOptionName; static const std::string lraMethodOptionName; static const std::string valueIterationMultiplicationStyleOptionName; + static const std::string intervalIterationSymmetricUpdatesOptionName; static const std::string forceBoundsOptionName; static const std::string quickValueIterationRestartOptionName; }; diff --git a/src/storm/settings/modules/NativeEquationSolverSettings.cpp b/src/storm/settings/modules/NativeEquationSolverSettings.cpp index a34679ae8..c07d56dff 100644 --- a/src/storm/settings/modules/NativeEquationSolverSettings.cpp +++ b/src/storm/settings/modules/NativeEquationSolverSettings.cpp @@ -24,6 +24,7 @@ namespace storm { const std::string NativeEquationSolverSettings::absoluteOptionName = "absolute"; const std::string NativeEquationSolverSettings::powerMethodMultiplicationStyleOptionName = "powmult"; const std::string NativeEquationSolverSettings::forceBoundsOptionName = "forcebounds"; + const std::string NativeEquationSolverSettings::powerMethodSymmetricUpdatesOptionName = "symmetricupdates"; NativeEquationSolverSettings::NativeEquationSolverSettings() : ModuleSettings(moduleName) { std::vector methods = { "jacobi", "gaussseidel", "sor", "walkerchae", "power", "ratsearch", "qpower" }; @@ -43,6 +44,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, forceBoundsOptionName, false, "If set, the equation solver always require that a priori bounds for the solution are computed.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, powerMethodSymmetricUpdatesOptionName, false, "If set, interval iteration performs an update on both, lower and upper bound in each iteration").build()); } bool NativeEquationSolverSettings::isLinearEquationSystemTechniqueSet() const { @@ -111,6 +113,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown multiplication style '" << multiplicationStyleString << "'."); } + bool NativeEquationSolverSettings::isForcePowerMethodSymmetricUpdatesSet() const { + return this->getOption(powerMethodSymmetricUpdatesOptionName).getHasOptionBeenSet(); + } + bool NativeEquationSolverSettings::isForceBoundsSet() const { return this->getOption(forceBoundsOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/NativeEquationSolverSettings.h b/src/storm/settings/modules/NativeEquationSolverSettings.h index 67d68cb2d..1562a89c2 100644 --- a/src/storm/settings/modules/NativeEquationSolverSettings.h +++ b/src/storm/settings/modules/NativeEquationSolverSettings.h @@ -93,6 +93,11 @@ namespace storm { */ ConvergenceCriterion getConvergenceCriterion() const; + /*! + * Retrievew whether updates in power method have to be made symmetrically + */ + bool isForcePowerMethodSymmetricUpdatesSet() const; + /*! * Retrieves the multiplication style to use in the power method. * @@ -118,6 +123,7 @@ namespace storm { static const std::string maximalIterationsOptionShortName; static const std::string precisionOptionName; static const std::string absoluteOptionName; + static const std::string powerMethodSymmetricUpdatesOptionName; static const std::string powerMethodMultiplicationStyleOptionName; static const std::string forceBoundsOptionName; diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 927c57d46..0acb770fe 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -465,7 +465,7 @@ namespace storm { SolverStatus status = SolverStatus::InProgress; bool doConvergenceCheck = true; - bool useDiffs = this->hasRelevantValues(); + bool useDiffs = this->hasRelevantValues() && !env.solver().minMax().isSymmetricUpdatesSet(); std::vector oldValues; if (useGaussSeidelMultiplication && useDiffs) { oldValues.resize(this->getRelevantValues().getNumberOfSetBits()); diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index 06e9efebb..b82737803 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -417,7 +417,7 @@ namespace storm { bool terminate = false; uint64_t iterations = 0; bool doConvergenceCheck = true; - bool useDiffs = this->hasRelevantValues(); + bool useDiffs = this->hasRelevantValues() && !env.solver().native().isSymmetricUpdatesSet(); std::vector oldValues; if (useGaussSeidelMultiplication && useDiffs) { oldValues.resize(this->getRelevantValues().getNumberOfSetBits());