diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index f18f76bb1..ebc0bc0da 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -34,7 +34,6 @@ #include "storm/settings/modules/ExplorationSettings.h" #include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/AbstractionSettings.h" -#include "storm/settings/modules/JaniExportSettings.h" #include "storm/settings/modules/JitBuilderSettings.h" #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm/settings/modules/MultiplierSettings.h" @@ -138,7 +137,7 @@ namespace storm { } // Include the options from a possibly specified configuration file, but don't overwrite existing settings. - if (storm::settings::getModule().isConfigSet()) { + if (storm::settings::hasModule() && storm::settings::getModule().isConfigSet()) { this->setFromConfigurationFile(storm::settings::getModule().getConfigFilename()); } @@ -546,7 +545,6 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); - storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm/settings/SettingsManager.h b/src/storm/settings/SettingsManager.h index 1ccb10bfa..1e02e4471 100644 --- a/src/storm/settings/SettingsManager.h +++ b/src/storm/settings/SettingsManager.h @@ -270,6 +270,20 @@ namespace storm { return dynamic_cast(manager().getModule(SettingsType::moduleName)); } + + /*! + * Returns true if the given module is registered. + * + */ + template + bool hasModule() { + static_assert(std::is_base_of::value, "Template argument must be derived from ModuleSettings"); + if (manager().hasModule(SettingsType::moduleName)) { + return dynamic_cast(&(manager().getModule(SettingsType::moduleName))) != nullptr; + } + return false; + } + /*! * Retrieves the core settings in a mutable form. This is only meant to be used for debug purposes or very * rare cases where it is necessary.