From 93a0f7f8bb997b6b6b9169d2e322d21648cce93d Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 9 Sep 2015 12:08:42 +0200 Subject: [PATCH] settings: checks after config file, added finalize Former-commit-id: 6b3769a7a9366ed86b5b8d3dc9288c65e71ad61d --- src/settings/SettingsManager.cpp | 8 ++++++-- src/settings/SettingsManager.h | 3 ++- src/settings/modules/ModuleSettings.cpp | 4 +++- src/settings/modules/ModuleSettings.h | 7 ++++++- 4 files changed, 17 insertions(+), 5 deletions(-) diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index 18225f712..618fbfe77 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -137,7 +137,7 @@ namespace storm { } // Finally, check whether all modules are okay with the current settings. - this->checkAllModules(); + this->finalizeAllModules(); } void SettingsManager::setFromConfigurationFile(std::string const& configFilename) { @@ -162,6 +162,8 @@ namespace storm { } } } + // Finally, check whether all modules are okay with the current settings. + this->finalizeAllModules(); } void SettingsManager::printHelp(std::string const& hint) const { @@ -379,9 +381,11 @@ namespace storm { } } - void SettingsManager::checkAllModules() const { + void SettingsManager::finalizeAllModules() { for (auto const& nameModulePair : this->modules) { + nameModulePair.second->finalize(); nameModulePair.second->check(); + } } diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index f4fad9919..fd00654c3 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -189,9 +189,10 @@ namespace storm { static void addOptionToMap(std::string const& name, std::shared_ptr