diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h
index 04face217..d98025597 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::counterexampleGeneratorSettings().useSchedulerCuts());
+ boost::container::flat_set<uint_fast64_t> usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isUseSchedulerCutsSet());
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/settings/Argument.h b/src/settings/Argument.h
index e93ce0c84..a9fe0f268 100644
--- a/src/settings/Argument.h
+++ b/src/settings/Argument.h
@@ -95,8 +95,8 @@ namespace storm {
template <typename S>
bool isCompatibleWith(Argument<S> const& other) const {
LOG_THROW(this->getType() == other.getType(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getName() << " and " << other.getName() << ", because they have different types.");
- LOG_THROW(this->getIsOptional() != other.getIsOptional(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getName() << " and " << other.getName() << ", because one of them is optional and the other one is not.");
- LOG_THROW(this->getHasDefaultValue() != other.getHasDefaultValue(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getName() << " and " << other.getName() << ", because one of them has a default value and the other one does not.");
+ LOG_THROW(this->getIsOptional() == other.getIsOptional(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments '" << this->getName() << "' and '" << other.getName() << "', because one of them is optional and the other one is not.");
+ LOG_THROW(this->getHasDefaultValue() == other.getHasDefaultValue(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getName() << " and " << other.getName() << ", because one of them has a default value and the other one does not.");
return true;
}
diff --git a/src/settings/ArgumentBase.cpp b/src/settings/ArgumentBase.cpp
new file mode 100644
index 000000000..79c1b574b
--- /dev/null
+++ b/src/settings/ArgumentBase.cpp
@@ -0,0 +1,76 @@
+#include "src/settings/ArgumentBase.h"
+
+#include <iomanip>
+
+namespace storm {
+ namespace settings {
+ uint_fast64_t ArgumentBase::getPrintLength() const {
+ return this->getName().length() + 2;
+ }
+
+ std::ostream& operator<<(std::ostream& out, ArgumentBase const& argument) {
+ std::streamsize width = out.width();
+ uint_fast64_t charactersPrinted = 0;
+ out << std::setw(0) << std::left << "<" << argument.getName() << "> ";
+ charactersPrinted += 2 + argument.getName().length();
+
+ for (uint_fast64_t i = charactersPrinted; i < width; ++i) {
+ out << out.fill();
+ }
+
+ out << "\t" << argument.getDescription();
+ return out;
+ }
+
+ template <typename TargetType>
+ TargetType ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful) {
+ std::istringstream stream(valueAsString);
+ TargetType t;
+ conversionSuccessful = (stream >> t) && (stream >> std::ws).eof();
+ return t;
+ }
+
+ template <>
+ bool ArgumentBase::convertFromString<bool>(std::string const& s, bool& ok) {
+ static const std::string lowerTrueString = "true";
+ static const std::string lowerFalseString = "false";
+ static const std::string lowerYesString = "yes";
+ static const std::string lowerNoString = "no";
+
+ std::string lowerInput = boost::algorithm::to_lower_copy(s);
+
+ if (s.compare(lowerTrueString) == 0 || s.compare(lowerYesString) == 0) {
+ ok = true;
+ return true;
+ } else if (s.compare(lowerFalseString) == 0 || s.compare(lowerNoString) == 0) {
+ ok = true;
+ return false;
+ }
+
+ std::istringstream stream(s);
+ bool t;
+ ok = (stream >> t) && (stream >> std::ws).eof();
+ return t;
+ }
+
+ template <typename ValueType>
+ std::string ArgumentBase::convertToString(ValueType const& value) {
+ std::ostringstream stream;
+ stream << value;
+ return stream.str();
+ }
+
+ // Explicitly instantiate the templates.
+ template std::string ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful);
+ template int_fast64_t ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful);
+ template uint_fast64_t ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful);
+ template double ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful);
+ template bool ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful);
+
+ template std::string ArgumentBase::convertToString(std::string const& value);
+ template std::string ArgumentBase::convertToString(int_fast64_t const& value);
+ template std::string ArgumentBase::convertToString(uint_fast64_t const& value);
+ template std::string ArgumentBase::convertToString(double const& value);
+ template std::string ArgumentBase::convertToString(bool const& value);
+ }
+}
\ No newline at end of file
diff --git a/src/settings/ArgumentBase.h b/src/settings/ArgumentBase.h
index 8a94dfe17..3531ccd20 100644
--- a/src/settings/ArgumentBase.h
+++ b/src/settings/ArgumentBase.h
@@ -127,6 +127,15 @@ namespace storm {
*/
virtual bool getValueAsBoolean() const = 0;
+ /*!
+ * Retrieves the (print) length of the argument.
+ *
+ * @return The length of the argument.
+ */
+ uint_fast64_t getPrintLength() const;
+
+ friend std::ostream& operator<<(std::ostream& out, ArgumentBase const& argument);
+
protected:
// A flag indicating whether the argument has been set.
bool hasBeenSet;
@@ -157,45 +166,6 @@ namespace storm {
template <typename ValueType>
static std::string convertToString(ValueType const& value);
};
-
- template <typename TargetType>
- TargetType ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful) {
- std::istringstream stream(valueAsString);
- TargetType t;
- conversionSuccessful = (stream >> t) && (stream >> std::ws).eof();
- return t;
- }
-
- template <>
- bool ArgumentBase::convertFromString<bool>(std::string const& s, bool& ok) {
- static const std::string lowerTrueString = "true";
- static const std::string lowerFalseString = "false";
- static const std::string lowerYesString = "yes";
- static const std::string lowerNoString = "no";
-
- std::string lowerInput = boost::algorithm::to_lower_copy(s);
-
- if (s.compare(lowerTrueString) == 0 || s.compare(lowerYesString) == 0) {
- ok = true;
- return true;
- } else if (s.compare(lowerFalseString) == 0 || s.compare(lowerNoString) == 0) {
- ok = true;
- return false;
- }
-
- std::istringstream stream(s);
- bool t;
- ok = (stream >> t) && (stream >> std::ws).eof();
- return t;
- }
-
- template <typename ValueType>
- std::string ArgumentBase::convertToString(ValueType const& value) {
- std::ostringstream stream;
- stream << value;
- return stream.str();
- }
-
}
}
diff --git a/src/settings/ArgumentType.cpp b/src/settings/ArgumentType.cpp
new file mode 100644
index 000000000..7ab53fcf0
--- /dev/null
+++ b/src/settings/ArgumentType.cpp
@@ -0,0 +1,17 @@
+#include "src/settings/ArgumentType.h"
+
+namespace storm {
+ namespace settings {
+ std::ostream& operator<<(std::ostream& out, ArgumentType& argumentType) {
+ switch (argumentType) {
+ case ArgumentType::String: out << "string"; break;
+ case ArgumentType::Integer: out << "integer"; break;
+ case ArgumentType::UnsignedInteger: out << "unsigned integer"; break;
+ case ArgumentType::Double: out << "double"; break;
+ case ArgumentType::Boolean: out << "boolean"; break;
+ }
+
+ return out;
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/settings/ArgumentType.h b/src/settings/ArgumentType.h
index 00fa3c362..843bb10e6 100644
--- a/src/settings/ArgumentType.h
+++ b/src/settings/ArgumentType.h
@@ -15,17 +15,7 @@ namespace storm {
String, Integer, UnsignedInteger, Double, Boolean
};
- std::ostream& operator<<(std::ostream& out, ArgumentType& argumentType) {
- switch (argumentType) {
- case ArgumentType::String: out << "string"; break;
- case ArgumentType::Integer: out << "integer"; break;
- case ArgumentType::UnsignedInteger: out << "unsigned integer"; break;
- case ArgumentType::Double: out << "double"; break;
- case ArgumentType::Boolean: out << "boolean"; break;
- }
-
- return out;
- }
+ std::ostream& operator<<(std::ostream& out, ArgumentType& argumentType);
} // namespace settings
} // namespace storm
diff --git a/src/settings/ArgumentTypeInferationHelper.cpp b/src/settings/ArgumentTypeInferationHelper.cpp
index c278c7108..4cf9b1251 100644
--- a/src/settings/ArgumentTypeInferationHelper.cpp
+++ b/src/settings/ArgumentTypeInferationHelper.cpp
@@ -86,5 +86,42 @@ namespace storm {
LOG_THROW(argumentType == ArgumentType::Boolean, storm::exceptions::InternalTypeErrorException, "Unable to infer boolean from non-boolean argument.");
return value;
}
+
+ // Explicitly instantiate the templates.
+ template ArgumentType ArgumentTypeInferation::inferToEnumType<std::string>();
+ template ArgumentType ArgumentTypeInferation::inferToEnumType<int_fast64_t>();
+ template ArgumentType ArgumentTypeInferation::inferToEnumType<uint_fast64_t>();
+ template ArgumentType ArgumentTypeInferation::inferToEnumType<double>();
+ template ArgumentType ArgumentTypeInferation::inferToEnumType<bool>();
+
+ template std::string const& ArgumentTypeInferation::inferToString<std::string>(ArgumentType const& argumentType, std::string const& value);
+ template std::string const& ArgumentTypeInferation::inferToString<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
+ template std::string const& ArgumentTypeInferation::inferToString<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
+ template std::string const& ArgumentTypeInferation::inferToString<double>(ArgumentType const& argumentType, double const& value);
+ template std::string const& ArgumentTypeInferation::inferToString<bool>(ArgumentType const& argumentType, bool const& value);
+
+ template int_fast64_t ArgumentTypeInferation::inferToInteger<std::string>(ArgumentType const& argumentType, std::string const& value);
+ template int_fast64_t ArgumentTypeInferation::inferToInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
+ template int_fast64_t ArgumentTypeInferation::inferToInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
+ template int_fast64_t ArgumentTypeInferation::inferToInteger<double>(ArgumentType const& argumentType, double const& value);
+ template int_fast64_t ArgumentTypeInferation::inferToInteger<bool>(ArgumentType const& argumentType, bool const& value);
+
+ template uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<std::string>(ArgumentType const& argumentType, std::string const& value);
+ template uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
+ template uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
+ template uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<double>(ArgumentType const& argumentType, double const& value);
+ template uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<bool>(ArgumentType const& argumentType, bool const& value);
+
+ template double ArgumentTypeInferation::inferToDouble<std::string>(ArgumentType const& argumentType, std::string const& value);
+ template double ArgumentTypeInferation::inferToDouble<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
+ template double ArgumentTypeInferation::inferToDouble<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
+ template double ArgumentTypeInferation::inferToDouble<double>(ArgumentType const& argumentType, double const& value);
+ template double ArgumentTypeInferation::inferToDouble<bool>(ArgumentType const& argumentType, bool const& value);
+
+ template bool ArgumentTypeInferation::inferToBoolean<std::string>(ArgumentType const& argumentType, std::string const& value);
+ template bool ArgumentTypeInferation::inferToBoolean<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
+ template bool ArgumentTypeInferation::inferToBoolean<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
+ template bool ArgumentTypeInferation::inferToBoolean<double>(ArgumentType const& argumentType, double const& value);
+ template bool ArgumentTypeInferation::inferToBoolean<bool>(ArgumentType const& argumentType, bool const& value);
}
}
\ No newline at end of file
diff --git a/src/settings/Option.cpp b/src/settings/Option.cpp
new file mode 100644
index 000000000..384dc1c04
--- /dev/null
+++ b/src/settings/Option.cpp
@@ -0,0 +1,87 @@
+#include "src/settings/Option.h"
+
+#include <iomanip>
+
+namespace storm {
+ namespace settings {
+ uint_fast64_t Option::getPrintLength() const {
+ uint_fast64_t length = 2;
+ if (!this->getRequiresModulePrefix()) {
+ length += 2;
+ }
+ length += this->getModuleName().length() + 1;
+ length += this->getLongName().length();
+ if (this->getHasShortName()) {
+ length += 4;
+ if (!this->getRequiresModulePrefix()) {
+ length += 2;
+ }
+ length += this->getModuleName().length() + 1;
+ length += this->getShortName().length();
+ }
+ return length;
+ }
+
+ std::vector<std::shared_ptr<ArgumentBase>> const& Option::getArguments() const {
+ return this->arguments;
+ }
+
+ std::ostream& operator<<(std::ostream& out, Option const& option) {
+ std::streamsize width = out.width();
+
+ uint_fast64_t charactersPrinted = 0;
+ out << std::setw(0) << "--";
+ charactersPrinted += 2;
+ if (!option.getRequiresModulePrefix()) {
+ out << "[";
+ ++charactersPrinted;
+ }
+ out << option.getModuleName() << ":";
+ charactersPrinted += option.getModuleName().length() + 1;
+ if (!option.getRequiresModulePrefix()) {
+ out << "]";
+ ++charactersPrinted;
+ }
+ out << option.getLongName();
+ charactersPrinted += option.getLongName().length();
+ if (option.getHasShortName()) {
+ out << " | -";
+ charactersPrinted += 4;
+ if (!option.getRequiresModulePrefix()) {
+ out << "[";
+ ++charactersPrinted;
+ }
+ out << option.getModuleName() << ":";
+ charactersPrinted += option.getModuleName().length() + 1;
+ if (!option.getRequiresModulePrefix()) {
+ out << "]";
+ ++charactersPrinted;
+ }
+ out << option.getShortName();
+ charactersPrinted += option.getShortName().length();
+ }
+
+ // Now fill the width.
+ for (uint_fast64_t i = charactersPrinted; i < width; ++i) {
+ out << out.fill();
+ }
+
+ out << "\t" << option.getDescription();
+
+ if (option.getArgumentCount() > 0) {
+ // Start by determining the longest print length of the arguments.
+ uint_fast64_t maxLength = 0;
+ for (auto const& argument : option.getArguments()) {
+ maxLength = std::max(maxLength, argument->getPrintLength());
+ }
+
+ for (auto const& argument : option.getArguments()) {
+ out << std::endl;
+ out << "\t* " << std::setw(maxLength) << std::left << *argument;
+ }
+ }
+
+ return out;
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/settings/Option.h b/src/settings/Option.h
index 2c2f5912f..3345175eb 100644
--- a/src/settings/Option.h
+++ b/src/settings/Option.h
@@ -74,6 +74,7 @@ namespace storm {
* @return True iff the given argument is compatible with the current one.
*/
bool isCompatibleWith(Option const& other) {
+ std::cout << "unifying " << *this << " and " << other << std::endl;
LOG_THROW(this->getArgumentCount() == other.getArgumentCount(), storm::exceptions::OptionUnificationException, "Unable to unify two options, because their argument count differs.");
for(size_t i = 0; i != this->arguments.size(); i++) {
@@ -206,7 +207,7 @@ namespace storm {
* @return True iff the option requires the module name as a prefix.
*/
bool getRequiresModulePrefix() const {
- return this->requiresModulePrefix;
+ return this->requireModulePrefix;
}
/*!
@@ -218,6 +219,22 @@ namespace storm {
return this->hasBeenSet;
}
+ /*!
+ * Retrieves the arguments of the option.
+ *
+ * @return The arguments of the option.
+ */
+ std::vector<std::shared_ptr<ArgumentBase>> const& getArguments() const;
+
+ /*!
+ * Retrieves the (print) length of the option.
+ *
+ * @return The length of the option.
+ */
+ uint_fast64_t getPrintLength() const;
+
+ friend std::ostream& operator<<(std::ostream& out, Option const& option);
+
private:
// The long name of the option.
std::string longName;
@@ -262,7 +279,7 @@ namespace storm {
* module name.
* @param optionArguments The arguments of the option.
*/
- Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>()) : longName(longOptionName), hasShortName(hasShortOptionName), shortName(shortOptionName), description(optionDescription), moduleName(moduleName), isRequired(isOptionRequired), requireModulePrefix(requireModulePrefix), hasBeenSet(false), arguments(), argumentNameMap() {
+ Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>()) : longName(longOptionName), hasShortName(hasShortOptionName), shortName(shortOptionName), description(optionDescription), moduleName(moduleName), isRequired(isOptionRequired), requireModulePrefix(requireModulePrefix), hasBeenSet(false), arguments(optionArguments), argumentNameMap() {
// First, do some sanity checks.
LOG_THROW(!longName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty name.");
diff --git a/src/settings/OptionBuilder.h b/src/settings/OptionBuilder.h
index 0823d0e05..4217d3471 100644
--- a/src/settings/OptionBuilder.h
+++ b/src/settings/OptionBuilder.h
@@ -88,7 +88,11 @@ namespace storm {
LOG_THROW(!this->isBuild, storm::exceptions::IllegalFunctionCallException, "Cannot rebuild an option with one builder.")
this->isBuild = true;
- return std::shared_ptr<Option>(new Option(this->moduleName, this->longName, this->shortName, this->description, this->isRequired, this->requireModulePrefix, this->arguments));
+ if (this->hasShortName) {
+ return std::shared_ptr<Option>(new Option(this->moduleName, this->longName, this->shortName, this->description, this->isRequired, this->requireModulePrefix, this->arguments));
+ } else {
+ return std::shared_ptr<Option>(new Option(this->moduleName, this->longName, this->description, this->isRequired, this->requireModulePrefix, this->arguments));
+ }
}
private:
diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index 525cefc29..e36f61d06 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -3,7 +3,9 @@
#include <cstring>
#include <cctype>
#include <mutex>
+#include <iomanip>
#include <boost/algorithm/string.hpp>
+#include <boost/io/ios_state.hpp>
#include "src/exceptions/IllegalFunctionCallException.h"
#include "src/exceptions/OptionParserException.h"
@@ -44,6 +46,9 @@ namespace storm {
}
void SettingsManager::setFromString(std::string const& commandLineString) {
+ if (commandLineString.empty()) {
+ return;
+ }
std::vector<std::string> argumentVector;
boost::split(argumentVector, commandLineString, boost::is_any_of("\t "));
this->setFromExplodedString(argumentVector);
@@ -57,15 +62,21 @@ namespace storm {
std::vector<std::string> argumentCache;
// Walk through all arguments.
+ std::cout << "before... "<< std::endl;
for (uint_fast64_t i = 0; i < commandLineArguments.size(); ++i) {
+ std::cout << "in ... " << i << std::endl;
bool existsNextArgument = i < commandLineArguments.size() - 1;
std::string const& currentArgument = commandLineArguments[i];
// Check if the given argument is a new option or belongs to a previously given option.
if (currentArgument.at(0) == '-') {
- // At this point we know that a new option is about to come. Hence, we need to assign the current
- // cache content to the option that was active until now.
- setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->longNameToOptions : this->shortNameToOptions, argumentCache);
+ if (optionActive) {
+ // At this point we know that a new option is about to come. Hence, we need to assign the current
+ // cache content to the option that was active until now.
+ setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->shortNameToOptions : this->longNameToOptions, argumentCache);
+ } else {
+ optionActive = true;
+ }
if (currentArgument.at(1) == '-') {
// In this case, the argument has to be the long name of an option. Try to get all options that
@@ -91,6 +102,11 @@ namespace storm {
LOG_THROW(false, storm::exceptions::OptionParserException, "Found stray argument '" << currentArgument << "' that is not preceeded by a matching option.");
}
}
+
+ // If an option is still active at this point, we need to set it.
+ if (optionActive) {
+ setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->shortNameToOptions : this->longNameToOptions, argumentCache);
+ }
}
void SettingsManager::setFromConfigurationFile(std::string const& configFilename) {
@@ -98,15 +114,67 @@ namespace storm {
}
void SettingsManager::printHelp(std::string const& moduleName) const {
- LOG_ASSERT(false, "Not yet implemented");
+ std::cout << "usage: storm [options]" << std::endl << std::endl;
+
+ if (moduleName == "all") {
+ // Find longest option name.
+ uint_fast64_t maxLength = getPrintLengthOfLongestOption();
+ for (auto const& moduleName : this->moduleNames) {
+ printHelpForModule(moduleName, maxLength);
+ }
+ } else {
+ uint_fast64_t maxLength = getPrintLengthOfLongestOption(moduleName);
+ printHelpForModule(moduleName, maxLength);
+ }
+ }
+
+ void SettingsManager::printHelpForModule(std::string const& moduleName, uint_fast64_t maxLength) const {
+ auto moduleIterator = moduleOptions.find(moduleName);
+ LOG_THROW(moduleIterator != moduleOptions.end(), storm::exceptions::IllegalFunctionCallException, "Cannot print help for unknown module '" << moduleName << "'.");
+ std::cout << "##### Module '" << moduleName << "' ";
+ for (uint_fast64_t i = 0; i < std::min(maxLength, maxLength - moduleName.length() - 16); ++i) {
+ std::cout << "#";
+ }
+ std::cout << std::endl;
+
+ // Save the flags for std::cout so we can manipulate them and be sure they will be restored as soon as this
+ // stream goes out of scope.
+ boost::io::ios_flags_saver out(std::cout);
+
+ for (auto const& option : moduleIterator->second) {
+ std::cout << std::setw(maxLength) << std::left << *option << std::endl;
+ }
+ std::cout << std::endl;
+ }
+
+ uint_fast64_t SettingsManager::getPrintLengthOfLongestOption() const {
+ uint_fast64_t length = 0;
+ for (auto const& moduleName : this->moduleNames) {
+ length = std::max(getPrintLengthOfLongestOption(moduleName), length);
+ }
+ return length;
+ }
+
+ uint_fast64_t SettingsManager::getPrintLengthOfLongestOption(std::string const& moduleName) const {
+ auto moduleIterator = modules.find(moduleName);
+ LOG_THROW(moduleIterator != modules.end(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve option length of unknown module '" << moduleName << "'.");
+ return moduleIterator->second->getPrintLengthOfLongestOption();
}
void SettingsManager::addModule(std::unique_ptr<modules::ModuleSettings>&& moduleSettings) {
auto moduleIterator = this->modules.find(moduleSettings->getModuleName());
LOG_THROW(moduleIterator == this->modules.end(), storm::exceptions::IllegalFunctionCallException, "Unable to register module '" << moduleSettings->getModuleName() << "' because a module with the same name already exists.");
+
+ // Take over the module settings object.
+ std::string const& moduleName = moduleSettings->getModuleName();
+ this->moduleNames.push_back(moduleName);
this->modules.emplace(moduleSettings->getModuleName(), std::move(moduleSettings));
+ auto iterator = this->modules.find(moduleName);
+ std::unique_ptr<modules::ModuleSettings> const& settings = iterator->second;
- for (auto const& option : moduleSettings->getOptions()) {
+ // Now register the options of the module.
+ this->moduleOptions.emplace(moduleName, std::vector<std::shared_ptr<Option>>());
+ for (auto const& option : settings->getOptions()) {
this->addOption(option);
}
}
@@ -123,20 +191,32 @@ namespace storm {
if (!option->getRequiresModulePrefix()) {
bool isCompatible = this->isCompatible(option, option->getLongName(), this->longNameToOptions);
LOG_THROW(isCompatible, storm::exceptions::IllegalFunctionCallException, "Unable to add option '" << option->getLongName() << "', because an option with the same name is incompatible with it.");
- this->longNameToOptions.emplace(option->getLongName(), option);
+ addOptionToMap(option->getLongName(), option, this->longNameToOptions);
}
// For the prefixed name, we don't need a compatibility check, because a module is not allowed to register the same option twice.
- this->longNameToOptions.emplace(option->getModuleName() + ":" + option->getLongName(), option);
+ addOptionToMap(option->getModuleName() + ":" + option->getLongName(), option, this->longNameToOptions);
if (option->getHasShortName()) {
if (!option->getRequiresModulePrefix()) {
- this->shortNameToOptions.emplace(option->getShortName(), option);
bool isCompatible = this->isCompatible(option, option->getShortName(), this->shortNameToOptions);
LOG_THROW(isCompatible, storm::exceptions::IllegalFunctionCallException, "Unable to add option '" << option->getLongName() << "', because an option with the same name is incompatible with it.");
+ addOptionToMap(option->getShortName(), option, this->shortNameToOptions);
}
- this->shortNameToOptions.emplace(option->getModuleName() + ":" + option->getShortName(), option);
+ addOptionToMap(option->getModuleName() + ":" + option->getShortName(), option, this->shortNameToOptions);
}
}
+
+ modules::ModuleSettings const& SettingsManager::getModule(std::string const& moduleName) const {
+ auto moduleIterator = this->modules.find(moduleName);
+ LOG_THROW(moduleIterator != this->modules.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown module '" << moduleName << "'.");
+ return *moduleIterator->second;
+ }
+
+ modules::ModuleSettings& SettingsManager::getModule(std::string const& moduleName) {
+ auto moduleIterator = this->modules.find(moduleName);
+ LOG_THROW(moduleIterator != this->modules.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown module '" << moduleName << "'.");
+ return *moduleIterator->second;
+ }
bool SettingsManager::isCompatible(std::shared_ptr<Option> const& option, std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap) {
auto optionIterator = optionMap.find(optionName);
@@ -174,5 +254,59 @@ namespace storm {
}
}
+ void SettingsManager::addOptionToMap(std::string const& name, std::shared_ptr<Option> const& option, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>>& optionMap) {
+ auto optionIterator = optionMap.find(name);
+ if (optionIterator == optionMap.end()) {
+ std::vector<std::shared_ptr<Option>> optionVector;
+ optionVector.push_back(option);
+ optionMap.emplace(name, optionVector);
+ } else {
+ optionIterator->second.push_back(option);
+ }
+ }
+
+ SettingsManager const& manager() {
+ return SettingsManager::manager();
+ }
+
+ SettingsManager& mutableManager() {
+ return SettingsManager::manager();
+ }
+
+ storm::settings::modules::GeneralSettings const& generalSettings() {
+ return dynamic_cast<storm::settings::modules::GeneralSettings const&>(manager().getModule(storm::settings::modules::GeneralSettings::moduleName));
+ }
+
+ storm::settings::modules::GeneralSettings& mutableGeneralSettings() {
+ return dynamic_cast<storm::settings::modules::GeneralSettings&>(storm::settings::SettingsManager::manager().getModule(storm::settings::modules::GeneralSettings::moduleName));
+ }
+
+ storm::settings::modules::DebugSettings const& debugSettings() {
+ return dynamic_cast<storm::settings::modules::DebugSettings const&>(manager().getModule(storm::settings::modules::DebugSettings::moduleName));
+ }
+
+ storm::settings::modules::CounterexampleGeneratorSettings const& counterexampleGeneratorSettings() {
+ return dynamic_cast<storm::settings::modules::CounterexampleGeneratorSettings const&>(manager().getModule(storm::settings::modules::CounterexampleGeneratorSettings::moduleName));
+ }
+
+ storm::settings::modules::CuddSettings const& cuddSettings() {
+ return dynamic_cast<storm::settings::modules::CuddSettings const&>(manager().getModule(storm::settings::modules::CuddSettings::moduleName));
+ }
+
+ storm::settings::modules::GmmxxEquationSolverSettings const& gmmxxEquationSolverSettings() {
+ return dynamic_cast<storm::settings::modules::GmmxxEquationSolverSettings const&>(manager().getModule(storm::settings::modules::GmmxxEquationSolverSettings::moduleName));
+ }
+
+ storm::settings::modules::NativeEquationSolverSettings const& nativeEquationSolverSettings() {
+ return dynamic_cast<storm::settings::modules::NativeEquationSolverSettings const&>(manager().getModule(storm::settings::modules::NativeEquationSolverSettings::moduleName));
+ }
+
+ storm::settings::modules::GlpkSettings const& glpkSettings() {
+ return dynamic_cast<storm::settings::modules::GlpkSettings const&>(manager().getModule(storm::settings::modules::GlpkSettings::moduleName));
+ }
+
+ storm::settings::modules::GurobiSettings const& gurobiSettings() {
+ return dynamic_cast<storm::settings::modules::GurobiSettings const&>(manager().getModule(storm::settings::modules::GurobiSettings::moduleName));
+ }
}
}
\ No newline at end of file
diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h
index 40421019a..def33aadf 100644
--- a/src/settings/SettingsManager.h
+++ b/src/settings/SettingsManager.h
@@ -79,11 +79,19 @@ namespace storm {
* 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
+ * @param 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;
+ /*!
+ * This function prints a help message for the specified module to the standard output.
+ *
+ * @param moduleName The name of the module for which to show the help.
+ * @param maxLength The maximal length of an option name (necessary for proper alignment).
+ */
+ void printHelpForModule(std::string const& moduleName, uint_fast64_t maxLength = 30) const;
+
/*!
* Retrieves the only existing instance of a settings manager.
*
@@ -106,6 +114,14 @@ namespace storm {
* @return An object that provides access to the settings of the module.
*/
modules::ModuleSettings const& getModule(std::string const& moduleName) const;
+
+ /*!
+ * Retrieves the settings of the module with the given name.
+ *
+ * @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.
+ */
+ modules::ModuleSettings& getModule(std::string const& moduleName);
private:
/*!
@@ -120,6 +136,7 @@ namespace storm {
virtual ~SettingsManager();
// The registered modules.
+ std::vector<std::string> moduleNames;
std::unordered_map<std::string, std::unique_ptr<modules::ModuleSettings>> modules;
// Mappings from all known option names to the options that match it. All options for one option name need
@@ -150,6 +167,30 @@ namespace storm {
* Checks whether the given option is compatible with all options with the given name in the given mapping.
*/
static bool isCompatible(std::shared_ptr<Option> const& option, std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap);
+
+ /*!
+ * Inserts the given option to the options with the given name in the given map.
+ *
+ * @param name The name of the option.
+ * @param option The option to add.
+ * @param optionMap The map into which the option is to be inserted.
+ */
+ static void addOptionToMap(std::string const& name, std::shared_ptr<Option> const& option, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>>& optionMap);
+
+ /*!
+ * Retrieves the (print) length of the longest option of all modules.
+ *
+ * @return The length of the longest option.
+ */
+ uint_fast64_t getPrintLengthOfLongestOption() const;
+
+ /*!
+ * Retrieves the (print) length of the longest option in the given module, so we can align the options.
+ *
+ * @param moduleName The module name for which to retrieve the length of the longest option.
+ * @return The length of the longest option name.
+ */
+ uint_fast64_t getPrintLengthOfLongestOption(std::string const& moduleName) const;
};
/*!
@@ -157,81 +198,78 @@ namespace storm {
*
* @return The only settings manager.
*/
- SettingsManager& manager() {
- return SettingsManager::manager();
- }
+ SettingsManager const& manager();
+
+ /*!
+ * Retrieves the settings manager.
+ *
+ * @return The only settings manager.
+ */
+ SettingsManager& mutableManager();
/*!
* 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));
- }
+ storm::settings::modules::GeneralSettings const& generalSettings();
+
+ /*!
+ * Retrieves the general settings in a mutable form. This is only meant to be used for debug purposes or very
+ * rare cases where it is necessary.
+ *
+ * @return An object that allows accessing and modifying the general settings.
+ */
+ storm::settings::modules::GeneralSettings& mutableGeneralSettings();
/*!
* 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));
- }
+ storm::settings::modules::DebugSettings const& debugSettings();
/*!
* 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));
- }
+ storm::settings::modules::CounterexampleGeneratorSettings const& counterexampleGeneratorSettings();
/*!
* 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));
- }
+ storm::settings::modules::CuddSettings const& cuddSettings();
/*!
* 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));
- }
+ storm::settings::modules::GmmxxEquationSolverSettings const& gmmxxEquationSolverSettings();
/*!
* 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));
- }
+ storm::settings::modules::NativeEquationSolverSettings const& nativeEquationSolverSettings();
/*!
* 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));
- }
+ storm::settings::modules::GlpkSettings const& glpkSettings();
/*!
* 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));
- }
+ storm::settings::modules::GurobiSettings const& gurobiSettings();
} // namespace settings
} // namespace storm
diff --git a/src/settings/modules/CuddSettings.cpp b/src/settings/modules/CuddSettings.cpp
index f9eb09699..6404b77ac 100644
--- a/src/settings/modules/CuddSettings.cpp
+++ b/src/settings/modules/CuddSettings.cpp
@@ -6,10 +6,10 @@ namespace storm {
namespace settings {
namespace modules {
- const std::string moduleName = "cudd";
- const std::string precisionOptionName = "precision";
- const std::string maximalMemoryOptionName = "maxmem";
- const std::string reorderOptionName = "reorder";
+ const std::string CuddSettings::moduleName = "cudd";
+ const std::string CuddSettings::precisionOptionName = "precision";
+ const std::string CuddSettings::maximalMemoryOptionName = "maxmem";
+ const std::string CuddSettings::reorderOptionName = "reorder";
CuddSettings::CuddSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
this->addOption(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());
diff --git a/src/settings/modules/DebugSettings.cpp b/src/settings/modules/DebugSettings.cpp
index 946667732..e0236d2ea 100644
--- a/src/settings/modules/DebugSettings.cpp
+++ b/src/settings/modules/DebugSettings.cpp
@@ -16,7 +16,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Print debug output.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, traceOptionName, false, "Print even more debug output.").build());
this->addOption(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());
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to write the log.").build()).build());
}
bool DebugSettings::isDebugSet() const {
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index 0ba8cf70a..34f6049aa 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -1,6 +1,7 @@
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/SettingsManager.h"
+#include "src/settings/SettingMemento.h"
namespace storm {
namespace settings {
@@ -183,6 +184,10 @@ namespace storm {
return this->getOption(fixDeadlockOptionName).getHasOptionBeenSet();
}
+ std::unique_ptr<storm::settings::SettingMemento> GeneralSettings::overrideFixDeadlocksSet(bool stateToSet) {
+ return this->overrideOption(fixDeadlockOptionName, stateToSet);
+ }
+
bool GeneralSettings::isTimeoutSet() const {
return this->getOption(timeoutOptionName).getHasOptionBeenSet();
}
@@ -208,7 +213,7 @@ namespace storm {
} else if (lpSolverName == "glpk") {
return GeneralSettings::LpSolver::glpk;
}
- LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << equationSolverName << "'.");
+ LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'.");
}
bool GeneralSettings::isConstantsSet() const {
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index 504114d48..472668188 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/src/settings/modules/GeneralSettings.h
@@ -214,6 +214,15 @@ namespace storm {
*/
bool isFixDeadlocksSet() const;
+ /*!
+ * Overrides the option to fix deadlocks by setting it to the specified value. As soon as the returned
+ * memento goes out of scope, the original value is restored.
+ *
+ * @param stateToSet The value that is to be set for the fix-deadlocks option.
+ * @return The memento that will eventually restore the original value.
+ */
+ std::unique_ptr<storm::settings::SettingMemento> overrideFixDeadlocksSet(bool stateToSet);
+
/*!
* Retrieves whether the timeout option was set.
*
@@ -288,7 +297,6 @@ namespace storm {
static const std::string lpSolverOptionName;
static const std::string constantsOptionName;
static const std::string constantsOptionShortName;
-
};
} // namespace modules
diff --git a/src/settings/modules/GlpkSettings.cpp b/src/settings/modules/GlpkSettings.cpp
index 9534fc4e3..c45eb93a5 100644
--- a/src/settings/modules/GlpkSettings.cpp
+++ b/src/settings/modules/GlpkSettings.cpp
@@ -11,8 +11,16 @@ namespace storm {
const std::string GlpkSettings::outputOptionName = "output";
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());
+ this->addOption(storm::settings::OptionBuilder(moduleName, outputOptionName, true, "If set, the glpk output will be printed to the command line.").build());
+ this->addOption(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());
+ }
+
+ bool GlpkSettings::isOutputSet() const {
+ return this->getOption(outputOptionName).getHasOptionBeenSet();
+ }
+
+ double GlpkSettings::getIntegerTolerance() const {
+ return this->getOption(integerToleranceOption).getArgumentByName("value").getValueAsDouble();
}
} // namespace modules
diff --git a/src/settings/modules/GmmxxEquationSolverSettings.cpp b/src/settings/modules/GmmxxEquationSolverSettings.cpp
index 2658fd0e2..fb940ff50 100644
--- a/src/settings/modules/GmmxxEquationSolverSettings.cpp
+++ b/src/settings/modules/GmmxxEquationSolverSettings.cpp
@@ -17,19 +17,61 @@ namespace storm {
GmmxxEquationSolverSettings::GmmxxEquationSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
std::vector<std::string> methods = {"bicgstab", "qmr", "gmres", "jacobi"};
- 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());
+ this->addOption(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"};
- 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());
+ std::vector<std::string> preconditioner = {"ilu", "diagonal", "none"};
+ this->addOption(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, 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->addOption(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, 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->addOption(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, 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->addOption(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, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
+ }
+
+ GmmxxEquationSolverSettings::LinearEquationTechnique GmmxxEquationSolverSettings::getLinearEquationSystemTechnique() const {
+ std::string linearEquationSystemTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
+ if (linearEquationSystemTechniqueAsString == "bicgstab") {
+ return GmmxxEquationSolverSettings::LinearEquationTechnique::Bicgstab;
+ } else if (linearEquationSystemTechniqueAsString == "qmr") {
+ return GmmxxEquationSolverSettings::LinearEquationTechnique::Qmr;
+ } else if (linearEquationSystemTechniqueAsString == "gmres") {
+ return GmmxxEquationSolverSettings::LinearEquationTechnique::Gmres;
+ } else if (linearEquationSystemTechniqueAsString == "jacobi") {
+ return GmmxxEquationSolverSettings::LinearEquationTechnique::Jacobi;
+ }
+ LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
+ }
+
+ GmmxxEquationSolverSettings::PreconditioningTechnique GmmxxEquationSolverSettings::getPreconditioningTechnique() const {
+ std::string preconditioningTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
+ if (preconditioningTechniqueAsString == "ilu") {
+ return GmmxxEquationSolverSettings::PreconditioningTechnique::Ilu;
+ } else if (preconditioningTechniqueAsString == "diagonal") {
+ return GmmxxEquationSolverSettings::PreconditioningTechnique::Diagonal;
+ } else if (preconditioningTechniqueAsString == "none") {
+ return GmmxxEquationSolverSettings::PreconditioningTechnique::None;
+ }
+ LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown preconditioning technique '" << preconditioningTechniqueAsString << "' selected.");
+ }
+
+ uint_fast64_t GmmxxEquationSolverSettings::getRestartIterationCount() const {
+ return this->getOption(restartOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
+ }
+
+ uint_fast64_t GmmxxEquationSolverSettings::getMaximalIterationCount() const {
+ return this->getOption(maximalIterationsOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
+ }
+
+ double GmmxxEquationSolverSettings::getPrecision() const {
+ return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
+ }
+
+ GmmxxEquationSolverSettings::ConvergenceCriterion GmmxxEquationSolverSettings::getConvergenceCriterion() const {
+ return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? GmmxxEquationSolverSettings::ConvergenceCriterion::Absolute : GmmxxEquationSolverSettings::ConvergenceCriterion::Relative;
}
} // namespace modules
diff --git a/src/settings/modules/GurobiSettings.cpp b/src/settings/modules/GurobiSettings.cpp
index be78a59ee..1038fce26 100644
--- a/src/settings/modules/GurobiSettings.cpp
+++ b/src/settings/modules/GurobiSettings.cpp
@@ -12,11 +12,23 @@ namespace storm {
const std::string GurobiSettings::outputOption = "output";
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());
+ this->addOption(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());
- this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, outputOption, true, "If set, the Gurobi output will be printed to the command line.").build());
+ this->addOption(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, 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());
+ this->addOption(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());
+ }
+
+ double GurobiSettings::getIntegerTolerance() const {
+ return this->getOption(integerToleranceOption).getArgumentByName("value").getValueAsDouble();
+ }
+
+ uint_fast64_t GurobiSettings::getNumberOfThreads() const {
+ return this->getOption(threadsOption).getArgumentByName("count").getValueAsUnsignedInteger();
+ }
+
+ bool GurobiSettings::isOutputSet() const {
+ return this->getOption(outputOption).getHasOptionBeenSet();
}
} // namespace modules
diff --git a/src/settings/modules/ModuleSettings.cpp b/src/settings/modules/ModuleSettings.cpp
index 782a58fa7..fbdad7b93 100644
--- a/src/settings/modules/ModuleSettings.cpp
+++ b/src/settings/modules/ModuleSettings.cpp
@@ -1,5 +1,8 @@
#include "src/settings/modules/ModuleSettings.h"
+#include "src/settings/SettingMemento.h"
+#include "src/exceptions/InvalidStateException.h"
+
namespace storm {
namespace settings {
namespace modules {
@@ -24,29 +27,55 @@ namespace storm {
return this->getOption(name).setHasOptionBeenSet(false);
}
- std::vector<std::shared_ptr<Option>> ModuleSettings::getOptions() const {
- std::vector<std::shared_ptr<Option>> result;
- result.reserve(this->options.size());
-
- for (auto const& option : this->options) {
- result.push_back(option.second);
- }
-
- return result;
+ std::vector<std::shared_ptr<Option>> const& ModuleSettings::getOptions() const {
+ return this->options;
}
Option const& ModuleSettings::getOption(std::string const& longName) const {
- auto optionIterator = this->options.find(longName);
- LOG_THROW(optionIterator != this->options.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'.");
+ auto optionIterator = this->optionMap.find(longName);
+ LOG_THROW(optionIterator != this->optionMap.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'.");
return *optionIterator->second;
}
Option& ModuleSettings::getOption(std::string const& longName) {
- auto optionIterator = this->options.find(longName);
- LOG_THROW(optionIterator != this->options.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'.");
+ auto optionIterator = this->optionMap.find(longName);
+ LOG_THROW(optionIterator != this->optionMap.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'.");
return *optionIterator->second;
}
+ std::string const& ModuleSettings::getModuleName() const {
+ return this->moduleName;
+ }
+
+ std::unique_ptr<storm::settings::SettingMemento> ModuleSettings::overrideOption(std::string const& name, bool requiredStatus) {
+ bool currentStatus = this->isSet(name);
+ if (currentStatus) {
+ this->unset(name);
+ } else {
+ this->set(name);
+ }
+ return std::unique_ptr<storm::settings::SettingMemento>(new storm::settings::SettingMemento(*this, name, currentStatus));
+ }
+
+ bool ModuleSettings::isSet(std::string const& optionName) const {
+ return this->getOption(optionName).getHasOptionBeenSet();
+ }
+
+ void ModuleSettings::addOption(std::shared_ptr<Option> const& option) {
+ auto optionIterator = this->optionMap.find(option->getLongName());
+ LOG_THROW(optionIterator == this->optionMap.end(), storm::exceptions::IllegalFunctionCallException, "Unable to register the option '" << option->getLongName() << "' in module '" << this->getModuleName() << "', because an option with this name already exists.");
+ this->optionMap.emplace(option->getLongName(), option);
+ this->options.push_back(option);
+ }
+
+ uint_fast64_t ModuleSettings::getPrintLengthOfLongestOption() const {
+ uint_fast64_t length = 0;
+ for (auto const& option : this->options) {
+ length = std::max(length, option->getPrintLength());
+ }
+ return length;
+ }
+
} // namespace modules
} // namespace settings
} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/ModuleSettings.h b/src/settings/modules/ModuleSettings.h
index ec3c1231b..383174647 100644
--- a/src/settings/modules/ModuleSettings.h
+++ b/src/settings/modules/ModuleSettings.h
@@ -60,7 +60,14 @@ namespace storm {
*
* @return A list of options of this module.
*/
- std::vector<std::shared_ptr<Option>> getOptions() const;
+ std::vector<std::shared_ptr<Option>> const& getOptions() const;
+
+ /*!
+ * Retrieves the (print) length of the longest option.
+ *
+ * @return The length of the longest option.
+ */
+ uint_fast64_t getPrintLengthOfLongestOption() const;
protected:
/*!
@@ -115,7 +122,7 @@ namespace storm {
*
* @param option The option to add and register.
*/
- void addOption(std::shared_ptr<Option> option) const;
+ void addOption(std::shared_ptr<Option> const& option);
private:
// The settings manager responsible for the settings.
@@ -125,7 +132,10 @@ namespace storm {
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;
+ std::unordered_map<std::string, std::shared_ptr<Option>> optionMap;
+
+ // The list of known option names in the order they were registered.
+ std::vector<std::shared_ptr<Option>> options;
};
} // namespace modules
diff --git a/src/settings/modules/NativeEquationSolverSettings.cpp b/src/settings/modules/NativeEquationSolverSettings.cpp
index ddf50650b..2749ccbec 100644
--- a/src/settings/modules/NativeEquationSolverSettings.cpp
+++ b/src/settings/modules/NativeEquationSolverSettings.cpp
@@ -15,13 +15,33 @@ namespace storm {
NativeEquationSolverSettings::NativeEquationSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
std::vector<std::string> methods = { "jacobi" };
- 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());
+ this->addOption(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, 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->addOption(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, 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->addOption(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, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
+ }
+
+ NativeEquationSolverSettings::LinearEquationTechnique NativeEquationSolverSettings::getLinearEquationSystemTechnique() const {
+ std::string linearEquationSystemTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
+ if (linearEquationSystemTechniqueAsString == "jacobi") {
+ return NativeEquationSolverSettings::LinearEquationTechnique::Jacobi;
+ }
+ LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
+ }
+
+ uint_fast64_t NativeEquationSolverSettings::getMaximalIterationCount() const {
+ return this->getOption(maximalIterationsOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
+ }
+
+ double NativeEquationSolverSettings::getPrecision() const {
+ return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
+ }
+
+ NativeEquationSolverSettings::ConvergenceCriterion NativeEquationSolverSettings::getConvergenceCriterion() const {
+ return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? NativeEquationSolverSettings::ConvergenceCriterion::Absolute : NativeEquationSolverSettings::ConvergenceCriterion::Relative;
}
} // namespace modules
diff --git a/src/settings/modules/NativeEquationSolverSettings.h b/src/settings/modules/NativeEquationSolverSettings.h
index 04b58822a..826d40941 100644
--- a/src/settings/modules/NativeEquationSolverSettings.h
+++ b/src/settings/modules/NativeEquationSolverSettings.h
@@ -18,6 +18,11 @@ namespace storm {
// An enumeration of all available convergence criteria.
enum class ConvergenceCriterion { Absolute, Relative };
+ /*!
+ * Creates a new set of native equation solver settings that is managed by the given manager.
+ *
+ * @param settingsManager The responsible manager.
+ */
NativeEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
/*!
diff --git a/src/storm.cpp b/src/storm.cpp
index eafdb78c8..502e28c93 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -245,7 +245,7 @@ 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 = storm::settings::counterexampleGeneratorSettings().useMilpBasedMinimalCommandSetGeneration();
+ bool useMILP = storm::settings::counterexampleGeneratorSettings().isUseMilpBasedMinimalCommandSetGenerationSet();
// MinCMD Time Measurement, Start
std::chrono::high_resolution_clock::time_point minCmdStart = std::chrono::high_resolution_clock::now();
diff --git a/src/utility/CLI.h b/src/utility/CLI.h
index d70c89f57..a94caa94a 100644
--- a/src/utility/CLI.h
+++ b/src/utility/CLI.h
@@ -127,7 +127,7 @@ 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& manager = storm::settings::manager();
+ storm::settings::SettingsManager& manager = storm::settings::mutableManager();
try {
manager.setFromCommandLine(argc, argv);
} catch (storm::exceptions::OptionParserException& e) {
@@ -138,7 +138,7 @@ bool parseOptions(const int argc, const char* argv[]) {
}
if (storm::settings::generalSettings().isHelpSet()) {
- storm::settings::manager().printHelp();
+ storm::settings::manager().printHelp(storm::settings::generalSettings().getHelpModuleName());
return false;
}
diff --git a/test/functional/modelchecker/ActionTest.cpp b/test/functional/modelchecker/ActionTest.cpp
index d96452187..75fa37106 100644
--- a/test/functional/modelchecker/ActionTest.cpp
+++ b/test/functional/modelchecker/ActionTest.cpp
@@ -27,7 +27,7 @@ TEST(ActionTest, BoundActionFunctionality) {
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
- storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@@ -112,7 +112,7 @@ TEST(ActionTest, BoundActionSafety) {
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
- storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@@ -173,7 +173,7 @@ TEST(ActionTest, FormulaActionFunctionality) {
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
- storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@@ -245,7 +245,7 @@ TEST(ActionTest, FormulaActionFunctionality) {
TEST(ActionTest, FormulaActionSafety){
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
- storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@@ -278,7 +278,7 @@ TEST(ActionTest, FormulaActionSafety){
TEST(ActionTest, InvertActionFunctionality){
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
- storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@@ -312,7 +312,7 @@ TEST(ActionTest, InvertActionFunctionality){
TEST(ActionTest, RangeActionFunctionality){
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
- storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@@ -394,7 +394,7 @@ TEST(ActionTest, RangeActionFunctionality){
TEST(ActionTest, RangeActionSafety){
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
- storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@@ -434,7 +434,7 @@ TEST(ActionTest, RangeActionSafety){
TEST(ActionTest, SortActionFunctionality){
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
- storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@@ -547,7 +547,7 @@ TEST(ActionTest, SortActionSafety){
// Check that the path result has priority over the state result if for some erronous reason both are given.
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
- storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
diff --git a/test/functional/modelchecker/FilterTest.cpp b/test/functional/modelchecker/FilterTest.cpp
index 5dccda193..3d460cbd3 100644
--- a/test/functional/modelchecker/FilterTest.cpp
+++ b/test/functional/modelchecker/FilterTest.cpp
@@ -30,7 +30,7 @@ TEST(PrctlFilterTest, generalFunctionality) {
// Setup model and modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
- storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Find the best valued state to finally reach a 'b' state.
std::string input = "filter[sort(value, descending); range(0,0)](F b)";
@@ -148,7 +148,7 @@ TEST(PrctlFilterTest, generalFunctionality) {
TEST(PrctlFilterTest, Safety) {
// Setup model and modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
- storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Make a stub formula as child.
auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("a");
diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
index a673994d5..a1caceb80 100644
--- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
@@ -4,13 +4,11 @@
#include "src/solver/GmmxxLinearEquationSolver.h"
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "src/settings/SettingsManager.h"
-#include "src/settings/InternalOptionMemento.h"
+#include "src/settings/SettingMemento.h"
#include "src/parser/AutoParser.h"
TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
- storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
- storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true);
- ASSERT_TRUE(s->isSet("fixDeadlocks"));
+ std::unique_ptr<storm::settings::SettingMemento> deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
@@ -20,41 +18,39 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
- storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("one");
auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
std::vector<double> result = eventuallyFormula->check(mc, false);
- ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("two");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
result = eventuallyFormula->check(mc, false);
- ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("three");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
result = eventuallyFormula->check(mc, false);
- ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
auto done = std::make_shared<storm::properties::prctl::Ap<double>>("done");
auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(done);
result = reachabilityRewardFormula->check(mc, false);
- ASSERT_LT(std::abs(result[0] - ((double)11/3)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - ((double)11/3)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
- storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
- storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true);
- ASSERT_TRUE(s->isSet("fixDeadlocks"));
+ std::unique_ptr<storm::settings::SettingMemento> deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", "");
ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
@@ -64,34 +60,32 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(8607ull, dtmc->getNumberOfStates());
ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions());
- storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observe0Greater1");
auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
std::vector<double> result = eventuallyFormula->check(mc, false);
- ASSERT_LT(std::abs(result[0] - 0.3328800375801578281), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.3328800375801578281), storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeIGreater1");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
result = eventuallyFormula->check(mc, false);
- ASSERT_LT(std::abs(result[0] - 0.1522194965), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.1522194965), storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeOnlyTrueSender");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
result = eventuallyFormula->check(mc, false);
- ASSERT_LT(std::abs(result[0] - 0.32153724292835045), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.32153724292835045), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
- storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
- storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true);
- ASSERT_TRUE(s->isSet("fixDeadlocks"));
+ std::unique_ptr<storm::settings::SettingMemento> deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
@@ -100,26 +94,26 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(12400ull, dtmc->getNumberOfStates());
ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions());
- storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
std::vector<double> result = eventuallyFormula->check(mc, false);
- ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto boundedUntilFormula = std::make_shared<storm::properties::prctl::BoundedUntil<double>>(std::make_shared<storm::properties::prctl::Ap<double>>("true"), apFormula, 20);
result = boundedUntilFormula->check(mc, false);
- ASSERT_LT(std::abs(result[0] - 0.9999965911265462636), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.9999965911265462636), storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
result = reachabilityRewardFormula->check(mc, false);
- ASSERT_LT(std::abs(result[0] - 1.044879046), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1.044879046), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
index be1ef8674..106502b8f 100644
--- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
@@ -7,7 +7,6 @@
#include "src/parser/AutoParser.h"
TEST(SparseMdpPrctlModelCheckerTest, Dice) {
- storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
@@ -24,44 +23,44 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
- ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*eventuallyFormula, false);
- ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("three");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
result = mc.checkOptimizingOperator(*eventuallyFormula, true);
- ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*eventuallyFormula, false);
- ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("four");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
result = mc.checkOptimizingOperator(*eventuallyFormula, true);
- ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*eventuallyFormula, false);
- ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("done");
auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
- ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
- ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision());
abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "");
@@ -76,11 +75,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = stateRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, true);
- ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision());
result = stateRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, false);
- ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision());
abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
@@ -95,15 +94,14 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = stateAndTransitionRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, true);
- ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 14.666658998), storm::settings::nativeEquationSolverSettings().getPrecision());
result = stateAndTransitionRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, false);
- ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 14.666658998), storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
- storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew");
ASSERT_EQ(storm::models::MDP, abstractModel->getType());
@@ -120,31 +118,31 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
- ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*eventuallyFormula, false);
- ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto boundedEventuallyFormula = std::make_shared<storm::properties::prctl::BoundedEventually<double>>(apFormula, 25);
result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true);
- ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0625), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false);
- ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0625), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
- ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 4.285689611), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
- ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 4.285689611), storm::settings::nativeEquationSolverSettings().getPrecision());
}
diff --git a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp
index 89c5c9c6e..f7e83a01d 100644
--- a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp
+++ b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp
@@ -10,7 +10,7 @@
#include "src/parser/DeterministicSparseTransitionParser.h"
#include "src/storage/SparseMatrix.h"
-#include "src/settings/InternalOptionMemento.h"
+#include "src/settings/SettingMemento.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFormatException.h"
@@ -192,7 +192,7 @@ TEST(DeterministicSparseTransitionParserTest, MixedTransitionOrder) {
TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) {
// Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed.
- storm::settings::InternalOptionMemento setDeadlockOption("fixDeadlocks", true);
+ std::unique_ptr<storm::settings::SettingMemento> setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
// Parse a transitions file with the fixDeadlocks Flag set and test if it works.
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra");
@@ -217,7 +217,7 @@ TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) {
TEST(DeterministicSparseTransitionParserTest, DontFixDeadlocks) {
// Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception.
- storm::settings::InternalOptionMemento unsetDeadlockOption("fixDeadlocks", false);
+ std::unique_ptr<storm::settings::SettingMemento> unsetDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(false);
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra"), storm::exceptions::WrongFormatException);
}
diff --git a/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp
index 0d1dbb682..26869fbcd 100644
--- a/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp
+++ b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp
@@ -14,7 +14,7 @@
#include "src/parser/MarkovAutomatonSparseTransitionParser.h"
#include "src/utility/cstring.h"
#include "src/parser/MarkovAutomatonParser.h"
-#include "src/settings/InternalOptionMemento.h"
+#include "src/settings/SettingMemento.h"
#include "src/exceptions/WrongFormatException.h"
#include "src/exceptions/FileIoException.h"
@@ -186,7 +186,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) {
TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) {
// Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed.
- storm::settings::InternalOptionMemento setDeadlockOption("fixDeadlocks", true);
+ std::unique_ptr<storm::settings::SettingMemento> setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
// Parse a Markov Automaton transition file with the fixDeadlocks Flag set and test if it works.
storm::parser::MarkovAutomatonSparseTransitionParser::Result result = storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_deadlock.tra");
@@ -205,7 +205,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) {
TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) {
// Try to parse a Markov Automaton transition file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception.
- storm::settings::InternalOptionMemento unsetDeadlockOption("fixDeadlocks", false);
+ std::unique_ptr<storm::settings::SettingMemento> setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(false);
ASSERT_THROW(storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_deadlock.tra"), storm::exceptions::WrongFormatException);
}
diff --git a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp
index 9494c983f..b7323f363 100644
--- a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp
+++ b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp
@@ -10,7 +10,7 @@
#include "src/parser/NondeterministicSparseTransitionParser.h"
#include "src/storage/SparseMatrix.h"
-#include "src/settings/InternalOptionMemento.h"
+#include "src/settings/SettingMemento.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFormatException.h"
@@ -208,7 +208,7 @@ TEST(NondeterministicSparseTransitionParserTest, MixedTransitionOrder) {
TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) {
// Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed.
- storm::settings::InternalOptionMemento setDeadlockOption("fixDeadlocks", true);
+ std::unique_ptr<storm::settings::SettingMemento> setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
// Parse a transitions file with the fixDeadlocks Flag set and test if it works.
storm::storage::SparseMatrix<double> result(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra"));
@@ -249,7 +249,7 @@ TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) {
TEST(NondeterministicSparseTransitionParserTest, DontFixDeadlocks) {
// Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception.
- storm::settings::InternalOptionMemento unsetDeadlockOption("fixDeadlocks", false);
+ std::unique_ptr<storm::settings::SettingMemento> unsetDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(false);
ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra"), storm::exceptions::WrongFormatException);
}
diff --git a/test/functional/solver/GlpkLpSolverTest.cpp b/test/functional/solver/GlpkLpSolverTest.cpp
index 0dd33f80c..0db9fdfbd 100644
--- a/test/functional/solver/GlpkLpSolverTest.cpp
+++ b/test/functional/solver/GlpkLpSolverTest.cpp
@@ -25,16 +25,16 @@ TEST(GlpkLpSolver, LPOptimizeMax) {
ASSERT_FALSE(solver.isInfeasible());
double xValue = 0;
ASSERT_NO_THROW(xValue = solver.getContinuousValue("x"));
- ASSERT_LT(std::abs(xValue - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(xValue - 1), storm::settings::generalSettings().getPrecision());
double yValue = 0;
ASSERT_NO_THROW(yValue = solver.getContinuousValue("y"));
- ASSERT_LT(std::abs(yValue - 6.5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(yValue - 6.5), storm::settings::generalSettings().getPrecision());
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue("z"));
- ASSERT_LT(std::abs(zValue - 2.75), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(zValue - 2.75), storm::settings::generalSettings().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
- ASSERT_LT(std::abs(objectiveValue - 14.75), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(objectiveValue - 14.75), storm::settings::generalSettings().getPrecision());
}
TEST(GlpkLpSolver, LPOptimizeMin) {
@@ -55,16 +55,16 @@ TEST(GlpkLpSolver, LPOptimizeMin) {
ASSERT_FALSE(solver.isInfeasible());
double xValue = 0;
ASSERT_NO_THROW(xValue = solver.getContinuousValue("x"));
- ASSERT_LT(std::abs(xValue - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(xValue - 1), storm::settings::generalSettings().getPrecision());
double yValue = 0;
ASSERT_NO_THROW(yValue = solver.getContinuousValue("y"));
- ASSERT_LT(std::abs(yValue - 0), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(yValue - 0), storm::settings::generalSettings().getPrecision());
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue("z"));
- ASSERT_LT(std::abs(zValue - 5.7), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(zValue - 5.7), storm::settings::generalSettings().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
- ASSERT_LT(std::abs(objectiveValue - (-6.7)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(objectiveValue - (-6.7)), storm::settings::generalSettings().getPrecision());
}
TEST(GlpkLpSolver, MILPOptimizeMax) {
@@ -91,10 +91,10 @@ TEST(GlpkLpSolver, MILPOptimizeMax) {
ASSERT_EQ(6, yValue);
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue("z"));
- ASSERT_LT(std::abs(zValue - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(zValue - 3), storm::settings::generalSettings().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
- ASSERT_LT(std::abs(objectiveValue - 14), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(objectiveValue - 14), storm::settings::generalSettings().getPrecision());
}
TEST(GlpkLpSolver, MILPOptimizeMin) {
@@ -121,10 +121,10 @@ TEST(GlpkLpSolver, MILPOptimizeMin) {
ASSERT_EQ(0, yValue);
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue("z"));
- ASSERT_LT(std::abs(zValue - 5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(zValue - 5), storm::settings::generalSettings().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
- ASSERT_LT(std::abs(objectiveValue - (-6)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(objectiveValue - (-6)), storm::settings::generalSettings().getPrecision());
}
TEST(GlpkLpSolver, LPInfeasible) {
diff --git a/test/functional/solver/GmmxxLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxLinearEquationSolverTest.cpp
index e714c24b6..a044c4f3b 100644
--- a/test/functional/solver/GmmxxLinearEquationSolverTest.cpp
+++ b/test/functional/solver/GmmxxLinearEquationSolverTest.cpp
@@ -27,9 +27,9 @@ TEST(GmmxxLinearEquationSolver, SolveWithStandardOptions) {
storm::solver::GmmxxLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
- ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[1] - 3), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxLinearEquationSolver, gmres) {
@@ -51,13 +51,13 @@ TEST(GmmxxLinearEquationSolver, gmres) {
std::vector<double> x(3);
std::vector<double> b = {16, -4, -7};
- ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::GMRES, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE, true, 50));
+ ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None, true, 50));
- storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::GMRES, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE, true, 50);
+ storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None, true, 50);
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
- ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[1] - 3), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxLinearEquationSolver, qmr) {
@@ -79,13 +79,13 @@ TEST(GmmxxLinearEquationSolver, qmr) {
std::vector<double> x(3);
std::vector<double> b = {16, -4, -7};
- ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::QMR, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE));
+ ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Qmr, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None));
- storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::QMR, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE, true, 50);
+ storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Qmr, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None, true, 50);
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
- ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[1] - 3), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxLinearEquationSolver, bicgstab) {
@@ -107,13 +107,13 @@ TEST(GmmxxLinearEquationSolver, bicgstab) {
std::vector<double> x(3);
std::vector<double> b = {16, -4, -7};
- ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::BICGSTAB, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE));
+ ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Bicgstab, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None));
- storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::BICGSTAB, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE);
+ storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Bicgstab, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None);
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
- ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[1] - 3), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxLinearEquationSolver, jacobi) {
@@ -135,13 +135,13 @@ TEST(GmmxxLinearEquationSolver, jacobi) {
std::vector<double> x(3);
std::vector<double> b = {11, -16, 1};
- ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::JACOBI, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE));
+ ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Jacobi, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None));
- storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::JACOBI, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE);
+ storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Jacobi, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None);
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
- ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[1] - 3), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxLinearEquationSolver, gmresilu) {
@@ -163,13 +163,13 @@ TEST(GmmxxLinearEquationSolver, gmresilu) {
std::vector<double> x(3);
std::vector<double> b = {16, -4, -7};
- ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::GMRES, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::ILU, true, 50));
+ ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::Ilu, true, 50));
- storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::GMRES, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE, true, 50);
+ storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None, true, 50);
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
- ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[1] - 3), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxLinearEquationSolver, gmresdiag) {
@@ -191,13 +191,13 @@ TEST(GmmxxLinearEquationSolver, gmresdiag) {
std::vector<double> x(3);
std::vector<double> b = {16, -4, -7};
- ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::GMRES, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::DIAGONAL, true, 50));
+ ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::Diagonal, true, 50));
- storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::GMRES, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE, true, 50);
+ storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None, true, 50);
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
- ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[1] - 3), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxLinearEquationSolver, MatrixVectorMultplication) {
@@ -220,5 +220,5 @@ TEST(GmmxxLinearEquationSolver, MatrixVectorMultplication) {
storm::solver::GmmxxLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(A, x, nullptr, 4));
- ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
\ No newline at end of file
diff --git a/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp
index 13488bd1c..e2263d38f 100644
--- a/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp
+++ b/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp
@@ -17,10 +17,10 @@ TEST(GmmxxNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
storm::solver::GmmxxNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.solveEquationSystem(true, A, x, b));
- ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_NO_THROW(solver.solveEquationSystem(false, A, x, b));
- ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
@@ -45,21 +45,21 @@ TEST(GmmxxNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
storm::solver::GmmxxNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 1));
- ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::gmmxxEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 2));
- ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::gmmxxEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 20));
- ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nullptr, 1));
- ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nullptr, 20));
- ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
\ No newline at end of file
diff --git a/test/functional/solver/NativeLinearEquationSolverTest.cpp b/test/functional/solver/NativeLinearEquationSolverTest.cpp
index 5cfa01bcb..d4eccb561 100644
--- a/test/functional/solver/NativeLinearEquationSolverTest.cpp
+++ b/test/functional/solver/NativeLinearEquationSolverTest.cpp
@@ -27,9 +27,9 @@ TEST(NativeLinearEquationSolver, SolveWithStandardOptions) {
storm::solver::NativeLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
- ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
- ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 1), storm::settings::nativeEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[1] - 3), storm::settings::nativeEquationSolverSettings().getPrecision());
+ ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(NativeLinearEquationSolver, MatrixVectorMultplication) {
@@ -52,5 +52,5 @@ TEST(NativeLinearEquationSolver, MatrixVectorMultplication) {
storm::solver::NativeLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(A, x, nullptr, 4));
- ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 1), storm::settings::nativeEquationSolverSettings().getPrecision());
}
\ No newline at end of file
diff --git a/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp b/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp
index c1c019c47..652c88ee1 100644
--- a/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp
+++ b/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp
@@ -17,10 +17,10 @@ TEST(NativeNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
storm::solver::NativeNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.solveEquationSystem(true, A, x, b));
- ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::nativeEquationSolverSettings().getPrecision());
ASSERT_NO_THROW(solver.solveEquationSystem(false, A, x, b));
- ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(NativeNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
@@ -45,21 +45,21 @@ TEST(NativeNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
storm::solver::NativeNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 1));
- ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::nativeEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 2));
- ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::nativeEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 20));
- ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::nativeEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nullptr, 1));
- ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::nativeEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nullptr, 20));
- ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::nativeEquationSolverSettings().getPrecision());
}
\ No newline at end of file
diff --git a/test/functional/storm-functional-tests.cpp b/test/functional/storm-functional-tests.cpp
index 8dbbd98ba..648fe8df0 100644
--- a/test/functional/storm-functional-tests.cpp
+++ b/test/functional/storm-functional-tests.cpp
@@ -29,37 +29,11 @@ void setUpLogging() {
// logger.addAppender(consoleLogAppender);
}
-/*!
- * Creates an empty settings object as the standard instance of the Settings class.
- */
-void createEmptyOptions() {
- const char* newArgv[] = {"storm-functional-tests"};
- storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
- try {
- storm::settings::SettingsManager::parse(1, newArgv);
- } catch (storm::exceptions::OptionParserException& e) {
- std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
- std::cout << std::endl << s->getHelpText();
- }
-}
-
int main(int argc, char* argv[]) {
setUpLogging();
- createEmptyOptions();
std::cout << "StoRM (Functional) Testing Suite" << std::endl;
testing::InitGoogleTest(&argc, argv);
-
- // now all Google Test Options have been removed
- storm::settings::SettingsManager* instance = storm::settings::SettingsManager::getInstance();
-
- try {
- storm::settings::SettingsManager::parse(argc, argv);
- } catch (storm::exceptions::OptionParserException& e) {
- std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
- std::cout << std::endl << instance->getHelpText();
- return false;
- }
int result = RUN_ALL_TESTS();