Further work on option system (we're getting there...).

Former-commit-id: cae593d5a1

src/settings/SettingsManager.cpp

@@ -65,7 +65,7 @@ namespace storm {
                 if (currentArgument.at(0) == '-') {
                     // At this point we know that a new option is about to come. Hence, we need to assign the current
                     // cache content to the option that was active until now.
-                    this->setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->longNameToOptions : this->shortNameToOptions, argumentCache);
+                    setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->longNameToOptions : this->shortNameToOptions, argumentCache);
                     
                     if (currentArgument.at(1) == '-') {
                         // In this case, the argument has to be the long name of an option. Try to get all options that
@@ -121,18 +121,36 @@ namespace storm {
             // not required for this option, we have to add both versions to our mappings, the prefixed one and the
             // non-prefixed one.
             if (!option->getRequiresModulePrefix()) {
+                bool isCompatible = this->isCompatible(option, option->getLongName(), this->longNameToOptions);
+                LOG_THROW(isCompatible, storm::exceptions::IllegalFunctionCallException, "Unable to add option '" << option->getLongName() << "', because an option with the same name is incompatible with it.");
                 this->longNameToOptions.emplace(option->getLongName(), option);
             }
+            // For the prefixed name, we don't need a compatibility check, because a module is not allowed to register the same option twice.
             this->longNameToOptions.emplace(option->getModuleName() + ":" + option->getLongName(), option);
             
             if (option->getHasShortName()) {
                 if (!option->getRequiresModulePrefix()) {
-                    this->shortNameToOptions.emplace(option->getLongName(), option);
+                    this->shortNameToOptions.emplace(option->getShortName(), option);
+                    bool isCompatible = this->isCompatible(option, option->getShortName(), this->shortNameToOptions);
+                    LOG_THROW(isCompatible, storm::exceptions::IllegalFunctionCallException, "Unable to add option '" << option->getLongName() << "', because an option with the same name is incompatible with it.");
                 }
                 this->shortNameToOptions.emplace(option->getModuleName() + ":" + option->getShortName(), option);
             }
         }
         
+        bool SettingsManager::isCompatible(std::shared_ptr<Option> const& option, std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap) {
+            auto optionIterator = optionMap.find(optionName);
+            if (optionIterator != optionMap.end()) {
+                for (auto const& otherOption : optionIterator->second) {
+                    bool locallyCompatible = option->isCompatibleWith(*otherOption);
+                    if (!locallyCompatible) {
+                        return false;
+                    }
+                }
+            }
+            return true;
+        }
+        
         void SettingsManager::setOptionsArguments(std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap, std::vector<std::string> const& argumentCache) {
             auto optionIterator = optionMap.find(optionName);
             LOG_THROW(optionIterator != optionMap.end(), storm::exceptions::OptionParserException, "Unknown option '" << optionName << "'.");

src/settings/SettingsManager.h

@@ -144,7 +144,12 @@ namespace storm {
              * @param optionMap The mapping from option names to options.
              * @param argumentCache The arguments of the option as string values.
              */
-            void setOptionsArguments(std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap, std::vector<std::string> const& argumentCache);
+            static void setOptionsArguments(std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap, std::vector<std::string> const& argumentCache);
+            
+            /*!
+             * Checks whether the given option is compatible with all options with the given name in the given mapping.
+             */
+            static bool isCompatible(std::shared_ptr<Option> const& option, std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap);
         };
         
         /*!

src/settings/modules/CounterexampleGeneratorSettings.cpp

@@ -14,12 +14,40 @@ namespace storm {
             
             CounterexampleGeneratorSettings::CounterexampleGeneratorSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
                 std::vector<std::string> techniques = {"sat", "milp"};
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command set. Note that this requires the model to be given in a symbolic format.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command set. Note that this requires the model to be given in a symbolic format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file containing the properties for which counterexamples are to be generated.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample. Available are {milp, maxsat}").setDefaultValueString("maxsat").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(techniques)).build()).build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, true, "Sets whether to display statistics for counterexample generation.").build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based minimal command counterexample generation.").build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, true, "Sets whether to display statistics for counterexample generation.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based minimal command counterexample generation.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build());
+            }
+            
+            bool CounterexampleGeneratorSettings::isMinimalCommandGenerationSet() const {
+                return this->getOption(minimalCommandSetOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string CounterexampleGeneratorSettings::minimalCommandSetPropertyFilename() const {
+                return this->getOption(minimalCommandSetOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            bool CounterexampleGeneratorSettings::isUseMilpBasedMinimalCommandSetGenerationSet() const {
+                return this->getOption(minimalCommandSetOptionName).getArgumentByName("method").getValueAsString() == "milp";
+            }
+            
+            bool CounterexampleGeneratorSettings::isUseMaxSatBasedMinimalCommandSetGenerationSet() const {
+                return this->getOption(minimalCommandSetOptionName).getArgumentByName("method").getValueAsString() == "maxsat";
+            }
+            
+            bool CounterexampleGeneratorSettings::isEncodeReachabilitySet() const {
+                return this->getOption(encodeReachabilityOptionName).getHasOptionBeenSet();
+            }
+            
+            bool CounterexampleGeneratorSettings::isUseSchedulerCutsSet() const {
+                return this->getOption(schedulerCutsOptionName).getHasOptionBeenSet();
+            }
+            
+            bool CounterexampleGeneratorSettings::isShowStatisticsSet() const {
+                return this->getOption(statisticsOptionName).getHasOptionBeenSet();
             }
             
         } // namespace modules

src/settings/modules/CounterexampleGeneratorSettings.h

@@ -40,7 +40,7 @@ namespace storm {
                  *
                  * @return True iff the MILP-based technique is to be used.
                  */
-                bool useMilpBasedMinimalCommandSetGeneration() const;
+                bool isUseMilpBasedMinimalCommandSetGenerationSet() const;
 
                 /*!
                  * Retrieves whether the MAXSAT-based technique is to be used to generate a minimal command set
@@ -48,7 +48,7 @@ namespace storm {
                  *
                  * @return True iff the MAXSAT-based technique is to be used.
                  */
-                bool useMaxSatBasedMinimalCommandSetGeneration() const;
+                bool isUseMaxSatBasedMinimalCommandSetGenerationSet() const;
                 
                 /*!
                  * Retrieves whether reachability of a target state is to be encoded if the MAXSAT-based technique is
@@ -64,14 +64,14 @@ namespace storm {
                  *
                  * @return True iff scheduler cuts are to be used.
                  */
-                bool useSchedulerCuts() const;
+                bool isUseSchedulerCutsSet() const;
                 
                 /*!
                  * Retrieves whether statistics are to be shown for counterexample generation.
                  *
                  * @return True iff statistics are to be shown for counterexample generation.
                  */
-                bool showStatistics() const;
+                bool isShowStatisticsSet() const;
                 
                 // The name of the module.
                 static const std::string moduleName;

src/settings/modules/CuddSettings.cpp

@@ -12,9 +12,9 @@ namespace storm {
             const std::string reorderOptionName = "reorder";
             
             CuddSettings::CuddSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
                 
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mb", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(2048).build()).build());
+                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(2048).build()).build());
                 
                 std::vector<std::string> reorderingTechniques;
                 reorderingTechniques.push_back("none");
@@ -35,7 +35,57 @@ namespace storm {
                 reorderingTechniques.push_back("annealing");
                 reorderingTechniques.push_back("genetic");
                 reorderingTechniques.push_back("exact");
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, reorderOptionName, true, "Sets the reordering technique used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used by Cudd's reordering routines. Must be in {none, random, randompivot, sift, siftconv, ssift, ssiftconv, gsift, gsiftconv, win2, win2conv, win3, win3conv, win4, win4conv, annealing, genetic, exact}.").setDefaultValueString("gsift").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(reorderingTechniques)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, reorderOptionName, true, "Sets the reordering technique used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used by Cudd's reordering routines. Must be in {none, random, randompivot, sift, siftconv, ssift, ssiftconv, gsift, gsiftconv, win2, win2conv, win3, win3conv, win4, win4conv, annealing, genetic, exact}.").setDefaultValueString("gsift").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(reorderingTechniques)).build()).build());
+            }
+            
+            double CuddSettings::getConstantPrecision() const {
+                return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
+            }
+            
+            uint_fast64_t CuddSettings::getMaximalMemory() const {
+                return this->getOption(maximalMemoryOptionName).getArgumentByName("value").getValueAsUnsignedInteger();
+            }
+            
+            CuddSettings::ReorderingTechnique CuddSettings::getReorderingTechnique() const {
+                std::string reorderingTechniqueAsString = this->getOption(reorderOptionName).getArgumentByName("method").getValueAsString();
+                if (reorderingTechniqueAsString == "none") {
+                    return CuddSettings::ReorderingTechnique::None;
+                } else if (reorderingTechniqueAsString == "random") {
+                    return CuddSettings::ReorderingTechnique::Random;
+                } else if (reorderingTechniqueAsString == "randompivot") {
+                    return CuddSettings::ReorderingTechnique::RandomPivot;
+                } else if (reorderingTechniqueAsString == "sift") {
+                    return CuddSettings::ReorderingTechnique::Sift;
+                } else if (reorderingTechniqueAsString == "siftconv") {
+                    return CuddSettings::ReorderingTechnique::SiftConv;
+                } else if (reorderingTechniqueAsString == "ssift") {
+                    return CuddSettings::ReorderingTechnique::SymmetricSift;
+                } else if (reorderingTechniqueAsString == "ssiftconv") {
+                    return CuddSettings::ReorderingTechnique::SymmetricSiftConv;
+                } else if (reorderingTechniqueAsString == "gsift") {
+                    return CuddSettings::ReorderingTechnique::GroupSift;
+                } else if (reorderingTechniqueAsString == "gsiftconv") {
+                    return CuddSettings::ReorderingTechnique::GroupSiftConv;
+                } else if (reorderingTechniqueAsString == "win2") {
+                    return CuddSettings::ReorderingTechnique::Win2;
+                } else if (reorderingTechniqueAsString == "win2conv") {
+                    return CuddSettings::ReorderingTechnique::Win2Conv;
+                } else if (reorderingTechniqueAsString == "win3") {
+                    return CuddSettings::ReorderingTechnique::Win3;
+                } else if (reorderingTechniqueAsString == "win3conv") {
+                    return CuddSettings::ReorderingTechnique::Win3Conv;
+                } else if (reorderingTechniqueAsString == "win4") {
+                    return CuddSettings::ReorderingTechnique::Win4;
+                } else if (reorderingTechniqueAsString == "win4conv") {
+                    return CuddSettings::ReorderingTechnique::Win4Conv;
+                } else if (reorderingTechniqueAsString == "annealing") {
+                    return CuddSettings::ReorderingTechnique::Annealing;
+                } else if (reorderingTechniqueAsString == "genetic") {
+                    return CuddSettings::ReorderingTechnique::Genetic;
+                } else if (reorderingTechniqueAsString == "exact") {
+                    return CuddSettings::ReorderingTechnique::Exact;
+                }
+                LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << reorderingTechniqueAsString << "' set as reordering technique of Cudd.");
             }
             
         } // namespace modules

