diff --git a/src/storm/settings/Option.cpp b/src/storm/settings/Option.cpp index 1ab2aa23a..99d03aede 100644 --- a/src/storm/settings/Option.cpp +++ b/src/storm/settings/Option.cpp @@ -117,8 +117,12 @@ namespace storm { bool Option::getHasOptionBeenSet() const { return this->hasBeenSet; } + + bool Option::getHasOptionBeenSetWithModulePrefix() const { + return this->hasBeenSetWithModulePrefix; + } - 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> const& optionArguments) : longName(longOptionName), hasShortName(hasShortOptionName), shortName(shortOptionName), description(optionDescription), moduleName(moduleName), isRequired(isOptionRequired), requireModulePrefix(requireModulePrefix), isAdvanced(isAdvanced), 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> const& optionArguments) : longName(longOptionName), hasShortName(hasShortOptionName), shortName(shortOptionName), description(optionDescription), moduleName(moduleName), isRequired(isOptionRequired), requireModulePrefix(requireModulePrefix), isAdvanced(isAdvanced), hasBeenSet(false), hasBeenSetWithModulePrefix(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."); @@ -138,6 +142,10 @@ namespace storm { void Option::setHasOptionBeenSet(bool newValue) { this->hasBeenSet = newValue; } + + void Option::setHasOptionBeenSetWithModulePrefix(bool newValue) { + this->hasBeenSetWithModulePrefix = newValue; + } uint_fast64_t Option::getPrintLength() const { uint_fast64_t length = 2; diff --git a/src/storm/settings/Option.h b/src/storm/settings/Option.h index 0ff675d21..926dad8d9 100644 --- a/src/storm/settings/Option.h +++ b/src/storm/settings/Option.h @@ -161,6 +161,13 @@ namespace storm { * @return True iff the option has been set. */ bool getHasOptionBeenSet() const; + + /*! + * Retrieves whether the option has been set by including the module prefix. + * + * @return True iff the option has been set by including the module prefix. + */ + bool getHasOptionBeenSetWithModulePrefix() const; /*! * Retrieves whether the option is only displayed in the advanced help. @@ -210,6 +217,9 @@ namespace storm { // A flag that indicates whether this option has been set. bool hasBeenSet; + + // A flag that indicates whether this option has been set. + bool hasBeenSetWithModulePrefix; // The arguments of this option (possibly empty). std::vector> arguments; @@ -239,6 +249,13 @@ namespace storm { * @param newValue The new status of the flag. */ void setHasOptionBeenSet(bool newValue = true); + + /*! + * Sets the flag that marks the option as being (un)set by including the module prefix. + * + * @param newValue The new status of the flag. + */ + void setHasOptionBeenSetWithModulePrefix(bool newValue = true); }; } } diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 04cb48621..f3b9009b2 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -494,6 +494,9 @@ namespace storm { } option->setHasOptionBeenSet(); + if (optionName != option->getLongName() && optionName != option->getShortName() && boost::starts_with(optionName, option->getModuleName())) { + option->setHasOptionBeenSetWithModulePrefix(); + } } void SettingsManager::setOptionsArguments(std::string const& optionName, std::unordered_map>> const& optionMap, std::vector const& argumentCache) { diff --git a/src/storm/settings/modules/ModuleSettings.cpp b/src/storm/settings/modules/ModuleSettings.cpp index 528535ec2..b9dde8b08 100644 --- a/src/storm/settings/modules/ModuleSettings.cpp +++ b/src/storm/settings/modules/ModuleSettings.cpp @@ -26,6 +26,7 @@ namespace storm { void ModuleSettings::unset(std::string const& name) { return this->getOption(name).setHasOptionBeenSet(false); + return this->getOption(name).setHasOptionBeenSetWithModulePrefix(false); } std::vector> const& ModuleSettings::getOptions() const {