beautified help message printing. all requirements and default values are now printed automatically for all options

src/storm/settings/Argument.cpp

@@ -9,148 +9,190 @@
 #include "storm/utility/macros.h"
 
 namespace storm {
-	namespace settings {
-      
+    namespace settings {
+        
         template<typename T>
-			Argument<T>::Argument(std::string const& name, std::string const& description, std::vector<std::shared_ptr<ArgumentValidator<T>>> const& validators): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validators(validators), isOptional(false), defaultValue(), hasDefaultValue(false) {
-                // Intentionally left empty.
-			}
-            
-           template<typename T>
-            Argument<T>::Argument(std::string const& name, std::string const& description, std::vector<std::shared_ptr<ArgumentValidator<T>>> const& validators, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validators(validators), isOptional(isOptional), defaultValue(), hasDefaultValue(true) {
-                this->setDefaultValue(defaultValue);
+        Argument<T>::Argument(std::string const& name, std::string const& description, std::vector<std::shared_ptr<ArgumentValidator<T>>> const& validators): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validators(validators), isOptional(false), defaultValue(), hasDefaultValue(false) {
+            // Intentionally left empty.
+        }
+        
+        template<typename T>
+        Argument<T>::Argument(std::string const& name, std::string const& description, std::vector<std::shared_ptr<ArgumentValidator<T>>> const& validators, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validators(validators), isOptional(isOptional), defaultValue(), hasDefaultValue(true) {
+            this->setDefaultValue(defaultValue);
+        }
+        
+        template<typename T>
+        bool Argument<T>::getIsOptional() const  {
+            return this->isOptional;
+        }
+        
+        template<typename T>
+        bool Argument<T>::setFromStringValue(std::string const& fromStringValue)  {
+            bool conversionOk = false;
+            T newValue = ArgumentBase::convertFromString<T>(fromStringValue, conversionOk);
+            if (!conversionOk) {
+                return false;
             }
-            
-           template<typename T>
-		    bool Argument<T>::getIsOptional() const  {
-                return this->isOptional;
+            return this->setFromTypeValue(newValue);
+        }
+        
+        template<typename T>
+        bool Argument<T>::setFromTypeValue(T const& newValue, bool hasBeenSet) {
+            if (!this->validate(newValue)) {
+                return false;
             }
-            
-			template<typename T>
-            bool Argument<T>::setFromStringValue(std::string const& fromStringValue)  {
-				bool conversionOk = false;
-				T newValue = ArgumentBase::convertFromString<T>(fromStringValue, conversionOk);
-				if (!conversionOk) {
-                    return false;
-				}
-				return this->setFromTypeValue(newValue);
-			}
-            
-			template<typename T>
-            bool Argument<T>::setFromTypeValue(T const& newValue, bool hasBeenSet) {
-				if (!this->validate(newValue)) {
-                    return false;
-				}
-				this->argumentValue = newValue;
-				this->hasBeenSet = hasBeenSet;
-				return true;
-			}
-            
-			template<typename T>
-            ArgumentType Argument<T>::getType() const  {
-				return this->argumentType;
-			}
-            
-			template<typename T>
-            T const& Argument<T>::getArgumentValue() const {
-                STORM_LOG_THROW(this->getHasBeenSet() || this->getHasDefaultValue(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve value of argument '" << this->getName() << "', because it was neither set nor specifies a default value.");
-                if (this->getHasBeenSet()) {
-                    return this->argumentValue;
-                } else {
-                    return this->defaultValue;
-                }
-			}
-            
-			template<typename T>
-            bool Argument<T>::getHasDefaultValue() const  {
-				return this->hasDefaultValue;
-			}
-            
-			template<typename T>
-            void Argument<T>::setFromDefaultValue()  {
-                STORM_LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to set value from default value, because the argument has none.");
-				bool result = this->setFromTypeValue(this->defaultValue, false);
-                STORM_LOG_THROW(result, storm::exceptions::IllegalArgumentValueException, "Unable to assign default value to argument, because it was rejected.");
-			}
-            
-			template<typename T>
-            std::string Argument<T>::getValueAsString() const  {
-				switch (this->argumentType) {
-					case ArgumentType::String:
-						return inferToString(ArgumentType::String, this->getArgumentValue());
-					case ArgumentType::Boolean: {
-						bool iValue = inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
-						if (iValue) {
-							return "true";
-						} else {
-							return "false";
-						}
-					}
-					default: return ArgumentBase::convertToString(this->argumentValue);
-				}
-			}
-			
-			template<typename T>
-            int_fast64_t Argument<T>::getValueAsInteger() const  {
-				switch (this->argumentType) {
-					case ArgumentType::Integer:
-						return inferToInteger(ArgumentType::Integer, this->getArgumentValue());
-					default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as integer."); break;
-                }
+            this->argumentValue = newValue;
+            this->hasBeenSet = hasBeenSet;
+            return true;
+        }
+        
+        template<typename T>
+        ArgumentType Argument<T>::getType() const  {
+            return this->argumentType;
+        }
+        
+        template<typename T>
+        T const& Argument<T>::getArgumentValue() const {
+            STORM_LOG_THROW(this->getHasBeenSet() || this->getHasDefaultValue(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve value of argument '" << this->getName() << "', because it was neither set nor specifies a default value.");
+            if (this->getHasBeenSet()) {
+                return this->argumentValue;
+            } else {
+                return this->defaultValue;
             }
-            
-            
-            template<typename T>
-            uint_fast64_t Argument<T>::getValueAsUnsignedInteger() const  {
-                switch (this->argumentType) {
-                    case ArgumentType::UnsignedInteger:
-                        return inferToUnsignedInteger(ArgumentType::UnsignedInteger, this->getArgumentValue());
-                    default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as unsigned integer."); break;
+        }
+        
+        template<typename T>
+        bool Argument<T>::getHasDefaultValue() const  {
+            return this->hasDefaultValue;
+        }
+        
+        template<typename T>
+        void Argument<T>::setFromDefaultValue()  {
+            STORM_LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to set value from default value, because the argument has none.");
+            bool result = this->setFromTypeValue(this->defaultValue, false);
+            STORM_LOG_THROW(result, storm::exceptions::IllegalArgumentValueException, "Unable to assign default value to argument, because it was rejected.");
+        }
+        
+        template<typename T>
+        std::string Argument<T>::getValueAsString() const  {
+            switch (this->argumentType) {
+                case ArgumentType::String:
+                    return inferToString(ArgumentType::String, this->getArgumentValue());
+                case ArgumentType::Boolean: {
+                    bool iValue = inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
+                    if (iValue) {
+                        return "true";
+                    } else {
+                        return "false";
+                    }
                 }
+                default: return ArgumentBase::convertToString(this->argumentValue);
             }
-            
-            
-            template<typename T>
-            double Argument<T>::getValueAsDouble() const  {
-                switch (this->argumentType) {
-                    case ArgumentType::Double:
-                        return inferToDouble(ArgumentType::Double, this->getArgumentValue());
-                    default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as double."); break;
-                }
+        }
+        
+        template<typename T>
+        int_fast64_t Argument<T>::getValueAsInteger() const  {
+            switch (this->argumentType) {
+                case ArgumentType::Integer:
+                    return inferToInteger(ArgumentType::Integer, this->getArgumentValue());
+                default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as integer."); break;
             }
-            
-            template<typename T>
-            bool Argument<T>::getValueAsBoolean() const  {
-                switch (this->argumentType) {
-                    case ArgumentType::Boolean:
-                        return inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
-                    default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as boolean."); break;
-                }
+        }
+        
+        
+        template<typename T>
+        uint_fast64_t Argument<T>::getValueAsUnsignedInteger() const  {
+            switch (this->argumentType) {
+                case ArgumentType::UnsignedInteger:
+                    return inferToUnsignedInteger(ArgumentType::UnsignedInteger, this->getArgumentValue());
+                default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as unsigned integer."); break;
             }
-    
-           
-            template<typename T>
-            void Argument<T>::setDefaultValue(T const& newDefault) {
-                STORM_LOG_THROW(this->validate(newDefault), storm::exceptions::IllegalArgumentValueException, "The default value for the argument did not pass all validation functions.");
-                this->defaultValue = newDefault;
-                this->hasDefaultValue = true;
+        }
+        
+        
+        template<typename T>
+        double Argument<T>::getValueAsDouble() const  {
+            switch (this->argumentType) {
+                case ArgumentType::Double:
+                    return inferToDouble(ArgumentType::Double, this->getArgumentValue());
+                default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as double."); break;
             }
-                        
-            
-            template<typename T>
-            bool Argument<T>::validate(T const& value) const {
-                bool result = true;
-                for (auto const& validator : validators) {
-                    result &= validator->isValid(value);
+        }
+        
+        template<typename T>
+        bool Argument<T>::getValueAsBoolean() const  {
+            switch (this->argumentType) {
+                case ArgumentType::Boolean:
+                    return inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
+                default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as boolean."); break;
+            }
+        }
+        
+        
+        template<typename T>
+        void Argument<T>::setDefaultValue(T const& newDefault) {
+            STORM_LOG_THROW(this->validate(newDefault), storm::exceptions::IllegalArgumentValueException, "The default value for the argument did not pass all validation functions.");
+            this->defaultValue = newDefault;
+            this->hasDefaultValue = true;
+        }
+        
+        
+        template<typename T>
+        bool Argument<T>::validate(T const& value) const {
+            bool result = true;
+            for (auto const& validator : validators) {
+                result &= validator->isValid(value);
+            }
+            return result;
+        }
+        
+        template<typename T>
+        void printValue(std::ostream& out, T const& value) {
+            out << value;
+        }
+
+        template<>
+        void printValue(std::ostream& out, std::string const& value) {
+            if (value.empty()) {
+                out << "empty";
+            } else {
+                out << value;
+            }
+        }
+
+        template<typename T>
+        void Argument<T>::printToStream(std::ostream& out) const {
+            out << std::setw(0) << std::left << "<" << this->getName() << ">";
+            if (!this->validators.empty() || this->hasDefaultValue) {
+                out << " (";
+                if (!this->validators.empty()) {
+                    for (uint64_t i = 0; i < this->validators.size(); ++i) {
+                        out << this->validators[i]->toString();
+                        if (i + 1 < this->validators.size()) {
+                            out << ", ";
+                        }
+                    }
+                    
+                    if (this->hasDefaultValue) {
+                        out << "; ";
+                    }
                 }
-                return result;
+                
+                if (this->hasDefaultValue) {
+                    out << "default: ";
+                    printValue(out, defaultValue);
+                }
+                out << ")";
             }
             
-            template class Argument<std::string>;
-            template class Argument<int_fast64_t>;
-            template class Argument<uint_fast64_t>;
-            template class Argument<double>;
-            template class Argument<bool>;
+            out << ": " << this->getDescription();
+        }
+        
+        template class Argument<std::string>;
+        template class Argument<int_fast64_t>;
+        template class Argument<uint_fast64_t>;
+        template class Argument<double>;
+        template class Argument<bool>;
     }
 }
-        
+

src/storm/settings/Argument.h

@@ -95,6 +95,8 @@ namespace storm {
             
             virtual bool getValueAsBoolean() const override;
             
+            virtual void printToStream(std::ostream& out) const override;
+            
         private:
             // The value of the argument (in case it has been set).
             T argumentValue;

src/storm/settings/ArgumentBase.cpp

@@ -6,21 +6,8 @@
 
 namespace storm {
     namespace settings {
-        uint_fast64_t ArgumentBase::getPrintLength() const {
-            return this->getName().length() + 2;
-        }
-        
         std::ostream& operator<<(std::ostream& out, ArgumentBase const& argument) {
-            uint_fast64_t width = static_cast<uint_fast64_t>(out.width());
-            uint_fast64_t charactersPrinted = 0;
-            out << std::setw(0) << std::left << "<" << argument.getName() << "> ";
-            charactersPrinted += 2 + argument.getName().length();
-    
-            for (uint_fast64_t i = charactersPrinted; i < width; ++i) {
-                out << out.fill();
-            }
-            
-            out << "\t" << argument.getDescription();
+            argument.printToStream(out);
             return out;
         }
         

src/storm/settings/ArgumentBase.h

@@ -128,11 +128,9 @@ namespace storm {
 			virtual bool getValueAsBoolean() const = 0;
             
             /*!
-             * Retrieves the (print) length of the argument.
-             *
-             * @return The length of the argument.
+             * Prints a string representation of the argument to the provided stream.
              */
-            uint_fast64_t getPrintLength() const;
+            virtual void printToStream(std::ostream& out) const = 0;
             
             friend std::ostream& operator<<(std::ostream& out, ArgumentBase const& argument);
             

src/storm/settings/Option.cpp

@@ -140,12 +140,13 @@ namespace storm {
                 length += this->getModuleName().length() + 1;
                 length += this->getLongName().length();
                 if (this->getHasShortName()) {
-                    length += 4;
-                    if (!this->getRequiresModulePrefix()) {
-                        length += 2;
+                    length += this->getShortName().length() + 3;
+                }
+                
+                if (this->getArgumentCount() > 0) {
+                    for (auto const& argument : this->getArguments()) {
+                        length += argument->getName().size() + 3;
                     }
-                    length += this->getModuleName().length() + 1;
-                    length += this->getShortName().length();
                 }
                 return length;
             }
@@ -164,7 +165,7 @@ namespace storm {
                 out << "[";
                 ++charactersPrinted;
             }
-            out <<  option.getModuleName() << ":";
+            out << option.getModuleName() << ":";
             charactersPrinted += option.getModuleName().length() + 1;
             if (!option.getRequiresModulePrefix()) {
                 out << "]";
@@ -173,42 +174,32 @@ namespace storm {
             out << option.getLongName();
             charactersPrinted += option.getLongName().length();
             if (option.getHasShortName()) {
-                out << " | -";
-                charactersPrinted += 4;
-                if (!option.getRequiresModulePrefix()) {
-                    out << "[";
-                    ++charactersPrinted;
-                }
-                out << option.getModuleName() << ":";
-                charactersPrinted += option.getModuleName().length() + 1;
-                if (!option.getRequiresModulePrefix()) {
-                    out << "]";
-                    ++charactersPrinted;
-                }
-                out << option.getShortName();
-                charactersPrinted += option.getShortName().length();
+                out << " (" << option.getShortName() << ")";
+                charactersPrinted += option.getShortName().length() + 3;
             }
             
-            // Now fill the width.
-            for (uint_fast64_t i = charactersPrinted; i < width; ++i) {
-                out << out.fill();
-            }
-            
-            out << "\t" << option.getDescription();
-            
             if (option.getArgumentCount() > 0) {
-                // Start by determining the longest print length of the arguments.
-                uint_fast64_t maxLength = 0;
                 for (auto const& argument : option.getArguments()) {
-                    maxLength = std::max(maxLength, argument->getPrintLength());
+                    out << " <" << argument->getName() << ">";
+                    charactersPrinted += argument->getName().size() + 3;
                 }
-                
-                for (auto const& argument : option.getArguments()) {
-                    out << std::endl;
-                    out << "\t* " << std::setw(maxLength) << std::left << *argument;
+            }
+            
+            // Now fill the width.
+            for (uint_fast64_t i = charactersPrinted; i < width; ++i) {
+                if (i == charactersPrinted) {
+                    out << " ";
+                } else {
+                    out << ".";
                 }
             }
+
+            out << " " << option.getDescription();
             
+            for (auto const& argument : option.getArguments()) {
+                out << " " << *argument;
+            }
+
             return out;
         }
     }

src/storm/settings/modules/AbstractionSettings.cpp

@@ -25,24 +25,24 @@ namespace storm {
                 std::vector<std::string> onOff = {"on", "off"};
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, useDecompositionOptionName, true, "Sets whether to apply decomposition during the abstraction.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag ('on' or 'off').").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
                                              .setDefaultValueString("on").build())
                                 .build());
                 
                 std::vector<std::string> splitModes = {"all", "none", "non-guard"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, splitModeOptionName, true, "Sets which predicates are split into atoms for the refinement.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The split mode: 'all', 'none' or 'non-guard'.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(splitModes))
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(splitModes))
                                              .setDefaultValueString("all").build())
                                 .build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag ('on' or 'off').").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
                                              .setDefaultValueString("on").build())
                                 .build());
                 
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, useInterpolationOptionName, true, "Sets whether interpolation is to be used to eliminate spurious pivot blocks.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag ('on' or 'off').").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
                                              .setDefaultValueString("on").build())
                                 .build());
                 
@@ -50,12 +50,12 @@ namespace storm {
                 
                 std::vector<std::string> pivotHeuristic = {"nearest-max-dev", "most-prob-path", "max-weighted-dev"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, pivotHeuristicOptionName, true, "Sets the pivot selection heuristic.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available heuristic. Available are: 'nearest-max-dev', 'most-prob-path' and 'max-weighted-dev'.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(pivotHeuristic))
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available heuristic.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(pivotHeuristic))
                                              .setDefaultValueString("nearest-max-dev").build()).build());
                 
                 std::vector<std::string> reuseModes = {"all", "none", "qualitative", "quantitative"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, reuseResultsOptionName, true, "Sets whether to reuse all results.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The reuse mode: 'all', 'none', 'qualitative' or 'quantitative'.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reuseModes))
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reuseModes))
                                              .setDefaultValueString("all").build())
                                 .build());
             }

src/storm/settings/modules/BisimulationSettings.cpp

@@ -15,7 +15,7 @@ namespace storm {
             
             BisimulationSettings::BisimulationSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> types = { "strong", "weak" };
-                this->addOption(storm::settings::OptionBuilder(moduleName, typeOptionName, true, "Sets the kind of bisimulation quotienting used. Available are: { strong, weak }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(types)).setDefaultValueString("strong").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, typeOptionName, true, "Sets the kind of bisimulation quotienting used.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(types)).setDefaultValueString("strong").build()).build());
             }
             
             bool BisimulationSettings::isStrongBisimulationSet() const {

src/storm/settings/modules/CoreSettings.cpp

@@ -33,40 +33,35 @@ namespace storm {
             const std::string CoreSettings::cudaOptionName = "cuda";
             
             CoreSettings::CoreSettings() : ModuleSettings(moduleName), engine(CoreSettings::Engine::Sparse) {
-                this->addOption(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.").setDefaultValueString("-").setIsOptional(true).build()).setShortName(counterexampleOptionShortName).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model.").setShortName(counterexampleOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build());
                 
                 std::vector<std::string> engines = {"sparse", "hybrid", "dd", "expl", "abs"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName)
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd, expl, abs}.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(engines)).setDefaultValueString("sparse").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(engines)).setDefaultValueString("sparse").build()).build());
                 
                 std::vector<std::string> linearEquationSolver = {"gmm++", "native", "eigen", "elimination"};
                 this->addOption(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++, native, eigen, elimination.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build());
                 
                 std::vector<std::string> ddLibraries = {"cudd", "sylvan"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, ddLibraryOptionName, false, "Sets which library is preferred for decision-diagram operations.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the library to prefer. Available are: cudd and sylvan.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(ddLibraries)).setDefaultValueString("cudd").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the library to prefer.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(ddLibraries)).setDefaultValueString("cudd").build()).build());
                 
                 std::vector<std::string> lpSolvers = {"gurobi", "glpk"};
                 this->addOption(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.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(lpSolvers)).setDefaultValueString("glpk").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(lpSolvers)).setDefaultValueString("glpk").build()).build());
                 std::vector<std::string> smtSolvers = {"z3", "mathsat"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, smtSolverOptionName, false, "Sets which SMT solver is preferred.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an SMT solver. Available are: z3 and mathsat.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(smtSolvers)).setDefaultValueString("z3").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an SMT solver.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(smtSolvers)).setDefaultValueString("z3").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, false, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, cudaOptionName, false, "Sets whether to use CUDA to speed up computation time.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, cudaOptionName, false, "Sets whether to use CUDA.").build());
             }
 
             bool CoreSettings::isCounterexampleSet() const {
                 return this->getOption(counterexampleOptionName).getHasOptionBeenSet();
             }
             
-            std::string CoreSettings::getCounterexampleFilename() const {
-                return this->getOption(counterexampleOptionName).getArgumentByName("filename").getValueAsString();
-            }
-            
             bool CoreSettings::isDontFixDeadlocksSet() const {
                 return this->getOption(dontFixDeadlockOptionName).getHasOptionBeenSet();
             }

src/storm/settings/modules/CounterexampleGeneratorSettings.cpp

@@ -20,7 +20,7 @@ namespace storm {
             CounterexampleGeneratorSettings::CounterexampleGeneratorSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> techniques = {"maxsat", "milp"};
                 this->addOption(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("method", "Sets which technique is used to derive the counterexample. Available are {milp, maxsat}").setDefaultValueString("maxsat").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(techniques)).build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample.").setDefaultValueString("maxsat").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(techniques)).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based minimal command counterexample generation.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build());
             }

src/storm/settings/modules/CuddSettings.cpp

@@ -43,7 +43,7 @@ namespace storm {
                 reorderingTechniques.push_back("annealing");
                 reorderingTechniques.push_back("genetic");
                 reorderingTechniques.push_back("exact");
-                this->addOption(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").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reorderingTechniques)).build()).build());
+                this->addOption(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.").setDefaultValueString("gsift").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reorderingTechniques)).build()).build());
             }
             
             double CuddSettings::getConstantPrecision() const {

src/storm/settings/modules/EigenEquationSolverSettings.cpp

@@ -26,11 +26,11 @@ namespace storm {
             
             EigenEquationSolverSettings::EigenEquationSolverSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = {"sparselu", "bicgstab", "dgmres", "gmres"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the eigen solver. Available are {sparselu, bicgstab, dgmres, gmres}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("sparselu").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the eigen solver.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("sparselu").build()).build());
                 
                 // Register available preconditioners.
                 std::vector<std::string> preconditioner = {"ilu", "diagonal", "none"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, preconditionOptionName, true, "The preconditioning technique used for solving linear equation systems. Available are {ilu, diagonal, none}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(preconditioner)).setDefaultValueString("ilu").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, preconditionOptionName, true, "The preconditioning technique used for solving linear equation systems.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(preconditioner)).setDefaultValueString("ilu").build()).build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, restartOptionName, true, "The number of iteration until restarted methods are actually restarted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of iterations.").setDefaultValueUnsignedInteger(50).build()).build());
 

src/storm/settings/modules/EliminationSettings.cpp

@@ -21,10 +21,10 @@ namespace storm {
             
             EliminationSettings::EliminationSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> orders = {"fw", "fwrev", "bw", "bwrev", "rand", "spen", "dpen", "regex"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, eliminationOrderOptionName, true, "The order that is to be used for the elimination techniques. Available are {fw, fwrev, bw, bwrev, rand, spen, dpen, regex}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the order in which states are chosen for elimination.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(orders)).setDefaultValueString("fwrev").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, eliminationOrderOptionName, true, "The order that is to be used for the elimination techniques.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the order in which states are chosen for elimination.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(orders)).setDefaultValueString("fwrev").build()).build());
                 
                 std::vector<std::string> methods = {"state", "hybrid"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, eliminationMethodOptionName, true, "The elimination technique to use. Available are {state, hybrid}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the elimination technique to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("state").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, eliminationMethodOptionName, true, "The elimination technique to use.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the elimination technique to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("state").build()).build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, entryStatesLastOptionName, true, "Sets whether the entry states are eliminated last.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, maximalSccSizeOptionName, true, "Sets the maximal size of the SCCs for which state elimination is applied.")

src/storm/settings/modules/ExplorationSettings.cpp

@@ -23,12 +23,12 @@ namespace storm {
             
             ExplorationSettings::ExplorationSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> types = { "local", "global" };
-                    this->addOption(storm::settings::OptionBuilder(moduleName, precomputationTypeOptionName, true, "Sets the kind of precomputation used. Available are: { local, global }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(types)).setDefaultValueString("global").build()).build());
+                    this->addOption(storm::settings::OptionBuilder(moduleName, precomputationTypeOptionName, true, "Sets the kind of precomputation used.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(types)).setDefaultValueString("global").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, numberOfExplorationStepsUntilPrecomputationOptionName, true, "Sets the number of exploration steps to perform until a precomputation is triggered.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of exploration steps to perform.").setDefaultValueUnsignedInteger(100000).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, numberOfSampledPathsUntilPrecomputationOptionName, true, "If set, a precomputation is perfomed periodically after the given number of paths has been sampled.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of paths to sample until a precomputation is triggered.").setDefaultValueUnsignedInteger(100000).build()).build());
                 
                 std::vector<std::string> nextStateHeuristics = { "probdiffs", "prob", "unif" };
-                this->addOption(storm::settings::OptionBuilder(moduleName, nextStateHeuristicOptionName, true, "Sets the next-state heuristic to use. Available are: { probdiffs, prob, unif } where 'prob' samples according to the probabilities in the system, 'probdiffs' takes into account probabilities and the differences between the current bounds and 'unif' samples uniformly.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the heuristic to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(nextStateHeuristics)).setDefaultValueString("probdiffs").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, nextStateHeuristicOptionName, true, "Sets the next-state heuristic to use.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the heuristic to use. 'prob' samples according to the probabilities in the system, 'probdiffs' takes into account probabilities and the differences between the current bounds and 'unif' samples uniformly.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(nextStateHeuristics)).setDefaultValueString("probdiffs").build()).build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision to achieve.").setShortName(precisionOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The value to use to determine convergence.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());

src/storm/settings/modules/GmmxxEquationSolverSettings.cpp

@@ -27,11 +27,11 @@ namespace storm {
 
             GmmxxEquationSolverSettings::GmmxxEquationSolverSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = {"bicgstab", "qmr", "gmres", "jacobi"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the gmm++ engine. Available are {bicgstab, qmr, gmres, jacobi}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("gmres").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the gmm++ engine.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("gmres").build()).build());
                 
                 // Register available preconditioners.
                 std::vector<std::string> preconditioner = {"ilu", "diagonal", "none"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, preconditionOptionName, true, "The preconditioning technique used for solving linear equation systems. Available are {ilu, diagonal, none}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(preconditioner)).setDefaultValueString("ilu").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, preconditionOptionName, true, "The preconditioning technique used for solving linear equation systems.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(preconditioner)).setDefaultValueString("ilu").build()).build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, restartOptionName, true, "The number of iteration until restarted methods are actually restarted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of iterations.").setDefaultValueUnsignedInteger(50).build()).build());
                 

src/storm/settings/modules/IOSettings.cpp

@@ -62,7 +62,7 @@ namespace storm {
 
                 std::vector<std::string> explorationOrders = {"dfs", "bfs"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName)
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose. Available are: dfs and bfs.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build());
 
                 this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, false, "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 + ").")

src/storm/settings/modules/MinMaxEquationSolverSettings.cpp

@@ -21,7 +21,7 @@ namespace storm {
             MinMaxEquationSolverSettings::MinMaxEquationSolverSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, solvingMethodOptionName, false, "Sets which min/max linear equation solving technique is preferred.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a min/max linear equation solving technique. Available are: value-iteration (vi) and policy-iteration (pi).").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(minMaxSolvingTechniques)).setDefaultValueString("vi").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a min/max linear equation solving technique.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(minMaxSolvingTechniques)).setDefaultValueString("vi").build()).build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(20000).build()).build());
                 

