diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index 4c841acaa..62e791829 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -26,7 +26,8 @@ namespace storm { this->addModule(std::unique_ptr(new modules::NativeEquationSolverSettings(*this))); this->addModule(std::unique_ptr(new modules::BisimulationSettings(*this))); this->addModule(std::unique_ptr(new modules::GlpkSettings(*this))); - this->addModule(std::unique_ptr(new modules::GurobiSettings(*this))); + this->addModule(std::unique_ptr(new modules::GurobiSettings(*this))); + this->addModule(std::unique_ptr(new modules::TopologicalValueIterationEquationSolverSettings(*this))); } SettingsManager::~SettingsManager() { @@ -506,6 +507,10 @@ namespace storm { storm::settings::modules::GurobiSettings const& gurobiSettings() { return dynamic_cast(manager().getModule(storm::settings::modules::GurobiSettings::moduleName)); - } + } + + storm::settings::modules::TopologicalValueIterationEquationSolverSettings const& topologicalValueIterationEquationSolverSettings() { + return dynamic_cast(manager().getModule(storm::settings::modules::TopologicalValueIterationEquationSolverSettings::moduleName)); + } } } \ No newline at end of file diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index 9d597ca2e..00a679358 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -28,6 +28,7 @@ #include "src/settings/modules/BisimulationSettings.h" #include "src/settings/modules/GlpkSettings.h" #include "src/settings/modules/GurobiSettings.h" +#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" #include "src/utility/macros.h" #include "src/exceptions/OptionParserException.h" @@ -307,7 +308,14 @@ namespace storm { * * @return An object that allows accessing the settings of Gurobi. */ - storm::settings::modules::GurobiSettings const& gurobiSettings(); + storm::settings::modules::GurobiSettings const& gurobiSettings(); + + /*! + * Retrieves the settings of the topological value iteration-based equation solver. + * + * @return An object that allows accessing the settings of the topological value iteration-based equation solver. + */ + storm::settings::modules::TopologicalValueIterationEquationSolverSettings const& topologicalValueIterationEquationSolverSettings(); } // namespace settings } // namespace storm diff --git a/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp b/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp new file mode 100644 index 000000000..a277ac07a --- /dev/null +++ b/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp @@ -0,0 +1,58 @@ +#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" + +#include "src/settings/SettingsManager.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string TopologicalValueIterationEquationSolverSettings::moduleName = "topologicalValueIteration"; + const std::string TopologicalValueIterationEquationSolverSettings::maximalIterationsOptionName = "maxiter"; + const std::string TopologicalValueIterationEquationSolverSettings::maximalIterationsOptionShortName = "i"; + const std::string TopologicalValueIterationEquationSolverSettings::precisionOptionName = "precision"; + const std::string TopologicalValueIterationEquationSolverSettings::absoluteOptionName = "absolute"; + + TopologicalValueIterationEquationSolverSettings::TopologicalValueIterationEquationSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { + + this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(20000).build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build()); + } + + bool TopologicalValueIterationEquationSolverSettings::isMaximalIterationCountSet() const { + return this->getOption(maximalIterationsOptionName).getHasOptionBeenSet(); + } + + uint_fast64_t TopologicalValueIterationEquationSolverSettings::getMaximalIterationCount() const { + return this->getOption(maximalIterationsOptionName).getArgumentByName("count").getValueAsUnsignedInteger(); + } + + bool TopologicalValueIterationEquationSolverSettings::isPrecisionSet() const { + return this->getOption(precisionOptionName).getHasOptionBeenSet(); + } + + double TopologicalValueIterationEquationSolverSettings::getPrecision() const { + return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble(); + } + + bool TopologicalValueIterationEquationSolverSettings::isConvergenceCriterionSet() const { + return this->getOption(absoluteOptionName).getHasOptionBeenSet(); + } + + TopologicalValueIterationEquationSolverSettings::ConvergenceCriterion TopologicalValueIterationEquationSolverSettings::getConvergenceCriterion() const { + return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? TopologicalValueIterationEquationSolverSettings::ConvergenceCriterion::Absolute : TopologicalValueIterationEquationSolverSettings::ConvergenceCriterion::Relative; + } + + bool TopologicalValueIterationEquationSolverSettings::check() const { + bool optionsSet = isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet(); + + STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx || !optionsSet, "gmm++ is not selected as the equation solver, so setting options for gmm++ has no effect."); + + return true; + } + + } // namespace modules + } // namespace settings +} // namespace storm \ No newline at end of file diff --git a/src/settings/modules/TopologicalValueIterationEquationSolverSettings.h b/src/settings/modules/TopologicalValueIterationEquationSolverSettings.h new file mode 100644 index 000000000..fc9a901f2 --- /dev/null +++ b/src/settings/modules/TopologicalValueIterationEquationSolverSettings.h @@ -0,0 +1,87 @@ +#ifndef STORM_SETTINGS_MODULES_TOPOLOGICALVALUEITERATIONSETTINGS_H_ +#define STORM_SETTINGS_MODULES_TOPOLOGICALVALUEITERATIONSETTINGS_H_ + +#include "src/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the settings for topological value iteration. + */ + class TopologicalValueIterationEquationSolverSettings : public ModuleSettings { + public: + + // An enumeration of all available convergence criteria. + enum class ConvergenceCriterion { Absolute, Relative }; + + /*! + * Creates a new set of topological value iteration settings that is managed by the given manager. + * + * @param settingsManager The responsible manager. + */ + TopologicalValueIterationEquationSolverSettings(storm::settings::SettingsManager& settingsManager); + + + /*! + * Retrieves whether the maximal iteration count has been set. + * + * @return True iff the maximal iteration count has been set. + */ + bool isMaximalIterationCountSet() const; + + /*! + * Retrieves the maximal number of iterations to perform until giving up on converging. + * + * @return The maximal iteration count. + */ + uint_fast64_t getMaximalIterationCount() const; + + /*! + * Retrieves whether the precision has been set. + * + * @return True iff the precision has been set. + */ + bool isPrecisionSet() const; + + /*! + * Retrieves the precision that is used for detecting convergence. + * + * @return The precision to use for detecting convergence. + */ + double getPrecision() const; + + /*! + * Retrieves whether the convergence criterion has been set. + * + * @return True iff the convergence criterion has been set. + */ + bool isConvergenceCriterionSet() const; + + /*! + * Retrieves the selected convergence criterion. + * + * @return The selected convergence criterion. + */ + ConvergenceCriterion getConvergenceCriterion() const; + + bool check() const override; + + // The name of the module. + static const std::string moduleName; + + private: + // Define the string names of the options as constants. + static const std::string techniqueOptionName; + static const std::string maximalIterationsOptionName; + static const std::string maximalIterationsOptionShortName; + static const std::string precisionOptionName; + static const std::string absoluteOptionName; + }; + + } // namespace modules + } // namespace settings +} // namespace storm + +#endif /* STORM_SETTINGS_MODULES_TOPOLOGICALVALUEITERATIONSETTINGS_H_ */ diff --git a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp index c8fbf9a4e..41d8d8156 100644 --- a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp +++ b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp @@ -3,7 +3,7 @@ #include #include -#include "src/settings/Settings.h" +#include "src/settings/SettingsManager.h" #include "src/utility/vector.h" #include "src/utility/graph.h" #include "src/models/PseudoModel.h" @@ -26,12 +26,16 @@ namespace storm { template TopologicalValueIterationNondeterministicLinearEquationSolver::TopologicalValueIterationNondeterministicLinearEquationSolver() { // Get the settings object to customize solving. - storm::settings::Settings* settings = storm::settings::Settings::getInstance(); - + + //storm::settings::Settings* settings = storm::settings::Settings::getInstance(); + auto settings = storm::settings::topologicalValueIterationEquationSolverSettings(); // Get appropriate settings. - this->maximalNumberOfIterations = settings->getOptionByLongName("maxiter").getArgument(0).getValueAsUnsignedInteger(); - this->precision = settings->getOptionByLongName("precision").getArgument(0).getValueAsDouble(); - this->relative = !settings->isSet("absolute"); + //this->maximalNumberOfIterations = settings->getOptionByLongName("maxiter").getArgument(0).getValueAsUnsignedInteger(); + //this->precision = settings->getOptionByLongName("precision").getArgument(0).getValueAsDouble(); + //this->relative = !settings->isSet("absolute"); + this->maximalNumberOfIterations = settings.getMaximalIterationCount(); + this->precision = settings.getPrecision(); + this->relative = (settings.getConvergenceCriterion() == TopologicalValueIterationEquationSolverSettings::ConvergenceCriterion::Relative); } template diff --git a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h index bdbf788cd..1cfd98db4 100644 --- a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h +++ b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h @@ -48,13 +48,13 @@ namespace storm { std::vector> getOptimalGroupingFromTopologicalSccDecomposition(storm::storage::StronglyConnectedComponentDecomposition const& sccDecomposition, std::vector const& topologicalSort, storm::storage::SparseMatrix const& matrix) const; }; - template - bool __basicValueIteration_mvReduce_uint64_minimize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, size_t& iterationCount) { + template + bool __basicValueIteration_mvReduce_uint64_minimize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, size_t& iterationCount) { // throw; } template <> - inline bool __basicValueIteration_mvReduce_uint64_minimize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, size_t& iterationCount) { + inline bool __basicValueIteration_mvReduce_uint64_minimize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, size_t& iterationCount) { #ifdef STORM_HAVE_CUDAFORSTORM return basicValueIteration_mvReduce_uint64_double_minimize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount); #else @@ -62,7 +62,7 @@ namespace storm { #endif } template <> - inline bool __basicValueIteration_mvReduce_uint64_minimize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, size_t& iterationCount) { + inline bool __basicValueIteration_mvReduce_uint64_minimize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, size_t& iterationCount) { #ifdef STORM_HAVE_CUDAFORSTORM return basicValueIteration_mvReduce_uint64_float_minimize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount); #else @@ -70,13 +70,13 @@ namespace storm { #endif } - template - bool __basicValueIteration_mvReduce_uint64_maximize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, size_t& iterationCount) { + template + bool __basicValueIteration_mvReduce_uint64_maximize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, size_t& iterationCount) { // throw; } template <> - inline bool __basicValueIteration_mvReduce_uint64_maximize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, size_t& iterationCount) { + inline bool __basicValueIteration_mvReduce_uint64_maximize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, size_t& iterationCount) { #ifdef STORM_HAVE_CUDAFORSTORM return basicValueIteration_mvReduce_uint64_double_maximize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount); #else @@ -84,7 +84,7 @@ namespace storm { #endif } template <> - inline bool __basicValueIteration_mvReduce_uint64_maximize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, size_t& iterationCount) { + inline bool __basicValueIteration_mvReduce_uint64_maximize(uint_fast64_t const maxIterationCount, double const precision, bool const relativePrecisionCheck, std::vector const& matrixRowIndices, std::vector> const& columnIndicesAndValues, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, size_t& iterationCount) { #ifdef STORM_HAVE_CUDAFORSTORM return basicValueIteration_mvReduce_uint64_float_maximize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount); #else