Merge branch 'master' into deterministicScheds

src/storm-cli-utilities/cli.cpp

@@ -177,8 +177,7 @@ namespace storm {
             try {
                 storm::settings::mutableManager().setFromCommandLine(argc, argv);
             } catch (storm::exceptions::OptionParserException& e) {
-                storm::settings::manager().printHelp();
-                throw e;
+                STORM_LOG_ERROR("Unable to parse command line options. Type 'storm --help' or 'storm --help all' for help.");
                 return false;
             }
             
@@ -186,7 +185,7 @@ namespace storm {
 
             bool result = true;
             if (general.isHelpSet()) {
-                storm::settings::manager().printHelp(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getHelpModuleName());
+                storm::settings::manager().printHelp(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getHelpFilterExpression());
                 result = false;
             }
             

src/storm-conv-cli/storm-conv.cpp

@@ -275,8 +275,6 @@ bool parseOptions(const int argc, const char* argv[]) {
     try {
         storm::settings::mutableManager().setFromCommandLine(argc, argv);
     } catch (storm::exceptions::OptionParserException& e) {
-        storm::settings::manager().printHelp();
-        throw e;
         return false;
     }
     
@@ -289,7 +287,7 @@ bool parseOptions(const int argc, const char* argv[]) {
 
     bool result = true;
     if (general.isHelpSet()) {
-        storm::settings::manager().printHelp(general.getHelpModuleName());
+        storm::settings::manager().printHelp(general.getHelpFilterExpression());
         result = false;
     }
     

src/storm-conv/settings/modules/ConversionGeneralSettings.cpp

@@ -22,8 +22,8 @@ namespace storm {
             const std::string ConversionGeneralSettings::configOptionShortName = "c";
 
             ConversionGeneralSettings::ConversionGeneralSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("hint", "A regular expression to show help for all matching entities or 'all' for the complete help.").setDefaultValueString("all").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows available options, arguments and descriptions.").setShortName(helpOptionShortName)
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "'frequent' for frequently used options, 'all' for the complete help, or a regular expression to show help for all matching entities.").setDefaultValueString("frequent").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, versionOptionName, false, "Prints the version information.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Enables verbose and debug output.").build());
@@ -40,8 +40,8 @@ namespace storm {
                 return this->getOption(versionOptionName).getHasOptionBeenSet();
             }
             
-            std::string ConversionGeneralSettings::getHelpModuleName() const {
-                return this->getOption(helpOptionName).getArgumentByName("hint").getValueAsString();
+            std::string ConversionGeneralSettings::getHelpFilterExpression() const {
+                return this->getOption(helpOptionName).getArgumentByName("filter").getValueAsString();
             }
             
             bool ConversionGeneralSettings::isVerboseSet() const {

src/storm-conv/settings/modules/ConversionGeneralSettings.h

@@ -30,7 +30,7 @@ namespace storm {
                  *
                  * @return The name of the module for which to show the help or "all".
                  */
-                std::string getHelpModuleName() const;
+                std::string getHelpFilterExpression() const;
 
                 /*!
                  * Retrieves whether the verbose option was set.

src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp

@@ -20,11 +20,11 @@ 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/edge set. Note that this requires the model to be given in a symbolic format.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command/edge set. Note that this requires the model to be given in a symbolic format.").setIsAdvanced()
                                 .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 counterexample generation.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based counterexample generation.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, noDynamicConstraintsOptionName, true, "Disables the generation of dynamic constraints in the MAXSAT-based counterexample generation.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based counterexample generation.").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based counterexample generation.").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, noDynamicConstraintsOptionName, true, "Disables the generation of dynamic constraints in the MAXSAT-based counterexample generation.").setIsAdvanced().build());
             }
             
             bool CounterexampleGeneratorSettings::isMinimalCommandSetGenerationSet() const {

src/storm/settings/Option.cpp

@@ -14,11 +14,11 @@
 namespace storm {
     namespace settings {
        
-			Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments) : Option(moduleName, longOptionName, "", false, optionDescription, isOptionRequired, requireModulePrefix, optionArguments) {
+			Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, bool isAdvanced, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments) : Option(moduleName, longOptionName, "", false, optionDescription, isOptionRequired, requireModulePrefix, isAdvanced, optionArguments) {
 				// Intentionally left empty.
 			}
             
-            Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments) : Option(moduleName, longOptionName, shortOptionName, true, optionDescription, isOptionRequired, requireModulePrefix, optionArguments) {
+            Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, bool isAdvanced, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments) : Option(moduleName, longOptionName, shortOptionName, true, optionDescription, isOptionRequired, requireModulePrefix, isAdvanced, optionArguments) {
                 // Intentionally left empty.
             }
 
@@ -85,13 +85,11 @@ namespace storm {
 			std::string const& Option::getLongName() const {
 				return this->longName;
 			}
-
        
             bool Option::getHasShortName() const {
                 return this->hasShortName;
             }
             
-           
 			std::string const& Option::getShortName() const {
 				return this->shortName;
 			}
@@ -108,16 +106,19 @@ namespace storm {
 				return this->isRequired;
 			}
 
-           
             bool Option::getRequiresModulePrefix() const {
                 return this->requireModulePrefix;
             }
             
+			bool Option::getIsAdvanced() const {
+				return this->isAdvanced;
+			}
+   
 			bool Option::getHasOptionBeenSet() const {
 				return this->hasBeenSet;
 			}
 
-            Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments) : longName(longOptionName), hasShortName(hasShortOptionName), shortName(shortOptionName), description(optionDescription), moduleName(moduleName), isRequired(isOptionRequired), requireModulePrefix(requireModulePrefix), hasBeenSet(false), arguments(optionArguments), argumentNameMap() {
+            Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, bool isAdvanced, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments) : longName(longOptionName), hasShortName(hasShortOptionName), shortName(shortOptionName), description(optionDescription), moduleName(moduleName), isRequired(isOptionRequired), requireModulePrefix(requireModulePrefix), isAdvanced(isAdvanced), hasBeenSet(false), arguments(optionArguments), argumentNameMap() {
                 // First, do some sanity checks.
                 STORM_LOG_THROW(!longName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty name.");
                 STORM_LOG_THROW(!moduleName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty module name.");

src/storm/settings/Option.h

@@ -40,9 +40,10 @@ namespace storm {
              * @param isOptionRequired Sets whether the option is required to appear.
              * @param requireModulePrefix A flag that indicates whether this option requires to be prefixed with the
              * module name.
+             * @param isAdvanced A flag that indicates whether this option is only displayed in the advanced help
              * @param optionArguments The arguments of the option.
              */
-            Option(std::string const& moduleName, std::string const& longOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>());
+            Option(std::string const& moduleName, std::string const& longOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, bool isAdvanced, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>());
             
             /*!
              * Creates an option with the given parameters.
@@ -53,10 +54,10 @@ namespace storm {
              * @param optionDescription The description of the option.
              * @param isOptionRequired Sets whether the option is required to appear.
              * @param requireModulePrefix A flag that indicates whether this option requires to be prefixed with the
-             * module name.
+             * @param isAdvanced A flag that indicates whether this option is only displayed in the advanced help
              * @param optionArguments The arguments of the option.
              */
-            Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>());
+            Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, bool isAdvanced, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>());
 
             /*!
              * Checks whether the given option is compatible with the current one. If not, an exception is thrown.
@@ -161,6 +162,11 @@ namespace storm {
              */
             bool getHasOptionBeenSet() const;
 
+            /*!
+             * Retrieves whether the option is only displayed in the advanced help.
+             */
+            bool getIsAdvanced() const;
+            
             /*!
              * Retrieves the arguments of the option.
              *
@@ -199,6 +205,9 @@ namespace storm {
             // A flag that indicates whether this option is required to be prefixed with the module name.
             bool requireModulePrefix;
             
+            // A flag that indicates whether this option is only displayed in the advanced help.
+            bool isAdvanced;
+            
             // A flag that indicates whether this option has been set.
             bool hasBeenSet;
 
@@ -219,9 +228,10 @@ namespace storm {
              * @param isOptionRequired Sets whether the option is required to appear.
              * @param requireModulePrefix A flag that indicates whether this option requires to be prefixed with the
              * module name.
+             * @param isAdvanced A flag that indicates whether this option is only displayed in the advanced help
              * @param optionArguments The arguments of the option.
              */
-            Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>());
+            Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, bool isAdvanced, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>());
             
             /*!
              * Sets the flag that marks the option as being (un)set.

src/storm/settings/OptionBuilder.h

@@ -33,7 +33,7 @@ namespace storm {
              * @param requireModulePrefix Sets whether this option can only be set by specifying the module name as its prefix.
              * @param description A description that explains the purpose of this option.
              */
-			OptionBuilder(std::string const& moduleName, std::string const& longName, bool requireModulePrefix, std::string const& description) : longName(longName), shortName(""), hasShortName(false), description(description), moduleName(moduleName), requireModulePrefix(requireModulePrefix), isRequired(false), isBuild(false), arguments(), argumentNameSet() {
+			OptionBuilder(std::string const& moduleName, std::string const& longName, bool requireModulePrefix, std::string const& description) : longName(longName), shortName(""), hasShortName(false), description(description), moduleName(moduleName), requireModulePrefix(requireModulePrefix), isRequired(false), isAdvanced(false), isBuild(false), arguments(), argumentNameSet() {
                 // Intentionally left empty.
             }
 
@@ -60,6 +60,14 @@ namespace storm {
 				return *this;
 			}
 
+            /*!
+             * Sets whether the option is only displayed in the advanced help.
+             */
+            OptionBuilder& setIsAdvanced(bool isAdvanced = true) {
+			    this->isAdvanced = isAdvanced;
+			    return *this;
+			}
+			
             /*!
              * Adds the given argument to the arguments of this option.
              *
@@ -89,9 +97,9 @@ namespace storm {
 				this->isBuild = true;
 
                 if (this->hasShortName) {
-                    return std::shared_ptr<Option>(new Option(this->moduleName, this->longName, this->shortName, this->description, this->isRequired, this->requireModulePrefix, this->arguments));
+                    return std::shared_ptr<Option>(new Option(this->moduleName, this->longName, this->shortName, this->description, this->isRequired, this->requireModulePrefix, this->isAdvanced, this->arguments));
                 } else {
-                    return std::shared_ptr<Option>(new Option(this->moduleName, this->longName, this->description, this->isRequired, this->requireModulePrefix, this->arguments));
+                    return std::shared_ptr<Option>(new Option(this->moduleName, this->longName, this->description, this->isRequired, this->requireModulePrefix, this->isAdvanced, this->arguments));
                 }
 			}
             
@@ -116,7 +124,10 @@ namespace storm {
             
             // A flag indicating whether the option is required.
 			bool isRequired;
-            
+   
+			// A flag that indicates whether this option is only displayed in the advanced help.
+            bool isAdvanced;
+
             // A flag indicating whether the builder has already been used to build an option.
 			bool isBuild;
 

src/storm/settings/SettingsManager.cpp

@@ -86,13 +86,32 @@ namespace storm {
         void SettingsManager::handleUnknownOption(std::string const& optionName, bool isShort) const {
             std::string optionNameWithDashes = (isShort ? "-" : "--") + optionName;
             storm::utility::string::SimilarStrings similarStrings(optionNameWithDashes, 0.6, false);
+            std::map<std::string, std::vector<std::string>> similarOptionNames;
             for (auto const& longOption : longNameToOptions) {
-                similarStrings.add("--" + longOption.first);
+                if (similarStrings.add("--" + longOption.first)) {
+                    similarOptionNames["--" + longOption.first].push_back(longOption.first);
+                }
             }
             for (auto const& shortOption : shortNameToOptions) {
-                similarStrings.add("-" + shortOption.first);
+                if (similarStrings.add("-" + shortOption.first)) {
+                    for (auto const& option : shortOption.second) {
+                        similarOptionNames["-" + shortOption.first].push_back(option->getLongName());
+                    }
+                }
+            }
+            std::string errorMessage = "Unknown option '" + optionNameWithDashes + "'.";
+            if (!similarOptionNames.empty()) {
+                errorMessage += " " + similarStrings.toDidYouMeanString() + "\n\n";
+                std::vector<std::string> sortedSimilarOptionNames;
+                auto similarStringsList = similarStrings.toList();
+                for (auto const& s : similarStringsList) {
+                    for (auto const& longOptionName : similarOptionNames.at(s)) {
+                        sortedSimilarOptionNames.push_back(longOptionName);
+                    }
+                }
+                errorMessage += getHelpForSelection({}, sortedSimilarOptionNames, "", "##### Suggested options:");
             }
-            STORM_LOG_THROW(false, storm::exceptions::OptionParserException, "Unknown option '" << optionNameWithDashes << "'. " << similarStrings.toDidYouMeanString());
+            STORM_LOG_THROW(false, storm::exceptions::OptionParserException, errorMessage);
         }
         
         void SettingsManager::setFromExplodedString(std::vector<std::string> const& commandLineArguments) {
@@ -188,112 +207,184 @@ namespace storm {
             this->finalizeAllModules();
         }
         
-        void SettingsManager::printHelp(std::string const& hint) const {
+        void SettingsManager::printHelp(std::string const& filter) const {
             STORM_PRINT("usage: " << executableName << " [options]" << std::endl << std::endl);
             
-            if (hint == "all") {
+            if (filter == "frequent" || filter == "all") {
+                bool includeAdvanced = (filter == "all");
                 // Find longest option name.
-                uint_fast64_t maxLength = getPrintLengthOfLongestOption();
+                uint_fast64_t maxLength = getPrintLengthOfLongestOption(includeAdvanced);
+                
+                std::vector<std::string> invisibleModules;
+                uint64_t numHidden = 0;
                 for (auto const& moduleName : this->moduleNames) {
                     // Only print for visible modules.
                     if (hasModule(moduleName, true)) {
-                        printHelpForModule(moduleName, maxLength);
-                    };
+                        STORM_PRINT(getHelpForModule(moduleName, maxLength, includeAdvanced));
+                        // collect 'hidden' options
+                        if (!includeAdvanced) {
+                            auto moduleIterator = moduleOptions.find(moduleName);
+                            if (moduleIterator != this->moduleOptions.end()) {
+                                bool allAdvanced = true;
+                                for (auto const& option : moduleIterator->second) {
+                                    if (!option->getIsAdvanced()) {
+                                        allAdvanced = false;
+                                    } else {
+                                        ++numHidden;
+                                    }
+                                }
+                                if (!moduleIterator->second.empty() && allAdvanced) {
+                                    invisibleModules.push_back(moduleName);
+                                }
+                            }
+                        }
+                    }
+                }
+                if (numHidden > 0) {
+                    STORM_PRINT(numHidden << " hidden options." << std::endl);
+                }
+                if (!invisibleModules.empty()) {
+                    STORM_PRINT(invisibleModules.size() << " hidden modules (" << boost::join(invisibleModules, ", ") << ")." << std::endl);
+                }
+                if (numHidden > 0 || !invisibleModules.empty()) {
+                    STORM_PRINT(std::endl << "Type 'storm --help modulename' to display all options of a specific module or 'storm --help all' for a complete list of options." << std::endl);
                 }
             } else {
                 // Create a regular expression from the input hint.
-                std::regex hintRegex(hint, std::regex_constants::ECMAScript | std::regex_constants::icase);
-                
-                // Remember which options we printed, so we don't display options twice.
-                std::set<std::shared_ptr<Option>> printedOptions;
+                std::regex hintRegex(filter, std::regex_constants::ECMAScript | std::regex_constants::icase);
                 
                 // Try to match the regular expression against the known modules.
                 std::vector<std::string> matchingModuleNames;
-                uint_fast64_t maxLengthModules = 0;
                 for (auto const& moduleName : this->moduleNames) {
                     if (std::regex_search(moduleName, hintRegex)) {
                         if (hasModule(moduleName, true)) {
-                            // Only consider visible modules.
                             matchingModuleNames.push_back(moduleName);
-                            maxLengthModules = std::max(maxLengthModules, getPrintLengthOfLongestOption(moduleName));
-                            
-                            // Add all options of this module to the list of printed options so we don't print them twice.
-                            auto optionIterator = this->moduleOptions.find(moduleName);
-                            printedOptions.insert(optionIterator->second.begin(), optionIterator->second.end());
                         }
                     }
                 }
 
                 // Try to match the regular expression against the known options.
-                std::vector<std::shared_ptr<Option>> matchingOptions;
-                uint_fast64_t maxLengthOptions = 0;
+                std::vector<std::string> matchingOptionNames;
                 for (auto const& optionName : this->longOptionNames) {
                     if (std::regex_search(optionName, hintRegex)) {
-                        auto optionIterator = this->longNameToOptions.find(optionName);
-                        for (auto const& option : optionIterator->second) {
-                            // Only add the option if we have not already added it to the list of options that is going
-                            // to be printed anyway.
-                            if (printedOptions.find(option) == printedOptions.end()) {
-                                maxLengthOptions = std::max(maxLengthOptions, option->getPrintLength());
-                                matchingOptions.push_back(option);
-                            }
-                        }
+                        matchingOptionNames.push_back(optionName);
                     }
                 }
                 
-                // Print the matching modules.
-                uint_fast64_t maxLength = std::max(maxLengthModules, maxLengthOptions);
-                if (matchingModuleNames.size() > 0) {
-                    STORM_PRINT("Matching modules for hint '" << hint << "':" << std::endl)
-                    for (auto const& matchingModuleName : matchingModuleNames) {
-                        printHelpForModule(matchingModuleName, maxLength);
-                    }
+                std::string optionList = getHelpForSelection(matchingModuleNames, matchingOptionNames, "Matching modules for filter '" + filter +"':", "Matching options for filter '" + filter +"':");
+                if (optionList.empty()) {
+                    STORM_PRINT("Filter '" << filter << "' did not match any modules or options." << std::endl);
+                } else {
+                    STORM_PRINT(optionList);
                 }
-                
-                // Print the matching options.
-                if (matchingOptions.size() > 0) {
-                    STORM_PRINT("Matching options for hint '" << hint << "':" << std::endl);
-                    for (auto const& option : matchingOptions) {
-                        STORM_PRINT(std::setw(maxLength) << std::left << *option << std::endl);
+            }
+        }
+        
+        std::string SettingsManager::getHelpForSelection(std::vector<std::string> const& selectedModuleNames, std::vector<std::string> const& selectedLongOptionNames, std::string modulesHeader, std::string optionsHeader) const {
+            std::stringstream stream;
+        
+            // Remember which options we printed, so we don't display options twice.
+            std::set<std::shared_ptr<Option>> printedOptions;
+            
+            // Try to match the regular expression against the known modules.
+            uint_fast64_t maxLengthModules = 0;
+            for (auto const& moduleName : selectedModuleNames) {
+                maxLengthModules = std::max(maxLengthModules, getPrintLengthOfLongestOption(moduleName, true));
+                // Add all options of this module to the list of printed options so we don't print them twice.
+                auto optionIterator = this->moduleOptions.find(moduleName);
+                STORM_LOG_ASSERT(optionIterator != this->moduleOptions.end(), "Unable to find selected module " << moduleName << ".");
+                printedOptions.insert(optionIterator->second.begin(), optionIterator->second.end());
+            }
+
+            // Try to match the regular expression against the known options.
+            std::vector<std::shared_ptr<Option>> matchingOptions;
+            uint_fast64_t maxLengthOptions = 0;
+            for (auto const& optionName : selectedLongOptionNames) {
+                auto optionIterator = this->longNameToOptions.find(optionName);
+                STORM_LOG_ASSERT(optionIterator != this->longNameToOptions.end(), "Unable to find selected option " << optionName << ".");
+                for (auto const& option : optionIterator->second) {
+                    // Only add the option if we have not already added it to the list of options that is going
+                    // to be printed anyway.
+                    if (printedOptions.find(option) == printedOptions.end()) {
+                        maxLengthOptions = std::max(maxLengthOptions, option->getPrintLength());
+                        matchingOptions.push_back(option);
+                        printedOptions.insert(option);
                     }
                 }
-                
-                if (matchingModuleNames.empty() && matchingOptions.empty()) {
-                    STORM_PRINT("Hint '" << hint << "' did not match any modules or options." << std::endl);
+            }
+            
+            // Print the matching modules.
+            uint_fast64_t maxLength = std::max(maxLengthModules, maxLengthOptions);
+            if (selectedModuleNames.size() > 0) {
+                if (modulesHeader != "") {
+                    stream << modulesHeader << std::endl;
+                }
+                for (auto const& matchingModuleName : selectedModuleNames) {
+                    stream << getHelpForModule(matchingModuleName, maxLength, true);
+                }
+            }
+            
+            // Print the matching options.
+            if (matchingOptions.size() > 0) {
+                if (optionsHeader != "") {
+                    stream << optionsHeader << std::endl;
+                }
+                for (auto const& option : matchingOptions) {
+                    stream << std::setw(maxLength) << std::left << *option << std::endl;
                 }
             }
+            return stream.str();
         }
         
-        void SettingsManager::printHelpForModule(std::string const& moduleName, uint_fast64_t maxLength) const {
+        std::string SettingsManager::getHelpForModule(std::string const& moduleName, uint_fast64_t maxLength, bool includeAdvanced) const {
             auto moduleIterator = moduleOptions.find(moduleName);
             if(moduleIterator == this->moduleOptions.end()) {
-                return;
+                return "";
             }
             //STORM_LOG_THROW(moduleIterator != moduleOptions.end(), storm::exceptions::IllegalFunctionCallException, "Cannot print help for unknown module '" << moduleName << "'.");
-            STORM_PRINT("##### Module '" << moduleName << "' " << std::string(std::min(maxLength, maxLength - moduleName.length() - 16), '#') << std::endl);
-            
-            // Save the flags for std::cout so we can manipulate them and be sure they will be restored as soon as this
-            // stream goes out of scope.
-            boost::io::ios_flags_saver out(std::cout);
             
+            // Check whether there is at least one (enabled) option in this module
+            uint64_t numOfOptions = 0;
             for (auto const& option : moduleIterator->second) {
-                STORM_PRINT(std::setw(maxLength) << std::left << *option << std::endl);
+                if (includeAdvanced || !option->getIsAdvanced()) {
+                    ++numOfOptions;
+                }
             }
-            STORM_PRINT(std::endl);
+            
+            std::stringstream stream;
+            if (numOfOptions > 0) {
+                std::string displayedModuleName = "'" + moduleName + "'";
+                if (!includeAdvanced) {
+                    displayedModuleName += " (" + std::to_string(numOfOptions) + "/" + std::to_string(moduleIterator->second.size()) + " shown)";
+                }
+                stream << "##### Module " << displayedModuleName << " " << std::string(std::min(maxLength, maxLength - displayedModuleName.length() - 14), '#') << std::endl;
+                
+                // Save the flags for std::cout so we can manipulate them and be sure they will be restored as soon as this
+                // stream goes out of scope.
+                boost::io::ios_flags_saver out(std::cout);
+                
+                for (auto const& option : moduleIterator->second) {
+                    if (includeAdvanced || !option->getIsAdvanced()) {
+                        stream << std::setw(maxLength) << std::left << *option << std::endl;
+                    }
+                }
+                stream << std::endl;
+            }
+            return stream.str();
         }
         
-        uint_fast64_t SettingsManager::getPrintLengthOfLongestOption() const {
+        uint_fast64_t SettingsManager::getPrintLengthOfLongestOption(bool includeAdvanced) const {
             uint_fast64_t length = 0;
             for (auto const& moduleName : this->moduleNames) {
-                length = std::max(getPrintLengthOfLongestOption(moduleName), length);
+                length = std::max(getPrintLengthOfLongestOption(moduleName, includeAdvanced), length);
             }
             return length;
         }
         
-        uint_fast64_t SettingsManager::getPrintLengthOfLongestOption(std::string const& moduleName) const {
+        uint_fast64_t SettingsManager::getPrintLengthOfLongestOption(std::string const& moduleName, bool includeAdvanced) const {
             auto moduleIterator = modules.find(moduleName);
             STORM_LOG_THROW(moduleIterator != modules.end(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve option length of unknown module '" << moduleName << "'.");
-            return moduleIterator->second->getPrintLengthOfLongestOption();
+            return moduleIterator->second->getPrintLengthOfLongestOption(includeAdvanced);
         }
         
         void SettingsManager::addModule(std::unique_ptr<modules::ModuleSettings>&& moduleSettings, bool doRegister) {
@@ -387,10 +478,11 @@ namespace storm {
                 bool conversionOk = argument.setFromStringValue(argumentCache[i]);
                 STORM_LOG_THROW(conversionOk, storm::exceptions::OptionParserException, "Value '" << argumentCache[i] << "' is invalid for argument <" << argument.getName() << "> of option:\n" << *option);
             }
-            
+        
             // In case there are optional arguments that were not set, we set them to their default value.
             for (uint_fast64_t i = argumentCache.size(); i < option->getArgumentCount(); ++i) {
                 ArgumentBase& argument = option->getArgument(i);
+                STORM_LOG_THROW(argument.getHasDefaultValue() || argument.getIsOptional(), storm::exceptions::OptionParserException, "Non-optional argument <" << argument.getName() << "> of option:\n" << *option);
                 argument.setFromDefaultValue();
             }
             

src/storm/settings/SettingsManager.h

@@ -70,21 +70,24 @@ namespace storm {
             void handleUnknownOption(std::string const& optionName, bool isShort) const;
             
             /*!
-             * This function prints a help message to the standard output. Optionally, a string can be given as a hint.
-             * If it is 'all', the complete help is shown. Otherwise, the string is interpreted as a regular expression
+             * This function prints a help message to the standard output. A string can be given as a filter.
+             * If it is 'frequent', only the options that are not flagged as advanced will be shown.
+             * If it is 'all', the complete help is shown.
+             * Otherwise, the string is interpreted as a regular expression
              * and matched against the known modules and options to restrict the help output.
              *
-             * @param hint A regular expression to restrict the help output or "all" for the full help text.
+             * @param filter A regular expression to restrict the help output or "all" for the full help text.
              */
-            void printHelp(std::string const& hint = "all") const;
+            void printHelp(std::string const& filter = "frequent") const;
             
             /*!
              * This function prints a help message for the specified module to the standard output.
              *
              * @param moduleName The name of the module for which to show the help.
              * @param maxLength The maximal length of an option name (necessary for proper alignment).
+             * @param includeAdvanced if set, also includes options flagged as advanced.
              */
-            void printHelpForModule(std::string const& moduleName, uint_fast64_t maxLength = 30) const;
+            std::string getHelpForModule(std::string const& moduleName, uint_fast64_t maxLength = 30, bool includeAdvanced = true) const;
 			
             /*!
              * Retrieves the only existing instance of a settings manager.
@@ -144,7 +147,17 @@ namespace storm {
 			 * This destructor is private, since we need to forbid explicit destruction of the manager.
 			 */
 			virtual ~SettingsManager();
-            
+   
+			/*!
+             * This function prints a help message to the standard output.
+             *
+             * @param moduleFilter only modules where this function returns true are included
+             * @param optionFilter only options where this function returns true are included
+             * @return true if at least one module or option matched the filter.
+             *
+             */
+            std::string getHelpForSelection(std::vector<std::string> const& selectedModuleNames, std::vector<std::string> const& selectedLongOptionNames, std::string modulesHeader = "", std::string optionsHeader = "") const;
+			
             // The name of the tool
             std::string name;
             std::string executableName;
@@ -213,17 +226,19 @@ namespace storm {
             /*!
              * Retrieves the (print) length of the longest option of all modules.
              *
+             * @param includeAdvanced if set, also includes options flagged as advanced.
              * @return The length of the longest option.
              */
-            uint_fast64_t getPrintLengthOfLongestOption() const;
+            uint_fast64_t getPrintLengthOfLongestOption(bool includeAdvanced) const;
             
             /*!
              * Retrieves the (print) length of the longest option in the given module, so we can align the options.
              *
              * @param moduleName The module name for which to retrieve the length of the longest option.
+             * @param includeAdvanced if set, also includes options flagged as advanced.
              * @return The length of the longest option name.
              */
-            uint_fast64_t getPrintLengthOfLongestOption(std::string const& moduleName) const;
+            uint_fast64_t getPrintLengthOfLongestOption(std::string const& moduleName, bool includeAdvanced) const;
             
             /*!
              * Parses the given file and stores the settings in the returned map.

src/storm/settings/modules/AbstractionSettings.cpp

@@ -37,105 +37,106 @@ namespace storm {
             
             AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = {"games", "bisimulation", "bisim"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, methodOptionName, true, "Sets which abstraction-refinement method to use.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, methodOptionName, true, "Sets which abstraction-refinement method to use.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods))
                                              .setDefaultValueString("bisim").build())
                                 .build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, maximalAbstractionOptionName, false, "The maximal number of abstraction to perform before solving is aborted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal abstraction count.").setDefaultValueUnsignedInteger(20000).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, maximalAbstractionOptionName, false, "The maximal number of abstraction to perform before solving is aborted.").setIsAdvanced()
+                                .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal abstraction count.").setDefaultValueUnsignedInteger(20000).build()).build());
                 
                 std::vector<std::string> onOff = {"on", "off"};
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, useDecompositionOptionName, true, "Sets whether to apply decomposition during the abstraction.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, useDecompositionOptionName, true, "Sets whether to apply decomposition during the abstraction.").setIsAdvanced()
                                 .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.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, splitModeOptionName, true, "Sets which predicates are split into atoms for the refinement.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(splitModes))
                                              .setDefaultValueString("all").build())
                                 .build());
 
                 std::vector<std::string> solveModes = {"dd", "sparse"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, solveModeOptionName, true, "Sets how the abstractions are solved.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, solveModeOptionName, true, "Sets how the abstractions are solved.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(solveModes))
                                              .setDefaultValueString("sparse").build())
                                 .build());
 
-                this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.").setIsAdvanced()
                                 .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, addInitialExpressionsOptionName, true, "Sets whether all initial expressions are added as initial predicates.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, addInitialExpressionsOptionName, true, "Sets whether all initial expressions are added as initial predicates.").setIsAdvanced()
                                 .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.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, useInterpolationOptionName, true, "Sets whether interpolation is to be used to eliminate spurious pivot blocks.").setIsAdvanced()
                                 .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, precisionOptionName, true, "The precision used for detecting convergence.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-03).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for detecting convergence.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-03).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
                                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, relativeOptionName, true, "Sets whether to use a relative termination criterion.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, relativeOptionName, true, "Sets whether to use a relative termination criterion.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
                                              .setDefaultValueString("off").build())
                                 .build());
                 
                 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.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, pivotHeuristicOptionName, true, "Sets the pivot selection heuristic.").setIsAdvanced()
                                 .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.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, reuseResultsOptionName, true, "Sets whether to reuse all results.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reuseModes))
                                              .setDefaultValueString("all").build())
                                 .build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, restrictToRelevantStatesOptionName, true, "Sets whether to restrict to relevant states during the abstraction.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, restrictToRelevantStatesOptionName, true, "Sets whether to restrict to relevant states during the abstraction.").setIsAdvanced()
                                 .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, rankRefinementPredicatesOptionName, true, "Sets whether to rank the refinement predicates if there are multiple.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, rankRefinementPredicatesOptionName, true, "Sets whether to rank the refinement predicates if there are multiple.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
                                              .setDefaultValueString("off").build())
                                 .build());
 
-                this->addOption(storm::settings::OptionBuilder(moduleName, useEagerRefinementOptionName, true, "Sets whether to refine eagerly.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, useEagerRefinementOptionName, true, "Sets whether to refine eagerly.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
                                              .setDefaultValueString("off").build())
                                 .build());
 
-                this->addOption(storm::settings::OptionBuilder(moduleName, constraintsOptionName, true, "Specifies additional constraints used by the abstraction.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, constraintsOptionName, true, "Specifies additional constraints used by the abstraction.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("constraints", "The constraints to use.").setDefaultValueString("").build())
                                 .build());
 
-                this->addOption(storm::settings::OptionBuilder(moduleName, injectRefinementPredicatesOptionName, true, "Specifies predicates used by the refinement instead of the derived predicates.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, injectRefinementPredicatesOptionName, true, "Specifies predicates used by the refinement instead of the derived predicates.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("predicates", "The (semicolon-separated) refinement predicates to use.").setDefaultValueString("").build())
                                 .build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, fixPlayer1StrategyOptionName, true, "Sets whether to fix player 1 strategies.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, fixPlayer1StrategyOptionName, true, "Sets whether to fix player 1 strategies.").setIsAdvanced()
                                 .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, fixPlayer2StrategyOptionName, true, "Sets whether to fix player 2 strategies.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, fixPlayer2StrategyOptionName, true, "Sets whether to fix player 2 strategies.").setIsAdvanced()
                                 .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, debugOptionName, true, "Sets whether to enable debug mode.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, true, "Sets whether to enable debug mode.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
                                              .setDefaultValueString("off").build())
                                 .build());
                 
                 std::vector<std::string> validModes = {"morepreds", "blockenum"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, validBlockModeOptionName, true, "Sets the mode to guarantee valid blocks only.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, validBlockModeOptionName, true, "Sets the mode to guarantee valid blocks only.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(validModes))
                                              .setDefaultValueString("morepreds").build())
                                 .build());

src/storm/settings/modules/BisimulationSettings.cpp

@@ -25,32 +25,32 @@ 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.").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.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(types)).setDefaultValueString("strong").build()).build());
                 
                 std::vector<std::string> quotTypes = { "sparse", "dd" };
-                this->addOption(storm::settings::OptionBuilder(moduleName, quotientFormatOptionName, true, "Sets the format in which the quotient is extracted (only applies to DD-based bisimulation).").addArgument(storm::settings::ArgumentBuilder::createStringArgument("format", "The format of the quotient.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(quotTypes)).setDefaultValueString("dd").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, quotientFormatOptionName, true, "Sets the format in which the quotient is extracted (only applies to DD-based bisimulation).").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("format", "The format of the quotient.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(quotTypes)).setDefaultValueString("dd").build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, representativeOptionName, false, "Sets whether to use representatives in the quotient rather than block numbers.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, originalVariablesOptionName, false, "Sets whether to use the original variables in the quotient rather than the block variables.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, exactArithmeticDdOptionName, false, "Sets whether to use exact arithmetic in dd-based bisimulation.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, representativeOptionName, false, "Sets whether to use representatives in the quotient rather than block numbers.").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, originalVariablesOptionName, false, "Sets whether to use the original variables in the quotient rather than the block variables.").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exactArithmeticDdOptionName, false, "Sets whether to use exact arithmetic in dd-based bisimulation.").setIsAdvanced().build());
 
                 std::vector<std::string> signatureModes = { "eager", "lazy" };
-                this->addOption(storm::settings::OptionBuilder(moduleName, signatureModeOptionName, false, "Sets the signature computation mode.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(signatureModes)).setDefaultValueString("eager").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, signatureModeOptionName, false, "Sets the signature computation mode.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(signatureModes)).setDefaultValueString("eager").build()).build());
                 
                 std::vector<std::string> reuseModes = {"none", "blocks"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, reuseOptionName, true, "Sets whether to reuse all results.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, reuseOptionName, true, "Sets whether to reuse all results.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reuseModes))
                                              .setDefaultValueString("blocks").build())
                                 .build());
 
                 std::vector<std::string> initialPartitionModes = {"regular", "finer"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, initialPartitionOptionName, true, "Sets which initial partition mode to use.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, initialPartitionOptionName, true, "Sets which initial partition mode to use.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(initialPartitionModes))
                                              .setDefaultValueString("finer").build())
                                 .build());
                 
                 std::vector<std::string> refinementModes = {"full", "changed"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, refinementModeOptionName, true, "Sets which refinement mode to use.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, refinementModeOptionName, true, "Sets which refinement mode to use.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(refinementModes))
                                              .setDefaultValueString("full").build())
                                 .build());

src/storm/settings/modules/BuildSettings.cpp

@@ -33,19 +33,19 @@ namespace storm {
             const std::string bitsForUnboundedVariablesOptionName = "int-bits";
             BuildSettings::BuildSettings() : ModuleSettings(moduleName) {
 
-                std::vector<std::string> explorationOrders = {"dfs", "bfs"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, also build the choice labels").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, also build the choice labels").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").setIsAdvanced().build());
 
-                this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName)
+                std::vector<std::string> explorationOrders = {"dfs", "bfs"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName).setIsAdvanced()
                                         .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, buildOutOfBoundsStateOptionName, false, "If set, a state for out-of-bounds valuations is added").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, bitsForUnboundedVariablesOptionName, false, "Sets the number of bits that is used for unbounded integer variables.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, buildOutOfBoundsStateOptionName, false, "If set, a state for out-of-bounds valuations is added").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, bitsForUnboundedVariablesOptionName, false, "Sets the number of bits that is used for unbounded integer variables.").setIsAdvanced()
                                         .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("number", "The number of bits.").addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedRangeValidatorExcluding(0,63)).setDefaultValueUnsignedInteger(32).build()).build());
             }
 

src/storm/settings/modules/CoreSettings.cpp

@@ -38,7 +38,7 @@ namespace storm {
             
             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.").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());
+                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).setIsAdvanced().build());
                 
                 std::vector<std::string> engines = {"sparse", "hybrid", "dd", "dd-to-sparse", "expl", "abs"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName)
@@ -61,7 +61,7 @@ namespace storm {
                                 .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.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, cudaOptionName, false, "Sets whether to use CUDA.").setIsAdvanced().build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, intelTbbOptionName, false, "Sets whether to use Intel TBB (if Storm was built with support for TBB).").setShortName(intelTbbOptionShortName).build());
             }
 

src/storm/settings/modules/CuddSettings.cpp

@@ -21,11 +21,11 @@ namespace storm {
             const std::string CuddSettings::reorderTechniqueOptionName = "reordertechnique";
             
             CuddSettings::CuddSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(0.0, 1.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(0.0, 1.0)).build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(4096).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(4096).build()).build());
 
-                this->addOption(storm::settings::OptionBuilder(moduleName, reorderOptionName, false, "Sets whether dynamic reordering is allowed.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, reorderOptionName, false, "Sets whether dynamic reordering is allowed.").setIsAdvanced().build());
                 
                 std::vector<std::string> reorderingTechniques;
                 reorderingTechniques.push_back("none");
@@ -46,7 +46,7 @@ namespace storm {
                 reorderingTechniques.push_back("annealing");
                 reorderingTechniques.push_back("genetic");
                 reorderingTechniques.push_back("exact");
-                this->addOption(storm::settings::OptionBuilder(moduleName, reorderTechniqueOptionName, 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());
+                this->addOption(storm::settings::OptionBuilder(moduleName, reorderTechniqueOptionName, true, "Sets the reordering technique used by Cudd.").setIsAdvanced().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/DebugSettings.cpp

@@ -22,7 +22,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, traceOptionName, false, "Print even more debug output.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, logfileOptionName, false, "If specified, the log output will also be written to this file.").setShortName(logfileOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to write the log.").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, testOptionName, false, "Activate a test setting.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, testOptionName, false, "Activate a test setting.").setIsAdvanced().build());
             }
             
             bool DebugSettings::isDebugSet() const {

src/storm/settings/modules/EigenEquationSolverSettings.cpp

@@ -26,17 +26,17 @@ 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.").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 eigen solver.").setIsAdvanced().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.").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.").setIsAdvanced().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());
+                this->addOption(storm::settings::OptionBuilder(moduleName, restartOptionName, true, "The number of iteration until restarted methods are actually restarted.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of iterations.").setDefaultValueUnsignedInteger(50).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.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
             }
             
             bool EigenEquationSolverSettings::isLinearEquationSystemMethodSet() const {

src/storm/settings/modules/EliminationSettings.cpp

@@ -21,15 +21,15 @@ 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.").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.").setIsAdvanced().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.").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.").setIsAdvanced().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.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, entryStatesLastOptionName, true, "Sets whether the entry states are eliminated last.").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, maximalSccSizeOptionName, true, "Sets the maximal size of the SCCs for which state elimination is applied.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxsize", "The maximal size of an SCC on which state elimination is applied.").setDefaultValueUnsignedInteger(20).setIsOptional(true).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, useDedicatedModelCheckerOptionName, true, "Sets whether to use the dedicated model elimination checker (only DTMCs).").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, useDedicatedModelCheckerOptionName, true, "Sets whether to use the dedicated model elimination checker (only DTMCs).").setIsAdvanced().build());
             }
             
             EliminationSettings::EliminationMethod EliminationSettings::getEliminationMethod() const {

src/storm/settings/modules/ExplorationSettings.cpp

@@ -23,14 +23,14 @@ 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.").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());
+                    this->addOption(storm::settings::OptionBuilder(moduleName, precomputationTypeOptionName, true, "Sets the kind of precomputation used.").setIsAdvanced().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.").setIsAdvanced().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.").setIsAdvanced().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.").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, nextStateHeuristicOptionName, true, "Sets the next-state heuristic to use.").setIsAdvanced().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)
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision to achieve.").setShortName(precisionOptionShortName).setIsAdvanced()
                                 .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/GameSolverSettings.cpp

@@ -20,14 +20,14 @@ namespace storm {
 
             GameSolverSettings::GameSolverSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> gameSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, solvingMethodOptionName, false, "Sets which game solving technique is preferred.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, solvingMethodOptionName, false, "Sets which game solving technique is preferred.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a game solving technique.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(gameSolvingTechniques)).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.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
 
-                this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").setIsAdvanced().build());
             }
             
             storm::solver::GameMethod GameSolverSettings::getGameSolvingMethod() const {

src/storm/settings/modules/GeneralSettings.cpp

@@ -34,8 +34,8 @@ namespace storm {
             const std::string GeneralSettings::soundOptionName = "sound";
 
             GeneralSettings::GeneralSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("hint", "A regular expression to show help for all matching entities or 'all' for the complete help.").setDefaultValueString("all").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows available options, arguments and descriptions.").setShortName(helpOptionShortName)
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "'frequent' for frequently used options, 'all' for the complete help, or a regular expression to show help for all matching entities.").setDefaultValueString("frequent").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, versionOptionName, false, "Prints the version information.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, showProgressOptionName, false, "Sets when additional information (if available) about the progress is printed.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("delay", "The delay to wait (in seconds) between emitting information (0 means never print progress).").setDefaultValueUnsignedInteger(5).build()).build());
@@ -44,7 +44,7 @@ namespace storm {
                 this->addOption(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.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, bisimulationOptionName, false, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to enable parametric model checking.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to enable parametric model checking.").setIsAdvanced().build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exactOptionName, false, "Sets whether to enable exact model checking.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, soundOptionName, false, "Sets whether to force sound model checking.").build());
             }
@@ -57,8 +57,8 @@ namespace storm {
                 return this->getOption(versionOptionName).getHasOptionBeenSet();
             }
             
-            std::string GeneralSettings::getHelpModuleName() const {
-                return this->getOption(helpOptionName).getArgumentByName("hint").getValueAsString();
+            std::string GeneralSettings::getHelpFilterExpression() const {
+                return this->getOption(helpOptionName).getArgumentByName("filter").getValueAsString();
             }
             
             bool GeneralSettings::isVerboseSet() const {

src/storm/settings/modules/GeneralSettings.h

@@ -41,7 +41,7 @@ namespace storm {
                  *
                  * @return The name of the module for which to show the help or "all".
                  */
-                std::string getHelpModuleName() const;
+                std::string getHelpFilterExpression() const;
 
                 /*!
                  * Retrieves whether the verbose option was set.

src/storm/settings/modules/GlpkSettings.cpp

@@ -17,8 +17,8 @@ namespace storm {
             const std::string GlpkSettings::outputOptionName = "output";
             
             GlpkSettings::GlpkSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, outputOptionName, true, "If set, the glpk output will be printed to the command line.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets glpk's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, outputOptionName, true, "If set, the glpk output will be printed to the command line.").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets glpk's precision for integer variables.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
             }
             
             bool GlpkSettings::isOutputSet() const {

src/storm/settings/modules/GmmxxEquationSolverSettings.cpp

@@ -26,13 +26,13 @@ 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.").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.").setIsAdvanced().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.").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.").setIsAdvanced().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());
+                this->addOption(storm::settings::OptionBuilder(moduleName, restartOptionName, true, "The number of iteration until restarted methods are actually restarted.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of iterations.").setDefaultValueUnsignedInteger(50).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.").build()).build());
                 

src/storm/settings/modules/GurobiSettings.cpp

@@ -19,15 +19,15 @@ namespace storm {
             const std::string GurobiSettings::concurrentMipThreadsOption = "concurrentmip";
             
             GurobiSettings::GurobiSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, threadsOption, true, "The number of threads that may be used by Gurobi.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of threads.").setDefaultValueUnsignedInteger(1).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, threadsOption, true, "The number of threads that may be used by Gurobi.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of threads.").setDefaultValueUnsignedInteger(1).build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, outputOption, true, "If set, the Gurobi output will be printed to the command line.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, outputOption, true, "If set, the Gurobi output will be printed to the command line.").setIsAdvanced().build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets Gurobi's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets Gurobi's precision for integer variables.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, mipFocusOption, true, "The high level solution strategy used to solve MILPs.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The number of the strategy.").setDefaultValueUnsignedInteger(0).addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedRangeValidatorIncluding(0, 3)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, mipFocusOption, true, "The high level solution strategy used to solve MILPs.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The number of the strategy.").setDefaultValueUnsignedInteger(0).addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedRangeValidatorIncluding(0, 3)).build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, concurrentMipThreadsOption, true, "The number of MIP solvers Gurobi spawns in parallel. Shall not be larger then the number of threads.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The number of parallel solvers.").setDefaultValueUnsignedInteger(1).addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedGreaterEqualValidator(1)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, concurrentMipThreadsOption, true, "The number of MIP solvers Gurobi spawns in parallel. Shall not be larger then the number of threads.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The number of parallel solvers.").setDefaultValueUnsignedInteger(1).addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedGreaterEqualValidator(1)).build()).build());
             }
             
             bool GurobiSettings::isIntegerToleranceSet() const {

src/storm/settings/modules/IOSettings.cpp

@@ -49,11 +49,11 @@ namespace storm {
             const std::string IOSettings::qvbsRootOptionName = "qvbsroot";
             
             IOSettings::IOSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, "", "If given, the loaded jani model will be written to the specified file in the dot format.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, "", "If given, the loaded jani model will be written to the specified file in the dot format.").setIsAdvanced()
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setShortName(exportCdfOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory where the cdf files will be stored.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setIsAdvanced().setShortName(exportCdfOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory where the cdf files will be stored.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName)
@@ -69,7 +69,7 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the PRISM input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").setIsAdvanced().build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName)
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build())
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The names of the properties to check.").setDefaultValueString("all").build())
@@ -79,13 +79,13 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
                 this->addOption(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.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, choiceLabelingOptionName, false, "If given, the choice labels 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 + ").")
+                this->addOption(storm::settings::OptionBuilder(moduleName, choiceLabelingOptionName, false, "If given, the choice labels 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 + ").").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that this requires the model to be given as an symbolic model (i.e., via --" + prismInputOptionName + " or --" + janiInputOptionName + ").").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());
                 this->addOption(storm::settings::OptionBuilder(moduleName, janiPropertyOptionName, false, "Specifies the properties from the jani model (given by --" + janiInputOptionName + ")  to be checked.").setShortName(janiPropertyOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of properties to be checked").setDefaultValueString("").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, toNondetOptionName, false, "If set, DTMCs/CTMCs are converted to MDPs/MAs (without actual nondeterminism) before model checking.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, toNondetOptionName, false, "If set, DTMCs/CTMCs are converted to MDPs/MAs (without actual nondeterminism) before model checking.").setIsAdvanced().build());
 
                 this->addOption(storm::settings::OptionBuilder(moduleName, qvbsInputOptionName, false, "Selects a model from the Quantitative Verification Benchmark Set.").setShortName(qvbsInputOptionShortName)
                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("model", "The short model name as in the benchmark set.").build())

src/storm/settings/modules/JitBuilderSettings.cpp

@@ -23,18 +23,18 @@ namespace storm {
             const std::string JitBuilderSettings::optimizationLevelOptionName = "opt";
 
             JitBuilderSettings::JitBuilderSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, doctorOptionName, false, "Show debugging information on why the jit-based model builder is not working on your system.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, compilerOptionName, false, "The compiler in the jit-based model builder.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, doctorOptionName, false, "Show debugging information on why the jit-based model builder is not working on your system.").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, compilerOptionName, false, "The compiler in the jit-based model builder.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the executable. Defaults to c++.").setDefaultValueString("c++").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, stormIncludeDirectoryOptionName, false, "The include directory of storm.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, stormIncludeDirectoryOptionName, false, "The include directory of storm.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory that contains the headers of storm.").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, boostIncludeDirectoryOptionName, false, "The include directory of boost.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, boostIncludeDirectoryOptionName, false, "The include directory of boost.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory containing the boost headers version >= 1.61.").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, carlIncludeDirectoryOptionName, false, "The include directory of carl.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, carlIncludeDirectoryOptionName, false, "The include directory of carl.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory containing the carl headers.").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, compilerFlagsOptionName, false, "The flags passed to the compiler.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, compilerFlagsOptionName, false, "The flags passed to the compiler.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("flags", "The compiler flags.").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, optimizationLevelOptionName, false, "Sets the optimization level.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, optimizationLevelOptionName, false, "Sets the optimization level.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("level", "The level to use.").setDefaultValueUnsignedInteger(3).build()).build());
             }
             

src/storm/settings/modules/MinMaxEquationSolverSettings.cpp

@@ -24,27 +24,27 @@ namespace storm {
 
             MinMaxEquationSolverSettings::MinMaxEquationSolverSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "lp", "linear-programming", "rs", "ratsearch", "ii", "interval-iteration", "svi", "sound-value-iteration", "topological", "vi-to-pi"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, solvingMethodOptionName, false, "Sets which min/max linear equation solving technique is preferred.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, solvingMethodOptionName, false, "Sets which min/max linear equation solving technique is preferred.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a min/max linear equation solving technique.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(minMaxSolvingTechniques)).setDefaultValueString("topological").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.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
 
-                this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").setIsAdvanced().build());
 
                 std::vector<std::string> lraMethods = {"vi", "value-iteration", "linear-programming", "lp"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, lraMethodOptionName, false, "Sets which method is preferred for computing long run averages.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, lraMethodOptionName, false, "Sets which method is preferred for computing long run averages.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a long run average computation method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(lraMethods)).setDefaultValueString("vi").build()).build());
 
                 std::vector<std::string> maMethods = {"imca", "unifplus"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, markovAutomatonBoundedReachabilityMethodOptionName, false, "The method to use to solve bounded reachability queries on MAs.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(maMethods)).setDefaultValueString("unifplus").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, markovAutomatonBoundedReachabilityMethodOptionName, false, "The method to use to solve bounded reachability queries on MAs.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(maMethods)).setDefaultValueString("unifplus").build()).build());
                 
                 std::vector<std::string> multiplicationStyles = {"gaussseidel", "regular", "gs", "r"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, valueIterationMultiplicationStyleOptionName, false, "Sets which method multiplication style to prefer for value iteration.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, valueIterationMultiplicationStyleOptionName, false, "Sets which method multiplication style to prefer for value iteration.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a multiplication style.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(multiplicationStyles)).setDefaultValueString("gaussseidel").build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, intervalIterationSymmetricUpdatesOptionName, false, "If set, interval iteration performs an update on both, lower and upper bound in each iteration").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, intervalIterationSymmetricUpdatesOptionName, false, "If set, interval iteration performs an update on both, lower and upper bound in each iteration").setIsAdvanced().build());
                 
             }
             

src/storm/settings/modules/ModelCheckerSettings.cpp

@@ -16,7 +16,7 @@ namespace storm {
             const std::string ModelCheckerSettings::filterRewZeroOptionName = "filterrewzero";
 
             ModelCheckerSettings::ModelCheckerSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, filterRewZeroOptionName, false, "If set, states with reward zero are filtered out, potentially reducing the size of the equation system").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, filterRewZeroOptionName, false, "If set, states with reward zero are filtered out, potentially reducing the size of the equation system").setIsAdvanced().build());
             }
             
             bool ModelCheckerSettings::isFilterRewZeroSet() const {

src/storm/settings/modules/ModuleSettings.cpp

@@ -69,10 +69,12 @@ namespace storm {
                 this->options.push_back(option);
             }
             
-            uint_fast64_t ModuleSettings::getPrintLengthOfLongestOption() const {
+            uint_fast64_t ModuleSettings::getPrintLengthOfLongestOption(bool includeAdvanced) const {
                 uint_fast64_t length = 0;
                 for (auto const& option : this->options) {
-                    length = std::max(length, option->getPrintLength());
+                    if (includeAdvanced || !option->getIsAdvanced()) {
+                        length = std::max(length, option->getPrintLength());
+                    }
                 }
                 return length;
             }

src/storm/settings/modules/ModuleSettings.h

@@ -72,9 +72,10 @@ namespace storm {
                 /*!
                  * Retrieves the (print) length of the longest option.
                  *
+                 * @param includeAdvanced if set, also includes options flagged as advanced.
                  * @return The length of the longest option.
                  */
-                uint_fast64_t getPrintLengthOfLongestOption() const;
+                uint_fast64_t getPrintLengthOfLongestOption(bool includeAdvanced) const;
                 
                 /*!
                  * Restores the default values for all arguments of all options.

src/storm/settings/modules/MultiObjectiveSettings.cpp

@@ -21,12 +21,12 @@ namespace storm {
             
             MultiObjectiveSettings::MultiObjectiveSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = {"pcaa", "constraintbased"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, methodOptionName, true, "The method to be used for multi objective model checking.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("pcaa").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, exportPlotOptionName, true, "Saves data for plotting of pareto curves and achievable values.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, methodOptionName, true, "The method to be used for multi objective model checking.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("pcaa").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportPlotOptionName, true, "Saves data for plotting of pareto curves and achievable values.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing 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.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for the approximation of numerical- and pareto queries.").setIsAdvanced()
                                 .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).")
+                this->addOption(storm::settings::OptionBuilder(moduleName, maxStepsOptionName, true, "Aborts the computation after the given number of refinement steps (= computed pareto optimal points).").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "the threshold for the number of refinement steps to be performed.").build()).build());
                 std::vector<std::string> memoryPatterns = {"positional", "goalmemory", "arbitrary"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, schedulerRestrictionOptionName, false, "Restricts the class of considered schedulers to non-randomized schedulers with the provided memory pattern.")

src/storm/settings/modules/MultiplierSettings.cpp

@@ -16,7 +16,7 @@ namespace storm {
 
             MultiplierSettings::MultiplierSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> multiplierTypes = {"native", "gmmxx"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, multiplierTypeOptionName, true, "Sets which type of multiplier is preferred.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, multiplierTypeOptionName, true, "Sets which type of multiplier is preferred.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a multiplier.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(multiplierTypes)).setDefaultValueString("gmmxx").build()).build());
                 
             }

src/storm/settings/modules/NativeEquationSolverSettings.cpp

@@ -27,21 +27,21 @@ namespace storm {
 
             NativeEquationSolverSettings::NativeEquationSolverSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = { "jacobi", "gaussseidel", "sor", "walkerchae", "power", "sound-value-iteration", "svi", "interval-iteration", "ii", "ratsearch" };
-                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, techniqueOptionName, true, "The method to be used for solving linear equation systems with the native engine.").setIsAdvanced().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.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setIsAdvanced().setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, omegaOptionName, false, "The omega used for SOR.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The value of the SOR parameter.").setDefaultValueDouble(0.9).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, omegaOptionName, false, "The omega used for SOR.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The value of the SOR parameter.").setDefaultValueDouble(0.9).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").setIsAdvanced().build());
                 
                 std::vector<std::string> multiplicationStyles = {"gaussseidel", "regular", "gs", "r"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, powerMethodMultiplicationStyleOptionName, false, "Sets which method multiplication style to prefer for the power method.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, powerMethodMultiplicationStyleOptionName, false, "Sets which method multiplication style to prefer for the power method.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a multiplication style.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(multiplicationStyles)).setDefaultValueString("gaussseidel").build()).build());
                                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, intervalIterationSymmetricUpdatesOptionName, false, "If set, interval iteration performs an update on both, lower and upper bound in each iteration").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, intervalIterationSymmetricUpdatesOptionName, false, "If set, interval iteration performs an update on both, lower and upper bound in each iteration").setIsAdvanced().build());
             }
             
             bool NativeEquationSolverSettings::isLinearEquationSystemTechniqueSet() const {

src/storm/settings/modules/Smt2SmtSolverSettings.cpp

@@ -16,9 +16,9 @@ namespace storm {
             const std::string Smt2SmtSolverSettings::exportScriptOption = "exportscript";
             
             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, 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.").setIsAdvanced().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 exported to.").setDefaultValueString("").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportScriptOption, true, "If set, the SMT-LIBv2 script will be exportet to this file.").setIsAdvanced().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{

src/storm/settings/modules/SylvanSettings.cpp

@@ -16,8 +16,8 @@ namespace storm {
             const std::string SylvanSettings::threadCountOptionName = "threads";
             
             SylvanSettings::SylvanSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Sylvan in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Sylvan.").setDefaultValueUnsignedInteger(4096).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, threadCountOptionName, true, "Sets the number of threads used by Sylvan.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The number of threads available to Sylvan (0 means 'auto-detect').").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Sylvan in MB.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Sylvan.").setDefaultValueUnsignedInteger(4096).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, threadCountOptionName, true, "Sets the number of threads used by Sylvan.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The number of threads available to Sylvan (0 means 'auto-detect').").build()).build());
             }
             
             uint_fast64_t SylvanSettings::getMaximalMemory() const {

src/storm/utility/string.cpp

@@ -9,9 +9,13 @@ namespace storm {
                 // intentionally left empty.
             }
             
-            bool SimilarStrings::add(std::string const& string) {
+            bool SimilarStrings::isSimilar(std::string const& string) const {
                 double distance = levenshteinDistance(reference, string, caseSensitive);
-                if (distance <= static_cast<double>(std::max(reference.size(), string.size())) * (1.0 - similarityFactor)) {
+                return distance <= static_cast<double>(std::max(reference.size(), string.size())) * (1.0 - similarityFactor);
+            }
+            
+            bool SimilarStrings::add(std::string const& string) {
+                if (isSimilar(string)) {
                     distances.emplace(storm::utility::string::levenshteinDistance(reference, string, caseSensitive), string);
                     return true;
                 }
@@ -32,9 +36,9 @@ namespace storm {
                 if (size == 0) {
                     return "";
                 } else if (size == 1) {
-                    return "Did you mean " + result + " ?";
+                    return "Did you mean '" + result + "'?";
                 } else {
-                    return "Did you mean any of [ " + result + " ] ?";
+                    return "Did you mean any of [" + result + "] ?";
                 }
             }
             
@@ -51,11 +55,11 @@ namespace storm {
                     for (uint64_t col = 1; col < d[row].size(); ++col) {
                         uint64_t cost = 1;
                         if (caseSensitive) {
-                            if (tolower(lhs[row-1]) == tolower(rhs[col-1])) {
+                            if (lhs[row-1] == rhs[col-1]) {
                                 cost = 0;
                             }
                         } else {
-                            if (lhs[row-1] == rhs[col-1]) {
+                            if (tolower(lhs[row-1]) == tolower(rhs[col-1])) {
                                 cost = 0;
                             }
                         }

src/storm/utility/string.h

@@ -18,6 +18,11 @@ namespace storm {
                  */
                 SimilarStrings(std::string reference, double similarityFactor = 0.6, bool caseSensitive = true);
                 
+                /*!
+                 * @return true, if the given string is considered similar.
+                 */
+                bool isSimilar(std::string const& string) const;
+                
                 /*!
                  * Adds the given string to the set of similar strings (if it is similar)
                  * @return true, if the given string is considered similar.
@@ -26,7 +31,6 @@ namespace storm {
                 
                 /*!
                  * Gets a list of all added strings that are similar to the reference string.
-                 * Erases all strings gathered so far.
                  */
                 std::vector<std::string> toList() const;