From 9547f3a91aca3dddf274ef7b255638ea2697cd7e Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 20 Sep 2014 16:27:04 +0200 Subject: [PATCH] Further refactoring of option system. Former-commit-id: 350ac4c6544eb903ffe3c681cc9bd9fb6106ecab --- src/settings/Argument.cpp | 8 + src/settings/Argument.h | 22 ++- src/settings/ArgumentBase.h | 80 +++++---- src/settings/ArgumentBuilder.h | 30 ++-- src/settings/ArgumentTypeInferationHelper.cpp | 90 ++++++++++ src/settings/ArgumentTypeInferationHelper.h | 167 ++---------------- src/settings/ArgumentValidators.h | 36 ++-- src/settings/Option.h | 28 +-- src/settings/OptionBuilder.h | 2 +- src/settings/SettingsManager.h | 35 ++-- .../CounterexampleGeneratorSettings.cpp | 27 ++- .../modules/CounterexampleGeneratorSettings.h | 65 +++++++ src/settings/modules/CuddSettings.cpp | 18 +- src/settings/modules/CuddSettings.h | 36 ++++ src/settings/modules/DebugSettings.cpp | 19 +- src/settings/modules/DebugSettings.h | 41 +++++ src/settings/modules/GeneralSettings.cpp | 42 ++--- src/settings/modules/GeneralSettings.h | 142 ++++++++++++++- src/settings/modules/GlpkSettings.cpp | 10 +- src/settings/modules/GlpkSettings.h | 17 ++ src/settings/modules/GmmxxSettings.cpp | 47 +++-- src/settings/modules/GmmxxSettings.h | 71 ++++++++ ...r.cpp => NativeEquationSolverSettings.cpp} | 0 23 files changed, 700 insertions(+), 333 deletions(-) create mode 100644 src/settings/Argument.cpp create mode 100644 src/settings/ArgumentTypeInferationHelper.cpp rename src/settings/modules/{NativeEquationSolver.cpp => NativeEquationSolverSettings.cpp} (100%) diff --git a/src/settings/Argument.cpp b/src/settings/Argument.cpp new file mode 100644 index 000000000..047dc13e9 --- /dev/null +++ b/src/settings/Argument.cpp @@ -0,0 +1,8 @@ +#include "src/settings/Argument.h" + +namespace storm { + namespace settings { + const std::string Argument::trueString = "true"; + const std::string Argument::falseString = "false"; + } +} \ No newline at end of file diff --git a/src/settings/Argument.h b/src/settings/Argument.h index 5a138bf89..c756ff5d8 100644 --- a/src/settings/Argument.h +++ b/src/settings/Argument.h @@ -56,7 +56,7 @@ namespace storm { * to this argument. * @param isOptional A flag indicating whether the argument is optional. */ - Argument(std::string const& name, std::string const& description, std::vector const& validationFunctions, bool isOptional, T defaultValue): ArgumentBase(argumentName, argumentDescription), argumentValue(), argumentType(ArgumentTypeInferation::inferToEnumType()), validationFunctions(validationFunctions), isOptional(isOptional), defaultValue(defaultValue), hasDefaultValue(true) { + Argument(std::string const& name, std::string const& description, std::vector const& validationFunctions, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(ArgumentTypeInferation::inferToEnumType()), validationFunctions(validationFunctions), isOptional(isOptional), defaultValue(defaultValue), hasDefaultValue(true) { // Intentionally left empty. } @@ -66,11 +66,11 @@ namespace storm { bool setFromStringValue(std::string const& fromStringValue) override { bool conversionOk = false; - T newValue = ArgumentBase::convertFromString(fromStringValue, conversionOk); + T newValue = ArgumentBase::convertFromString(fromStringValue, conversionOk); if (!conversionOk) { return false; } - return this->fromTypeValue(newValue); + return this->setFromTypeValue(newValue); } bool setFromTypeValue(T const& newValue) { @@ -93,10 +93,10 @@ namespace storm { * @return True iff the given argument is compatible with the current one. */ template - bool isCompatibleWith(Argument const& other) { - LOG_THROW(this->getArgumentType() == other.getArgumentType(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getArgumentName() << " and " << other.getArgumentName() << ", because they have different types."); - LOG_THROW(this->getIsOptional() != other.getIsOptional(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getArgumentName() << " and " << other.getArgumentName() << ", 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->getArgumentName() << " and " << other.getArgumentName() << ", because one of them has a default value and the other one does not."); + bool isCompatibleWith(Argument 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."); return true; } @@ -127,9 +127,9 @@ namespace storm { case ArgumentType::Boolean: { bool iValue = ArgumentTypeInferation::inferToBoolean(ArgumentType::Boolean, this->getArgumentValue()); if (iValue) { - return "true"; + return trueString; } else { - return "false"; + return falseString; } } default: return ArgumentBase::convertToString(this->argumentValue); @@ -190,6 +190,10 @@ namespace storm { // A flag indicating whether a default value has been provided. bool hasDefaultValue; + // Static constants for the string representations of true and false. + static const std::string trueString; + static const std::string falseString; + void setDefaultValue(T const& newDefault) { LOG_THROW(this->validate(newDefault), storm::exceptions::IllegalArgumentValueException, "The default value for the argument did not pass all validation functions."); this->defaultValue = newDefault; diff --git a/src/settings/ArgumentBase.h b/src/settings/ArgumentBase.h index 1f8f38c6f..8a94dfe17 100644 --- a/src/settings/ArgumentBase.h +++ b/src/settings/ArgumentBase.h @@ -146,44 +146,56 @@ namespace storm { * whether the conversion was successful. */ template - static TargetType convertFromString(std::string const& valueAsString, bool& conversionSuccessful) { - std::istringstream stream(valueAsString); - TargetType t; - conversionSuccessful = (stream >> t) && (stream >> std::ws).eof(); - return t; - } - - template <> - static bool convertFromString(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; - } + static TargetType convertFromString(std::string const& valueAsString, bool& conversionSuccessful); + /*! + * Converts the given value to a string representation. + * + * @param value The value to convert. + * @return The string representation of the value. + */ template - std::string convertToString(ValueType const& value) const { - std::ostringstream stream; - stream << value; - return stream.str(); - } + static std::string convertToString(ValueType const& value); }; + template + 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(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 + std::string ArgumentBase::convertToString(ValueType const& value) { + std::ostringstream stream; + stream << value; + return stream.str(); + } + } } diff --git a/src/settings/ArgumentBuilder.h b/src/settings/ArgumentBuilder.h index ba04142b8..521dfc2c8 100644 --- a/src/settings/ArgumentBuilder.h +++ b/src/settings/ArgumentBuilder.h @@ -37,7 +37,7 @@ namespace storm { * @return The builder of the argument. */ static ArgumentBuilder createStringArgument(std::string const& name, std::string const& description) { - ArgumentBuilder ab(ArgumentType::String, name, argumentDescription); + ArgumentBuilder ab(ArgumentType::String, name, description); return ab; } @@ -103,8 +103,8 @@ namespace storm { #define PPCAT_NX(A, B) A ## B #define PPCAT(A, B) PPCAT_NX(A, B) #define MACROaddValidationFunction(funcName, funcType) ArgumentBuilder& PPCAT(addValidationFunction, funcName) (storm::settings::Argument< funcType >::userValidationFunction_t userValidationFunction) { \ -LOG_THROW(this->argumentType == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal validation function for argument, because it takes arguments of different type.") \ -( PPCAT(this->userValidationFunction_, funcName) ).push_back(userValidationFunction); \ +LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal validation function for argument, because it takes arguments of different type.") \ +( PPCAT(this->userValidationFunctions_, funcName) ).push_back(userValidationFunction); \ return *this; \ } @@ -117,7 +117,7 @@ return *this; \ #define MACROsetDefaultValue(funcName, funcType) ArgumentBuilder& PPCAT(setDefaultValue, funcName) (funcType const& defaultValue) { \ -LOG_THROW(this->argumentType == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal default value for argument" << this->argumentName << ", because it is of different type.") \ +LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal default value for argument" << this->name << ", because it is of different type.") \ PPCAT(this->defaultValue_, funcName) = defaultValue; \ this->hasDefaultValue = true; \ return *this; \ @@ -138,41 +138,41 @@ return *this; \ std::shared_ptr build() { LOG_THROW(!this->hasBeenBuilt, storm::exceptions::IllegalFunctionCallException, "Cannot rebuild argument with builder that was already used to build an argument."); this->hasBeenBuilt = true; - switch (this->argumentType) { + switch (this->type) { case ArgumentType::String: { if (this->hasDefaultValue) { - return std::shared_ptr(new Argument(this->argumentName, this->argumentDescription, userValidationFunction_String, this->isOptional, this->defaultValue_String)); + return std::shared_ptr(new Argument(this->name, this->description, userValidationFunctions_String, this->isOptional, this->defaultValue_String)); } else { - return std::shared_ptr(new Argument(this->argumentName, this->argumentDescription, userValidationFunction_String)); + return std::shared_ptr(new Argument(this->name, this->description, userValidationFunctions_String)); } break; } case ArgumentType::Integer: if (this->hasDefaultValue) { - return std::shared_ptr(new Argument(this->argumentName, this->argumentDescription, userValidationFunction_Integer, this->isOptional, this->defaultValue_Integer)); + return std::shared_ptr(new Argument(this->name, this->description, userValidationFunctions_Integer, this->isOptional, this->defaultValue_Integer)); } else { - return std::shared_ptr(new Argument(this->argumentName, this->argumentDescription, userValidationFunction_Integer)); + return std::shared_ptr(new Argument(this->name, this->description, userValidationFunctions_Integer)); } break; case ArgumentType::UnsignedInteger: if (this->hasDefaultValue) { - return std::shared_ptr(new Argument(this->argumentName, this->argumentDescription, userValidationFunction_UnsignedInteger, this->isOptional, this->defaultValue_UnsignedInteger)); + return std::shared_ptr(new Argument(this->name, this->description, userValidationFunctions_UnsignedInteger, this->isOptional, this->defaultValue_UnsignedInteger)); } else { - return std::shared_ptr(new Argument(this->argumentName, this->argumentDescription, userValidationFunction_UnsignedInteger)); + return std::shared_ptr(new Argument(this->name, this->description, userValidationFunctions_UnsignedInteger)); } break; case ArgumentType::Double: if (this->hasDefaultValue) { - return std::shared_ptr(new Argument(this->argumentName, this->argumentDescription, userValidationFunction_Double, this->isOptional, this->defaultValue_Double)); + return std::shared_ptr(new Argument(this->name, this->description, userValidationFunctions_Double, this->isOptional, this->defaultValue_Double)); } else { - return std::shared_ptr(new Argument(this->argumentName, this->argumentDescription, userValidationFunction_Double)); + return std::shared_ptr(new Argument(this->name, this->description, userValidationFunctions_Double)); } break; case ArgumentType::Boolean: if (this->hasDefaultValue) { - return std::shared_ptr(new Argument(this->argumentName, this->argumentDescription, userValidationFunction_Boolean, this->isOptional, this->defaultValue_Boolean)); + return std::shared_ptr(new Argument(this->name, this->description, userValidationFunctions_Boolean, this->isOptional, this->defaultValue_Boolean)); } else { - return std::shared_ptr(new Argument(this->argumentName, this->argumentDescription, userValidationFunction_Boolean)); + return std::shared_ptr(new Argument(this->name, this->description, userValidationFunctions_Boolean)); } break; } diff --git a/src/settings/ArgumentTypeInferationHelper.cpp b/src/settings/ArgumentTypeInferationHelper.cpp new file mode 100644 index 000000000..c278c7108 --- /dev/null +++ b/src/settings/ArgumentTypeInferationHelper.cpp @@ -0,0 +1,90 @@ +#include "src/settings/ArgumentTypeInferationHelper.h" + +namespace storm { + namespace settings { + template + ArgumentType ArgumentTypeInferation::inferToEnumType() { + LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer type of argument."); + } + + template <> + ArgumentType ArgumentTypeInferation::inferToEnumType() { + return ArgumentType::String; + } + + template <> + ArgumentType ArgumentTypeInferation::inferToEnumType() { + return ArgumentType::Integer; + } + + template <> + ArgumentType ArgumentTypeInferation::inferToEnumType() { + return ArgumentType::UnsignedInteger; + } + + template <> + ArgumentType ArgumentTypeInferation::inferToEnumType() { + return ArgumentType::Double; + } + + template <> + ArgumentType ArgumentTypeInferation::inferToEnumType() { + return ArgumentType::Boolean; + } + + template + std::string const& ArgumentTypeInferation::inferToString(ArgumentType const& argumentType, T const& value) { + LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer string from non-string argument value."); + } + + template <> + std::string const& ArgumentTypeInferation::inferToString(ArgumentType const& argumentType, std::string const& value) { + LOG_THROW(argumentType == ArgumentType::String, storm::exceptions::InternalTypeErrorException, "Unable to infer string from non-string argument."); + return value; + } + + template + int_fast64_t ArgumentTypeInferation::inferToInteger(ArgumentType const& argumentType, T const& value) { + LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer integer from non-integer argument value."); + } + + template <> + int_fast64_t ArgumentTypeInferation::inferToInteger(ArgumentType const& argumentType, int_fast64_t const& value) { + LOG_THROW(argumentType == ArgumentType::Integer, storm::exceptions::InternalTypeErrorException, "Unable to infer integer from non-integer argument."); + return value; + } + + template + uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger(ArgumentType const& argumentType, T const& value) { + LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer unsigned integer from non-unsigned argument value."); + } + + template <> + uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger(ArgumentType const& argumentType, uint_fast64_t const& value) { + LOG_THROW(argumentType == ArgumentType::UnsignedInteger, storm::exceptions::InternalTypeErrorException, "Unable to infer integer from non-integer argument."); + return value; + } + + template + double ArgumentTypeInferation::inferToDouble(ArgumentType const& argumentType, T const& value) { + LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer double from non-double argument value."); + } + + template <> + double ArgumentTypeInferation::inferToDouble(ArgumentType const& argumentType, double const& value) { + LOG_THROW(argumentType == ArgumentType::UnsignedInteger, storm::exceptions::InternalTypeErrorException, "Unable to infer double from non-double argument."); + return value; + } + + template + bool ArgumentTypeInferation::inferToBoolean(ArgumentType const& argumentType, T const& value) { + LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer boolean from non-boolean argument value."); + } + + template <> + bool ArgumentTypeInferation::inferToBoolean(ArgumentType const& argumentType, bool const& value) { + LOG_THROW(argumentType == ArgumentType::Boolean, storm::exceptions::InternalTypeErrorException, "Unable to infer boolean from non-boolean argument."); + return value; + } + } +} \ No newline at end of file diff --git a/src/settings/ArgumentTypeInferationHelper.h b/src/settings/ArgumentTypeInferationHelper.h index 87b16ac12..981e09caf 100644 --- a/src/settings/ArgumentTypeInferationHelper.h +++ b/src/settings/ArgumentTypeInferationHelper.h @@ -1,167 +1,38 @@ -/* - * ArgumentTypeInferationHelper.h - * - * Created on: 19.07.2013 - * Author: Philipp Berger - * Static Lookup Helper that detects whether the given Template Type is valid. - */ - #ifndef STORM_SETTINGS_ARGUMENTTYPEINFERATIONHELPER_H_ #define STORM_SETTINGS_ARGUMENTTYPEINFERATIONHELPER_H_ #include #include -#include "ArgumentType.h" +#include "src/settings/ArgumentType.h" +#include "src/exceptions/ExceptionMacros.h" #include "src/exceptions/InternalTypeErrorException.h" -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; - namespace storm { namespace settings { + /*! + * This class serves as a helper class to infer the types of arguments. + */ class ArgumentTypeInferation { public: // Specialized function template that infers the Type of T to our local enum + /*! + * This function infers the type in our enum of possible types from the template parameter. + * + * @return The argument type that has been inferred. + */ template static ArgumentType inferToEnumType(); - // Specialized function templates that allow casting using the Enum Class as Target - template static std::string inferToString(ArgumentType argumentType, T value); - template static int_fast64_t inferToInteger(ArgumentType argumentType, T value); - template static uint_fast64_t inferToUnsignedInteger(ArgumentType argumentType, T value); - template static double inferToDouble(ArgumentType argumentType, T value); - template static bool inferToBoolean(ArgumentType argumentType, T value); - - private: - ArgumentTypeInferation(); - ~ArgumentTypeInferation(); + // Specialized function templates that allow casting the given value to the correct type. If the conversion + // fails, an exception is thrown. + template static std::string const& inferToString(ArgumentType const& argumentType, T const& value); + template static int_fast64_t inferToInteger(ArgumentType const& argumentType, T const& value); + template static uint_fast64_t inferToUnsignedInteger(ArgumentType const& argumentType, T const& value); + template static double inferToDouble(ArgumentType const& argumentType, T const& value); + template static bool inferToBoolean(ArgumentType const& argumentType, T const& value); }; - - /* - * All functions related to the EnumType Inferation from the Template Parameter - */ - template - ArgumentType ArgumentTypeInferation::inferToEnumType() { - // "Missing Template Specialization Case in ArgumentTypeInferation" - LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToEnumType: Missing a template specialization case in the ArgumentTypeInferationHelper."); - throw storm::exceptions::InternalTypeErrorException() << "Missing a template specialization case in the ArgumentTypeInferationHelper."; - - return ArgumentType::Invalid; - } - - template <> inline ArgumentType ArgumentTypeInferation::inferToEnumType() { - return ArgumentType::String; - } - template <> inline ArgumentType ArgumentTypeInferation::inferToEnumType() { - return ArgumentType::Integer; - } - template <> inline ArgumentType ArgumentTypeInferation::inferToEnumType() { - return ArgumentType::UnsignedInteger; - } - template <> inline ArgumentType ArgumentTypeInferation::inferToEnumType() { - return ArgumentType::Double; - } - template <> inline ArgumentType ArgumentTypeInferation::inferToEnumType() { - return ArgumentType::Boolean; - } - - /* - * All functions related to the conversion to std::string based on the Template and Enum Type - */ - template - std::string ArgumentTypeInferation::inferToString(ArgumentType argumentType, T value) { - LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToString: Unable to perform inferToString on a non-string template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."); - throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToString on a non-string template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."; - - return std::string(); - } - - template <> inline std::string ArgumentTypeInferation::inferToString(ArgumentType argumentType, std::string value) { - if (argumentType != ArgumentType::String) { - LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToString: Unable to perform inferToString on a non-string template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!"); - throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToString on a non-string template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!"; - } - return value; - } - - /* - * All functions related to the conversion to int_fast64_t based on the Template and Enum Type - */ - template - int_fast64_t ArgumentTypeInferation::inferToInteger(ArgumentType argumentType, T value) { - LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToInteger: Unable to perform inferToInteger on a non-int_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."); - throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToInteger on a non-int_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."; - - return 0; - } - - template <> inline int_fast64_t ArgumentTypeInferation::inferToInteger(ArgumentType argumentType, int_fast64_t value) { - if (argumentType != ArgumentType::Integer) { - LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToInteger: Unable to perform inferToInteger on a non-int_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!"); - throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToInteger on a non-int_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!"; - } - return value; - } - - /* - * All functions related to the conversion to uint_fast64_t based on the Template and Enum Type - */ - template - uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger(ArgumentType argumentType, T value) { - LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToUnsignedInteger: Unable to perform inferToUnsignedInteger on a non-uint_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."); - throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToUnsignedInteger on a non-uint_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."; - - return 0; - } - - template <> inline uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger(ArgumentType argumentType, uint_fast64_t value) { - if (argumentType != ArgumentType::UnsignedInteger) { - LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToUnsignedInteger: Unable to perform inferToUnsignedInteger on a non-uint_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."); - throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToUnsignedInteger on a non-uint_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."; - } - return value; - } - - /* - * All functions related to the conversion to double based on the Template and Enum Type - */ - template - double ArgumentTypeInferation::inferToDouble(ArgumentType argumentType, T value) { - LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToDouble: Unable to perform inferToDouble on a non-double template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."); - throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToDouble on a non-double template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."; - - return 0.0; - } - - template <> inline double ArgumentTypeInferation::inferToDouble(ArgumentType argumentType, double value) { - if (argumentType != ArgumentType::Double) { - LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToDouble: Unable to perform inferToDouble on a double template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."); - throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToDouble on a double template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."; - } - return value; - } - - /* - * All functions related to the conversion to bool based on the Template and Enum Type - */ - template - bool ArgumentTypeInferation::inferToBoolean(ArgumentType argumentType, T value) { - LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToBoolean: Unable to perform inferToBoolean on a non-bool template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."); - throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToBoolean on a non-bool template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."; - - return false; - } - - template <> inline bool ArgumentTypeInferation::inferToBoolean(ArgumentType argumentType, bool value) { - if (argumentType != ArgumentType::Boolean) { - LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToBoolean: Unable to perform inferToBoolean on a non-bool template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."); - throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToBoolean on a non-bool template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "."; - } - return value; - } - } -} + } // namespace settings +} // namespace storm #endif // STORM_SETTINGS_ARGUMENTTYPEINFERATIONHELPER_H_ \ No newline at end of file diff --git a/src/settings/ArgumentValidators.h b/src/settings/ArgumentValidators.h index 0758500cf..619773cf2 100644 --- a/src/settings/ArgumentValidators.h +++ b/src/settings/ArgumentValidators.h @@ -12,6 +12,8 @@ #include #include "src/settings/Argument.h" +#include "src/exceptions/ExceptionMacros.h" +#include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace settings { @@ -24,7 +26,7 @@ namespace storm { * @param upperBound The upper bound of the valid range. * @return The resulting validation function. */ - static std::function integerRangeValidatorIncluding(int_fast64_t const lowerBound, int_fast64_t const upperBound) { + static std::function integerRangeValidatorIncluding(int_fast64_t lowerBound, int_fast64_t upperBound) { return rangeValidatorIncluding(lowerBound, upperBound); } @@ -35,7 +37,7 @@ namespace storm { * @param upperBound The upper bound of the valid range. * @return The resulting validation function. */ - static std::function integerRangeValidatorExcluding(int_fast64_t const lowerBound, int_fast64_t const upperBound) { + static std::function integerRangeValidatorExcluding(int_fast64_t lowerBound, int_fast64_t upperBound) { return rangeValidatorExcluding(lowerBound, upperBound); } @@ -46,7 +48,7 @@ namespace storm { * @param upperBound The upper bound of the valid range. * @return The resulting validation function. */ - static std::function unsignedIntegerRangeValidatorIncluding(uint_fast64_t const lowerBound, uint_fast64_t const upperBound) { + static std::function unsignedIntegerRangeValidatorIncluding(uint_fast64_t lowerBound, uint_fast64_t upperBound) { return rangeValidatorIncluding(lowerBound, upperBound); } @@ -57,7 +59,7 @@ namespace storm { * @param upperBound The upper bound of the valid range. * @return The resulting validation function. */ - static std::function unsignedIntegerRangeValidatorExcluding(uint_fast64_t const lowerBound, uint_fast64_t const upperBound) { + static std::function unsignedIntegerRangeValidatorExcluding(uint_fast64_t lowerBound, uint_fast64_t upperBound) { return rangeValidatorExcluding(lowerBound, upperBound); } @@ -68,7 +70,7 @@ namespace storm { * @param upperBound The upper bound of the valid range. * @return The resulting validation function. */ - static std::function doubleRangeValidatorIncluding(double const lowerBound, double const upperBound) { + static std::function doubleRangeValidatorIncluding(double lowerBound, double upperBound) { return rangeValidatorIncluding(lowerBound, upperBound); } @@ -79,7 +81,7 @@ namespace storm { * @param upperBound The upper bound of the valid range. * @return The resulting validation function. */ - static std::function doubleRangeValidatorExcluding(double const lowerBound, double const upperBound) { + static std::function doubleRangeValidatorExcluding(double lowerBound, double upperBound) { return rangeValidatorExcluding(lowerBound, upperBound); } @@ -106,11 +108,9 @@ namespace storm { * @return The resulting validation function. */ static std::function stringInListValidator(std::vector const& list) { - return [list] (std::string const inputString) -> bool { - std::string lowerInputString = boost::algorithm::to_lower_copy(inputString); + return [list] (std::string const& inputString) -> bool { for (auto const& validString : list) { - std::string lowerValidString = boost::algorithm::to_lower_copy(validString); - if (lowerInputString == lowerValidString) { + if (inputString == validString) { return true; } } @@ -129,11 +129,11 @@ namespace storm { * @return The resulting validation function. */ template - static std::function rangeValidatorIncluding(T const lowerBound, T const upperBound) { - return std::bind([](T const& lowerBound, T const& upperBound, T const& value) -> bool { - LOG_THROW(lowerBound <= value && value <= upperBound, storm::exceptions::InvalidArgumentException, "Value " << value " is out range."); + static std::function rangeValidatorIncluding(T lowerBound, T upperBound) { + return std::bind([](T lowerBound, T upperBound, T value) -> bool { + LOG_THROW(lowerBound <= value && value <= upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out range."); return true; - }, lowerBound, upperBound, std::placeholders::_1, std::placeholders::_2); + }, lowerBound, upperBound, std::placeholders::_1); } /*! @@ -144,11 +144,11 @@ namespace storm { * @return The resulting validation function. */ template - static std::function rangeValidatorExcluding(T const& lowerBound, T const& upperBound) { - return std::bind([](T const& lowerBound, T const& upperBound, T const& value) -> bool { - LOG_THROW(lowerBound < value && value < upperBound, storm::exceptions::InvalidArgumentException, "Value " << value " is out range."); + static std::function rangeValidatorExcluding(T lowerBound, T upperBound) { + return std::bind([](T lowerBound, T upperBound, T value) -> bool { + LOG_THROW(lowerBound < value && value < upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out range."); return true; - }, lowerBound, upperBound, std::placeholders::_1, std::placeholders::_2); + }, lowerBound, upperBound, std::placeholders::_1); } }; } diff --git a/src/settings/Option.h b/src/settings/Option.h index ebec3acb8..689c11191 100644 --- a/src/settings/Option.h +++ b/src/settings/Option.h @@ -14,7 +14,6 @@ #include "ArgumentBase.h" #include "Argument.h" -#include "src/utility/StringHelper.h" #include "src/exceptions/ExceptionMacros.h" #include "src/exceptions/IllegalArgumentException.h" #include "src/exceptions/OptionUnificationException.h" @@ -22,13 +21,16 @@ namespace storm { namespace settings { + // Forward-declare settings manager class. + class SettingsManager; + /*! * This class represents one command-line option. */ class Option { public: - // (Forward-)declare settings manager class as friend. - friend class storm::settings::SettingsManager; + // Declare settings manager class as friend. + friend class SettingsManager; /*! * Creates an option with the given parameters. @@ -74,23 +76,23 @@ namespace storm { ArgumentBase const& firstArgument = this->getArgument(i); ArgumentBase const& secondArgument = other.getArgument(i); - LOG_THROW(firstArgument.getArgumentType() == secondArgument.getArgumentType(), storm::exceptions::OptionUnificationException, "Unable to unify two options, because their arguments are incompatible."); + LOG_THROW(firstArgument.getType() == secondArgument.getType(), storm::exceptions::OptionUnificationException, "Unable to unify two options, because their arguments are incompatible."); - switch (firstArgument->getArgumentType()) { + switch (firstArgument.getType()) { case ArgumentType::String: - static_cast&>(firstArgument).isCompatibleWith(static_cast&>(secondArgument)); + static_cast const&>(firstArgument).isCompatibleWith(static_cast const&>(secondArgument)); break; case ArgumentType::Integer: - static_cast&>(firstArgument).isCompatibleWith(static_cast&>(secondArgument)); + static_cast const&>(firstArgument).isCompatibleWith(static_cast const&>(secondArgument)); break; case ArgumentType::UnsignedInteger: - static_cast&>(firstArgument).isCompatibleWith(static_cast&>(secondArgument)); + static_cast const&>(firstArgument).isCompatibleWith(static_cast const&>(secondArgument)); break; case ArgumentType::Double: - static_cast&>(firstArgument).isCompatibleWith(static_cast&>(secondArgument)); + static_cast const&>(firstArgument).isCompatibleWith(static_cast const&>(secondArgument)); break; case ArgumentType::Boolean: - static_cast&>(firstArgument).isCompatibleWith(static_cast&>(secondArgument)); + static_cast const&>(firstArgument).isCompatibleWith(static_cast const&>(secondArgument)); break; } } @@ -113,7 +115,7 @@ namespace storm { * @return The i-th argument of this option. */ ArgumentBase const& getArgument(uint_fast64_t argumentIndex) const { - LOG_THROW(argumentIndex < this->getArgumentCount(), storm::exceptions::IllegalArgumentException, "Index of argument is out of bounds.") + LOG_THROW(argumentIndex < this->getArgumentCount(), storm::exceptions::IllegalArgumentException, "Index of argument is out of bounds."); return *this->arguments.at(argumentIndex); } @@ -124,7 +126,7 @@ namespace storm { * @return The argument with the given name. */ ArgumentBase const& getArgumentByName(std::string const& argumentName) const { - auto argumentIterator = this->argumentNameMap.find(storm::utility::StringHelper::stringToLower(argumentName)); + auto argumentIterator = this->argumentNameMap.find(argumentName); LOG_THROW(argumentIterator != this->argumentNameMap.end(), storm::exceptions::IllegalArgumentException, "Unable to retrieve argument with unknown name " << argumentName << "."); return *argumentIterator->second; } @@ -250,7 +252,7 @@ namespace storm { // Then index all arguments. for (auto const& argument : arguments) { - argumentNameMap.emplace(lowerArgumentName, std::shared_ptr(*i)); + argumentNameMap.emplace(argument->getName(), argument); } } diff --git a/src/settings/OptionBuilder.h b/src/settings/OptionBuilder.h index a7b04f725..0823d0e05 100644 --- a/src/settings/OptionBuilder.h +++ b/src/settings/OptionBuilder.h @@ -71,7 +71,7 @@ namespace storm { LOG_THROW(this->arguments.empty() || !argument->getIsOptional() || this->arguments.back()->getIsOptional(), storm::exceptions::IllegalArgumentException, "Unable to add non-optional argument after an option that is optional."); std::string lowerArgumentName = boost::algorithm::to_lower_copy(argument->getName()); - LOG_THROW(argumentNamSet.find(lowerArgumentName) == argumentNameSet.end(), storm::exceptions::IllegalArgumentException, "Unable to add argument to option, because it already has an argument with the same name."); + LOG_THROW(argumentNameSet.find(lowerArgumentName) == argumentNameSet.end(), storm::exceptions::IllegalArgumentException, "Unable to add argument to option, because it already has an argument with the same name."); argumentNameSet.insert(lowerArgumentName); this->arguments.push_back(argument); diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index 2aaba3cd2..e1bf4f46b 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -1,5 +1,5 @@ -#ifndef STORM_SETTINGS_SETTINGS_H_ -#define STORM_SETTINGS_SETTINGS_H_ +#ifndef STORM_SETTINGS_SETTINGSMANAGER_H_ +#define STORM_SETTINGS_SETTINGSMANAGER_H_ #include #include @@ -10,7 +10,6 @@ #include #include - #include "src/settings/Option.h" #include "src/settings/OptionBuilder.h" #include "src/settings/ArgumentBase.h" @@ -28,28 +27,14 @@ #include "src/settings/modules/GlpkSettings.h" #include "src/settings/modules/GurobiSettings.h" -// Exceptions that should be catched when performing a parsing run +#include "src/exceptions/ExceptionMacros.h" #include "src/exceptions/OptionParserException.h" -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" - -extern log4cplus::Logger logger; - namespace storm { - /*! - * @brief Contains Settings class and associated methods. - */ namespace settings { - typedef bool (*stringValidationFunction_t)(const std::string); - typedef bool (*integerValidationFunction_t)(const int_fast64_t); - typedef bool (*unsignedIntegerValidationFunction_t)(const uint_fast64_t); - typedef bool (*doubleValidationFunction_t)(const double); - typedef bool (*booleanValidationFunction_t)(const bool); typedef std::pair stringPair_t; - typedef std::pair fromStringAssignmentResult_t; class InternalOptionMemento; @@ -226,7 +211,7 @@ namespace storm { * @return bool true iff there is an option with the specified longName */ bool containsLongName(std::string const& longName) const { - return (this->options.find(storm::utility::StringHelper::stringToLower(longName)) != this->options.end()); + return (this->options.find(longName) != this->options.end()); } /*! @@ -234,7 +219,7 @@ namespace storm { * @return bool true iff there is an option with the specified shortName */ bool containsShortName(std::string const& shortName) const { - return (this->shortNames.find(storm::utility::StringHelper::stringToLower(shortName)) != this->shortNames.end()); + return (this->shortNames.find(shortName) != this->shortNames.end()); } /*! @@ -243,7 +228,7 @@ namespace storm { * @throws InvalidArgumentException */ Option& getByLongName(std::string const& longName) const { - auto longNameIterator = this->options.find(storm::utility::StringHelper::stringToLower(longName)); + auto longNameIterator = this->options.find(longName); if (longNameIterator == this->options.end()) { LOG4CPLUS_ERROR(logger, "Settings::getByLongName: This program does not contain an option named \"" << longName << "\"."); throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << longName << "\"."; @@ -257,7 +242,7 @@ namespace storm { * @throws InvalidArgumentException */ Option* getPtrByLongName(std::string const& longName) const { - auto longNameIterator = this->options.find(storm::utility::StringHelper::stringToLower(longName)); + auto longNameIterator = this->options.find(longName); if (longNameIterator == this->options.end()) { LOG4CPLUS_ERROR(logger, "Settings::getPtrByLongName: This program does not contain an option named \"" << longName << "\"."); throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << longName << "\"."; @@ -271,7 +256,7 @@ namespace storm { * @throws InvalidArgumentException */ Option& getByShortName(std::string const& shortName) const { - auto shortNameIterator = this->shortNames.find(storm::utility::StringHelper::stringToLower(shortName)); + auto shortNameIterator = this->shortNames.find(shortName); if (shortNameIterator == this->shortNames.end()) { LOG4CPLUS_ERROR(logger, "Settings::getByShortName: This program does not contain an option named \"" << shortName << "\"."); throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << shortName << "\""; @@ -285,7 +270,7 @@ namespace storm { * @throws InvalidArgumentException */ Option* getPtrByShortName(std::string const& shortName) const { - auto shortNameIterator = this->shortNames.find(storm::utility::StringHelper::stringToLower(shortName)); + auto shortNameIterator = this->shortNames.find(shortName); if (shortNameIterator == this->shortNames.end()) { LOG4CPLUS_ERROR(logger, "Settings::getPtrByShortName: This program does not contain an option named \"" << shortName << "\"."); throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << shortName << "\"."; @@ -317,4 +302,4 @@ namespace storm { } // namespace settings } // namespace storm -#endif // \ No newline at end of file +#endif /* STORM_SETTINGS_SETTINGSMANAGER_H_ */ \ No newline at end of file diff --git a/src/settings/modules/CounterexampleGeneratorSettings.cpp b/src/settings/modules/CounterexampleGeneratorSettings.cpp index 6ac14d7ec..0fad20609 100644 --- a/src/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/src/settings/modules/CounterexampleGeneratorSettings.cpp @@ -6,16 +6,25 @@ namespace storm { namespace settings { namespace modules { + const std::string CounterexampleGeneratorSettings::moduleName = "counterexample"; + const std::string CounterexampleGeneratorSettings::minimalCommandSetOptionName = "mincmd"; + const std::string CounterexampleGeneratorSettings::encodeReachabilityOptionName = "encreach"; + const std::string CounterexampleGeneratorSettings::schedulerCutsOptionName = "schedcuts"; + const std::string CounterexampleGeneratorSettings::statisticsOptionName = "stats"; + CounterexampleGeneratorSettings::CounterexampleGeneratorSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) { - std::vector techniques; - techniques.push_back("sat"); - techniques.push_back("milp"); - settingsManager.addOption(storm::settings::OptionBuilder("CounterexampleGenerator", "mincmd", "", "Computes a counterexample for the given symbolic model in terms of a minimal command set.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("propertyFile", "The file containing the properties for which counterexamples are to be generated.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample. Must be either \"milp\" or \"sat\".").setDefaultValueString("sat").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(techniques)).build()).build()); - settingsManager.addOption(storm::settings::OptionBuilder("CounterexampleGenerator", "stats", "", "Sets whether to display statistics for certain functionalities.").build()); - settingsManager.addOption(storm::settings::OptionBuilder("CounterexampleGenerator", "encreach", "", "Sets whether to encode reachability for SAT-based minimal command counterexample generation.").build()); - settingsManager.addOption(storm::settings::OptionBuilder("CounterexampleGenerator", "schedcuts", "", "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build()); + // First, we need to create all options of this module. + std::vector> options; + std::vector techniques = {"sat", "milp"}; + options.push_back(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command set. Note that this requires the model to be given in a symbolic format.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file containing the properties for which counterexamples are to be generated.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample. Available are {milp, maxsat}").setDefaultValueString("maxsat").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(techniques)).build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, statisticsOptionName, true, "Sets whether to display statistics for counterexample generation.").build()); + options.push_back(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based minimal command counterexample generation.").build()); + options.push_back(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build()); + + // Finally, register all options that we just created. + settingsManager.registerModule(moduleName, options); } } // namespace modules diff --git a/src/settings/modules/CounterexampleGeneratorSettings.h b/src/settings/modules/CounterexampleGeneratorSettings.h index 176311f80..d3a9626ab 100644 --- a/src/settings/modules/CounterexampleGeneratorSettings.h +++ b/src/settings/modules/CounterexampleGeneratorSettings.h @@ -12,7 +12,72 @@ namespace storm { */ class CounterexampleGeneratorSettings : public ModuleSettings { public: + /*! + * Creates a new set of counterexample settings that is managed by the given manager. + * + * @param settingsManager The responsible manager. + */ CounterexampleGeneratorSettings(storm::settings::SettingsManager& settingsManager); + + /*! + * Retrieves whether the option to generate a minimal command set was set. + * + * @return True iff a minimal command set counterexample is to be generated. + */ + bool isMinimalCommandGenerationSet() const; + + /*! + * Retrieves the name of the file that contains the properties for which a minimal command set + * counterexample is to be generated if the option to generate such a counterexample was set. + * + * @return The name of the file that contains the properties. + */ + std::string minimalCommandSetPropertyFilename() const; + + /*! + * Retrieves whether the MILP-based technique is to be used to generate a minimal command set + * counterexample. + * + * @return True iff the MILP-based technique is to be used. + */ + bool useMilpBasedMinimalCommandSetGeneration() const; + + /*! + * Retrieves whether the MAXSAT-based technique is to be used to generate a minimal command set + * counterexample. + * + * @return True iff the MAXSAT-based technique is to be used. + */ + bool useMaxSatBasedMinimalCommandSetGeneration() const; + + /*! + * Retrieves whether reachability of a target state is to be encoded if the MAXSAT-based technique is + * used to generate a minimal command set counterexample. + * + * @return True iff reachability of a target state is to be encoded. + */ + bool isEncodeReachabilitySet() const; + + /*! + * Retrieves whether scheduler cuts are to be used if the MAXSAT-based technique is used to generate a + * minimal command set counterexample + */ + bool useSchedulerCuts() const; + + /*! + * Retrieves whether statistics are to be shown for counterexample generation. + * + * @return True iff statistics are to be shown for counterexample generation. + */ + bool showStatistics() const; + + private: + // Define the string names of the options as constants. + static const std::string moduleName; + static const std::string minimalCommandSetOptionName; + static const std::string encodeReachabilityOptionName; + static const std::string schedulerCutsOptionName; + static const std::string statisticsOptionName; }; } // namespace modules diff --git a/src/settings/modules/CuddSettings.cpp b/src/settings/modules/CuddSettings.cpp index e092f6f4a..406cac4b7 100644 --- a/src/settings/modules/CuddSettings.cpp +++ b/src/settings/modules/CuddSettings.cpp @@ -6,13 +6,18 @@ 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"; + CuddSettings::CuddSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) { - // Set up options for precision and maximal memory available to Cudd. - settingsManager.addOption(storm::settings::OptionBuilder("Cudd", "cuddprec", "", "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()); + // First, we need to create all options of this module. + std::vector> options; + options.push_back(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); - settingsManager.addOption(storm::settings::OptionBuilder("Cudd", "cuddmaxmem", "", "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mb", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(2048).build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mb", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(2048).build()).build()); - // Set up option for reordering. std::vector reorderingTechniques; reorderingTechniques.push_back("none"); reorderingTechniques.push_back("random"); @@ -32,7 +37,10 @@ namespace storm { reorderingTechniques.push_back("annealing"); reorderingTechniques.push_back("genetic"); reorderingTechniques.push_back("exact"); - settingsManager.addOption(storm::settings::OptionBuilder("Cudd", "reorder", "", "Sets the reordering technique used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used by Cudd's reordering routines. Must be in {\"none\", \"random\", \"randompivot\", \"sift\", \"siftconv\", \"ssift\", \"ssiftconv\", \"gsift\", \"gsiftconv\", \"win2\", \"win2conv\", \"win3\", \"win3conv\", \"win4\", \"win4conv\", \"annealing\", \"genetic\", \"exact\"}.").setDefaultValueString("gsift").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(reorderingTechniques)).build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, reorderOptionName, true, "Sets the reordering technique used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used by Cudd's reordering routines. Must be in {none, random, randompivot, sift, siftconv, ssift, ssiftconv, gsift, gsiftconv, win2, win2conv, win3, win3conv, win4, win4conv, annealing, genetic, exact}.").setDefaultValueString("gsift").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(reorderingTechniques)).build()).build()); + + // Finally, register all options that we just created. + settingsManager.registerModule(moduleName, options); } } // namespace modules diff --git a/src/settings/modules/CuddSettings.h b/src/settings/modules/CuddSettings.h index d8c2efde8..e0e588953 100644 --- a/src/settings/modules/CuddSettings.h +++ b/src/settings/modules/CuddSettings.h @@ -12,7 +12,43 @@ namespace storm { */ class CuddSettings : public ModuleSettings { public: + // An enumeration of all available reordering techniques of CUDD. + enum class ReorderingTechnique { None, Random, RandomPivot, Sift, SiftConv, SymmetricSift, SymmetricSiftConv, GroupSift, GroupSiftConv, Win2, Win2Conv, Win3, Win3Conv, Win4, Win4Conv, Annealing, Genetic, Exact }; + + /*! + * Creates a new set of CUDD settings that is managed by the given manager. + * + * @param settingsManager The responsible manager. + */ CuddSettings(storm::settings::SettingsManager& settingsManager); + + /*! + * Retrieves the precision that CUDD is supposed to use for distinguishing constants. + * + * @return The desired precision of CUDD. + */ + double getConstantPrecision() const; + + /*! + * Retrieves the maximal amount of memory (in megabytes) that CUDD can occupy. + * + * @return The maximal amount of memory to use. + */ + uint_fast64_t getMaximalMemory() const; + + /*! + * Retrieves the reordering technique that CUDD is supposed to use. + * + * @return The reordering technique to use. + */ + ReorderingTechnique getReorderingTechnique() const; + + private: + // Define the string names of the options as constants. + static const std::string moduleName; + static const std::string precisionOptionName; + static const std::string maximalMemoryOptionName; + static const std::string reorderOptionName; }; } // namespace modules diff --git a/src/settings/modules/DebugSettings.cpp b/src/settings/modules/DebugSettings.cpp index 652364586..3fa44529a 100644 --- a/src/settings/modules/DebugSettings.cpp +++ b/src/settings/modules/DebugSettings.cpp @@ -6,11 +6,22 @@ namespace storm { namespace settings { namespace modules { + const std::string DebugSettings::moduleName = "debug"; + const std::string DebugSettings::debugOptionName = "debug"; + const std::string DebugSettings::traceOptionName = "trace"; + const std::string DebugSettings::logfileOptionName = "logfile"; + const std::string DebugSettings::logfileOptionShortName = "l"; + DebugSettings::DebugSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) { - settingsManager.addOption(storm::settings::OptionBuilder("debug", "debug", "", "Be very verbose (intended for debugging).").build()); - settingsManager.addOption(storm::settings::OptionBuilder("debug", "trace", "", "Be extremly verbose (intended for debugging, heavy performance impacts).").build()); - settingsManager.addOption(storm::settings::OptionBuilder("debug", "logfile", "l", "If specified, the log output will also be written to this file.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("logFileName", "The path and name of the file to write to.").build()).build()); + // First, we need to create all options of this module. + std::vector> options; + options.push_back(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Print debug output.").build()); + options.push_back(storm::settings::OptionBuilder(moduleName, traceOptionName, false, "Print even more debug output.").build()); + options.push_back(storm::settings::OptionBuilder(moduleName, logfileOptionName, false, "If specified, the log output will also be written to this file.").setShortName(logfileOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to write the log.").build()).build()); + + // Finally, register all options that we just created. + settingsManager.registerModule(moduleName, options); } } // namespace modules diff --git a/src/settings/modules/DebugSettings.h b/src/settings/modules/DebugSettings.h index d1edf843f..9a65c53c9 100644 --- a/src/settings/modules/DebugSettings.h +++ b/src/settings/modules/DebugSettings.h @@ -12,7 +12,48 @@ namespace storm { */ class DebugSettings : public ModuleSettings { public: + /*! + * Creates a new set of debug settings that is managed by the given manager. + * + * @param settingsManager The responsible manager. + */ DebugSettings(storm::settings::SettingsManager& settingsManager); + + /*! + * Retrieves whether the debug option was set. + * + * @return True iff the debug option was set. + */ + bool isDebugSet() const; + + /*! + * Retrieves whether the trace option was set. + * + * @return True iff the trace option was set. + */ + bool isTraceSet() const; + + /*! + * Retrieves whether the logfile option was set. + * + * @return True iff the logfile option was set. + */ + bool isLogfileSet() const; + + /*! + * Retrieves the name of the log file if the logfile option was set. + * + * @return The name of the log file. + */ + std::string getLogfilename() const; + + private: + // Define the string names of the options as constants. + static const std::string moduleName; + static const std::string debugOptionName; + static const std::string traceOptionName; + static const std::string logfileOptionName; + static const std::string logfileOptionShortName; }; } // namespace modules diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index d48ab5554..a13ea57e6 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -36,48 +36,44 @@ namespace storm { GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) { // First, we need to create all options of this module. std::vector> options; - options.push_back(storm::settings::OptionBuilder(moduleName, helpOptionName, helpOptionShortName, "Shows all available options, arguments and descriptions.").build()); - options.push_back(storm::settings::OptionBuilder(moduleName, verboseOptionName, verboseOptionShortName, "Enables more verbose output.").build()); + std::vector moduleNames = {"all", "general", "debug", "cudd", "counterexample", "glpk", "gurobi", "gmm++", "native"}; + options.push_back(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("module", "The module for which to show the help or 'all' for all modules.").setDefaultValueString("all").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(moduleNames)).build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build()); options.push_back(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); - options.push_back(storm::settings::OptionBuilder(moduleName, configOptionName, configOptionShortName, "If given, this file will be read and parsed for additional configuration settings.") + options.push_back(storm::settings::OptionBuilder(moduleName, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the configuration.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - options.push_back(storm::settings::OptionBuilder(moduleName, explicitOptionName, explicitOptionShortName, "Parses the model given in an explicit (sparse) representation.") + options.push_back(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - options.push_back(storm::settings::OptionBuilder(moduleName, symbolicOptionName, symbolicOptionShortName, "Parses the model given in a symbolic representation.") + options.push_back(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - options.push_back(storm::settings::OptionBuilder(moduleName, pctlOptionName, "", "Specifies the PCTL formulas that are to be checked on the model.") + options.push_back(storm::settings::OptionBuilder(moduleName, pctlOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the PCTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - options.push_back(storm::settings::OptionBuilder(moduleName, cslOptionName, "", "Specifies the CSL formulas that are to be checked on the model.") + options.push_back(storm::settings::OptionBuilder(moduleName, cslOptionName, false, "Specifies the CSL formulas that are to be checked on the model.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the CSL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - options.push_back(storm::settings::OptionBuilder(moduleName, ltlOptionName, "", "Specifies the LTL formulas that are to be checked on the model.") + options.push_back(storm::settings::OptionBuilder(moduleName, ltlOptionName, false, "Specifies the LTL formulas that are to be checked on the model.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - options.push_back(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, "", "Generates a counterexample for the given PRCTL formulas if not satisfied by the model") + options.push_back(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the counterexample is to be written.").build()).build()); options.push_back(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, "", "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - options.push_back(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, "", "If given, the state rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ")."); + options.push_back(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, false, "If given, the state rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - options.push_back(storm::settings::OptionBuilder(moduleName, fixDeadlockOptionName, fixDeadlockOptionShortName, "If the model contains deadlock states, they need to be fixed by setting this option.").build()); + options.push_back(storm::settings::OptionBuilder(moduleName, fixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(fixDeadlockOptionShortName).build()); - std::vector linearEquationSolver; - linearEquationSolver.push_back("gmm++"); - linearEquationSolver.push_back("native"); - settingsManager.addOption(); - options.push_back(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, "", "Sets which solver is preferred for solving systems of linear equations.") + std::vector linearEquationSolver = {"gmm++", "native"}; + options.push_back(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build()); - options.push_back(storm::settings::OptionBuilder(moduleName, timeoutOptionName, timeoutOptionShortName, "If given, computation will abort after the timeout has been reached.") + options.push_back(storm::settings::OptionBuilder(moduleName, timeoutOptionName, false, "If given, computation will abort after the timeout has been reached.").setShortName(timeoutOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "The number of seconds after which to timeout.").setDefaultValueUnsignedInteger(0).build()).build()); - std::vector lpSolvers; - lpSolvers.push_back("gurobi"); - lpSolvers.push_back("glpk"); - settingsManager.addOption(); - options.push_back(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, "", "Sets which LP solver is preferred.") + std::vector lpSolvers = {"gurobi", "glpk"}; + options.push_back(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build()); - options.push_back(storm::settings::OptionBuilder(moduleName, constantsOptionName, constantsOptionShortName, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").") + options.push_back(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); // Finally, register all options that we just created. diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index ca7cc4c40..9640c5acc 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -12,6 +12,11 @@ namespace storm { */ class GeneralSettings : public ModuleSettings { public: + /*! + * Creates a new set of general settings that is managed by the given manager. + * + * @param settingsManager The responsible manager. + */ GeneralSettings(storm::settings::SettingsManager& settingsManager); /*! @@ -21,6 +26,14 @@ namespace storm { */ bool isHelpSet() const; + /*! + * Retrieves the name of the module for which to show the help or "all" to indicate that the full help + * needs to be shown. + * + * @return The name of the module for which to show the help or "all". + */ + std::string getHelpModuleName() const; + /*! * Retrieves whether the verbose option was set. * @@ -35,6 +48,13 @@ namespace storm { */ bool isExportDotSet() const; + /*! + * Retrieves the name in which to write the model in dot format, if the export-to-dot option was set. + * + * @return The name of the file in which to write the exported model. + */ + std::string getExportDotFilename() const; + /*! * Retrieves whether the config option was set. * @@ -42,19 +62,50 @@ namespace storm { */ bool isConfigSet() const; + /*! + * Retrieves the name of the file that is to be scanned for settings. + * + * @return The name of the file that is to be scanned for settings. + */ + std::string getConfigFilename() const; + /*! * Retrieves whether the explicit option was set. * * @return True if the explicit option was set. */ bool isExplicitSet() const; + + /*! + * Retrieves the name of the file that contains the transitions if the model was given using the explicit + * option. + * + * @return The name of the file that contains the transitions. + */ + std::string getTransitionFilename() const; + /*! + * Retrieves the name of the file that contains the state labeling if the model was given using the + * explicit option. + * + * @return The name of the file that contains the state labeling. + */ + std::string getLabelingFilename() const; + /*! * Retrieves whether the symbolic option was set. * * @return True if the symbolic option was set. */ bool isSymbolicSet() const; + + /*! + * Retrieves the name of the file that contains the symbolic model specification if the model was given + * using the symbolic option. + * + * @return The name of the file that contains the symbolic model specification. + */ + std::string getSymbolicModelFilename() const; /*! * Retrieves whether the pctl option was set. @@ -62,6 +113,13 @@ namespace storm { * @return True if the pctl option was set. */ bool isPctlSet() const; + + /*! + * Retrieves the name of the file that contains the PCTL properties to be checked on the model. + * + * @return The name of the file that contains the PCTL properties to be checked on the model. + */ + std::string getPctlPropertiesFilename() const; /*! * Retrieves whether the csl option was set. @@ -70,6 +128,13 @@ namespace storm { */ bool isCslSet() const; + /*! + * Retrieves the name of the file that contains the CSL properties to be checked on the model. + * + * @return The name of the file that contains the CSL properties to be checked on the model. + */ + std::string getCslPropertiesFilename() const; + /*! * Retrieves whether the ltl option was set. * @@ -77,6 +142,13 @@ namespace storm { */ bool isLtlSet() const; + /*! + * Retrieves the name of the file that contains the LTL properties to be checked on the model. + * + * @return The name of the file that contains the LTL properties to be checked on the model. + */ + std::string getLtlPropertiesFilename() const; + /*! * Retrieves whether the transition reward option was set. * @@ -84,6 +156,14 @@ namespace storm { */ bool isTransitionRewardsSet() const; + /*! + * Retrieves the name of the file that contains the transition rewards if the model was given using the + * explicit option. + * + * @return The name of the file that contains the transition rewards. + */ + std::string getTransitionRewardsFilename() const; + /*! * Retrieves whether the state reward option was set. * @@ -91,6 +171,14 @@ namespace storm { */ bool isStateRewardsSet() const; + /*! + * Retrieves the name of the file that contains the state rewards if the model was given using the + * explicit option. + * + * @return The name of the file that contains the state rewards. + */ + std::string getStateRewardsFilename() const; + /*! * Retrieves whether the counterexample option was set. * @@ -98,6 +186,14 @@ namespace storm { */ bool isCounterexampleSet() const; + /*! + * Retrieves the name of the file to which the counterexample is to be written if the counterexample + * option was set. + * + * @return The name of the file to which the counterexample is to be written. + */ + std::string getCounterexampleFilename() const; + /*! * Retrieves whether the fix-deadlocks option was set. * @@ -111,6 +207,13 @@ namespace storm { * @return True if the timeout option was set. */ bool isTimeoutSet() const; + + /*! + * Retrieves the time after which the computation has to be aborted in case the timeout option was set. + * + * @return The number of seconds after which to timeout. + */ + uint_fast64_t getTimeoutInSeconds() const; /*! * Retrieves whether the eqsolver option was set. @@ -120,12 +223,40 @@ namespace storm { bool isEqSolverSet() const; /*! - * Retrieves whether the export-to-dot option was set. + * Retrieves whether the gmm++ equation solver is to be used. * - * @return True if the export-to-dot option was set. + * @return True iff the gmm++ equation solver is to be used. + */ + bool useGmmxxEquationSolver() const; + + /*! + * Retrieves whether the native equation solver is to be used. + * + * @return True iff the native equation solver is to be used. + */ + bool useNativeEquationSolver() const; + + /*! + * Retrieves whether the lpsolver option was set. + * + * @return True if the lpsolver option was set. */ bool isLpSolverSet() const; + /*! + * Retrieves whether glpk is to be used. + * + * @return True iff glpk is to be used. + */ + bool useGlpk() const; + + /*! + * Retrieves whether Gurobi is to be used. + * + * @return True iff Gurobi is to be used. + */ + bool useGurobi() const; + /*! * Retrieves whether the export-to-dot option was set. * @@ -133,6 +264,13 @@ namespace storm { */ bool isConstantsSet() const; + /*! + * Retrieves the string that defines the constants of a symbolic model (given via the symbolic option). + * + * @return The string that defines the constants of a symbolic model. + */ + std::string getConstantDefinitionString() const; + private: // Define the string names of the options as constants. static const std::string moduleName; diff --git a/src/settings/modules/GlpkSettings.cpp b/src/settings/modules/GlpkSettings.cpp index bbd4f53cf..ebeb91905 100644 --- a/src/settings/modules/GlpkSettings.cpp +++ b/src/settings/modules/GlpkSettings.cpp @@ -6,8 +6,16 @@ namespace storm { namespace settings { namespace modules { + const std::string GlpkSettings::moduleName = "glpk"; + const std::string GlpkSettings::outputOptionName = "output"; + GlpkSettings::GlpkSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) { - settingsManager.addOption(storm::settings::OptionBuilder("GlpkLpSolver", "glpkoutput", "", "If set, the glpk output will be printed to the command line.").build()); + // First, we need to create all options of this module. + std::vector> options; + options.push_back(storm::settings::OptionBuilder(moduleName, outputOptionName, true, "If set, the glpk output will be printed to the command line.").build()); + + // Finally, register all options that we just created. + settingsManager.registerModule(moduleName, options); } } // namespace modules diff --git a/src/settings/modules/GlpkSettings.h b/src/settings/modules/GlpkSettings.h index 79e59253b..9d0cd0f54 100644 --- a/src/settings/modules/GlpkSettings.h +++ b/src/settings/modules/GlpkSettings.h @@ -12,7 +12,24 @@ namespace storm { */ class GlpkSettings : public ModuleSettings { public: + /*! + * Creates a new set of glpk settings that is managed by the given manager. + * + * @param settingsManager The responsible manager. + */ GlpkSettings(storm::settings::SettingsManager& settingsManager); + + /*! + * Retrieves whether the output option was set. + * + * @return True iff the output option was set. + */ + bool isOutputSet() const; + + private: + // Define the string names of the options as constants. + static const std::string moduleName; + static const std::string outputOptionName; }; } // namespace modules diff --git a/src/settings/modules/GmmxxSettings.cpp b/src/settings/modules/GmmxxSettings.cpp index e7b5eede6..2dc68b3f4 100644 --- a/src/settings/modules/GmmxxSettings.cpp +++ b/src/settings/modules/GmmxxSettings.cpp @@ -6,40 +6,35 @@ namespace storm { namespace settings { namespace modules { + const std::string GmmxxSettings::moduleName = "gmm++"; + const std::string GmmxxSettings::techniqueOptionName = "tech"; + const std::string GmmxxSettings::preconditionOptionName = "precond"; + const std::string GmmxxSettings::restartOptionName = "restart"; + const std::string GmmxxSettings::maximalIterationsOptionName = "maxiter"; + const std::string GmmxxSettings::maximalIterationsOptionShortName = "maxiter"; + const std::string GmmxxSettings::precisionOptionName = "precision"; + const std::string GmmxxSettings::absoluteOptionName = "absolute"; + GmmxxSettings::GmmxxSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager) { - settingsManager.addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "digiprecision", "", "Precision used for iterative solving of linear equation systems").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("precision value", "Precision").setDefaultValueDouble(1e-4).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); - - // Offer all available methods as a command line option. - std::vector methods; - methods.push_back("bicgstab"); - methods.push_back("qmr"); - methods.push_back("gmres"); - methods.push_back("jacobi"); - settingsManager.addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "gmmlin", "", "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()); + // First, we need to create all options of this module. + std::vector> options; + std::vector methods = {"bicgstab", "qmr", "gmres", "jacobi"}; + options.push_back(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the gmm++ engine. Available are {bicgstab, qmr, gmres, jacobi}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("gmres").build()).build()); // Register available preconditioners. - std::vector preconditioner; - preconditioner.push_back("ilu"); - preconditioner.push_back("diagonal"); - preconditioner.push_back("ildlt"); - preconditioner.push_back("none"); - settingsManager.addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "gmmpre", "", "The preconditioning technique used for solving linear equation systems with the gmm++ engine. 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()); - - settingsManager.addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "gmmrestart", "", "The number of iteration until restarted methods are actually restarted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of iterations.").setDefaultValueUnsignedInteger(50).build()).build()); + std::vector preconditioner = {"ilu", "diagonal", "ildlt", "none"}; + options.push_back(storm::settings::OptionBuilder(moduleName, preconditionOptionName, true, "The preconditioning technique used for solving linear equation systems. Available are {ilu, diagonal, none}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(preconditioner)).setDefaultValueString("ilu").build()).build()); - settingsManager.addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "maxiter", "i", "The maximal number of iterations to perform before iterative solving is aborted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(10000).build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, 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()); - settingsManager.addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "precision", "", "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, 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()); - settingsManager.addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "absolute", "", "Whether the relative or the absolute error is considered for deciding convergence.").build()); + options.push_back(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); - settingsManager.addOption(storm::settings::OptionBuilder("GmmxxNondeterminsticLinearEquationSolver", "maxiter", "i", "The maximal number of iterations to perform before iterative solving is aborted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(10000).build()).build()); + options.push_back(storm::settings::OptionBuilder(moduleName, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for deciding convergence.").build()); - settingsManager.addOption(storm::settings::OptionBuilder("GmmxxNondeterminsticLinearEquationSolver", "precision", "", "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-6).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); - - settingsManager.addOption(storm::settings::OptionBuilder("GmmxxNondeterminsticLinearEquationSolver", "absolute", "", "Whether the relative or the absolute error is considered for deciding convergence.").build()); - - + // Finally, register all options that we just created. + settingsManager.registerModule(moduleName, options); } } // namespace modules diff --git a/src/settings/modules/GmmxxSettings.h b/src/settings/modules/GmmxxSettings.h index 69486b47d..7f5ad75a4 100644 --- a/src/settings/modules/GmmxxSettings.h +++ b/src/settings/modules/GmmxxSettings.h @@ -12,7 +12,78 @@ namespace storm { */ class GmmxxSettings : public ModuleSettings { public: + // An enumeration of all available techniques for solving linear equations. + enum class LinearEquationTechnique { Bicgstab, Qmr, Gmres, Jacobi }; + + // An enumeration of all available preconditioning techniques. + enum class PreconditioningTechnique { Ilu, Diagonal, Ildlt, None }; + + /*! + * Creates a new set of gmm++ settings that is managed by the given manager. + * + * @param settingsManager The responsible manager. + */ GmmxxSettings(storm::settings::SettingsManager& settingsManager); + + /*! + * Retrieves the technique that is to be used for solving systems of linear equations. + * + * @return The technique to use. + */ + LinearEquationTechnique getLinearEquationSystemTechnique() const; + + /*! + * Retrieves the technique that is to be used for preconditioning solving systems of linear equations. + * + * @return The technique to use. + */ + PreconditioningTechnique getPreconditioningTechnique() const; + + /*! + * Retrieves the number of iterations after which restarted techniques are to be restarted. + * + * @return The number of iterations after which to restart. + */ + uint_fast64_t getRestartIterationCount() const; + + /*! + * Retrieves the maximal number of iterations to perform until giving up on converging. + * + * @return The maximal iteration count. + */ + uint_fast64_t getMaximalIterationCount() const; + + /*! + * Retrieves the precision that is used for detecting convergence. + * + * @return The precision to use for detecting convergence. + */ + double getPrecision() const; + + /*! + * Retrieves whether the absolute error is used for detecting convergence. + * + * @return True iff the absolute error is used convergence detection. + */ + bool useAbsoluteConvergenceCriterion() const; + + /*! + * Retrieves whether the relative error is used for detecting convergence. + * + * @return True iff the relative error is used convergence detection. + */ + bool useRelativeConvergenceCriterion() const; + + private: + // Define the string names of the options as constants. + static const std::string moduleName; + static const std::string techniqueOptionName; + static const std::string preconditionOptionName; + static const std::string restartOptionName; + static const std::string maximalIterationsOptionName; + static const std::string maximalIterationsOptionShortName; + static const std::string precisionOptionName; + static const std::string absoluteOptionName; }; } // namespace modules diff --git a/src/settings/modules/NativeEquationSolver.cpp b/src/settings/modules/NativeEquationSolverSettings.cpp similarity index 100% rename from src/settings/modules/NativeEquationSolver.cpp rename to src/settings/modules/NativeEquationSolverSettings.cpp