src/settings/modules/DebugSettings.cpp

@@ -13,12 +13,28 @@ namespace storm {
             const std::string DebugSettings::logfileOptionShortName = "l";
 
             DebugSettings::DebugSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Print debug output.").build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, traceOptionName, false, "Print even more debug output.").build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, logfileOptionName, false, "If specified, the log output will also be written to this file.").setShortName(logfileOptionShortName)
+                this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Print debug output.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, traceOptionName, false, "Print even more debug output.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, logfileOptionName, false, "If specified, the log output will also be written to this file.").setShortName(logfileOptionShortName)
                                           .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to write the log.").build()).build());
             }
             
+            bool DebugSettings::isDebugSet() const {
+                return this->getOption(debugOptionName).getHasOptionBeenSet();
+            }
+            
+            bool DebugSettings::isTraceSet() const {
+                return this->getOption(traceOptionName).getHasOptionBeenSet();
+            }
+            
+            bool DebugSettings::isLogfileSet() const {
+                return this->getOption(logfileOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string DebugSettings::getLogfilename() const {
+                return this->getOption(traceOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm

src/settings/modules/GeneralSettings.cpp

@@ -37,48 +37,188 @@ namespace storm {
             
             GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
                 std::vector<std::string> moduleNames = {"all", "general", "debug", "cudd", "counterexample", "glpk", "gurobi", "gmm++", "native"};
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
+                this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("module", "The module for which to show the help or 'all' for all modules.").setDefaultValueString("all").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(moduleNames)).build()).build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The internally used precision.").setShortName(precisionOptionShortName)
+                this->addOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The internally used precision.").setShortName(precisionOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
-                this->addAndRegisterOption(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.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName)
+                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.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName)
+                this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName)
+                this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, pctlOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, pctlOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the PCTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, cslOptionName, false, "Specifies the CSL formulas that are to be checked on the model.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, cslOptionName, false, "Specifies the CSL formulas that are to be checked on the model.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the CSL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, ltlOptionName, false, "Specifies the LTL formulas that are to be checked on the model.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, ltlOptionName, false, "Specifies the LTL formulas that are to be checked on the model.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model")
+                this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the counterexample is to be written.").build()).build());
                 
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, "", "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
+                this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, "", "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-                this->addAndRegisterOption(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 + ").")
+                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.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, fixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(fixDeadlockOptionShortName).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, fixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(fixDeadlockOptionShortName).build());
                 
                 std::vector<std::string> linearEquationSolver = {"gmm++", "native"};
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, timeoutOptionName, false, "If given, computation will abort after the timeout has been reached.").setShortName(timeoutOptionShortName)
+                this->addOption(storm::settings::OptionBuilder(moduleName, timeoutOptionName, false, "If given, computation will abort after the timeout has been reached.").setShortName(timeoutOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "The number of seconds after which to timeout.").setDefaultValueUnsignedInteger(0).build()).build());
-
+                
                 std::vector<std::string> lpSolvers = {"gurobi", "glpk"};
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build());
-                this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName)
+                this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build());
             }
             
