Further refactoring of option system.

Former-commit-id: 350ac4c654

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";
+    }
+}

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<userValidationFunction_t> const& validationFunctions, bool isOptional, T defaultValue): ArgumentBase(argumentName, argumentDescription), argumentValue(), argumentType(ArgumentTypeInferation::inferToEnumType<T>()), validationFunctions(validationFunctions), isOptional(isOptional), defaultValue(defaultValue), hasDefaultValue(true) {
+			Argument(std::string const& name, std::string const& description, std::vector<userValidationFunction_t> const& validationFunctions, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(ArgumentTypeInferation::inferToEnumType<T>()), 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<T>(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 <typename S>
-			bool isCompatibleWith(Argument<S> 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<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.");
                 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;

src/settings/ArgumentBase.h

@@ -146,44 +146,56 @@ namespace storm {
              * whether the conversion was successful.
              */
             template <typename TargetType>
-            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<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;
-            }
+            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 <typename ValueType>
-            std::string convertToString(ValueType const& value) const {
-                std::ostringstream stream;
-                stream << value;
-                return stream.str();
-            }
+            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();
+        }
+        
 	}
 }
 

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<ArgumentBase> 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<ArgumentBase>(new Argument<std::string>(this->argumentName, this->argumentDescription, userValidationFunction_String, this->isOptional, this->defaultValue_String));
+							return std::shared_ptr<ArgumentBase>(new Argument<std::string>(this->name, this->description, userValidationFunctions_String, this->isOptional, this->defaultValue_String));
 						} else {
-							return std::shared_ptr<ArgumentBase>(new Argument<std::string>(this->argumentName, this->argumentDescription, userValidationFunction_String));
+							return std::shared_ptr<ArgumentBase>(new Argument<std::string>(this->name, this->description, userValidationFunctions_String));
 						}
 						break;
                     }
 					case ArgumentType::Integer:
 						if (this->hasDefaultValue) {
-							return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->argumentName, this->argumentDescription, userValidationFunction_Integer, this->isOptional, this->defaultValue_Integer));
+							return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->name, this->description, userValidationFunctions_Integer, this->isOptional, this->defaultValue_Integer));
 						} else {
-							return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->argumentName, this->argumentDescription, userValidationFunction_Integer));
+							return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->name, this->description, userValidationFunctions_Integer));
 						}
 						break;
 					case ArgumentType::UnsignedInteger:
 						if (this->hasDefaultValue) {
-							return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->argumentName, this->argumentDescription, userValidationFunction_UnsignedInteger, this->isOptional, this->defaultValue_UnsignedInteger));
+							return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->name, this->description, userValidationFunctions_UnsignedInteger, this->isOptional, this->defaultValue_UnsignedInteger));
 						} else {
-							return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->argumentName, this->argumentDescription, userValidationFunction_UnsignedInteger));
+							return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->name, this->description, userValidationFunctions_UnsignedInteger));
 						}
 						break;
 					case ArgumentType::Double:
 						if (this->hasDefaultValue) {
-							return std::shared_ptr<ArgumentBase>(new Argument<double>(this->argumentName, this->argumentDescription, userValidationFunction_Double, this->isOptional, this->defaultValue_Double));
+							return std::shared_ptr<ArgumentBase>(new Argument<double>(this->name, this->description, userValidationFunctions_Double, this->isOptional, this->defaultValue_Double));
 						} else {
-							return std::shared_ptr<ArgumentBase>(new Argument<double>(this->argumentName, this->argumentDescription, userValidationFunction_Double));
+							return std::shared_ptr<ArgumentBase>(new Argument<double>(this->name, this->description, userValidationFunctions_Double));
 						}
 						break;
 					case ArgumentType::Boolean:
 						if (this->hasDefaultValue) {
-							return std::shared_ptr<ArgumentBase>(new Argument<bool>(this->argumentName, this->argumentDescription, userValidationFunction_Boolean, this->isOptional, this->defaultValue_Boolean));
+							return std::shared_ptr<ArgumentBase>(new Argument<bool>(this->name, this->description, userValidationFunctions_Boolean, this->isOptional, this->defaultValue_Boolean));
 						} else {
-							return std::shared_ptr<ArgumentBase>(new Argument<bool>(this->argumentName, this->argumentDescription, userValidationFunction_Boolean));
+							return std::shared_ptr<ArgumentBase>(new Argument<bool>(this->name, this->description, userValidationFunctions_Boolean));
 						}
 						break;
 				}