src/storm/settings/modules/MultiObjectiveSettings.cpp

@@ -20,7 +20,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportPlotOptionName, true, "Saves data for plotting of pareto curves and achievable values.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to a directory in which the results will be saved.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for the approximation of numerical- and pareto queries.")
-                                .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision. Default is 1e-04.").setDefaultValueDouble(1e-04).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision.").setDefaultValueDouble(1e-04).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, maxStepsOptionName, true, "Aborts the computation after the given number of refinement steps (= computed pareto optimal points).")
                                 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "the threshold for the number of refinement steps to be performed.").build()).build());
             }

src/storm/settings/modules/NativeEquationSolverSettings.cpp

@@ -25,7 +25,7 @@ namespace storm {
             
             NativeEquationSolverSettings::NativeEquationSolverSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = { "jacobi", "gaussseidel", "sor" };
-                this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the native engine. Available are: { jacobi }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("jacobi").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the native engine.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("jacobi").build()).build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(20000).build()).build());
                 

src/storm/settings/modules/RegionSettings.cpp

@@ -27,18 +27,18 @@ namespace storm {
                             .addArgument(storm::settings::ArgumentBuilder::createStringArgument("regions", "The considered regions.").build()).build());
                 std::vector<std::string> approxModes = {"off", "testfirst", "guessallsat", "guessallviolated"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, approxmodeOptionName, true, "Sets whether approximation should be done and whether lower or upper bounds are computed first.")
