diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index 7befe5ee8..6fbb8cb00 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/src/adapters/ExplicitModelAdapter.h
@@ -312,7 +312,7 @@ namespace storm {
}
// Check that the resulting distribution is in fact a distribution.
- LOG_THROW(std::abs(1 - probabilitySum) < storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble(), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "'.");
+ LOG_THROW(std::abs(1 - probabilitySum) < storm::settings::generalSettings().getPrecision(), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "'.");
}
}
@@ -418,7 +418,7 @@ namespace storm {
}
// Check that the resulting distribution is in fact a distribution.
- if (std::abs(1 - probabilitySum) > storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) {
+ if (std::abs(1 - probabilitySum) > storm::settings::generalSettings().getPrecision()) {
LOG4CPLUS_ERROR(logger, "Sum of update probabilities do not some to one for some command.");
throw storm::exceptions::WrongFormatException() << "Sum of update probabilities do not some to one for some command.";
}
@@ -502,7 +502,7 @@ namespace storm {
// If the current state does not have a single choice, we equip it with a self-loop if that was
// requested and issue an error otherwise.
if (totalNumberOfChoices == 0) {
- if (storm::settings::SettingsManager::getInstance()->isSet("fixDeadlocks")) {
+ if (storm::settings::generalSettings().isFixDeadlocksSet()) {
// Insert empty choice labeling for added self-loop transitions.
choiceLabels.push_back(boost::container::flat_set<uint_fast64_t>());
transitionMatrixBuilder.addNextValue(currentRow, currentState, storm::utility::constantOne<ValueType>());
diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h
index 5f999b06e..04face217 100644
--- a/src/counterexamples/MILPMinimalLabelSetGenerator.h
+++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h
@@ -1025,7 +1025,7 @@ namespace storm {
// Delegate the actual computation work to the function of equal name.
auto startTime = std::chrono::high_resolution_clock::now();
- boost::container::flat_set<uint_fast64_t> usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::SettingsManager::getInstance()->isSet("schedcuts"));
+ boost::container::flat_set<uint_fast64_t> usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().useSchedulerCuts());
auto endTime = std::chrono::high_resolution_clock::now();
std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;
diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
index 345d9d721..b927b6203 100644
--- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
+++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
@@ -235,7 +235,7 @@ namespace storm {
// (1) Compute the accuracy we need to achieve the required error bound.
ValueType maxExitRate = this->getModel().getMaximalExitRate();
- ValueType delta = (2 * storm::settings::SettingsManager::getInstance()->getOptionByLongName("digiprecision").getArgument(0).getValueAsDouble()) / (upperBound * maxExitRate * maxExitRate);
+ ValueType delta = (2 * storm::settings::generalSettings().getPrecision()) / (upperBound * maxExitRate * maxExitRate);
// (2) Compute the number of steps we need to make for the interval.
uint_fast64_t numberOfSteps = static_cast<uint_fast64_t>(std::ceil((upperBound - lowerBound) / delta));
diff --git a/src/modelchecker/prctl/CreatePrctlModelChecker.h b/src/modelchecker/prctl/CreatePrctlModelChecker.h
index d07261ebc..f31fb246a 100644
--- a/src/modelchecker/prctl/CreatePrctlModelChecker.h
+++ b/src/modelchecker/prctl/CreatePrctlModelChecker.h
@@ -13,20 +13,8 @@
* @param dtmc A reference to the DTMC for which the model checker is to be created.
* @return A pointer to the resulting model checker.
*/
-storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Dtmc<double> const & dtmc) {
- // Create the appropriate model checker.
- storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
- std::string const& linsolver = s->getOptionByLongName("linsolver").getArgument(0).getValueAsString();
- if (linsolver == "gmm++") {
- return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double>(dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
- } else if (linsolver == "native") {
- return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double>(dtmc, new storm::solver::NativeLinearEquationSolver<double>());
- }
-
- // The control flow should never reach this point, as there is a default setting for matrixlib.
- std::string message = "No matrix library suitable for DTMC model checking has been set.";
- throw storm::exceptions::InvalidSettingsException() << message;
- return nullptr;
+storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Dtmc<double> const& dtmc) {
+ return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double>(dtmc);
}
/*!
diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
index 40cec5558..a6fb9dd39 100644
--- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
@@ -11,6 +11,7 @@
#include "src/modelchecker/prctl/AbstractModelChecker.h"
#include "src/models/Dtmc.h"
#include "src/solver/LinearEquationSolver.h"
+#include "src/utility/solver.h"
#include "src/utility/vector.h"
#include "src/utility/graph.h"
@@ -33,10 +34,14 @@ public:
*
* @param model The DTMC to be checked.
*/
- explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc<Type> const& model, storm::solver::LinearEquationSolver<Type>* linearEquationSolver) : AbstractModelChecker<Type>(model), linearEquationSolver(linearEquationSolver) {
+ explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc<Type> const& model, std::unique_ptr<storm::solver::LinearEquationSolver<Type>>&& linearEquationSolver) : AbstractModelChecker<Type>(model), linearEquationSolver(std::move(linearEquationSolver)) {
// Intentionally left empty.
}
+ explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc<Type> const& model) : AbstractModelChecker<Type>(model), linearEquationSolver(storm::utility::solver::getLinearEquationSolver<Type>()) {
+ // Intentionally left empty.
+ }
+
/*!
* Copy constructs a SparseDtmcPrctlModelChecker from the given model checker. In particular, this means that the newly
* constructed model checker will have the model of the given model checker as its associated model.
diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h
index c29c16b8c..103e3d264 100644
--- a/src/models/Ctmdp.h
+++ b/src/models/Ctmdp.h
@@ -126,9 +126,7 @@ private:
* Checks probability matrix if all rows sum up to one.
*/
bool checkValidityOfProbabilityMatrix() {
- // Get the settings object to customize linear solving.
- storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
- double precision = s->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
+ double precision = storm::settings::generalSettings().getPrecision();
for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); row++) {
T sum = this->getTransitionMatrix().getRowSum(row);
if (sum == 0) continue;
diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h
index ec625b6d8..0252b7533 100644
--- a/src/models/Dtmc.h
+++ b/src/models/Dtmc.h
@@ -297,9 +297,7 @@ private:
* Checks probability matrix if all rows sum up to one.
*/
bool checkValidityOfProbabilityMatrix() {
- // Get the settings object to customize linear solving.
- storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
- double precision = s->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
+ double precision = storm::settings::generalSettings().getPrecision();
if (this->getTransitionMatrix().getRowCount() != this->getTransitionMatrix().getColumnCount()) {
// not square
diff --git a/src/models/Mdp.h b/src/models/Mdp.h
index b647f6813..53d7cc192 100644
--- a/src/models/Mdp.h
+++ b/src/models/Mdp.h
@@ -197,9 +197,7 @@ private:
* Checks probability matrix if all rows sum up to one.
*/
bool checkValidityOfProbabilityMatrix() {
- // Get the settings object to customize linear solving.
- storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
- double precision = s->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
+ double precision = storm::settings::generalSettings().getPrecision();
for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); row++) {
T sum = this->getTransitionMatrix().getRowSum(row);
diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp
index 165f8d8f2..43c26f8fb 100644
--- a/src/parser/DeterministicSparseTransitionParser.cpp
+++ b/src/parser/DeterministicSparseTransitionParser.cpp
@@ -93,7 +93,7 @@ namespace storm {
uint_fast64_t row, col, lastRow = 0;
double val;
- bool fixDeadlocks = storm::settings::SettingsManager::getInstance()->isSet("fixDeadlocks");
+ bool fixDeadlocks = storm::settings::generalSettings().isFixDeadlocksSet();
bool hadDeadlocks = false;
bool rowHadDiagonalEntry = false;
diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp
index 7e235827c..e001d2b1d 100644
--- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp
+++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp
@@ -15,7 +15,7 @@ namespace storm {
MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char const* buf) {
MarkovAutomatonSparseTransitionParser::FirstPassResult result;
- bool fixDeadlocks = storm::settings::SettingsManager::getInstance()->isSet("fixDeadlocks");
+ bool fixDeadlocks = storm::settings::generalSettings().isFixDeadlocksSet();
// Skip the format hint if it is there.
buf = trimWhitespaces(buf);
@@ -157,7 +157,7 @@ namespace storm {
MarkovAutomatonSparseTransitionParser::Result MarkovAutomatonSparseTransitionParser::secondPass(char const* buf, FirstPassResult const& firstPassResult) {
Result result(firstPassResult);
- bool fixDeadlocks = storm::settings::SettingsManager::getInstance()->isSet("fixDeadlocks");
+ bool fixDeadlocks = storm::settings::generalSettings().isFixDeadlocksSet();
// Skip the format hint if it is there.
buf = trimWhitespaces(buf);
diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp
index 01f3281cd..971f7cdfe 100644
--- a/src/parser/NondeterministicSparseTransitionParser.cpp
+++ b/src/parser/NondeterministicSparseTransitionParser.cpp
@@ -100,7 +100,7 @@ namespace storm {
// Initialize variables for the parsing run.
uint_fast64_t source = 0, target = 0, lastSource = 0, choice = 0, lastChoice = 0, curRow = 0;
double val = 0.0;
- bool fixDeadlocks = storm::settings::SettingsManager::getInstance()->isSet("fixDeadlocks");
+ bool fixDeadlocks = storm::settings::generalSettings().isFixDeadlocksSet();
bool hadDeadlocks = false;
// The first state already starts a new row group of the matrix.
diff --git a/src/settings/Argument.cpp b/src/settings/Argument.cpp
deleted file mode 100644
index 047dc13e9..000000000
--- a/src/settings/Argument.cpp
+++ /dev/null
@@ -1,8 +0,0 @@
-#include "src/settings/Argument.h"
-
-namespace storm {
- namespace settings {
- const std::string Argument::trueString = "true";
- const std::string Argument::falseString = "false";
- }
-}
\ No newline at end of file
diff --git a/src/settings/Argument.h b/src/settings/Argument.h
index c756ff5d8..e93ce0c84 100644
--- a/src/settings/Argument.h
+++ b/src/settings/Argument.h
@@ -127,9 +127,9 @@ namespace storm {
case ArgumentType::Boolean: {
bool iValue = ArgumentTypeInferation::inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
if (iValue) {
- return trueString;
+ return "true";
} else {
- return falseString;
+ return "false";
}
}
default: return ArgumentBase::convertToString(this->argumentValue);
@@ -190,10 +190,6 @@ namespace storm {
// A flag indicating whether a default value has been provided.
bool hasDefaultValue;
- // Static constants for the string representations of true and false.
- static const std::string trueString;
- static const std::string falseString;
-
void setDefaultValue(T const& newDefault) {
LOG_THROW(this->validate(newDefault), storm::exceptions::IllegalArgumentValueException, "The default value for the argument did not pass all validation functions.");
this->defaultValue = newDefault;
diff --git a/src/settings/Option.h b/src/settings/Option.h
index 689c11191..0876b8741 100644
--- a/src/settings/Option.h
+++ b/src/settings/Option.h
@@ -21,16 +21,20 @@
namespace storm {
namespace settings {
- // Forward-declare settings manager class.
+ // Forward-declare settings manager and module settings classes.
class SettingsManager;
+ namespace modules {
+ class ModuleSettings;
+ }
/*!
* This class represents one command-line option.
*/
class Option {
public:
- // Declare settings manager class as friend.
+ // Declare settings manager and module settings classes as friends.
friend class SettingsManager;
+ friend class modules::ModuleSettings;
/*!
* Creates an option with the given parameters.
diff --git a/src/settings/SettingMemento.cpp b/src/settings/SettingMemento.cpp
index 5a1a55390..3f031b34a 100644
--- a/src/settings/SettingMemento.cpp
+++ b/src/settings/SettingMemento.cpp
@@ -1,17 +1,17 @@
-#include "src/settings/SettingsMemento.h"
+#include "src/settings/SettingMemento.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) {
+ SettingMemento::SettingMemento(modules::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() {
+ SettingMemento::~SettingMemento() {
if (resetToState) {
settings.set(optionName);
} else {
diff --git a/src/settings/SettingMemento.h b/src/settings/SettingMemento.h
index 342cdd666..551142fd2 100644
--- a/src/settings/SettingMemento.h
+++ b/src/settings/SettingMemento.h
@@ -6,7 +6,10 @@
namespace storm {
namespace settings {
- class ModuleSettings;
+ // Forward-declare the module settings.
+ namespace modules {
+ class ModuleSettings;
+ }
/*!
* This class is used to reset the state of an option that was temporarily set to a different status.
@@ -21,7 +24,7 @@ namespace storm {
* @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);
+ SettingMemento(modules::ModuleSettings& settings, std::string const& longOptionName, bool resetToState);
/*!
* Destructs the memento object and resets the value of the option to its original state.
@@ -30,7 +33,7 @@ namespace storm {
private:
// The settings object in which the setting is to be restored.
- ModuleSettings& settings;
+ modules::ModuleSettings& settings;
// The long name of the option that was temporarily set.
std::string const optionName;
diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index 2581edd52..d9a109835 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -3,14 +3,23 @@
#include <cstring>
#include <cctype>
#include <mutex>
+#include <boost/algorithm/string.hpp>
#include "src/exceptions/OptionParserException.h"
namespace storm {
namespace settings {
- SettingsManager::SettingsManager() : generalSettings(*this), debugSettings(*this), counterexampleGeneratorSettings(*this), cuddSettings(*this), gmmxxSettings(*this), nativeEquationSolverSettings(*this), glpkSettings(*this), gurobiSettings(*this) {
- // Intentionally left empty.
+ SettingsManager::SettingsManager() {
+ // Register all known settings modules.
+ this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GeneralSettings(*this)));
+ this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::DebugSettings(*this)));
+ this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::CounterexampleGeneratorSettings(*this)));
+ this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::CuddSettings(*this)));
+ this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GmmxxEquationSolverSettings(*this)));
+ this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::NativeEquationSolverSettings(*this)));
+ this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GlpkSettings(*this)));
+ this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GurobiSettings(*this)));
}
SettingsManager::~SettingsManager() {
@@ -18,283 +27,42 @@ namespace storm {
}
SettingsManager& SettingsManager::manager() {
+ static SettingsManager settingsManager;
return settingsManager;
}
+ void SettingsManager::setFromCommandLine(int const argc, char const * const argv[]) {
+ // We convert the arguments to a vector of strings and strip off the first element since it refers to the
+ // name of the program.
+ std::vector<std::string> argumentVector(argc - 1);
+ for (uint_fast64_t i = 1; i < argc; ++i) {
+ argumentVector[i - 1] = std::string(argv[i]);
+ }
+
+ this->setFromExplodedString(argumentVector);
+ }
- }
-}
-
-
-/*!
- * @brief Create new instance.
- *
- * Creates a new Settings instance and passes the arguments to the constructor of Settings.
- *
- * @param argc should be argc passed to main function
- * @param argv should be argv passed to main function
- * @param filename either NULL or name of config file
- * @return The new instance of Settings.
- */
-void storm::settings::SettingsManager::parse(int const argc, char const * const argv[]) {
- storm::settings::SettingsManager* myInstance = storm::settings::SettingsManager::getInstance();
- myInstance->parseCommandLine(argc, argv);
-}
-
-bool storm::settings::SettingsManager::hasAssignment(std::string const& option) {
- return (option.find_first_of('=', 0) != std::string::npos);
-}
-
-storm::settings::stringPair_t storm::settings::SettingsManager::splitOptionString(std::string const& option) {
- size_t splitLocation = option.find_first_of('=', 0);
- if (splitLocation == std::string::npos) {
- // Second half is empty
- return std::make_pair(option, "");
- } else if (splitLocation + 1 >= option.length()) {
- // Remove the = character
- return std::make_pair(option.substr(0, option.size() - 1), "");
- }
- return std::make_pair(option.substr(0, splitLocation), option.substr(splitLocation + 1, std::string::npos));
-}
-
-void storm::settings::SettingsManager::handleAssignment(std::string const& longOptionName, std::vector<std::string> arguments) {
- std::string optionName = storm::utility::StringHelper::stringToLower(longOptionName);
-
- Option* option = this->getPtrByLongName(optionName);
-
- // Mark as Set
- option->setHasOptionBeenSet();
-
- uint_fast64_t givenArgsCount = arguments.size();
-
- if (givenArgsCount > option->getArgumentCount()) {
- LOG4CPLUS_ERROR(logger, "SettingsManager::handleAssignment: Unable to parse arguments for option \"" << longOptionName << "\": " << arguments.size() << " arguments given, but expected no more than " << option->getArgumentCount() << ".");
- throw storm::exceptions::OptionParserException() << "Unable to parse arguments for option \"" << longOptionName << "\": " << arguments.size() << " arguments given, but expected no more than " << option->getArgumentCount() << ".";
- }
-
- for (uint_fast64_t i = 0; i < option->getArgumentCount(); ++i) {
- if (i < givenArgsCount) {
- storm::settings::fromStringAssignmentResult_t assignmentResult = option->getArgument(i).fromStringValue(arguments.at(i));
- if (!assignmentResult.first) {
- LOG4CPLUS_ERROR(logger, "SettingsManager::handleAssignment: Unable to parse arguments for option \"" << longOptionName << "\": argument " << option->getArgument(i).getArgumentName() << " rejected the given value \"" << arguments.at(i) << "\" with message:\r\n" << assignmentResult.second << ".");
- throw storm::exceptions::OptionParserException() << "Unable to parse arguments for option \"" << longOptionName << "\": argument " << option->getArgument(i).getArgumentName() << " rejected the given value \"" << arguments.at(i) << "\" with message:\r\n" << assignmentResult.second << ".";
- }
- } else {
- // There is no given value for this argument, only optional
- if (!option->getArgument(i).getIsOptional()) {
- LOG4CPLUS_ERROR(logger, "Settings::handleAssignment: Unable to parse arguments for option \"" << longOptionName << "\": " << arguments.size() << " arguments given, but more arguments were expected.");
- throw storm::exceptions::OptionParserException() << "Unable to parse arguments for option \"" << longOptionName << "\": " << arguments.size() << " arguments given, but more arguments were expected.";
- } else {
- option->getArgument(i).setFromDefaultValue();
- }
- }
- }
-}
-
-std::vector<std::string> storm::settings::SettingsManager::argvToStringArray(int const argc, char const * const argv[]) {
- // Ignore argv[0], it contains the program path and name
- std::vector<std::string> result;
- for (int i = 1; i < argc; ++i) {
- result.push_back(std::string(argv[i]));
- }
- return result;
-}
-
-bool storm::settings::SettingsManager::checkArgumentSyntaxForOption(std::string const& argvString) {
- if (argvString.size() < 2) {
- return false;
- }
-
- if ((argvString.at(0) != '-') || ((argvString.at(1) != '-') && !isalpha(argvString.at(1)))) {
- return false;
- }
-
- for (size_t i = 2; i < argvString.size(); ++i) {
- if (!isalpha(argvString.at(i))) {
- return false;
- }
- }
- return true;
-}
-
-std::vector<bool> storm::settings::SettingsManager::scanForOptions(std::vector<std::string> const& arguments) {
- std::vector<bool> result;
- result.reserve(arguments.size());
- for (auto it = arguments.cbegin(); it != arguments.cend(); ++it) {
- result.push_back(checkArgumentSyntaxForOption(*it));
- }
- return result;
-}
-
-void storm::settings::SettingsManager::parseCommandLine(int const argc, char const * const argv[]) {
- LOG4CPLUS_DEBUG(logger, "Settings::parseCommandLine: Parsing " << argc << " arguments.");
-
- std::vector<std::string> stringArgv = argvToStringArray(argc, argv);
- std::vector<bool> optionPositions = scanForOptions(stringArgv);
-
- bool optionActive = false;
- std::string longOptionName;
- std::vector<std::string> argCache;
- for (size_t i = 0; i <= stringArgv.size(); ++i) {
- if (i == stringArgv.size()) {
- if (optionActive) {
- this->handleAssignment(longOptionName, argCache);
- argCache.clear();
- }
- break;
- } else if (optionPositions.at(i)) {
- if (optionActive) {
- this->handleAssignment(longOptionName, argCache);
- argCache.clear();
- }
-
- std::string const& nextOption = stringArgv.at(i);
- if (nextOption.at(0) == '-' && nextOption.at(1) != '-') {
- // Short Option
- std::string nextShortOptionName = storm::utility::StringHelper::stringToLower(nextOption.substr(1, nextOption.size() - 1));
- if (!this->containsShortName(nextShortOptionName)) {
- LOG4CPLUS_ERROR(logger, "Settings::parseCommandLine: Unknown option name \"" << nextShortOptionName << "\".");
- throw storm::exceptions::OptionParserException() << "Unknown option name \"" << nextShortOptionName << "\".";
- } else {
- longOptionName = this->getByShortName(nextShortOptionName).getLongName();
- optionActive = true;
- }
- } else {
- // Long Option
- std::string nextLongOptionName = storm::utility::StringHelper::stringToLower(nextOption.substr(2, nextOption.size() - 2));
- if (!this->containsLongName(nextLongOptionName)) {
- LOG4CPLUS_ERROR(logger, "Settings::parseCommandLine: Unknown option name \"" << nextLongOptionName << "\".");
- throw storm::exceptions::OptionParserException() << "Unknown option name \"" << nextLongOptionName << "\".";
- } else {
- longOptionName = this->getByLongName(nextLongOptionName).getLongName();
- optionActive = true;
- }
- }
- } else if (optionActive) {
- // Next argument for an Option found
- argCache.push_back(stringArgv.at(i));
- } else {
- // No Option active and this is no option.
- LOG4CPLUS_ERROR(logger, "Settings::parseCommandLine: Found stray argument while parsing a given configuration, \"" << stringArgv.at(i) << "\" is neither a known option nor preceeded by an option.");
- throw storm::exceptions::OptionParserException() << "Found stray argument while parsing a given configuration; \"" << stringArgv.at(i) << "\" is neither a known option nor preceeded by an option.";
- }
- }
-
- for (auto it = this->options.cbegin(); it != this->options.cend(); ++it) {
- if (!it->second.get()->getHasOptionBeenSet()) {
- if (it->second.get()->getIsRequired()) {
- LOG4CPLUS_ERROR(logger, "Settings::parseCommandLine: Missing required option \"" << it->second.get()->getLongName() << "\".");
- throw storm::exceptions::OptionParserException() << "Missing required option \"" << it->second.get()->getLongName() << "\".";
- } else {
- // Set defaults on optional values
- for (uint_fast64_t i = 0; i < it->second.get()->getArgumentCount(); ++i) {
- if (it->second.get()->getArgument(i).getHasDefaultValue()) {
- it->second.get()->getArgument(i).setFromDefaultValue();
- }
- }
- }
- }
- }
-}
-
-storm::settings::SettingsManager* storm::settings::SettingsManager::getInstance() {
- // Usually, this would require double-checked locking.
- // But since C++11, this is the way to go:
- static storm::settings::SettingsManager pInstance;
-
- return &pInstance;
-}
-
-storm::settings::SettingsManager& storm::settings::SettingsManager::addOption(Option* option) {
- // For automatic management of option's lifetime
- std::shared_ptr<Option> optionPtr(option);
-
- std::string lowerLongName = storm::utility::StringHelper::stringToLower(option->getLongName());
- std::string lowerShortName = storm::utility::StringHelper::stringToLower(option->getShortName());
-
- auto longNameIterator = this->options.find(lowerLongName);
- auto shortNameIterator = this->shortNames.find(lowerShortName);
-
- if (longNameIterator == this->options.end()) {
- // Not found
- if (!(shortNameIterator == this->shortNames.end())) {
- // There exists an option which uses the same shortname
- //LOG4CPLUS_ERROR(logger, "Settings::addOption: Error: The Option \"" << shortNameIterator->second << "\" from Module \"" << this->options.find(shortNameIterator->second)->second.get()->getModuleName() << "\" uses the same ShortName as the Option \"" << option->getLongName() << "\" from Module \"" << option->getModuleName() << "\"!");
- throw storm::exceptions::OptionUnificationException() << "Error: The option \"" << shortNameIterator->second << "\" of module \"" << this->options.find(shortNameIterator->second)->second.get()->getModuleName() << "\" uses the same name as option \"" << option->getLongName() << "\" of module \"" << option->getModuleName() << "\".";
- }
-
- // Copy Shared_ptr
- this->options.insert(std::make_pair(lowerLongName, std::shared_ptr<Option>(optionPtr)));
- this->optionPointers.push_back(std::shared_ptr<Option>(optionPtr));
- // Ignore Options with empty shortName
- if (!lowerShortName.empty()) {
- this->shortNames.insert(std::make_pair(lowerShortName, lowerLongName));
- }
- } else {
- // This will fail if the shortNames are not identical, so no additional checks here.
- longNameIterator->second.get()->unify(*option);
- }
-
- return *this;
-}
-
-std::string storm::settings::SettingsManager::getHelpText() const {
-
- // Copy all option names into a vector and sort it
- std::vector<std::string> optionNames;
- optionNames.reserve(this->options.size());
-
- size_t longNameMaxSize = 0;
- size_t shortNameMaxSize = 0;
- size_t argumentNameMaxSize = 0;
- // Get the maximum size of the long and short Names and copy the long names for sorting
- std::for_each(this->options.cbegin(), this->options.cend(), [&] (std::pair<std::string, std::shared_ptr<storm::settings::Option>> const& it) -> void {
- longNameMaxSize = std::max(longNameMaxSize, it.first.size());
- shortNameMaxSize = std::max(shortNameMaxSize, it.second.get()->getShortName().size());
- optionNames.push_back(it.first);
- std::for_each(it.second.get()->arguments.cbegin(), it.second.get()->arguments.cend(), [&] (std::shared_ptr<ArgumentBase> const& arg) -> void {
- argumentNameMaxSize = std::max(argumentNameMaxSize, arg.get()->getArgumentName().size());
- });
- });
- // Sort the long names
- std::sort(optionNames.begin(), optionNames.end(), [] (std::string const& a, std::string const& b) -> bool { return a.compare(b) < 0; });
-
- std::stringstream ss;
-
- /*
- Layout:
- --longName -shortName Description
- ArgumentName (ArgumentType) ArgumentDescription
- */
- const std::string delimiter = " ";
-
- for (auto it = optionNames.cbegin(); it != optionNames.cend(); ++it) {
- Option const& o = this->getByLongName(*it);
- std::string const& longName = o.getLongName();
- ss << delimiter << "--" << longName;
- // Fill up the remaining space after the long Name
- for (uint_fast64_t i = longName.size(); i < longNameMaxSize; ++i) {
- ss << " ";
- }
- std::string const& shortName = o.getShortName();
- ss << delimiter << "-" << shortName;
- // Fill up the remaining space after the short Name
- for (uint_fast64_t i = shortName.size(); i < shortNameMaxSize; ++i) {
- ss << " ";
- }
- ss << delimiter << o.getDescription() << std::endl;
-
- for (auto i = 0; i < o.getArgumentCount(); ++i) {
- ArgumentBase const& a = o.getArgument(i);
- std::string const& argumentName = a.getArgumentName();
- ss << delimiter << delimiter << delimiter << delimiter << "argument <" << (i+1) << "> - " << argumentName;
- // Fill up the remaining space after the argument Name
- for (uint_fast64_t i = argumentName.size(); i < argumentNameMaxSize; ++i) {
- ss << " ";
- }
- ss << "(" << ArgumentTypeHelper::toString(a.getArgumentType()) << ")" << delimiter << a.getArgumentDescription() << std::endl;
- }
- }
+ void SettingsManager::setFromString(std::string const& commandLineString) {
+ std::vector<std::string> argumentVector;
+ boost::split(argumentVector, commandLineString, boost::is_any_of("\t "));
+ this->setFromExplodedString(argumentVector);
+ }
+
+ void SettingsManager::setFromExplodedString(std::vector<std::string> const& commandLineArguments) {
+ LOG_ASSERT(false, "Not yet implemented");
+ }
+
+ void SettingsManager::setFromConfigurationFile(std::string const& configFilename) {
+ LOG_ASSERT(false, "Not yet implemented");
+ }
+
+ void SettingsManager::printHelp(std::string const& moduleName) const {
+ LOG_ASSERT(false, "Not yet implemented");
+ }
+
+ void SettingsManager::addModule(std::unique_ptr<modules::ModuleSettings>&& moduleSettings) {
+ LOG_ASSERT(false, "Not yet implemented");
+ }
- return ss.str();
+ }
}
\ No newline at end of file
diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h
index 2f719b6f2..89913bf7a 100644
--- a/src/settings/SettingsManager.h
+++ b/src/settings/SettingsManager.h
@@ -34,8 +34,6 @@
namespace storm {
namespace settings {
- class InternalOptionMemento;
-
/*!
* 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()
@@ -43,9 +41,6 @@ namespace storm {
*/
class SettingsManager {
public:
- // Declare the memento class as a friend so it can manipulate the internal state.
- friend class InternalOptionMemento;
-
/*!
* 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.
@@ -53,7 +48,7 @@ namespace storm {
* @param argc The number of command line arguments.
* @param argv The command line arguments.
*/
- static void setFromCommandLine(int const argc, char const * const argv[]);
+ void setFromCommandLine(int const argc, char const * const argv[]);
/*!
* This function parses the given command line arguments (represented by one big string) and sets all
@@ -62,7 +57,7 @@ namespace storm {
*
* @param commandLineString The command line arguments as one string.
*/
- static void setFromString(std::string const& commandLineString);
+ void setFromString(std::string const& commandLineString);
/*!
* This function parses the given command line arguments (represented by several strings) and sets all
@@ -71,69 +66,46 @@ namespace storm {
*
* @param commandLineArguments The command line arguments.
*/
- static void setFromExplodedString(std::vector<std::string> const& commandLineArguments);
+ void setFromExplodedString(std::vector<std::string> const& commandLineArguments);
/*!
* 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.
*/
- static void setFromConfigurationFile(std::string const& configFilename);
+ void setFromConfigurationFile(std::string const& configFilename);
/*!
- * Retrieves the general settings.
- *
- * @return An object that allows accessing the general settings.
- */
- storm::settings::modules::GeneralSettings const& getGeneralSettings() const;
-
- /*!
- * Retrieves the debug settings.
- *
- * @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.
+ * 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 An object that allows accessing the settings of the gmm++-based equation solver.
+ * @return moduleName The name of the module for which to show the help or "all" if the full help text is to
+ * be printed.
*/
- storm::settings::modules::GmmxxEquationSolverSettings const& getGmmxxEquationSolverSettings() const;
-
+ void printHelp(std::string const& moduleName = "all") const;
+
/*!
- * Retrieves the settings of the native equation solver.
+ * Retrieves the only existing instance of a settings manager.
*
- * @return An object that allows accessing the settings of the native equation solver.
+ * @return The only existing instance of a settings manager
*/
- storm::settings::modules::NativeEquationSolverSettings const& getNativeEquationSolverSettings() const;
-
+ static SettingsManager& manager();
+
/*!
- * Retrieves the settings of glpk.
+ * Adds a new module with the given name. If the module could not be successfully added, an exception is
+ * thrown.
*
- * @return An object that allows accessing the settings of glpk.
+ * @param moduleSettings The settings of the module to add.
*/
- storm::settings::modules::GlpkSettings const& getGlpkSettings() const;
-
+ void addModule(std::unique_ptr<modules::ModuleSettings>&& moduleSettings);
+
/*!
- * Retrieves the settings of Gurobi.
+ * Retrieves the settings of the module with the given name.
*
- * @return An object that allows accessing the settings of Gurobi.
+ * @param moduleName The name of the module for which to retrieve the settings.
+ * @return An object that provides access to the settings of the module.
*/
- storm::settings::modules::GurobiSettings const& getGurobiSettings() const;
+ modules::ModuleSettings const& getModule(std::string const& moduleName) const;
private:
/*!
@@ -146,33 +118,6 @@ namespace storm {
* This destructor is private, since we need to forbid explicit destruction of the manager.
*/
virtual ~SettingsManager();
-
- // An object that provides access to the general settings.
- storm::settings::modules::GeneralSettings generalSettings;
-
- // An object that provides access to the debug settings.
- storm::settings::modules::DebugSettings debugSettings;
-
- // An object that provides access to the counterexample generator settings.
- storm::settings::modules::CounterexampleGeneratorSettings counterexampleGeneratorSettings;
-
- // An object that provides access to the CUDD settings.
- storm::settings::modules::CuddSettings cuddSettings;
-
- // An object that provides access to the gmm++ settings.
- storm::settings::modules::GmmxxEquationSolverSettings gmmxxEquationSolverSettings;
-
- // An object that provides access to the native equation solver settings.
- storm::settings::modules::NativeEquationSolverSettings nativeEquationSolverSettings;
-
- // An object that provides access to the glpk settings.
- storm::settings::modules::GlpkSettings glpkSettings;
-
- // An object that provides access to the Gurobi settings.
- storm::settings::modules::GurobiSettings gurobiSettings;
-
- // 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;
@@ -181,41 +126,93 @@ namespace storm {
// 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;
- /*!
- * 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.
- */
- void printHelp(std::string const& moduleName = "all") const;
-
- /*!
- * 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.
- */
- void registerModule(std::string const& moduleName, std::vector<std::shared_ptr<Option>> const& options);
-
- /*!
- * Retrieves the only existing instance of a settings manager.
- *
- * @return The only existing instance of a settings manager
- */
- static SettingsManager& manager();
-
// Helper functions
- stringPair_t splitOptionString(std::string const& option);
- bool hasAssignment(std::string const& option);
void handleAssignment(std::string const& longOptionName, std::vector<std::string> arguments);
- 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);
};
+ /*!
+ * Retrieves the settings manager.
+ *
+ * @return The only settings manager.
+ */
+ SettingsManager& manager() {
+ return SettingsManager::manager();
+ }
+
+ /*!
+ * Retrieves the general settings.
+ *
+ * @return An object that allows accessing the general settings.
+ */
+ storm::settings::modules::GeneralSettings const& generalSettings() {
+ return dynamic_cast<storm::settings::modules::GeneralSettings const&>(manager().getModule(storm::settings::modules::GeneralSettings::moduleName));
+ }
+
+ /*!
+ * Retrieves the debug settings.
+ *
+ * @return An object that allows accessing the debug settings.
+ */
+ storm::settings::modules::DebugSettings const& debugSettings() {
+ return dynamic_cast<storm::settings::modules::DebugSettings const&>(manager().getModule(storm::settings::modules::DebugSettings::moduleName));
+ }
+
+ /*!
+ * Retrieves the counterexample generator settings.
+ *
+ * @return An object that allows accessing the counterexample generator settings.
+ */
+ storm::settings::modules::CounterexampleGeneratorSettings const& counterexampleGeneratorSettings() {
+ return dynamic_cast<storm::settings::modules::CounterexampleGeneratorSettings const&>(manager().getModule(storm::settings::modules::CounterexampleGeneratorSettings::moduleName));
+ }
+
+ /*!
+ * Retrieves the CUDD settings.
+ *
+ * @return An object that allows accessing the CUDD settings.
+ */
+ storm::settings::modules::CuddSettings const& cuddSettings() {
+ return dynamic_cast<storm::settings::modules::CuddSettings const&>(manager().getModule(storm::settings::modules::CuddSettings::moduleName));
+ }
+
+ /*!
+ * 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& gmmxxEquationSolverSettings() {
+ return dynamic_cast<storm::settings::modules::GmmxxEquationSolverSettings const&>(manager().getModule(storm::settings::modules::GmmxxEquationSolverSettings::moduleName));
+ }
+
+ /*!
+ * 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& nativeEquationSolverSettings() {
+ return dynamic_cast<storm::settings::modules::NativeEquationSolverSettings const&>(manager().getModule(storm::settings::modules::NativeEquationSolverSettings::moduleName));
+ }
+
+ /*!
+ * Retrieves the settings of glpk.
+ *
+ * @return An object that allows accessing the settings of glpk.
+ */
+ storm::settings::modules::GlpkSettings const& glpkSettings() {
+ return dynamic_cast<storm::settings::modules::GlpkSettings const&>(manager().getModule(storm::settings::modules::GlpkSettings::moduleName));
+ }
+
+ /*!
+ * Retrieves the settings of Gurobi.
+ *
+ * @return An object that allows accessing the settings of Gurobi.
+ */
+ storm::settings::modules::GurobiSettings const& gurobiSettings() {
+ return dynamic_cast<storm::settings::modules::GurobiSettings const&>(manager().getModule(storm::settings::modules::GurobiSettings::moduleName));
+ }
+
} // namespace settings
} // namespace storm
diff --git a/src/settings/modules/CounterexampleGeneratorSettings.cpp b/src/settings/modules/CounterexampleGeneratorSettings.cpp
index 0fad20609..f6ff3347c 100644
--- a/src/settings/modules/CounterexampleGeneratorSettings.cpp
+++ b/src/settings/modules/CounterexampleGeneratorSettings.cpp
@@ -12,19 +12,14 @@ namespace storm {
const std::string CounterexampleGeneratorSettings::schedulerCutsOptionName = "schedcuts";
const std::string CounterexampleGeneratorSettings::statisticsOptionName = "stats";
- CounterexampleGeneratorSettings::CounterexampleGeneratorSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
- // First, we need to create all options of this module.
- std::vector<std::shared_ptr<Option>> options;
+ CounterexampleGeneratorSettings::CounterexampleGeneratorSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
std::vector<std::string> techniques = {"sat", "milp"};
- options.push_back(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command set. Note that this requires the model to be given in a symbolic format.")
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command set. Note that this requires the model to be given in a symbolic format.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file containing the properties for which counterexamples are to be generated.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample. Available are {milp, maxsat}").setDefaultValueString("maxsat").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(techniques)).build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, statisticsOptionName, true, "Sets whether to display statistics for counterexample generation.").build());
- options.push_back(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based minimal command counterexample generation.").build());
- options.push_back(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build());
-
- // Finally, register all options that we just created.
- settingsManager.registerModule(moduleName, options);
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, true, "Sets whether to display statistics for counterexample generation.").build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based minimal command counterexample generation.").build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build());
}
} // namespace modules
diff --git a/src/settings/modules/CounterexampleGeneratorSettings.h b/src/settings/modules/CounterexampleGeneratorSettings.h
index d3a9626ab..33b394a6e 100644
--- a/src/settings/modules/CounterexampleGeneratorSettings.h
+++ b/src/settings/modules/CounterexampleGeneratorSettings.h
@@ -60,7 +60,9 @@ namespace storm {
/*!
* Retrieves whether scheduler cuts are to be used if the MAXSAT-based technique is used to generate a
- * minimal command set counterexample
+ * minimal command set counterexample.
+ *
+ * @return True iff scheduler cuts are to be used.
*/
bool useSchedulerCuts() const;
@@ -71,9 +73,11 @@ namespace storm {
*/
bool showStatistics() const;
+ // The name of the module.
+ static const std::string moduleName;
+
private:
// Define the string names of the options as constants.
- static const std::string moduleName;
static const std::string minimalCommandSetOptionName;
static const std::string encodeReachabilityOptionName;
static const std::string schedulerCutsOptionName;
diff --git a/src/settings/modules/CuddSettings.cpp b/src/settings/modules/CuddSettings.cpp
index 406cac4b7..dffef2457 100644
--- a/src/settings/modules/CuddSettings.cpp
+++ b/src/settings/modules/CuddSettings.cpp
@@ -11,12 +11,10 @@ namespace storm {
const std::string maximalMemoryOptionName = "maxmem";
const std::string reorderOptionName = "reorder";
- CuddSettings::CuddSettings(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, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+ CuddSettings::CuddSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mb", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(2048).build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mb", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(2048).build()).build());
std::vector<std::string> reorderingTechniques;
reorderingTechniques.push_back("none");
@@ -37,10 +35,7 @@ namespace storm {
reorderingTechniques.push_back("annealing");
reorderingTechniques.push_back("genetic");
reorderingTechniques.push_back("exact");
- options.push_back(storm::settings::OptionBuilder(moduleName, reorderOptionName, true, "Sets the reordering technique used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used by Cudd's reordering routines. Must be in {none, random, randompivot, sift, siftconv, ssift, ssiftconv, gsift, gsiftconv, win2, win2conv, win3, win3conv, win4, win4conv, annealing, genetic, exact}.").setDefaultValueString("gsift").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(reorderingTechniques)).build()).build());
-
- // Finally, register all options that we just created.
- settingsManager.registerModule(moduleName, options);
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, reorderOptionName, true, "Sets the reordering technique used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used by Cudd's reordering routines. Must be in {none, random, randompivot, sift, siftconv, ssift, ssiftconv, gsift, gsiftconv, win2, win2conv, win3, win3conv, win4, win4conv, annealing, genetic, exact}.").setDefaultValueString("gsift").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(reorderingTechniques)).build()).build());
}
} // namespace modules
diff --git a/src/settings/modules/CuddSettings.h b/src/settings/modules/CuddSettings.h
index e0e588953..db59ddc77 100644
--- a/src/settings/modules/CuddSettings.h
+++ b/src/settings/modules/CuddSettings.h
@@ -43,9 +43,11 @@ namespace storm {
*/
ReorderingTechnique getReorderingTechnique() const;
+ // The name of the module.
+ static const std::string moduleName;
+
private:
// Define the string names of the options as constants.
- static const std::string moduleName;
static const std::string precisionOptionName;
static const std::string maximalMemoryOptionName;
static const std::string reorderOptionName;
diff --git a/src/settings/modules/DebugSettings.cpp b/src/settings/modules/DebugSettings.cpp
index 3fa44529a..c78f47b14 100644
--- a/src/settings/modules/DebugSettings.cpp
+++ b/src/settings/modules/DebugSettings.cpp
@@ -12,16 +12,11 @@ namespace storm {
const std::string DebugSettings::logfileOptionName = "logfile";
const std::string DebugSettings::logfileOptionShortName = "l";
- DebugSettings::DebugSettings(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, debugOptionName, false, "Print debug output.").build());
- options.push_back(storm::settings::OptionBuilder(moduleName, traceOptionName, false, "Print even more debug output.").build());
- options.push_back(storm::settings::OptionBuilder(moduleName, logfileOptionName, false, "If specified, the log output will also be written to this file.").setShortName(logfileOptionShortName)
+ DebugSettings::DebugSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Print debug output.").build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, traceOptionName, false, "Print even more debug output.").build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, logfileOptionName, false, "If specified, the log output will also be written to this file.").setShortName(logfileOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to write the log.").build()).build());
-
- // Finally, register all options that we just created.
- settingsManager.registerModule(moduleName, options);
}
} // namespace modules
diff --git a/src/settings/modules/DebugSettings.h b/src/settings/modules/DebugSettings.h
index 9a65c53c9..024246b68 100644
--- a/src/settings/modules/DebugSettings.h
+++ b/src/settings/modules/DebugSettings.h
@@ -47,9 +47,11 @@ namespace storm {
*/
std::string getLogfilename() const;
+ // The name of the module.
+ static const std::string moduleName;
+
private:
// Define the string names of the options as constants.
- static const std::string moduleName;
static const std::string debugOptionName;
static const std::string traceOptionName;
static const std::string logfileOptionName;
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index a13ea57e6..961f1e140 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -11,6 +11,8 @@ namespace storm {
const std::string GeneralSettings::helpOptionShortName = "h";
const std::string GeneralSettings::verboseOptionName = "verbose";
const std::string GeneralSettings::verboseOptionShortName = "v";
+ const std::string GeneralSettings::precisionOptionName = "precision";
+ const std::string GeneralSettings::precisionOptionShortName = "p";
const std::string GeneralSettings::exportDotOptionName = "exportdot";
const std::string GeneralSettings::configOptionName = "config";
const std::string GeneralSettings::configOptionShortName = "c";
@@ -33,51 +35,48 @@ namespace storm {
const std::string GeneralSettings::constantsOptionName = "constants";
const std::string GeneralSettings::constantsOptionShortName = "const";
- GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
- // First, we need to create all options of this module.
- std::vector<std::shared_ptr<Option>> options;
+ GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
std::vector<std::string> moduleNames = {"all", "general", "debug", "cudd", "counterexample", "glpk", "gurobi", "gmm++", "native"};
- options.push_back(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("module", "The module for which to show the help or 'all' for all modules.").setDefaultValueString("all").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(moduleNames)).build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.")
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName)
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the configuration.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName)
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName)
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, pctlOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.")
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the PCTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, cslOptionName, false, "Specifies the CSL formulas that are to be checked on the model.")
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the CSL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, ltlOptionName, false, "Specifies the LTL formulas that are to be checked on the model.")
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model")
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the counterexample is to be written.").build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("module", "The module for which to show the help or 'all' for all modules.").setDefaultValueString("all").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(moduleNames)).build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The internally used precision.").setShortName(precisionOptionShortName)
+ .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName)
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the configuration.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName)
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName)
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, pctlOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the PCTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, cslOptionName, false, "Specifies the CSL formulas that are to be checked on the model.")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the CSL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, ltlOptionName, false, "Specifies the LTL formulas that are to be checked on the model.")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the counterexample is to be written.").build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, "", "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, false, "If given, the state rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, fixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(fixDeadlockOptionShortName).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, "", "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, false, "If given, the state rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, fixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(fixDeadlockOptionShortName).build());
std::vector<std::string> linearEquationSolver = {"gmm++", "native"};
- options.push_back(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.")
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, timeoutOptionName, false, "If given, computation will abort after the timeout has been reached.").setShortName(timeoutOptionShortName)
- .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "The number of seconds after which to timeout.").setDefaultValueUnsignedInteger(0).build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, timeoutOptionName, false, "If given, computation will abort after the timeout has been reached.").setShortName(timeoutOptionShortName)
+ .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "The number of seconds after which to timeout.").setDefaultValueUnsignedInteger(0).build()).build());
std::vector<std::string> lpSolvers = {"gurobi", "glpk"};
- options.push_back(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.")
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName)
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build());
-
- // Finally, register all options that we just created.
- settingsManager.registerModule(moduleName, options);
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName)
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build());
}
} // namespace modules
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index 9f5c55c7f..504114d48 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/src/settings/modules/GeneralSettings.h
@@ -11,7 +11,7 @@ namespace storm {
* This class represents the general settings.
*/
class GeneralSettings : public ModuleSettings {
- public:
+ public:
// An enumeration of all available LP solvers.
enum class LpSolver { Gurobi, glpk };
@@ -47,6 +47,13 @@ namespace storm {
*/
bool isVerboseSet() const;
+ /*!
+ * Retrieves the precision to use for numerical operations.
+ *
+ * @return The precision to use for numerical operations.
+ */
+ double getPrecision() const;
+
/*!
* Retrieves whether the export-to-dot option was set.
*
@@ -248,14 +255,18 @@ namespace storm {
* @return The string that defines the constants of a symbolic model.
*/
std::string getConstantDefinitionString() const;
-
+
+ // The name of the module.
+ static const std::string moduleName;
+
private:
// Define the string names of the options as constants.
- static const std::string moduleName;
static const std::string helpOptionName;
static const std::string helpOptionShortName;
static const std::string verboseOptionName;
static const std::string verboseOptionShortName;
+ static const std::string precisionOptionName;
+ static const std::string precisionOptionShortName;
static const std::string exportDotOptionName;
static const std::string configOptionName;
static const std::string configOptionShortName;
diff --git a/src/settings/modules/GlpkSettings.cpp b/src/settings/modules/GlpkSettings.cpp
index 7b859c143..9534fc4e3 100644
--- a/src/settings/modules/GlpkSettings.cpp
+++ b/src/settings/modules/GlpkSettings.cpp
@@ -10,13 +10,9 @@ namespace storm {
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);
+ GlpkSettings::GlpkSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, outputOptionName, true, "If set, the glpk output will be printed to the command line.").build());
+ this->addAndRegisterOption(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());
}
} // namespace modules
diff --git a/src/settings/modules/GlpkSettings.h b/src/settings/modules/GlpkSettings.h
index 37420d117..c23b2add0 100644
--- a/src/settings/modules/GlpkSettings.h
+++ b/src/settings/modules/GlpkSettings.h
@@ -26,9 +26,18 @@ namespace storm {
*/
bool isOutputSet() const;
+ /*!
+ * Retrieves the integer tolerance to be used.
+ *
+ * @return The integer tolerance to be used.
+ */
+ double getIntegerTolerance() const;
+
+ // The name of the module.
+ static const std::string moduleName;
+
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/GmmxxEquationSolverSettings.cpp b/src/settings/modules/GmmxxEquationSolverSettings.cpp
index 1e66f2b4f..2658fd0e2 100644
--- a/src/settings/modules/GmmxxEquationSolverSettings.cpp
+++ b/src/settings/modules/GmmxxEquationSolverSettings.cpp
@@ -15,26 +15,21 @@ namespace storm {
const std::string GmmxxEquationSolverSettings::precisionOptionName = "precision";
const std::string GmmxxEquationSolverSettings::absoluteOptionName = "absolute";
- 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;
+ GmmxxEquationSolverSettings::GmmxxEquationSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
std::vector<std::string> methods = {"bicgstab", "qmr", "gmres", "jacobi"};
- options.push_back(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the gmm++ engine. Available are {bicgstab, qmr, gmres, jacobi}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("gmres").build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the gmm++ engine. Available are {bicgstab, qmr, gmres, jacobi}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("gmres").build()).build());
// Register available preconditioners.
std::vector<std::string> preconditioner = {"ilu", "diagonal", "ildlt", "none"};
- options.push_back(storm::settings::OptionBuilder(moduleName, preconditionOptionName, true, "The preconditioning technique used for solving linear equation systems. Available are {ilu, diagonal, none}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(preconditioner)).setDefaultValueString("ilu").build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, preconditionOptionName, true, "The preconditioning technique used for solving linear equation systems. Available are {ilu, diagonal, none}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(preconditioner)).setDefaultValueString("ilu").build()).build());
- options.push_back(storm::settings::OptionBuilder(moduleName, restartOptionName, true, "The number of iteration until restarted methods are actually restarted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of iterations.").setDefaultValueUnsignedInteger(50).build()).build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, restartOptionName, true, "The number of iteration until restarted methods are actually restarted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of iterations.").setDefaultValueUnsignedInteger(50).build()).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("iterations", "The maximal iteration count.").setDefaultValueUnsignedInteger(10000).build()).build());
+ this->addAndRegisterOption(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("iterations", "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());
+ this->addAndRegisterOption(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 detecting convergence.").build());
-
- // Finally, register all options that we just created.
- settingsManager.registerModule(moduleName, options);
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
}
} // namespace modules
diff --git a/src/settings/modules/GmmxxEquationSolverSettings.h b/src/settings/modules/GmmxxEquationSolverSettings.h
index 3fc1295a0..7504f7456 100644
--- a/src/settings/modules/GmmxxEquationSolverSettings.h
+++ b/src/settings/modules/GmmxxEquationSolverSettings.h
@@ -16,7 +16,7 @@ namespace storm {
enum class LinearEquationTechnique { Bicgstab, Qmr, Gmres, Jacobi };
// An enumeration of all available preconditioning techniques.
- enum class PreconditioningTechnique { Ilu, Diagonal, Ildlt, None };
+ enum class PreconditioningTechnique { Ilu, Diagonal, None };
// An enumeration of all available convergence criteria.
enum class ConvergenceCriterion { Absolute, Relative };
@@ -70,9 +70,11 @@ namespace storm {
*/
ConvergenceCriterion getConvergenceCriterion() const;
+ // The name of the module.
+ static const std::string moduleName;
+
private:
// Define the string names of the options as constants.
- static const std::string moduleName;
static const std::string techniqueOptionName;
static const std::string preconditionOptionName;
static const std::string restartOptionName;
diff --git a/src/settings/modules/GurobiSettings.cpp b/src/settings/modules/GurobiSettings.cpp
index a9713b31e..be78a59ee 100644
--- a/src/settings/modules/GurobiSettings.cpp
+++ b/src/settings/modules/GurobiSettings.cpp
@@ -11,17 +11,12 @@ namespace storm {
const std::string GurobiSettings::threadsOption = "threads";
const std::string GurobiSettings::outputOption = "output";
- GurobiSettings::GurobiSettings(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, 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());
+ GurobiSettings::GurobiSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
+ this->addAndRegisterOption(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());
- options.push_back(storm::settings::OptionBuilder(moduleName, outputOption, true, "If set, the Gurobi output will be printed to the command line.").build());
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, outputOption, true, "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());
-
- // Finally, register all options that we just created.
- settingsManager.registerModule(moduleName, options);
+ this->addAndRegisterOption(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());
}
} // namespace modules
diff --git a/src/settings/modules/GurobiSettings.h b/src/settings/modules/GurobiSettings.h
index 763490ae9..d0e92127b 100644
--- a/src/settings/modules/GurobiSettings.h
+++ b/src/settings/modules/GurobiSettings.h
@@ -40,9 +40,11 @@ namespace storm {
*/
bool isOutputSet() const;
+ // The name of the module.
+ static const std::string moduleName;
+
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;
diff --git a/src/settings/modules/ModuleSettings.cpp b/src/settings/modules/ModuleSettings.cpp
index 239bd822e..8a877c6d7 100644
--- a/src/settings/modules/ModuleSettings.cpp
+++ b/src/settings/modules/ModuleSettings.cpp
@@ -4,7 +4,7 @@ namespace storm {
namespace settings {
namespace modules {
- ModuleSettings::ModuleSettings(storm::settings::SettingsManager& settingsManager) : settingsManager(settingsManager) {
+ ModuleSettings::ModuleSettings(storm::settings::SettingsManager& settingsManager, std::string const& moduleName) : settingsManager(settingsManager), moduleName(moduleName) {
// Intentionally left empty.
}
@@ -16,12 +16,12 @@ namespace storm {
return this->settingsManager;
}
- void ModuleSettings::set(std::string const& name) const {
- return this->getOption(longName).setHasOptionBeenSet();
+ void ModuleSettings::set(std::string const& name) {
+ return this->getOption(name).setHasOptionBeenSet();
}
- void ModuleSettings::unset(std::string const& longName) const {
- return this->getOption(longName).setHasOptionBeenSet(false);
+ void ModuleSettings::unset(std::string const& name) {
+ return this->getOption(name).setHasOptionBeenSet(false);
}
} // namespace modules
diff --git a/src/settings/modules/ModuleSettings.h b/src/settings/modules/ModuleSettings.h
index 6f3e70ad2..6acb7d200 100644
--- a/src/settings/modules/ModuleSettings.h
+++ b/src/settings/modules/ModuleSettings.h
@@ -5,12 +5,12 @@
#include <unordered_map>
#include "src/settings/Option.h"
-#include "src/settings/SettingMemento.h"
namespace storm {
namespace settings {
- // Forward-declare SettingsManager class.
+ // Forward-declare some classes.
class SettingsManager;
+ class SettingMemento;
namespace modules {
@@ -19,12 +19,16 @@ namespace storm {
*/
class ModuleSettings {
public:
+ // Declare the memento class as a friend so it can manipulate the internal state.
+ friend class storm::settings::SettingMemento;
+
/*!
* Constructs a new settings object.
*
* @param settingsManager The manager responsible for these settings.
+ * @param moduleName The name of the module for which to build the settings.
*/
- ModuleSettings(storm::settings::SettingsManager& settingsManager);
+ ModuleSettings(storm::settings::SettingsManager& settingsManager, std::string const& moduleName);
/*!
* Checks whether the settings are consistent. If they are inconsistent, an exception is thrown.
@@ -53,12 +57,9 @@ 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.
+ * Retrieves the name of the module to which these settings belong.
*/
- void addOption(std::string const& longName, std::shared_ptr<Option> const& option);
+ std::string const& getModuleName() const;
/*!
* Retrieves the option with the given long name. If no such option exists, an exception is thrown.
@@ -82,7 +83,7 @@ namespace storm {
*
* @param name The name of the option to set.
*/
- void set(std::string const& name) const;
+ void set(std::string const& name);
/*!
* Unsets the option with the specified name. This requires the option to not have any arguments. This
@@ -90,12 +91,22 @@ namespace storm {
*
* @param name The name of the option to unset.
*/
- void unset(std::string const& longName) const;
+ void unset(std::string const& name);
+
+ /*!
+ * Adds and registers the given option.
+ *
+ * @param option The option to add and register.
+ */
+ void addAndRegisterOption(std::shared_ptr<Option> option) const;
private:
// The settings manager responsible for the settings.
storm::settings::SettingsManager const& settingsManager;
+ // The name of the module.
+ std::string moduleName;
+
// A mapping of option names of the module to the actual options.
std::unordered_map<std::string, std::shared_ptr<Option>> options;
};
diff --git a/src/settings/modules/NativeEquationSolverSettings.cpp b/src/settings/modules/NativeEquationSolverSettings.cpp
index 191df9371..ddf50650b 100644
--- a/src/settings/modules/NativeEquationSolverSettings.cpp
+++ b/src/settings/modules/NativeEquationSolverSettings.cpp
@@ -13,20 +13,15 @@ namespace storm {
const std::string NativeEquationSolverSettings::precisionOptionName = "precision";
const std::string NativeEquationSolverSettings::absoluteOptionName = "absolute";
- NativeEquationSolverSettings::NativeEquationSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) {
- // First, we need to create all options of this module.
- std::vector<std::shared_ptr<Option>> options;
+ NativeEquationSolverSettings::NativeEquationSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
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());
+ this->addAndRegisterOption(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());
- 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());
+ this->addAndRegisterOption(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());
- 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());
+ this->addAndRegisterOption(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 detecting convergence.").build());
-
- // Finally, register all options that we just created.
- settingsManager.registerModule(moduleName, options);
+ this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
}
} // namespace modules
diff --git a/src/settings/modules/NativeEquationSolverSettings.h b/src/settings/modules/NativeEquationSolverSettings.h
index da3d06fa4..04b58822a 100644
--- a/src/settings/modules/NativeEquationSolverSettings.h
+++ b/src/settings/modules/NativeEquationSolverSettings.h
@@ -48,9 +48,11 @@ namespace storm {
*/
ConvergenceCriterion getConvergenceCriterion() const;
+ // The name of the module.
+ static const std::string moduleName;
+
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;
diff --git a/src/solver/GlpkLpSolver.cpp b/src/solver/GlpkLpSolver.cpp
index e68528fa6..b61679929 100644
--- a/src/solver/GlpkLpSolver.cpp
+++ b/src/solver/GlpkLpSolver.cpp
@@ -21,7 +21,7 @@ namespace storm {
glp_set_prob_name(lp, name.c_str());
// Set whether the glpk output shall be printed to the command line.
- glp_term_out(storm::settings::SettingsManager::getInstance()->isSet("debug") || storm::settings::SettingsManager::getInstance()->isSet("glpkoutput") ? GLP_ON : GLP_OFF);
+ glp_term_out(storm::settings::debugSettings().isDebugSet() || storm::settings::glpkSettings().isOutputSet() ? GLP_ON : GLP_OFF);
// Because glpk uses 1-based indexing (wtf!?), we need to put dummy elements into the matrix vectors.
rowIndices.push_back(0);
@@ -145,13 +145,13 @@ namespace storm {
// Determine the type of the constraint and add it properly.
switch (constraint.getOperator()) {
case storm::expressions::OperatorType::Less:
- glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_UP, 0, rightCoefficients.second - storm::settings::SettingsManager::getInstance()->getOptionByLongName("glpkinttol").getArgument(0).getValueAsDouble());
+ glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_UP, 0, rightCoefficients.second - storm::settings::glpkSettings().getIntegerTolerance());
break;
case storm::expressions::OperatorType::LessOrEqual:
glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_UP, 0, rightCoefficients.second);
break;
case storm::expressions::OperatorType::Greater:
- glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_LO, rightCoefficients.second + storm::settings::SettingsManager::getInstance()->getOptionByLongName("glpkinttol").getArgument(0).getValueAsDouble(), 0);
+ glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_LO, rightCoefficients.second + storm::settings::glpkSettings().getIntegerTolerance(), 0);
break;
case storm::expressions::OperatorType::GreaterOrEqual:
glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_LO, rightCoefficients.second, 0);
@@ -187,7 +187,7 @@ namespace storm {
glp_iocp* parameters = new glp_iocp();
glp_init_iocp(parameters);
parameters->presolve = GLP_ON;
- parameters->tol_int = storm::settings::SettingsManager::getInstance()->getOptionByLongName("glpkinttol").getArgument(0).getValueAsDouble();
+ parameters->tol_int = storm::settings::glpkSettings().getIntegerTolerance();
error = glp_intopt(this->lp, parameters);
delete parameters;
@@ -285,7 +285,7 @@ namespace storm {
}
// Now check the desired precision was actually achieved.
- LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::SettingsManager::getInstance()->getOptionByLongName("glpkinttol").getArgument(0).getValueAsDouble(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in glpk solution (" << value << ").");
+ LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::glpkSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in glpk solution (" << value << ").");
return static_cast<int_fast64_t>(value);
}
@@ -307,7 +307,7 @@ namespace storm {
value = glp_get_col_prim(this->lp, static_cast<int>(variableIndexPair->second));
}
- LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::SettingsManager::getInstance()->getOptionByLongName("glpkinttol").getArgument(0).getValueAsDouble(), storm::exceptions::InvalidStateException, "Illegal value for binary variable in glpk solution (" << value << ").");
+ LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::glpkSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for binary variable in glpk solution (" << value << ").");
return static_cast<bool>(value);
}
diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp
index 5f3d92275..6c0802996 100644
--- a/src/solver/GmmxxLinearEquationSolver.cpp
+++ b/src/solver/GmmxxLinearEquationSolver.cpp
@@ -24,34 +24,34 @@ namespace storm {
template<typename ValueType>
GmmxxLinearEquationSolver<ValueType>::GmmxxLinearEquationSolver() {
// Get the settings object to customize linear solving.
- storm::settings::SettingsManager* settings = storm::settings::SettingsManager::getInstance();
+ storm::settings::modules::GmmxxEquationSolverSettings const& settings =storm::settings::gmmxxEquationSolverSettings();
// Get appropriate settings.
- maximalNumberOfIterations = settings->getOptionByLongName("maxiter").getArgument(0).getValueAsUnsignedInteger();
- precision = settings->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
- relative = !settings->isSet("absolute");
- restart = settings->getOptionByLongName("gmmrestart").getArgument(0).getValueAsUnsignedInteger();
+ maximalNumberOfIterations = settings.getMaximalIterationCount();
+ precision = settings.getPrecision();;
+ relative = settings.getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative;
+ restart = settings.getRestartIterationCount();
// Determine the method to be used.
- std::string const& methodAsString = settings->getOptionByLongName("gmmlin").getArgument(0).getValueAsString();
- if (methodAsString == "bicgstab") {
- method = BICGSTAB;
- } else if (methodAsString == "qmr") {
- method = QMR;
- } else if (methodAsString == "gmres") {
- method = GMRES;
- } else if (methodAsString == "jacobi") {
- method = JACOBI;
+ storm::settings::modules::GmmxxEquationSolverSettings::LinearEquationTechnique methodAsSetting = settings.getLinearEquationSystemTechnique();
+ if (methodAsSetting == storm::settings::modules::GmmxxEquationSolverSettings::LinearEquationTechnique::Bicgstab) {
+ method = SolutionMethod::Bicgstab;
+ } else if (methodAsSetting == storm::settings::modules::GmmxxEquationSolverSettings::LinearEquationTechnique::Qmr) {
+ method = SolutionMethod::Qmr;
+ } else if (methodAsSetting == storm::settings::modules::GmmxxEquationSolverSettings::LinearEquationTechnique::Gmres) {
+ method = SolutionMethod::Gmres;
+ } else if (methodAsSetting == storm::settings::modules::GmmxxEquationSolverSettings::LinearEquationTechnique::Jacobi) {
+ method = SolutionMethod::Jacobi;
}
// Check which preconditioner to use.
- std::string const& preconditionAsString = settings->getOptionByLongName("gmmpre").getArgument(0).getValueAsString();
- if (preconditionAsString == "ilu") {
- preconditioner = ILU;
- } else if (preconditionAsString == "diagonal") {
- preconditioner = DIAGONAL;
- } else if (preconditionAsString == "none") {
- preconditioner = NONE;
+ storm::settings::modules::GmmxxEquationSolverSettings::PreconditioningTechnique preconditionAsSetting = settings.getPreconditioningTechnique();
+ if (preconditionAsSetting == storm::settings::modules::GmmxxEquationSolverSettings::PreconditioningTechnique::Ilu) {
+ preconditioner = Preconditioner::Ilu;
+ } else if (preconditionAsSetting == storm::settings::modules::GmmxxEquationSolverSettings::PreconditioningTechnique::Diagonal) {
+ preconditioner = Preconditioner::Diagonal;
+ } else if (preconditionAsSetting == storm::settings::modules::GmmxxEquationSolverSettings::PreconditioningTechnique::None) {
+ preconditioner = Preconditioner::None;
}
}
@@ -63,38 +63,38 @@ namespace storm {
template<typename ValueType>
void GmmxxLinearEquationSolver<ValueType>::solveEquationSystem(storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult) const {
LOG4CPLUS_INFO(logger, "Using method '" << methodToString() << "' with preconditioner " << preconditionerToString() << "'.");
- if (method == JACOBI && preconditioner != NONE) {
+ if (method == SolutionMethod::Jacobi && preconditioner != Preconditioner::None) {
LOG4CPLUS_WARN(logger, "Jacobi method currently does not support preconditioners. The requested preconditioner will be ignored.");
}
- if (method == BICGSTAB || method == QMR || method == GMRES) {
+ if (method == SolutionMethod::Bicgstab || method == SolutionMethod::Qmr || method == SolutionMethod::Gmres) {
std::unique_ptr<gmm::csr_matrix<ValueType>> gmmA = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(A);
// Prepare an iteration object that determines the accuracy and the maximum number of iterations.
gmm::iteration iter(precision, 0, maximalNumberOfIterations);
- if (method == BICGSTAB) {
- if (preconditioner == ILU) {
+ if (method == SolutionMethod::Bicgstab) {
+ if (preconditioner == Preconditioner::Ilu) {
gmm::bicgstab(*gmmA, x, b, gmm::ilu_precond<gmm::csr_matrix<ValueType>>(*gmmA), iter);
- } else if (preconditioner == DIAGONAL) {
+ } else if (preconditioner == Preconditioner::Diagonal) {
gmm::bicgstab(*gmmA, x, b, gmm::diagonal_precond<gmm::csr_matrix<ValueType>>(*gmmA), iter);
- } else if (preconditioner == NONE) {
+ } else if (preconditioner == Preconditioner::None) {
gmm::bicgstab(*gmmA, x, b, gmm::identity_matrix(), iter);
}
- } else if (method == QMR) {
- if (preconditioner == ILU) {
+ } else if (method == SolutionMethod::Qmr) {
+ if (preconditioner == Preconditioner::Ilu) {
gmm::qmr(*gmmA, x, b, gmm::ilu_precond<gmm::csr_matrix<ValueType>>(*gmmA), iter);
- } else if (preconditioner == DIAGONAL) {
+ } else if (preconditioner == Preconditioner::Diagonal) {
gmm::qmr(*gmmA, x, b, gmm::diagonal_precond<gmm::csr_matrix<ValueType>>(*gmmA), iter);
- } else if (preconditioner == NONE) {
+ } else if (preconditioner == Preconditioner::None) {
gmm::qmr(*gmmA, x, b, gmm::identity_matrix(), iter);
}
- } else if (method == GMRES) {
- if (preconditioner == ILU) {
+ } else if (method == SolutionMethod::Qmr) {
+ if (preconditioner == Preconditioner::Ilu) {
gmm::gmres(*gmmA, x, b, gmm::ilu_precond<gmm::csr_matrix<ValueType>>(*gmmA), restart, iter);
- } else if (preconditioner == DIAGONAL) {
+ } else if (preconditioner == Preconditioner::Diagonal) {
gmm::gmres(*gmmA, x, b, gmm::diagonal_precond<gmm::csr_matrix<ValueType>>(*gmmA), restart, iter);
- } else if (preconditioner == NONE) {
+ } else if (preconditioner == Preconditioner::None) {
gmm::gmres(*gmmA, x, b, gmm::identity_matrix(), restart, iter);
}
}
@@ -105,7 +105,7 @@ namespace storm {
} else {
LOG4CPLUS_WARN(logger, "Iterative solver did not converge.");
}
- } else if (method == JACOBI) {
+ } else if (method == SolutionMethod::Jacobi) {
uint_fast64_t iterations = solveLinearEquationSystemWithJacobi(A, x, b, multiplyResult);
// Check if the solver converged and issue a warning otherwise.
@@ -216,29 +216,20 @@ namespace storm {
template<typename ValueType>
std::string GmmxxLinearEquationSolver<ValueType>::methodToString() const {
- if (method == BICGSTAB) {
- return "bicgstab";
- } else if (method == QMR) {
- return "qmr";
- } else if (method == GMRES) {
- return "gmres";
- } else if (method == JACOBI) {
- return "jacobi";
- } else {
- throw storm::exceptions::InvalidStateException() << "Illegal method '" << method << "' set in GmmxxLinearEquationSolver.";
+ switch (method) {
+ case SolutionMethod::Bicgstab: return "bicgstab";
+ case SolutionMethod::Qmr: return "qmr";
+ case SolutionMethod::Gmres: return "gmres";
+ case SolutionMethod::Jacobi: return "jacobi";
}
}
template<typename ValueType>
std::string GmmxxLinearEquationSolver<ValueType>::preconditionerToString() const {
- if (preconditioner == ILU) {
- return "ilu";
- } else if (preconditioner == DIAGONAL) {
- return "diagonal";
- } else if (preconditioner == NONE) {
- return "none";
- } else {
- throw storm::exceptions::InvalidStateException() << "Illegal preconditioner '" << preconditioner << "' set in GmmxxLinearEquationSolver.";
+ switch (preconditioner) {
+ case Preconditioner::Ilu: return "ilu";
+ case Preconditioner::Diagonal: return "diagonal";
+ case Preconditioner::None: return "none";
}
}
diff --git a/src/solver/GmmxxLinearEquationSolver.h b/src/solver/GmmxxLinearEquationSolver.h
index a67de0764..63f97a9cb 100644
--- a/src/solver/GmmxxLinearEquationSolver.h
+++ b/src/solver/GmmxxLinearEquationSolver.h
@@ -13,13 +13,13 @@ namespace storm {
class GmmxxLinearEquationSolver : public LinearEquationSolver<ValueType> {
public:
// An enumeration specifying the available preconditioners.
- enum Preconditioner {
- ILU, DIAGONAL, NONE
+ enum class Preconditioner {
+ Ilu, Diagonal, None
};
// An enumeration specifying the available solution methods.
- enum SolutionMethod {
- BICGSTAB, QMR, GMRES, JACOBI
+ enum class SolutionMethod {
+ Bicgstab, Qmr, Gmres, Jacobi
};
/*!
diff --git a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp b/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp
index 5de34200e..abd11ad73 100644
--- a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp
+++ b/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp
@@ -12,12 +12,12 @@ namespace storm {
template<typename ValueType>
GmmxxNondeterministicLinearEquationSolver<ValueType>::GmmxxNondeterministicLinearEquationSolver() {
// Get the settings object to customize solving.
- storm::settings::SettingsManager* settings = storm::settings::SettingsManager::getInstance();
+ storm::settings::modules::GmmxxEquationSolverSettings const& settings = storm::settings::gmmxxEquationSolverSettings();
// Get appropriate settings.
- maximalNumberOfIterations = settings->getOptionByLongName("maxiter").getArgument(0).getValueAsUnsignedInteger();
- precision = settings->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
- relative = !settings->isSet("absolute");
+ maximalNumberOfIterations = settings.getMaximalIterationCount();
+ precision = settings.getPrecision();
+ relative = settings.getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative;
}
template<typename ValueType>
diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp
index 47ca2f0e4..14c520068 100644
--- a/src/solver/NativeLinearEquationSolver.cpp
+++ b/src/solver/NativeLinearEquationSolver.cpp
@@ -17,17 +17,17 @@ namespace storm {
template<typename ValueType>
NativeLinearEquationSolver<ValueType>::NativeLinearEquationSolver() {
// Get the settings object to customize linear solving.
- storm::settings::SettingsManager* settings = storm::settings::SettingsManager::getInstance();
+ storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings();
// Get appropriate settings.
- maximalNumberOfIterations = settings->getOptionByLongName("maxiter").getArgument(0).getValueAsUnsignedInteger();
- precision = settings->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
- relative = !settings->isSet("absolute");
+ maximalNumberOfIterations = settings.getMaximalIterationCount();
+ precision = settings.getPrecision();
+ relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative;
// Determine the method to be used.
- std::string const& methodAsString = settings->getOptionByLongName("nativelin").getArgument(0).getValueAsString();
- if (methodAsString == "jacobi") {
- method = JACOBI;
+ storm::settings::modules::NativeEquationSolverSettings::LinearEquationTechnique methodAsSetting = settings.getLinearEquationSystemTechnique();
+ if (methodAsSetting == storm::settings::modules::NativeEquationSolverSettings::LinearEquationTechnique::Jacobi) {
+ method = SolutionMethod::Jacobi;
}
}
@@ -127,10 +127,8 @@ namespace storm {
template<typename ValueType>
std::string NativeLinearEquationSolver<ValueType>::methodToString() const {
- if (method == JACOBI) {
- return "jacobi";
- } else {
- throw storm::exceptions::InvalidStateException() << "Illegal method '" << method << "' set in NativeLinearEquationSolver.";
+ switch (method) {
+ case SolutionMethod::Jacobi: return "jacobi";
}
}
diff --git a/src/solver/NativeLinearEquationSolver.h b/src/solver/NativeLinearEquationSolver.h
index af94cdb43..69504b627 100644
--- a/src/solver/NativeLinearEquationSolver.h
+++ b/src/solver/NativeLinearEquationSolver.h
@@ -13,8 +13,8 @@ namespace storm {
class NativeLinearEquationSolver : public LinearEquationSolver<ValueType> {
public:
// An enumeration specifying the available solution methods.
- enum SolutionMethod {
- JACOBI
+ enum class SolutionMethod {
+ Jacobi
};
/*!
diff --git a/src/solver/NativeNondeterministicLinearEquationSolver.cpp b/src/solver/NativeNondeterministicLinearEquationSolver.cpp
index 478448ed5..04867cab3 100644
--- a/src/solver/NativeNondeterministicLinearEquationSolver.cpp
+++ b/src/solver/NativeNondeterministicLinearEquationSolver.cpp
@@ -11,12 +11,12 @@ namespace storm {
template<typename ValueType>
NativeNondeterministicLinearEquationSolver<ValueType>::NativeNondeterministicLinearEquationSolver() {
// Get the settings object to customize solving.
- storm::settings::SettingsManager* settings = storm::settings::SettingsManager::getInstance();
+ storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings();
// Get appropriate settings.
- maximalNumberOfIterations = settings->getOptionByLongName("maxiter").getArgument(0).getValueAsUnsignedInteger();
- precision = settings->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
- relative = !settings->isSet("absolute");
+ maximalNumberOfIterations = settings.getMaximalIterationCount();
+ precision = settings.getPrecision();
+ relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative;
}
template<typename ValueType>
diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp
index e98d7f8fe..cd19fa037 100644
--- a/src/storage/dd/CuddDdManager.cpp
+++ b/src/storage/dd/CuddDdManager.cpp
@@ -10,47 +10,30 @@
namespace storm {
namespace dd {
DdManager<DdType::CUDD>::DdManager() : metaVariableMap(), cuddManager(), reorderingTechnique(CUDD_REORDER_NONE) {
- this->cuddManager.SetMaxMemory(static_cast<unsigned long>(storm::settings::SettingsManager::getInstance()->getOptionByLongName("cuddmaxmem").getArgument(0).getValueAsUnsignedInteger() * 1024ul * 1024ul));
- this->cuddManager.SetEpsilon(storm::settings::SettingsManager::getInstance()->getOptionByLongName("cuddprec").getArgument(0).getValueAsDouble());
+ this->cuddManager.SetMaxMemory(static_cast<unsigned long>(storm::settings::cuddSettings().getMaximalMemory() * 1024ul * 1024ul));
+ this->cuddManager.SetEpsilon(storm::settings::cuddSettings().getConstantPrecision());
// Now set the selected reordering technique.
- std::string const& reorderingTechnique = storm::settings::SettingsManager::getInstance()->getOptionByLongName("reorder").getArgument(0).getValueAsString();
- if (reorderingTechnique == "none") {
- this->reorderingTechnique = CUDD_REORDER_NONE;
- } else if (reorderingTechnique == "random") {
- this->reorderingTechnique = CUDD_REORDER_RANDOM;
- } else if (reorderingTechnique == "randompivot") {
- this->reorderingTechnique = CUDD_REORDER_RANDOM_PIVOT;
- } else if (reorderingTechnique == "sift") {
- this->reorderingTechnique = CUDD_REORDER_SIFT;
- } else if (reorderingTechnique == "siftconv") {
- this->reorderingTechnique = CUDD_REORDER_SIFT_CONVERGE;
- } else if (reorderingTechnique == "ssift") {
- this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT;
- } else if (reorderingTechnique == "ssiftconv") {
- this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT_CONV;
- } else if (reorderingTechnique == "gsift") {
- this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT;
- } else if (reorderingTechnique == "gsiftconv") {
- this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT_CONV;
- } else if (reorderingTechnique == "win2") {
- this->reorderingTechnique = CUDD_REORDER_WINDOW2;
- } else if (reorderingTechnique == "win2conv") {
- this->reorderingTechnique = CUDD_REORDER_WINDOW2_CONV;
- } else if (reorderingTechnique == "win3") {
- this->reorderingTechnique = CUDD_REORDER_WINDOW3;
- } else if (reorderingTechnique == "win3conv") {
- this->reorderingTechnique = CUDD_REORDER_WINDOW3_CONV;
- } else if (reorderingTechnique == "win4") {
- this->reorderingTechnique = CUDD_REORDER_WINDOW4;
- } else if (reorderingTechnique == "win4conv") {
- this->reorderingTechnique = CUDD_REORDER_WINDOW4_CONV;
- } else if (reorderingTechnique == "annealing") {
- this->reorderingTechnique = CUDD_REORDER_ANNEALING;
- } else if (reorderingTechnique == "genetic") {
- this->reorderingTechnique = CUDD_REORDER_GENETIC;
- } else if (reorderingTechnique == "exact") {
- this->reorderingTechnique = CUDD_REORDER_EXACT;
+ storm::settings::modules::CuddSettings::ReorderingTechnique reorderingTechniqueAsSetting = storm::settings::cuddSettings().getReorderingTechnique();
+ switch (reorderingTechniqueAsSetting) {
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::None: this->reorderingTechnique = CUDD_REORDER_NONE; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::Random: this->reorderingTechnique = CUDD_REORDER_RANDOM; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::RandomPivot: this->reorderingTechnique = CUDD_REORDER_RANDOM_PIVOT; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::Sift: this->reorderingTechnique = CUDD_REORDER_SIFT; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::SiftConv: this->reorderingTechnique = CUDD_REORDER_SIFT_CONVERGE; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::SymmetricSift: this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::SymmetricSiftConv: this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT_CONV; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::GroupSift: this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::GroupSiftConv: this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT_CONV; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::Win2: this->reorderingTechnique = CUDD_REORDER_WINDOW2; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::Win2Conv: this->reorderingTechnique = CUDD_REORDER_WINDOW2_CONV; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::Win3: this->reorderingTechnique = CUDD_REORDER_WINDOW3; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::Win3Conv: this->reorderingTechnique = CUDD_REORDER_WINDOW3_CONV; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::Win4: this->reorderingTechnique = CUDD_REORDER_WINDOW4; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::Win4Conv: this->reorderingTechnique = CUDD_REORDER_WINDOW4_CONV; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::Annealing: this->reorderingTechnique = CUDD_REORDER_ANNEALING; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::Genetic: this->reorderingTechnique = CUDD_REORDER_GENETIC; break;
+ case storm::settings::modules::CuddSettings::ReorderingTechnique::Exact: this->reorderingTechnique = CUDD_REORDER_EXACT; break;
}
}
diff --git a/src/storm.cpp b/src/storm.cpp
index 6bc2bad72..eafdb78c8 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -42,7 +42,7 @@
#include "src/solver/NativeLinearEquationSolver.h"
#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
#include "src/solver/GurobiLpSolver.h"
-#include "src/counterexamples/GenerateCounterexample.h"
+// #include "src/counterexamples/GenerateCounterexample.h"
#include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
#include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
#include "src/counterexamples/PathBasedSubsystemGenerator.h"
@@ -73,9 +73,9 @@
* @param modelchecker The model checker that is to be invoked on all given formulae.
*/
void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double> const& modelchecker) {
- storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
- if (s->isSet("prctl")) {
- std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString();
+ storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
+ if (settings.isPctlSet()) {
+ std::string chosenPrctlFile = settings.getPctlPropertiesFilename();
LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << ".");
std::list<std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile);
@@ -110,12 +110,12 @@ int main(const int argc, const char* argv[]) {
// If parsing failed or the option to see the usage was set, program execution stops here.
return 0;
}
-
+
+ storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings();
+
// If requested by the user, we install a timeout signal to abort computation.
- storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
- uint_fast64_t timeout = s->getOptionByLongName("timeout").getArgument(0).getValueAsUnsignedInteger();
- if (timeout != 0) {
- stormSetAlarm(timeout);
+ if (settings.isTimeoutSet()) {
+ stormSetAlarm(settings.getTimeoutInSeconds());
}
// Execution Time measurement, start
@@ -123,17 +123,17 @@ int main(const int argc, const char* argv[]) {
// Now, the settings are received and the specified model is parsed. The actual actions taken depend on whether
// the model was provided in explicit or symbolic format.
- if (s->isSet("explicit")) {
- std::string const chosenTransitionSystemFile = s->getOptionByLongName("explicit").getArgument(0).getValueAsString();
- std::string const chosenLabelingFile = s->getOptionByLongName("explicit").getArgument(1).getValueAsString();
+ if (settings.isExplicitSet()) {
+ std::string const chosenTransitionSystemFile = settings.getTransitionFilename();
+ std::string const chosenLabelingFile = settings.getLabelingFilename();
std::string chosenStateRewardsFile = "";
- if (s->isSet("stateRewards")) {
- chosenStateRewardsFile = s->getOptionByLongName("stateRewards").getArgument(0).getValueAsString();
+ if (settings.isStateRewardsSet()) {
+ chosenStateRewardsFile = settings.getStateRewardsFilename();
}
std::string chosenTransitionRewardsFile = "";
- if (s->isSet("transitionRewards")) {
- chosenTransitionRewardsFile = s->getOptionByLongName("transitionRewards").getArgument(0).getValueAsString();
+ if (settings.isTransitionRewardsSet()) {
+ chosenTransitionRewardsFile = settings.getTransitionRewardsFilename();
}
std::shared_ptr<storm::models::AbstractModel<double>> model = storm::parser::AutoParser::parseModel(chosenTransitionSystemFile, chosenLabelingFile, chosenStateRewardsFile, chosenTransitionRewardsFile);
@@ -142,19 +142,19 @@ int main(const int argc, const char* argv[]) {
std::chrono::high_resolution_clock::time_point parsingEnd = std::chrono::high_resolution_clock::now();
std::cout << "Parsing the given model took " << std::chrono::duration_cast<std::chrono::milliseconds>(parsingEnd - executionStart).count() << " milliseconds." << std::endl;
- if (s->isSet("exportdot")) {
+ if (settings.isExportDotSet()) {
std::ofstream outputFileStream;
- outputFileStream.open(s->getOptionByLongName("exportdot").getArgument(0).getValueAsString(), std::ofstream::out);
+ outputFileStream.open(settings.getExportDotFilename(), std::ofstream::out);
model->writeDotToStream(outputFileStream);
outputFileStream.close();
}
// Should there be a counterexample generated in case the formula is not satisfied?
- if(s->isSet("counterexample")) {
+ if(settings.isCounterexampleSet()) {
// Counterexample Time Measurement, Start
std::chrono::high_resolution_clock::time_point counterexampleStart = std::chrono::high_resolution_clock::now();
- generateCounterExample(model);
+ // generateCounterExample(model);
// Counterexample Time Measurement, End
std::chrono::high_resolution_clock::time_point counterexampleEnd = std::chrono::high_resolution_clock::now();
@@ -213,13 +213,13 @@ int main(const int argc, const char* argv[]) {
std::chrono::high_resolution_clock::time_point modelcheckingEnd = std::chrono::high_resolution_clock::now();
std::cout << "Running the ModelChecker took " << std::chrono::duration_cast<std::chrono::milliseconds>(modelcheckingEnd - modelcheckingStart).count() << " milliseconds." << std::endl;
}
- } else if (s->isSet("symbolic")) {
+ } else if (settings.isSymbolicSet()) {
// Program Translation Time Measurement, Start
std::chrono::high_resolution_clock::time_point programTranslationStart = std::chrono::high_resolution_clock::now();
// First, we build the model using the given symbolic model description and constant definitions.
- std::string const& programFile = s->getOptionByLongName("symbolic").getArgument(0).getValueAsString();
- std::string const& constants = s->getOptionByLongName("constants").getArgument(0).getValueAsString();
+ std::string const& programFile = settings.getSymbolicModelFilename();
+ std::string const& constants = settings.getConstantDefinitionString();
storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
std::shared_ptr<storm::models::AbstractModel<double>> model = storm::adapters::ExplicitModelAdapter<double>::translateProgram(program, constants);
model->printModelInformationToStream(std::cout);
@@ -236,7 +236,7 @@ int main(const int argc, const char* argv[]) {
double value = modelChecker.computeReachabilityProbability(*model->as<storm::models::Dtmc<double>>(), trueStates, targetStates);
std::cout << "computed value " << value << std::endl;
- if (s->isSet("mincmd")) {
+ if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandGenerationSet()) {
if (model->getType() != storm::models::MDP) {
LOG4CPLUS_ERROR(logger, "Minimal command counterexample generation is only supported for models of type MDP.");
throw storm::exceptions::InternalTypeErrorException() << "Minimal command counterexample generation is only supported for models of type MDP.";
@@ -245,13 +245,13 @@ int main(const int argc, const char* argv[]) {
std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();
// Determine whether we are required to use the MILP-version or the SAT-version.
- bool useMILP = s->getOptionByLongName("mincmd").getArgumentByName("method").getValueAsString() == "milp";
+ bool useMILP = storm::settings::counterexampleGeneratorSettings().useMilpBasedMinimalCommandSetGeneration();
// MinCMD Time Measurement, Start
std::chrono::high_resolution_clock::time_point minCmdStart = std::chrono::high_resolution_clock::now();
// Now parse the property file and receive the list of parsed formulas.
- std::string const& propertyFile = s->getOptionByLongName("mincmd").getArgumentByName("propertyFile").getValueAsString();
+ std::string const& propertyFile = storm::settings::generalSettings().getPctlPropertiesFilename();
std::list<std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(propertyFile);
// Now generate the counterexamples for each formula.
@@ -266,7 +266,7 @@ int main(const int argc, const char* argv[]) {
// MinCMD Time Measurement, End
std::chrono::high_resolution_clock::time_point minCmdEnd = std::chrono::high_resolution_clock::now();
std::cout << "Minimal command Counterexample generation took " << std::chrono::duration_cast<std::chrono::milliseconds>(minCmdEnd - minCmdStart).count() << " milliseconds." << std::endl;
- } else if (s->isSet("prctl")) {
+ } else if (settings.isPctlSet()) {
// // Depending on the model type, the appropriate model checking procedure is chosen.
// storm::modelchecker::prctl::AbstractModelChecker<double>* modelchecker = nullptr;
//
diff --git a/src/utility/CLI.h b/src/utility/CLI.h
index 5df81d10b..d70c89f57 100644
--- a/src/utility/CLI.h
+++ b/src/utility/CLI.h
@@ -127,35 +127,36 @@ void printHeader(const int argc, const char* argv[]) {
* @return True iff the program should continue to run after parsing the options.
*/
bool parseOptions(const int argc, const char* argv[]) {
- storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
+ storm::settings::SettingsManager& manager = storm::settings::manager();
try {
- storm::settings::SettingsManager::parse(argc, argv);
+ manager.setFromCommandLine(argc, argv);
} catch (storm::exceptions::OptionParserException& e) {
std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
- std::cout << std::endl << s->getHelpText();
+ std::cout << std::endl;
+ manager.printHelp();
return false;
}
- if (s->isSet("help")) {
- std::cout << storm::settings::SettingsManager::getInstance()->getHelpText();
+ if (storm::settings::generalSettings().isHelpSet()) {
+ storm::settings::manager().printHelp();
return false;
}
- if (s->isSet("verbose")) {
+ if (storm::settings::generalSettings().isVerboseSet()) {
logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL);
LOG4CPLUS_INFO(logger, "Enabled verbose mode, log output gets printed to console.");
}
- if (s->isSet("debug")) {
+ if (storm::settings::debugSettings().isDebugSet()) {
logger.setLogLevel(log4cplus::DEBUG_LOG_LEVEL);
logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::DEBUG_LOG_LEVEL);
LOG4CPLUS_INFO(logger, "Enabled very verbose mode, log output gets printed to console.");
}
- if (s->isSet("trace")) {
+ if (storm::settings::debugSettings().isTraceSet()) {
logger.setLogLevel(log4cplus::TRACE_LOG_LEVEL);
logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::TRACE_LOG_LEVEL);
LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console.");
}
- if (s->isSet("logfile")) {
+ if (storm::settings::debugSettings().isLogfileSet()) {
setUpFileLogging();
}
return true;
diff --git a/src/utility/InitializeLogging.h b/src/utility/InitializeLogging.h
index eefd0f604..ea8394705 100644
--- a/src/utility/InitializeLogging.h
+++ b/src/utility/InitializeLogging.h
@@ -27,8 +27,7 @@ void initializeLogger() {
* Sets up the logging to file.
*/
void setUpFileLogging() {
- storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
- log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(s->getOptionByLongName("logfile").getArgument(0).getValueAsString()));
+ log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(storm::settings::debugSettings().getLogfilename()));
fileLogAppender->setName("mainFileAppender");
fileLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n")));
logger.addAppender(fileLogAppender);
diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp
index 5531f61e5..e18cab3f2 100644
--- a/src/utility/solver.cpp
+++ b/src/utility/solver.cpp
@@ -14,44 +14,35 @@
namespace storm {
namespace utility {
namespace solver {
- std::shared_ptr<storm::solver::LpSolver> getLpSolver(std::string const& name) {
- std::string const& lpSolver = storm::settings::SettingsManager::getInstance()->getOptionByLongName("lpsolver").getArgument(0).getValueAsString();
- if (lpSolver == "gurobi") {
- return std::shared_ptr<storm::solver::LpSolver>(new storm::solver::GurobiLpSolver(name));
- } else if (lpSolver == "glpk") {
- return std::shared_ptr<storm::solver::LpSolver>(new storm::solver::GlpkLpSolver(name));
+ std::unique_ptr<storm::solver::LpSolver> getLpSolver(std::string const& name) {
+ storm::settings::modules::GeneralSettings::LpSolver lpSolver = storm::settings::generalSettings().getLpSolver();
+ switch (lpSolver) {
+ case storm::settings::modules::GeneralSettings::LpSolver::Gurobi: return std::unique_ptr<storm::solver::LpSolver>(new storm::solver::GurobiLpSolver(name));
+ case storm::settings::modules::GeneralSettings::LpSolver::glpk: return std::unique_ptr<storm::solver::LpSolver>(new storm::solver::GlpkLpSolver(name));
}
-
- throw storm::exceptions::InvalidSettingsException() << "No suitable LP solver selected.";
}
template<typename ValueType>
- std::shared_ptr<storm::solver::LinearEquationSolver<ValueType>> getLinearEquationSolver() {
- std::string const& linearEquationSolver = storm::settings::SettingsManager::getInstance()->getOptionByLongName("linsolver").getArgument(0).getValueAsString();
- if (linearEquationSolver == "gmm++") {
- return std::shared_ptr<storm::solver::LinearEquationSolver<ValueType>>(new storm::solver::GmmxxLinearEquationSolver<ValueType>());
- } else if (linearEquationSolver == "native") {
- return std::shared_ptr<storm::solver::LinearEquationSolver<ValueType>>(new storm::solver::NativeLinearEquationSolver<ValueType>());
+ std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> getLinearEquationSolver() {
+ storm::settings::modules::GeneralSettings::EquationSolver equationSolver = storm::settings::generalSettings().getEquationSolver();
+ switch (equationSolver) {
+ case storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx: return std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>(new storm::solver::GmmxxLinearEquationSolver<ValueType>());
+ case storm::settings::modules::GeneralSettings::EquationSolver::Native: return std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>(new storm::solver::NativeLinearEquationSolver<ValueType>());
}
-
- throw storm::exceptions::InvalidSettingsException() << "No suitable linear equation solver selected.";
}
template<typename ValueType>
- std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> getNondeterministicLinearEquationSolver() {
- std::string const& nondeterministicLinearEquationSolver = storm::settings::SettingsManager::getInstance()->getOptionByLongName("ndsolver").getArgument(0).getValueAsString();
- if (nondeterministicLinearEquationSolver == "gmm++") {
- return std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<ValueType>());
- } else if (nondeterministicLinearEquationSolver == "native") {
- return std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>>(new storm::solver::NativeNondeterministicLinearEquationSolver<ValueType>());
+ std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> getNondeterministicLinearEquationSolver() {
+ storm::settings::modules::GeneralSettings::EquationSolver equationSolver = storm::settings::generalSettings().getEquationSolver();
+ switch (equationSolver) {
+ case storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx: return std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<ValueType>());
+ case storm::settings::modules::GeneralSettings::EquationSolver::Native: return std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>>(new storm::solver::NativeNondeterministicLinearEquationSolver<ValueType>());
}
-
- throw storm::exceptions::InvalidSettingsException() << "No suitable nondeterministic linear equation solver selected.";
}
- template std::shared_ptr<storm::solver::LinearEquationSolver<double>> getLinearEquationSolver();
+ template std::unique_ptr<storm::solver::LinearEquationSolver<double>> getLinearEquationSolver();
- template std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<double>> getNondeterministicLinearEquationSolver();
+ template std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<double>> getNondeterministicLinearEquationSolver();
}
}
}
\ No newline at end of file
diff --git a/src/utility/solver.h b/src/utility/solver.h
index e5e7d456f..357a42f0a 100644
--- a/src/utility/solver.h
+++ b/src/utility/solver.h
@@ -11,13 +11,13 @@ namespace storm {
namespace utility {
namespace solver {
- std::shared_ptr<storm::solver::LpSolver> getLpSolver(std::string const& name);
+ std::unique_ptr<storm::solver::LpSolver> getLpSolver(std::string const& name);
template<typename ValueType>
- std::shared_ptr<storm::solver::LinearEquationSolver<ValueType>> getLinearEquationSolver();
+ std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> getLinearEquationSolver();
template<typename ValueType>
- std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> getNondeterministicLinearEquationSolver();
+ std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> getNondeterministicLinearEquationSolver();
}
}