src/settings/ArgumentTypeInferationHelper.cpp

@@ -0,0 +1,90 @@
+#include "src/settings/ArgumentTypeInferationHelper.h"
+
+namespace storm {
+    namespace settings {
+        template <typename T>
+        ArgumentType ArgumentTypeInferation::inferToEnumType() {
+            LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer type of argument.");
+        }
+        
+        template <>
+        ArgumentType ArgumentTypeInferation::inferToEnumType<std::string>() {
+            return ArgumentType::String;
+        }
+        
+        template <>
+        ArgumentType ArgumentTypeInferation::inferToEnumType<int_fast64_t>() {
+            return ArgumentType::Integer;
+        }
+        
+        template <>
+        ArgumentType ArgumentTypeInferation::inferToEnumType<uint_fast64_t>() {
+            return ArgumentType::UnsignedInteger;
+        }
+        
+        template <>
+        ArgumentType ArgumentTypeInferation::inferToEnumType<double>() {
+            return ArgumentType::Double;
+        }
+        
+        template <>
+        ArgumentType ArgumentTypeInferation::inferToEnumType<bool>() {
+            return ArgumentType::Boolean;
+        }
+        
+        template <typename T>
+        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<std::string>(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 <typename T>
+        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<int_fast64_t>(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 <typename T>
+        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<uint_fast64_t>(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 <typename T>
+        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<double>(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 <typename T>
+        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<bool>(ArgumentType const& argumentType, bool const& value) {
+            LOG_THROW(argumentType == ArgumentType::Boolean, storm::exceptions::InternalTypeErrorException, "Unable to infer boolean from non-boolean argument.");
+            return value;
+        }
+    }
+}

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 <cstdint>
 #include <string>
 
-#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 <typename T>
 			static ArgumentType inferToEnumType();
 
-			// Specialized function templates that allow casting using the Enum Class as Target
-			template <typename T> static std::string	inferToString(ArgumentType argumentType, T value);
-			template <typename T> static int_fast64_t	inferToInteger(ArgumentType argumentType, T value);
-			template <typename T> static uint_fast64_t	inferToUnsignedInteger(ArgumentType argumentType, T value);
-			template <typename T> static double			inferToDouble(ArgumentType argumentType, T value);
-			template <typename T> 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 <typename T> static std::string const& inferToString(ArgumentType const& argumentType, T const& value);
+			template <typename T> static int_fast64_t inferToInteger(ArgumentType const& argumentType, T const& value);
+			template <typename T> static uint_fast64_t inferToUnsignedInteger(ArgumentType const& argumentType, T const& value);
+			template <typename T> static double inferToDouble(ArgumentType const& argumentType, T const& value);
+			template <typename T> static bool inferToBoolean(ArgumentType const& argumentType, T const& value);
 		};
-
-		/*
-		 *	All functions related to the EnumType Inferation from the Template Parameter
-		 */
-		template <typename T> 
-		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<std::string>() {
-			return ArgumentType::String;
-		}
-		template <> inline ArgumentType ArgumentTypeInferation::inferToEnumType<int_fast64_t>() {
-			return ArgumentType::Integer;
-		}
-		template <> inline ArgumentType ArgumentTypeInferation::inferToEnumType<uint_fast64_t>() {
-			return ArgumentType::UnsignedInteger;
-		}
-		template <> inline ArgumentType ArgumentTypeInferation::inferToEnumType<double>() {
-			return ArgumentType::Double;
-		}
-		template <> inline ArgumentType ArgumentTypeInferation::inferToEnumType<bool>() {
-			return ArgumentType::Boolean;
-		}
-		
-		/*
-		 *	All functions related to the conversion to std::string based on the Template and Enum Type
-		 */
-		template <typename T> 
-		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<std::string>(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 <typename T> 
-		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<int_fast64_t>(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 <typename T> 
-		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<uint_fast64_t>(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 <typename T> 
-		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<double>(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 <typename T> 
-		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<bool>(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_

src/settings/ArgumentValidators.h

@@ -12,6 +12,8 @@
 #include <string>
 
 #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<bool (int_fast64_t const&)> integerRangeValidatorIncluding(int_fast64_t const lowerBound, int_fast64_t const upperBound) {
+			static std::function<bool (int_fast64_t const&)> integerRangeValidatorIncluding(int_fast64_t lowerBound, int_fast64_t upperBound) {
 				return rangeValidatorIncluding<int_fast64_t>(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<bool (int_fast64_t const&)> integerRangeValidatorExcluding(int_fast64_t const lowerBound, int_fast64_t const upperBound) {
+			static std::function<bool (int_fast64_t const&)> integerRangeValidatorExcluding(int_fast64_t lowerBound, int_fast64_t upperBound) {
 				return rangeValidatorExcluding<int_fast64_t>(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<bool (uint_fast64_t const&)> unsignedIntegerRangeValidatorIncluding(uint_fast64_t const lowerBound, uint_fast64_t const upperBound) {
+			static std::function<bool (uint_fast64_t const&)> unsignedIntegerRangeValidatorIncluding(uint_fast64_t lowerBound, uint_fast64_t upperBound) {
 				return rangeValidatorIncluding<uint_fast64_t>(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<bool (uint_fast64_t const&)> unsignedIntegerRangeValidatorExcluding(uint_fast64_t const lowerBound, uint_fast64_t const upperBound) {
+			static std::function<bool (uint_fast64_t const&)> unsignedIntegerRangeValidatorExcluding(uint_fast64_t lowerBound, uint_fast64_t upperBound) {
 				return rangeValidatorExcluding<uint_fast64_t>(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<bool (double const&)> doubleRangeValidatorIncluding(double const lowerBound, double const upperBound) {
+			static std::function<bool (double const&)> doubleRangeValidatorIncluding(double lowerBound, double upperBound) {
 				return rangeValidatorIncluding<double>(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<bool (double const&)> doubleRangeValidatorExcluding(double const lowerBound, double const upperBound) {
+			static std::function<bool (double const&)> doubleRangeValidatorExcluding(double lowerBound, double upperBound) {
 				return rangeValidatorExcluding<double>(lowerBound, upperBound);
 			}
 
@@ -106,11 +108,9 @@ namespace storm {
              * @return The resulting validation function.
              */
 			static std::function<bool (std::string const&)> stringInListValidator(std::vector<std::string> 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<typename T>
-			static std::function<bool (T const)> 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<bool (T const&)> 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<typename T>
-			static std::function<bool (T const)> 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<bool (T const&)> 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);
 			}
 		};
 	}

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<storm::settings::Argument<std::string>&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<std::string>&>(secondArgument));
+							static_cast<storm::settings::Argument<std::string> const&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<std::string> const&>(secondArgument));
 							break;
 						case ArgumentType::Integer:
-							static_cast<storm::settings::Argument<int_fast64_t>&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<int_fast64_t>&>(secondArgument));
+							static_cast<storm::settings::Argument<int_fast64_t> const&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<int_fast64_t> const&>(secondArgument));
 							break;
 						case ArgumentType::UnsignedInteger:
-							static_cast<storm::settings::Argument<uint_fast64_t>&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<uint_fast64_t>&>(secondArgument));
+							static_cast<storm::settings::Argument<uint_fast64_t> const&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<uint_fast64_t> const&>(secondArgument));
 							break;
 						case ArgumentType::Double:
-							static_cast<storm::settings::Argument<double>&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<double>&>(secondArgument));
+							static_cast<storm::settings::Argument<double> const&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<double> const&>(secondArgument));
 							break;
 						case ArgumentType::Boolean:
-							static_cast<storm::settings::Argument<bool>&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<bool>&>(secondArgument));
+							static_cast<storm::settings::Argument<bool> const&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<bool> 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<ArgumentBase>(*i));
+                    argumentNameMap.emplace(argument->getName(), argument);
                 }
             }
             

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);

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 <iostream>
 #include <sstream>
@@ -10,7 +10,6 @@
 #include <vector>
 #include <memory>
 
-
 #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<std::string, std::string> stringPair_t;
-        typedef std::pair<bool, std::string> 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 // 
+#endif /* STORM_SETTINGS_SETTINGSMANAGER_H_ */

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<std::string> 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<std::shared_ptr<Option>> options;
+                std::vector<std::string> techniques = {"sat", "milp"};
+                options.push_back(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command set. Note that this requires the model to be given in a symbolic format.")
+                                .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

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

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<std::shared_ptr<Option>> options;
+                options.push_back(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
                 
-                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<std::string> 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

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

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<std::shared_ptr<Option>> options;
+                options.push_back(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Print debug output.").build());
+                options.push_back(storm::settings::OptionBuilder(moduleName, traceOptionName, false, "Print even more debug output.").build());
+                options.push_back(storm::settings::OptionBuilder(moduleName, logfileOptionName, false, "If specified, the log output will also be written to this file.").setShortName(logfileOptionShortName)
+                                          .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

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

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<std::shared_ptr<Option>> 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<std::string> moduleNames = {"all", "general", "debug", "cudd", "counterexample", "glpk", "gurobi", "gmm++", "native"};
+                options.push_back(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
+                                  .addArgument(storm::settings::ArgumentBuilder::createStringArgument("module", "The module for which to show the help or 'all' for all modules.").setDefaultValueString("all").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(moduleNames)).build()).build());
+                options.push_back(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build());
                 options.push_back(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.")
                                   .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
-                options.push_back(storm::settings::OptionBuilder(moduleName, configOptionName, 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<std::string> 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<std::string> linearEquationSolver = {"gmm++", "native"};
+                options.push_back(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.")
                                   .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build());
-                options.push_back(storm::settings::OptionBuilder(moduleName, timeoutOptionName, 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<std::string> 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<std::string> lpSolvers = {"gurobi", "glpk"};
+                options.push_back(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.")
                                   .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build());
-                options.push_back(storm::settings::OptionBuilder(moduleName, constantsOptionName, 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.

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;

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<std::shared_ptr<Option>> options;
+                options.push_back(storm::settings::OptionBuilder(moduleName, outputOptionName, true, "If set, the glpk output will be printed to the command line.").build());
+                
+                // Finally, register all options that we just created.
+                settingsManager.registerModule(moduleName, options);
             }
             
         } // namespace modules

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

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<std::string> 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<std::shared_ptr<Option>> options;
+                std::vector<std::string> methods = {"bicgstab", "qmr", "gmres", "jacobi"};
+                options.push_back(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the gmm++ engine. Available are {bicgstab, qmr, gmres, jacobi}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("gmres").build()).build());
                 
                 // Register available preconditioners.
-                std::vector<std::string> 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<std::string> preconditioner = {"ilu", "diagonal", "ildlt", "none"};
+                options.push_back(storm::settings::OptionBuilder(moduleName, preconditionOptionName, true, "The preconditioning technique used for solving linear equation systems. Available are {ilu, diagonal, none}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(preconditioner)).setDefaultValueString("ilu").build()).build());
                 
-                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

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