From acdced1fee417ad088eef5d20164414f1e1ca6ab Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 20 Sep 2014 22:51:54 +0200
Subject: [PATCH] Will this ever end?
Former-commit-id: fbe20506cd1ffca6c36eee8d584d4f895f80141e
---
src/settings/InternalSettingsMemento.h | 61 ----
src/settings/SettingMemento.cpp | 22 ++
src/settings/SettingMemento.h | 45 +++
src/settings/SettingsManager.cpp | 1 +
src/settings/SettingsManager.h | 299 +++++++-----------
src/settings/modules/GeneralSettings.h | 46 +--
src/settings/modules/GlpkSettings.cpp | 3 +-
src/settings/modules/GlpkSettings.h | 1 +
...gs.cpp => GmmxxEquationSolverSettings.cpp} | 22 +-
...ttings.h => GmmxxEquationSolverSettings.h} | 20 +-
src/settings/modules/GurobiSettings.cpp | 17 +-
src/settings/modules/GurobiSettings.h | 33 ++
src/settings/modules/ModuleSettings.cpp | 8 +
src/settings/modules/ModuleSettings.h | 53 ++++
.../modules/NativeEquationSolverSettings.cpp | 29 +-
.../modules/NativeEquationSolverSettings.h | 43 +++
16 files changed, 375 insertions(+), 328 deletions(-)
delete mode 100644 src/settings/InternalSettingsMemento.h
create mode 100644 src/settings/SettingMemento.cpp
create mode 100644 src/settings/SettingMemento.h
rename src/settings/modules/{GmmxxSettings.cpp => GmmxxEquationSolverSettings.cpp} (74%)
rename src/settings/modules/{GmmxxSettings.h => GmmxxEquationSolverSettings.h} (83%)
diff --git a/src/settings/InternalSettingsMemento.h b/src/settings/InternalSettingsMemento.h
deleted file mode 100644
index 48b3bce9f..000000000
--- a/src/settings/InternalSettingsMemento.h
+++ /dev/null
@@ -1,61 +0,0 @@
-#ifndef STORM_SETTINGS_INTERNALSETTINGMEMENTO_H_
-#define STORM_SETTINGS_INTERNALSETTINGMEMENTO_H_
-
-#include "src/settings/SettingsManager.h"
-#include "log4cplus/logger.h"
-#include "log4cplus/loggingmacros.h"
-
-extern log4cplus::Logger logger;
-
-namespace storm {
- namespace settings {
-
- /*!
- * NOTE: THIS CLASS IS FOR INTERNAL USE IN THE TESTS ONLY.
- *
- * If an option is required to be set when executing a test the test may instantiate an object of this class
- * while the test itself is executed. This object then ensures that the option has the requested value and
- * resets it to its previous value as soon as its destructor is called.
- */
- class InternalSettingMemento {
- public:
- /*!
- * Constructs a new memento for the specified option.
- *
- * @param moduleName The name of the module that registered the option.
- * @param longOptionName The long name of the option.
- * @param requiredHasBeenSetState A flag that indicates whether the setting is to be temporarily set to
- * true or false.
- */
- InternalOptionMemento(std::string const& moduleName, std::string const& longOptionName, bool requiredHasBeenSetState): optionName(longOptionName), stateBefore() {
- this->stateBefore = storm::settings::SettingsManager::manager().isSet(optionName);
- if (requiredHasBeenSetState) {
- storm::settings::SettingsManager::manager()..set(optionName);
- } else {
- storm::settings::SettingsManager::manager().unset(optionName);
- }
- }
-
- /*!
- * Destructs the memento object and resets the value of the option to its original state.
- */
- virtual ~InternalOptionMemento() {
- if (stateBefore) {
- storm::settings::SettingsManager::manager().set(optionName);
- } else {
- storm::settings::SettingsManager::manager().unset(optionName);
- }
- }
-
- private:
- // The long name of the option that was temporarily set.
- std::string const optionName;
-
- // The state of the option before it was set.
- bool stateBefore;
- };
-
- } // namespace settings
-} // namespace storm
-
-#endif // STORM_SETTINGS_INTERNALSETTINGMEMENTO_H_
\ No newline at end of file
diff --git a/src/settings/SettingMemento.cpp b/src/settings/SettingMemento.cpp
new file mode 100644
index 000000000..5a1a55390
--- /dev/null
+++ b/src/settings/SettingMemento.cpp
@@ -0,0 +1,22 @@
+#include "src/settings/SettingsMemento.h"
+
+#include "src/settings/modules/ModuleSettings.h"
+
+namespace storm {
+ namespace settings {
+ SettingMemento::SettingMemento(ModuleSettings& settings, std::string const& longOptionName, bool resetToState) : settings(settings), optionName(longOptionName), resetToState(resetToState) {
+ // Intentionally left empty.
+ }
+
+ /*!
+ * Destructs the memento object and resets the value of the option to its original state.
+ */
+ virtual SettingMemento::~SettingMemento() {
+ if (resetToState) {
+ settings.set(optionName);
+ } else {
+ settings.unset(optionName);
+ }
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/settings/SettingMemento.h b/src/settings/SettingMemento.h
new file mode 100644
index 000000000..342cdd666
--- /dev/null
+++ b/src/settings/SettingMemento.h
@@ -0,0 +1,45 @@
+#ifndef STORM_SETTINGS_SETTINGMEMENTO_H_
+#define STORM_SETTINGS_SETTINGMEMENTO_H_
+
+#include "src/settings/SettingsManager.h"
+
+namespace storm {
+ namespace settings {
+
+ class ModuleSettings;
+
+ /*!
+ * This class is used to reset the state of an option that was temporarily set to a different status.
+ */
+ class SettingMemento {
+ public:
+ /*!
+ * Constructs a new memento for the specified option.
+ *
+ * @param settings The settings object in which to restore the state of the option.
+ * @param longOptionName The long name of the option.
+ * @param resetToState A flag that indicates the status to which the option is to be reset upon
+ * deconstruction of this object.
+ */
+ SettingMemento(ModuleSettings& settings, std::string const& longOptionName, bool resetToState);
+
+ /*!
+ * Destructs the memento object and resets the value of the option to its original state.
+ */
+ virtual ~SettingMemento();
+
+ private:
+ // The settings object in which the setting is to be restored.
+ ModuleSettings& settings;
+
+ // The long name of the option that was temporarily set.
+ std::string const optionName;
+
+ // The state of the option before it was set.
+ bool resetToState;
+ };
+
+ } // namespace settings
+} // namespace storm
+
+#endif // STORM_SETTINGS_SETTINGMEMENTO_H_
\ No newline at end of file
diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index 17f8a145e..2581edd52 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -21,6 +21,7 @@ namespace storm {
return settingsManager;
}
+
}
}
diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h
index e1bf4f46b..2f719b6f2 100644
--- a/src/settings/SettingsManager.h
+++ b/src/settings/SettingsManager.h
@@ -4,6 +4,7 @@
#include <iostream>
#include <sstream>
#include <list>
+#include <set>
#include <utility>
#include <functional>
#include <unordered_map>
@@ -22,7 +23,7 @@
#include "src/settings/modules/DebugSettings.h"
#include "src/settings/modules/CounterexampleGeneratorSettings.h"
#include "src/settings/modules/CuddSettings.h"
-#include "src/settings/modules/GmmxxSettings.h"
+#include "src/settings/modules/GmmxxEquationSolverSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/settings/modules/GlpkSettings.h"
#include "src/settings/modules/GurobiSettings.h"
@@ -31,109 +32,108 @@
#include "src/exceptions/OptionParserException.h"
namespace storm {
-
namespace settings {
- typedef std::pair<std::string, std::string> stringPair_t;
-
class InternalOptionMemento;
/*!
- * @brief Settings class with command line parser and type validation
- *
- *
- * It is meant to be used as a singleton. Call
- * @code storm::settings::Settings::getInstance() @endcode
- * to initialize it and obtain an instance.
- *
- * This class can be customized by other parts of the software using
- * option modules. An option module can be anything that implements the
- * interface specified by registerModule() and does a static initialization call to this function.
+ * Provides the central API for the registration of command line options and parsing the options from the
+ * command line. Since this class is a singleton, the only instance is accessible via a call to the manager()
+ * function.
*/
class SettingsManager {
public:
+ // Declare the memento class as a friend so it can manipulate the internal state.
friend class InternalOptionMemento;
- /*!
- * This parses the command line of the application and matches it to all prior registered options
- * @throws OptionParserException
- */
- static void parse(int const argc, char const * const argv[]);
-
- std::vector<std::shared_ptr<Option>> const& getOptions() const {
- return this->optionPointers;
- }
-
- // PUBLIC INTERFACE OF OPTIONSACCUMULATOR (now internal)
- /*!
- * Returns true IFF an option with the specified longName exists.
+ /*!
+ * This function parses the given command line arguments and sets all registered options accordingly. If the
+ * command line cannot be matched using the known options, an exception is thrown.
+ *
+ * @param argc The number of command line arguments.
+ * @param argv The command line arguments.
*/
- bool containsOptionByLongName(std::string const& longName) const {
- return this->containsLongName(longName);
- }
+ static void setFromCommandLine(int const argc, char const * const argv[]);
- /*!
- * Returns true IFF an option with the specified shortName exists.
+ /*!
+ * This function parses the given command line arguments (represented by one big string) and sets all
+ * registered options accordingly. If the command line cannot be matched using the known options, an
+ * exception is thrown.
+ *
+ * @param commandLineString The command line arguments as one string.
*/
- bool containsOptionByShortName(std::string const& shortName) const {
- return this->containsLongName(shortName);
- }
+ static void setFromString(std::string const& commandLineString);
- /*!
- * Returns a reference to the Option with the specified longName.
- * Throws an Exception of Type IllegalArgumentException if there is no such Option.
+ /*!
+ * This function parses the given command line arguments (represented by several strings) and sets all
+ * registered options accordingly. If the command line cannot be matched using the known options, an
+ * exception is thrown.
+ *
+ * @param commandLineArguments The command line arguments.
*/
- Option const& getOptionByLongName(std::string const& longName) const {
- return this->getByLongName(longName);
- }
+ static void setFromExplodedString(std::vector<std::string> const& commandLineArguments);
- /*!
- * Returns a reference to the Option with the specified shortName.
- * Throws an Exception of Type IllegalArgumentException if there is no such Option.
+ /*!
+ * This function parses the given file and sets all registered options accordingly. If the settings cannot
+ * be matched using the known options, an exception is thrown.
*/
- Option const& getOptionByShortName(std::string const& shortName) const {
- return this->getByShortName(shortName);
- }
-
- /*!
- * Adds the given option to the set of known options.
- * Unifying with existing options is done automatically.
- * Ownership of the Option is handed over when calling this function!
- * Returns a reference to the settings instance
- * @throws OptionUnificationException
- */
- SettingsManager& addOption(Option* option);
-
- /*!
- * Returns true iff there is an Option with the specified longName and it has been set
- * @return bool true if the option exists and has been set
- * @throws InvalidArgumentException
- */
- bool isSet(std::string const& longName) const {
- return this->getByLongName(longName).getHasOptionBeenSet();
- }
-
- /*!
- * This generated a list of all registered options and their arguments together with descriptions and defaults.
- * @return A std::string containing the help text, delimited by \n
- */
- std::string getHelpText() const;
+ static void setFromConfigurationFile(std::string const& configFilename);
/*!
- * Registers a new module with the given name and options. If the module could not be successfully registered,
- * an exception is thrown.
+ * Retrieves the general settings.
*
- * @param moduleName The name of the module to register.
- * @param options The set of options that the module registers.
+ * @return An object that allows accessing the general settings.
*/
- void registerModule(std::string const& moduleName, std::vector<std::shared_ptr<Option>> const& options);
-
- /*!
- * Retrieves the only existing instance of a settings manager.
+ storm::settings::modules::GeneralSettings const& getGeneralSettings() const;
+
+ /*!
+ * Retrieves the debug settings.
*
- * @return The only existing instance of a settings manager
- */
- static SettingsManager& manager();
+ * @return An object that allows accessing the debug settings.
+ */
+ storm::settings::modules::DebugSettings const& getDebugSettings() const;
+
+ /*!
+ * Retrieves the counterexample generator settings.
+ *
+ * @return An object that allows accessing the counterexample generator settings.
+ */
+ storm::settings::modules::CounterexampleGeneratorSettings const& getCounterexampleGeneratorSettings() const;
+
+ /*!
+ * Retrieves the CUDD settings.
+ *
+ * @return An object that allows accessing the CUDD settings.
+ */
+ storm::settings::modules::CuddSettings const& getCuddSettings() const;
+
+ /*!
+ * Retrieves the settings of the gmm++-based equation solver.
+ *
+ * @return An object that allows accessing the settings of the gmm++-based equation solver.
+ */
+ storm::settings::modules::GmmxxEquationSolverSettings const& getGmmxxEquationSolverSettings() const;
+
+ /*!
+ * Retrieves the settings of the native equation solver.
+ *
+ * @return An object that allows accessing the settings of the native equation solver.
+ */
+ storm::settings::modules::NativeEquationSolverSettings const& getNativeEquationSolverSettings() const;
+
+ /*!
+ * Retrieves the settings of glpk.
+ *
+ * @return An object that allows accessing the settings of glpk.
+ */
+ storm::settings::modules::GlpkSettings const& getGlpkSettings() const;
+
+ /*!
+ * Retrieves the settings of Gurobi.
+ *
+ * @return An object that allows accessing the settings of Gurobi.
+ */
+ storm::settings::modules::GurobiSettings const& getGurobiSettings() const;
private:
/*!
@@ -160,7 +160,7 @@ namespace storm {
storm::settings::modules::CuddSettings cuddSettings;
// An object that provides access to the gmm++ settings.
- storm::settings::modules::GmmxxSettings gmmxxSettings;
+ storm::settings::modules::GmmxxEquationSolverSettings gmmxxEquationSolverSettings;
// An object that provides access to the native equation solver settings.
storm::settings::modules::NativeEquationSolverSettings nativeEquationSolverSettings;
@@ -174,29 +174,38 @@ namespace storm {
// The single instance of the manager class. Since it's static, it will automatically be distructed upon termination.
static SettingsManager settingsManager;
-
+ // A set of all known (i.e. registered) module names.
+ std::set<std::string> moduleNames;
+
+ // A mapping from all known option names to the options that match it. All options for one option name need
+ // to be compatible in the sense that calling isCompatible(...) pairwise on all options must always return true.
+ std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> options;
/*!
- * Parser for the commdand line parameters of the program.
- * The first entry of argv will be ignored, as it represents the program name.
- * @throws OptionParserException
- */
- void parseCommandLine(int const argc, char const * const argv[]);
-
- /*!
- * The map holding the information regarding registered options and their types
+ * This function prints a help message to the standard output. Optionally, a module name can be given. If
+ * it is present, name must correspond to a known module. Then, only the help text for this module is
+ * printed.
+ *
+ * @return moduleName The name of the module for which to show the help or "all" if the full help text is to
+ * be printed.
*/
- std::unordered_map<std::string, std::shared_ptr<Option>> options;
+ void printHelp(std::string const& moduleName = "all") const;
- /*!
- * The vector holding a pointer to all options
+ /*!
+ * Registers a new module with the given name and options. If the module could not be successfully registered,
+ * an exception is thrown.
+ *
+ * @param moduleName The name of the module to register.
+ * @param options The set of options that the module registers.
*/
- std::vector<std::shared_ptr<Option>> optionPointers;
+ void registerModule(std::string const& moduleName, std::vector<std::shared_ptr<Option>> const& options);
- /*!
- * The map holding the information regarding registered options and their short names
+ /*!
+ * Retrieves the only existing instance of a settings manager.
+ *
+ * @return The only existing instance of a settings manager
*/
- std::unordered_map<std::string, std::string> shortNames;
+ static SettingsManager& manager();
// Helper functions
stringPair_t splitOptionString(std::string const& option);
@@ -205,98 +214,6 @@ namespace storm {
std::vector<std::string> argvToStringArray(int const argc, char const * const argv[]);
std::vector<bool> scanForOptions(std::vector<std::string> const& arguments);
bool checkArgumentSyntaxForOption(std::string const& argvString);
-
- /*!
- * Returns true IFF this contains an option with the specified longName.
- * @return bool true iff there is an option with the specified longName
- */
- bool containsLongName(std::string const& longName) const {
- return (this->options.find(longName) != this->options.end());
- }
-
- /*!
- * Returns true IFF this contains an option with the specified shortName.
- * @return bool true iff there is an option with the specified shortName
- */
- bool containsShortName(std::string const& shortName) const {
- return (this->shortNames.find(shortName) != this->shortNames.end());
- }
-
- /*!
- * Returns a reference to the Option with the specified longName.
- * Throws an Exception of Type InvalidArgumentException if there is no such Option.
- * @throws InvalidArgumentException
- */
- Option& getByLongName(std::string const& longName) const {
- auto longNameIterator = this->options.find(longName);
- if (longNameIterator == this->options.end()) {
- LOG4CPLUS_ERROR(logger, "Settings::getByLongName: This program does not contain an option named \"" << longName << "\".");
- throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << longName << "\".";
- }
- return *longNameIterator->second.get();
- }
-
- /*!
- * Returns a pointer to the Option with the specified longName.
- * Throws an Exception of Type InvalidArgumentException if there is no such Option.
- * @throws InvalidArgumentException
- */
- Option* getPtrByLongName(std::string const& longName) const {
- auto longNameIterator = this->options.find(longName);
- if (longNameIterator == this->options.end()) {
- LOG4CPLUS_ERROR(logger, "Settings::getPtrByLongName: This program does not contain an option named \"" << longName << "\".");
- throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << longName << "\".";
- }
- return longNameIterator->second.get();
- }
-
- /*!
- * Returns a reference to the Option with the specified shortName.
- * Throws an Exception of Type InvalidArgumentException if there is no such Option.
- * @throws InvalidArgumentException
- */
- Option& getByShortName(std::string const& shortName) const {
- auto shortNameIterator = this->shortNames.find(shortName);
- if (shortNameIterator == this->shortNames.end()) {
- LOG4CPLUS_ERROR(logger, "Settings::getByShortName: This program does not contain an option named \"" << shortName << "\".");
- throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << shortName << "\"";
- }
- return *(this->options.find(shortNameIterator->second)->second.get());
- }
-
- /*!
- * Returns a pointer to the Option with the specified shortName.
- * Throws an Exception of Type InvalidArgumentException if there is no such Option.
- * @throws InvalidArgumentException
- */
- Option* getPtrByShortName(std::string const& shortName) const {
- auto shortNameIterator = this->shortNames.find(shortName);
- if (shortNameIterator == this->shortNames.end()) {
- LOG4CPLUS_ERROR(logger, "Settings::getPtrByShortName: This program does not contain an option named \"" << shortName << "\".");
- throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << shortName << "\".";
- }
- return this->options.find(shortNameIterator->second)->second.get();
- }
-
- /*!
- * Sets the Option with the specified longName
- * This function requires the Option to have no arguments
- * This is for TESTING only and should not be used outside of the testing code!
- * @throws InvalidArgumentException
- */
- void set(std::string const& longName) const {
- return this->getByLongName(longName).setHasOptionBeenSet();
- }
-
- /*!
- * Unsets the Option with the specified longName
- * This function requires the Option to have no arguments
- * This is for TESTING only and should not be used outside of the testing code!
- * @throws InvalidArgumentException
- */
- void unset(std::string const& longName) const {
- return this->getByLongName(longName).setHasOptionBeenSet(false);
- }
};
} // namespace settings
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index 9640c5acc..9f5c55c7f 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/src/settings/modules/GeneralSettings.h
@@ -12,6 +12,12 @@ namespace storm {
*/
class GeneralSettings : public ModuleSettings {
public:
+ // An enumeration of all available LP solvers.
+ enum class LpSolver { Gurobi, glpk };
+
+ // An enumeration of all available equation solvers.
+ enum class EquationSolver { Gmmxx, Native };
+
/*!
* Creates a new set of general settings that is managed by the given manager.
*
@@ -216,46 +222,18 @@ namespace storm {
uint_fast64_t getTimeoutInSeconds() const;
/*!
- * Retrieves whether the eqsolver option was set.
- *
- * @return True if the eqsolver option was set.
- */
- bool isEqSolverSet() const;
-
- /*!
- * Retrieves whether the gmm++ equation solver is to be used.
- *
- * @return True iff the gmm++ equation solver is to be used.
- */
- bool useGmmxxEquationSolver() const;
-
- /*!
- * Retrieves whether the native equation solver is to be used.
- *
- * @return True iff the native equation solver is to be used.
- */
- bool useNativeEquationSolver() const;
-
- /*!
- * Retrieves whether the lpsolver option was set.
- *
- * @return True if the lpsolver option was set.
- */
- bool isLpSolverSet() const;
-
- /*!
- * Retrieves whether glpk is to be used.
+ * Retrieves the selected equation solver.
*
- * @return True iff glpk is to be used.
+ * @return The selected convergence criterion.
*/
- bool useGlpk() const;
+ EquationSolver getEquationSolver() const;
/*!
- * Retrieves whether Gurobi is to be used.
+ * Retrieves the selected LP solver.
*
- * @return True iff Gurobi is to be used.
+ * @return The selected LP solver.
*/
- bool useGurobi() const;
+ LpSolver getLpSolver() const;
/*!
* Retrieves whether the export-to-dot option was set.
diff --git a/src/settings/modules/GlpkSettings.cpp b/src/settings/modules/GlpkSettings.cpp
index ebeb91905..7b859c143 100644
--- a/src/settings/modules/GlpkSettings.cpp
+++ b/src/settings/modules/GlpkSettings.cpp
@@ -7,13 +7,14 @@ namespace storm {
namespace modules {
const std::string GlpkSettings::moduleName = "glpk";
+ const std::string GlpkSettings::integerToleranceOption = "inttol";
const std::string GlpkSettings::outputOptionName = "output";
GlpkSettings::GlpkSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
// First, we need to create all options of this module.
std::vector<std::shared_ptr<Option>> options;
options.push_back(storm::settings::OptionBuilder(moduleName, outputOptionName, true, "If set, the glpk output will be printed to the command line.").build());
-
+ options.push_back(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets glpk's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
// Finally, register all options that we just created.
settingsManager.registerModule(moduleName, options);
}
diff --git a/src/settings/modules/GlpkSettings.h b/src/settings/modules/GlpkSettings.h
index 9d0cd0f54..37420d117 100644
--- a/src/settings/modules/GlpkSettings.h
+++ b/src/settings/modules/GlpkSettings.h
@@ -29,6 +29,7 @@ namespace storm {
private:
// Define the string names of the options as constants.
static const std::string moduleName;
+ static const std::string integerToleranceOption;
static const std::string outputOptionName;
};
diff --git a/src/settings/modules/GmmxxSettings.cpp b/src/settings/modules/GmmxxEquationSolverSettings.cpp
similarity index 74%
rename from src/settings/modules/GmmxxSettings.cpp
rename to src/settings/modules/GmmxxEquationSolverSettings.cpp
index 2dc68b3f4..1e66f2b4f 100644
--- a/src/settings/modules/GmmxxSettings.cpp
+++ b/src/settings/modules/GmmxxEquationSolverSettings.cpp
@@ -1,4 +1,4 @@
-#include "src/settings/modules/GmmxxSettings.h"
+#include "src/settings/modules/GmmxxEquationSolverSettings.h"
#include "src/settings/SettingsManager.h"
@@ -6,16 +6,16 @@ namespace storm {
namespace settings {
namespace modules {
- const std::string GmmxxSettings::moduleName = "gmm++";
- const std::string GmmxxSettings::techniqueOptionName = "tech";
- const std::string GmmxxSettings::preconditionOptionName = "precond";
- const std::string GmmxxSettings::restartOptionName = "restart";
- const std::string GmmxxSettings::maximalIterationsOptionName = "maxiter";
- const std::string GmmxxSettings::maximalIterationsOptionShortName = "maxiter";
- const std::string GmmxxSettings::precisionOptionName = "precision";
- const std::string GmmxxSettings::absoluteOptionName = "absolute";
+ const std::string GmmxxEquationSolverSettings::moduleName = "gmm++";
+ const std::string GmmxxEquationSolverSettings::techniqueOptionName = "tech";
+ const std::string GmmxxEquationSolverSettings::preconditionOptionName = "precond";
+ const std::string GmmxxEquationSolverSettings::restartOptionName = "restart";
+ const std::string GmmxxEquationSolverSettings::maximalIterationsOptionName = "maxiter";
+ const std::string GmmxxEquationSolverSettings::maximalIterationsOptionShortName = "i";
+ const std::string GmmxxEquationSolverSettings::precisionOptionName = "precision";
+ const std::string GmmxxEquationSolverSettings::absoluteOptionName = "absolute";
- GmmxxSettings::GmmxxSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
+ GmmxxEquationSolverSettings::GmmxxEquationSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
// First, we need to create all options of this module.
std::vector<std::shared_ptr<Option>> options;
std::vector<std::string> methods = {"bicgstab", "qmr", "gmres", "jacobi"};
@@ -31,7 +31,7 @@ namespace storm {
options.push_back(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "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());
- options.push_back(storm::settings::OptionBuilder(moduleName, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for deciding convergence.").build());
+ options.push_back(storm::settings::OptionBuilder(moduleName, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
// Finally, register all options that we just created.
settingsManager.registerModule(moduleName, options);
diff --git a/src/settings/modules/GmmxxSettings.h b/src/settings/modules/GmmxxEquationSolverSettings.h
similarity index 83%
rename from src/settings/modules/GmmxxSettings.h
rename to src/settings/modules/GmmxxEquationSolverSettings.h
index 7f5ad75a4..3fc1295a0 100644
--- a/src/settings/modules/GmmxxSettings.h
+++ b/src/settings/modules/GmmxxEquationSolverSettings.h
@@ -10,7 +10,7 @@ namespace storm {
/*!
* This class represents the settings for gmm++.
*/
- class GmmxxSettings : public ModuleSettings {
+ class GmmxxEquationSolverSettings : public ModuleSettings {
public:
// An enumeration of all available techniques for solving linear equations.
enum class LinearEquationTechnique { Bicgstab, Qmr, Gmres, Jacobi };
@@ -18,12 +18,15 @@ namespace storm {
// An enumeration of all available preconditioning techniques.
enum class PreconditioningTechnique { Ilu, Diagonal, Ildlt, None };
+ // An enumeration of all available convergence criteria.
+ enum class ConvergenceCriterion { Absolute, Relative };
+
/*!
* Creates a new set of gmm++ settings that is managed by the given manager.
*
* @param settingsManager The responsible manager.
*/
- GmmxxSettings(storm::settings::SettingsManager& settingsManager);
+ GmmxxEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
/*!
* Retrieves the technique that is to be used for solving systems of linear equations.
@@ -61,18 +64,11 @@ namespace storm {
double getPrecision() const;
/*!
- * Retrieves whether the absolute error is used for detecting convergence.
- *
- * @return True iff the absolute error is used convergence detection.
- */
- bool useAbsoluteConvergenceCriterion() const;
-
- /*!
- * Retrieves whether the relative error is used for detecting convergence.
+ * Retrieves the selected convergence criterion.
*
- * @return True iff the relative error is used convergence detection.
+ * @return The selected convergence criterion.
*/
- bool useRelativeConvergenceCriterion() const;
+ ConvergenceCriterion getConvergenceCriterion() const;
private:
// Define the string names of the options as constants.
diff --git a/src/settings/modules/GurobiSettings.cpp b/src/settings/modules/GurobiSettings.cpp
index ac9122dd2..a9713b31e 100644
--- a/src/settings/modules/GurobiSettings.cpp
+++ b/src/settings/modules/GurobiSettings.cpp
@@ -6,15 +6,22 @@ namespace storm {
namespace settings {
namespace modules {
+ const std::string GurobiSettings::moduleName = "gurobi";
+ const std::string GurobiSettings::integerToleranceOption = "inttol";
+ const std::string GurobiSettings::threadsOption = "threads";
+ const std::string GurobiSettings::outputOption = "output";
+
GurobiSettings::GurobiSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
- settingsManager.addOption(storm::settings::OptionBuilder("GurobiLpSolver", "glpkinttol", "", "Sets glpk's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
-
+ // First, we need to create all options of this module.
+ std::vector<std::shared_ptr<Option>> options;
+ options.push_back(storm::settings::OptionBuilder(moduleName, threadsOption, true, "The number of threads that may be used by Gurobi.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of threads.").setDefaultValueUnsignedInteger(1).build()).build());
- settingsManager.addOption(storm::settings::OptionBuilder("GurobiLpSolver", "gurobithreads", "", "The number of threads that may be used by Gurobi.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of threads.").setDefaultValueUnsignedInteger(1).build()).build());
+ options.push_back(storm::settings::OptionBuilder(moduleName, outputOption, true, "If set, the Gurobi output will be printed to the command line.").build());
- settingsManager.addOption(storm::settings::OptionBuilder("GurobiLpSolver", "gurobioutput", "", "If set, the Gurobi output will be printed to the command line.").build());
+ options.push_back(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets Gurobi's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
- settingsManager.addOption(storm::settings::OptionBuilder("GurobiLpSolver", "gurobiinttol", "", "Sets Gurobi's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+ // Finally, register all options that we just created.
+ settingsManager.registerModule(moduleName, options);
}
} // namespace modules
diff --git a/src/settings/modules/GurobiSettings.h b/src/settings/modules/GurobiSettings.h
index 652033af1..763490ae9 100644
--- a/src/settings/modules/GurobiSettings.h
+++ b/src/settings/modules/GurobiSettings.h
@@ -12,7 +12,40 @@ namespace storm {
*/
class GurobiSettings : public ModuleSettings {
public:
+ /*!
+ * Creates a new set of Gurobi settings that is managed by the given manager.
+ *
+ * @param settingsManager The responsible manager.
+ */
GurobiSettings(storm::settings::SettingsManager& settingsManager);
+
+ /*!
+ * Retrieves the integer tolerance to be used.
+ *
+ * @return The integer tolerance to be used.
+ */
+ double getIntegerTolerance() const;
+
+ /*!
+ * Retrieves the maximal number of threads Gurobi is allowed to use.
+ *
+ * @return The maximally allowed number of threads.
+ */
+ uint_fast64_t getNumberOfThreads() const;
+
+ /*!
+ * Retrieves whether the output option was set.
+ *
+ * @return True iff the output option was set.
+ */
+ bool isOutputSet() const;
+
+ private:
+ // Define the string names of the options as constants.
+ static const std::string moduleName;
+ static const std::string integerToleranceOption;
+ static const std::string threadsOption;
+ static const std::string outputOption;
};
} // namespace modules
diff --git a/src/settings/modules/ModuleSettings.cpp b/src/settings/modules/ModuleSettings.cpp
index 0e32abb4a..239bd822e 100644
--- a/src/settings/modules/ModuleSettings.cpp
+++ b/src/settings/modules/ModuleSettings.cpp
@@ -16,6 +16,14 @@ namespace storm {
return this->settingsManager;
}
+ void ModuleSettings::set(std::string const& name) const {
+ return this->getOption(longName).setHasOptionBeenSet();
+ }
+
+ void ModuleSettings::unset(std::string const& longName) const {
+ return this->getOption(longName).setHasOptionBeenSet(false);
+ }
+
} // namespace modules
} // namespace settings
} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/ModuleSettings.h b/src/settings/modules/ModuleSettings.h
index e96d22e76..6f3e70ad2 100644
--- a/src/settings/modules/ModuleSettings.h
+++ b/src/settings/modules/ModuleSettings.h
@@ -2,6 +2,10 @@
#define STORM_SETTINGS_MODULES_MODULESETTINGS_H_
#include <string>
+#include <unordered_map>
+
+#include "src/settings/Option.h"
+#include "src/settings/SettingMemento.h"
namespace storm {
namespace settings {
@@ -29,6 +33,17 @@ namespace storm {
*/
virtual bool check() const;
+ /*!
+ * Sets the option with the given name to the required status. This requires the option to take no
+ * arguments. As a result, a pointer to an object is returned such that when the object is destroyed
+ * (i.e. the smart pointer goes out of scope), the option is reset to its original status.
+ *
+ * @param name The name of the option to (unset).
+ * @param requiredStatus The status that is to be set for the option.
+ * @return A pointer to an object that resets the change upon destruction.
+ */
+ std::unique_ptr<storm::settings::SettingMemento> overrideOption(std::string const& name, bool requiredStatus);
+
protected:
/*!
* Retrieves the manager responsible for the settings.
@@ -37,14 +52,52 @@ namespace storm {
*/
storm::settings::SettingsManager const& getSettingsManager() const;
+ /*!
+ * Adds the option with the given long name to the list of options of this module.
+ *
+ * @param longName The long name of the option.
+ * @param option The actual option associated with the given name.
+ */
+ void addOption(std::string const& longName, std::shared_ptr<Option> const& option);
+
+ /*!
+ * Retrieves the option with the given long name. If no such option exists, an exception is thrown.
+ *
+ * @param longName The long name of the option to retrieve.
+ * @return The option associated with the given option name.
+ */
+ Option& getOption(std::string const& longName);
+
/*!
* Retrieves whether the option with the given name was set.
+ *
+ * @param The name of the option.
+ * @return True iff the option was set.
*/
bool isSet(std::string const& optionName) const;
+ /*!
+ * Sets the option with the specified name. This requires the option to not have any arguments. This
+ * should be used with care and is primarily meant to be used by the SettingMemento.
+ *
+ * @param name The name of the option to set.
+ */
+ void set(std::string const& name) const;
+
+ /*!
+ * Unsets the option with the specified name. This requires the option to not have any arguments. This
+ * should be used with care and is primarily meant to be used by the SettingMemento.
+ *
+ * @param name The name of the option to unset.
+ */
+ void unset(std::string const& longName) const;
+
private:
// The settings manager responsible for the settings.
storm::settings::SettingsManager const& settingsManager;
+
+ // A mapping of option names of the module to the actual options.
+ std::unordered_map<std::string, std::shared_ptr<Option>> options;
};
} // namespace modules
diff --git a/src/settings/modules/NativeEquationSolverSettings.cpp b/src/settings/modules/NativeEquationSolverSettings.cpp
index 7fa803e27..191df9371 100644
--- a/src/settings/modules/NativeEquationSolverSettings.cpp
+++ b/src/settings/modules/NativeEquationSolverSettings.cpp
@@ -6,24 +6,27 @@ namespace storm {
namespace settings {
namespace modules {
+ const std::string NativeEquationSolverSettings::moduleName = "native";
+ const std::string NativeEquationSolverSettings::techniqueOptionName = "tech";
+ const std::string NativeEquationSolverSettings::maximalIterationsOptionName = "maxiter";
+ const std::string NativeEquationSolverSettings::maximalIterationsOptionShortName = "i";
+ const std::string NativeEquationSolverSettings::precisionOptionName = "precision";
+ const std::string NativeEquationSolverSettings::absoluteOptionName = "absolute";
+
NativeEquationSolverSettings::NativeEquationSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
- // Offer all available methods as a command line option.
- std::vector<std::string> methods;
- methods.clear();
- methods.push_back("jacobi");
- settingsManager.addOption(storm::settings::OptionBuilder("NativeLinearEquationSolver", "nativelin", "", "The method to be used for solving linear equation systems with the native engine. Available are: jacobi.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("jacobi").build()).build());
-
- settingsManager.addOption(storm::settings::OptionBuilder("NativeLinearEquationSolver", "maxiter", "i", "The maximal number of iterations to perform before iterative solving is aborted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(10000).build()).build());
-
- settingsManager.addOption(storm::settings::OptionBuilder("NativeLinearEquationSolver", "precision", "", "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());
+ // First, we need to create all options of this module.
+ std::vector<std::shared_ptr<Option>> options;
+ std::vector<std::string> methods = { "jacobi" };
+ options.push_back(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the native engine. Available are: { jacobi }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("jacobi").build()).build());
- settingsManager.addOption(storm::settings::OptionBuilder("NativeLinearEquationSolver", "absolute", "", "Whether the relative or the absolute error is considered for deciding convergence.").build());
+ options.push_back(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, true, "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(10000).build()).build());
- settingsManager.addOption(storm::settings::OptionBuilder("NativeNondeterminsticLinearEquationSolver", "maxiter", "i", "The maximal number of iterations to perform before iterative solving is aborted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(10000).build()).build());
+ options.push_back(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "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());
- settingsManager.addOption(storm::settings::OptionBuilder("NativeNondeterminsticLinearEquationSolver", "precision", "", "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());
+ options.push_back(storm::settings::OptionBuilder(moduleName, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
- settingsManager.addOption(storm::settings::OptionBuilder("NativeNondeterminsticLinearEquationSolver", "absolute", "", "Whether the relative or the absolute error is considered for deciding convergence.").build());
+ // Finally, register all options that we just created.
+ settingsManager.registerModule(moduleName, options);
}
} // namespace modules
diff --git a/src/settings/modules/NativeEquationSolverSettings.h b/src/settings/modules/NativeEquationSolverSettings.h
index 15b4e2d79..da3d06fa4 100644
--- a/src/settings/modules/NativeEquationSolverSettings.h
+++ b/src/settings/modules/NativeEquationSolverSettings.h
@@ -12,7 +12,50 @@ namespace storm {
*/
class NativeEquationSolverSettings : public ModuleSettings {
public:
+ // An enumeration of all available techniques for solving linear equations.
+ enum class LinearEquationTechnique { Jacobi };
+
+ // An enumeration of all available convergence criteria.
+ enum class ConvergenceCriterion { Absolute, Relative };
+
NativeEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
+
+ /*!
+ * Retrieves the technique that is to be used for solving systems of linear equations.
+ *
+ * @return The technique to use.
+ */
+ LinearEquationTechnique getLinearEquationSystemTechnique() 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 the precision that is used for detecting convergence.
+ *
+ * @return The precision to use for detecting convergence.
+ */
+ double getPrecision() const;
+
+ /*!
+ * Retrieves the selected convergence criterion.
+ *
+ * @return The selected convergence criterion.
+ */
+ ConvergenceCriterion getConvergenceCriterion() const;
+
+ private:
+ // Define the string names of the options as constants.
+ static const std::string moduleName;
+ 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