-                            .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, testfirst (default), guessallsat, guessallviolated). E.g. guessallsat will first try to prove ALLSAT")
+                            .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use. For example, guessallsat will first try to prove ALLSAT.")
                                 .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(approxModes)).setDefaultValueString("testfirst").build()).build());
                 std::vector<std::string> sampleModes = {"off", "instantiate", "evaluate"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, samplemodeOptionName, true, "Sets whether sampling should be done and whether to instantiate a model or compute+evaluate a function.")
-                            .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, instantiate (default), evaluate)")
+                            .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.")
                                 .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(sampleModes)).setDefaultValueString("instantiate").build()).build());
                 std::vector<std::string> smtModes = {"off", "function", "model"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, smtmodeOptionName, true, "Sets whether SMT solving should be done and whether to encode it via a function or the model.")
-                            .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, function (default), model)")
+                            .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.")
                                 .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(smtModes)).setDefaultValueString("off").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, refinementOptionName, true, "Sets whether refinement (iteratively split regions) should be done. Only works if exactly one region (the parameter spaces) is specified.")
-                            .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "Number between zero and one. Sets the fraction of undiscovered area at which refinement stops.").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "Sets the fraction of undiscovered area at which refinement stops.").addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0, 1)).build()).build());
             }
             
             bool RegionSettings::isRegionFileSet() const{

src/storm/settings/modules/Smt2SmtSolverSettings.cpp

@@ -18,7 +18,7 @@ namespace storm {
             Smt2SmtSolverSettings::Smt2SmtSolverSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, solverCommandOption, true, "If set, this command is used to call the solver and to let the solver know that it should read SMT-LIBv2 commands from standard input. If not set, only a SMT-LIB script file might be exported.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("command", "path to the solver + command line arguments.").setDefaultValueString("").build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, exportScriptOption, true, "If set, the SMT-LIBv2 script will be exportet to this file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "path and filename to the location where the script file should be exportet to").setDefaultValueString("").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportScriptOption, true, "If set, the SMT-LIBv2 script will be exportet to this file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "path and filename to the location where the script file should be exported to.").setDefaultValueString("").build()).build());
             }
             
             bool Smt2SmtSolverSettings::isSolverCommandSet() const{