+            bool GeneralSettings::isHelpSet() const {
+                return this->getOption(helpOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string GeneralSettings::getHelpModuleName() const {
+                return this->getOption(helpOptionName).getArgumentByName("module").getValueAsString();
+            }
+            
+            bool GeneralSettings::isVerboseSet() const {
+                return this->getOption(verboseOptionName).getHasOptionBeenSet();
+            }
+            
+            double GeneralSettings::getPrecision() const {
+                return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
+            }
+            
+            bool GeneralSettings::isExportDotSet() const {
+                return this->getOption(exportDotOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string GeneralSettings::getExportDotFilename() const {
+                return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            bool GeneralSettings::isConfigSet() const {
+                return this->getOption(configOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string GeneralSettings::getConfigFilename() const {
+                return this->getOption(configOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            bool GeneralSettings::isExplicitSet() const {
+                return this->getOption(explicitOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string GeneralSettings::getTransitionFilename() const {
+                return this->getOption(explicitOptionName).getArgumentByName("transition filename").getValueAsString();
+            }
+                        
+            std::string GeneralSettings::getLabelingFilename() const {
+                return this->getOption(explicitOptionName).getArgumentByName("labeling filename").getValueAsString();
+            }
+            
+            bool GeneralSettings::isSymbolicSet() const {
+                return this->getOption(symbolicOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string GeneralSettings::getSymbolicModelFilename() const {
+                return this->getOption(symbolicOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            bool GeneralSettings::isPctlSet() const {
+                return this->getOption(pctlOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string GeneralSettings::getPctlPropertiesFilename() const {
+                return this->getOption(pctlOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            bool GeneralSettings::isCslSet() const {
+                return this->getOption(cslOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string GeneralSettings::getCslPropertiesFilename() const {
+                return this->getOption(cslOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            bool GeneralSettings::isLtlSet() const {
+                return this->getOption(ltlOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string GeneralSettings::getLtlPropertiesFilename() const {
+                return this->getOption(ltlOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            bool GeneralSettings::isTransitionRewardsSet() const {
+                return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string GeneralSettings::getTransitionRewardsFilename() const {
+                return this->getOption(transitionRewardsOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            bool GeneralSettings::isStateRewardsSet() const {
+                return this->getOption(stateRewardsOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string GeneralSettings::getStateRewardsFilename() const {
+                return this->getOption(stateRewardsOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            bool GeneralSettings::isCounterexampleSet() const {
+                return this->getOption(counterexampleOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string GeneralSettings::getCounterexampleFilename() const {
+                return this->getOption(counterexampleOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            bool GeneralSettings::isFixDeadlocksSet() const {
+                return this->getOption(fixDeadlockOptionName).getHasOptionBeenSet();
+            }
+            
+            bool GeneralSettings::isTimeoutSet() const {
+                return this->getOption(timeoutOptionName).getHasOptionBeenSet();
+            }
+            
+            uint_fast64_t GeneralSettings::getTimeoutInSeconds() const {
+                return this->getOption(timeoutOptionName).getArgumentByName("time").getValueAsUnsignedInteger();
+            }
+            
+            GeneralSettings::EquationSolver GeneralSettings::getEquationSolver() const {
+                std::string equationSolverName = this->getOption(eqSolverOptionName).getArgumentByName("name").getValueAsString();
+                if (equationSolverName == "gmm++") {
+                    return GeneralSettings::EquationSolver::Gmmxx;
+                } else if (equationSolverName == "native") {
+                    return GeneralSettings::EquationSolver::Native;
+                }
+                LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown equation solver '" << equationSolverName << "'.");
+            }
+            
+            GeneralSettings::LpSolver GeneralSettings::getLpSolver() const {
+                std::string lpSolverName = this->getOption(lpSolverOptionName).getArgumentByName("name").getValueAsString();
+                if (lpSolverName == "gurobi") {
+                    return GeneralSettings::LpSolver::Gurobi;
+                } else if (lpSolverName == "glpk") {
+                    return GeneralSettings::LpSolver::glpk;
+                }
+                LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << equationSolverName << "'.");
+            }
+            
+            bool GeneralSettings::isConstantsSet() const {
+                return this->getOption(constantsOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string GeneralSettings::getConstantDefinitionString() const {
+                return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString();
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm

src/settings/modules/ModuleSettings.cpp

@@ -35,6 +35,18 @@ namespace storm {
                 return result;
             }
             
+            Option const& ModuleSettings::getOption(std::string const& longName) const {
+                auto optionIterator = this->options.find(longName);
+                LOG_THROW(optionIterator != this->options.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'.");
+                return *optionIterator->second;
+            }
+
+            Option& ModuleSettings::getOption(std::string const& longName)  {
+                auto optionIterator = this->options.find(longName);
+                LOG_THROW(optionIterator != this->options.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'.");
+                return *optionIterator->second;
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm

src/settings/modules/ModuleSettings.h

@@ -78,6 +78,14 @@ namespace storm {
                  */
                 Option& getOption(std::string const& longName);
                 
+                /*!
+                 * Retrieves the option with the given long name. If no such option exists, an exception is thrown.
+                 *
+                 * @param longName The long name of the option to retrieve.
+                 * @return The option associated with the given option name.
+                 */
+                Option const& getOption(std::string const& longName) const;
+                
                 /*!
                  * Retrieves whether the option with the given name was set.
                  *