Browse Source

Added test setting for quick activation/deactivation of test feature

Former-commit-id: a7bbfabcbe
tempestpy_adaptions
Mavo 9 years ago
parent
commit
3f06a51869
  1. 6
      src/settings/modules/DebugSettings.cpp
  2. 9
      src/settings/modules/DebugSettings.h

6
src/settings/modules/DebugSettings.cpp

@ -15,12 +15,14 @@ namespace storm {
const std::string DebugSettings::traceOptionName = "trace"; const std::string DebugSettings::traceOptionName = "trace";
const std::string DebugSettings::logfileOptionName = "logfile"; const std::string DebugSettings::logfileOptionName = "logfile";
const std::string DebugSettings::logfileOptionShortName = "l"; const std::string DebugSettings::logfileOptionShortName = "l";
const std::string DebugSettings::testOptionName = "test";
DebugSettings::DebugSettings() : ModuleSettings(moduleName) { DebugSettings::DebugSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Print debug output.").build()); 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, 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) 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()); .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());
} }
bool DebugSettings::isDebugSet() const { bool DebugSettings::isDebugSet() const {
@ -39,6 +41,10 @@ namespace storm {
return this->getOption(traceOptionName).getArgumentByName("filename").getValueAsString(); return this->getOption(traceOptionName).getArgumentByName("filename").getValueAsString();
} }
bool DebugSettings::isTestSet() const {
return this->getOption(testOptionName).getHasOptionBeenSet();
}
} // namespace modules } // namespace modules
} // namespace settings } // namespace settings
} // namespace storm } // namespace storm

9
src/settings/modules/DebugSettings.h

@ -45,6 +45,14 @@ namespace storm {
*/ */
std::string getLogfilename() const; std::string getLogfilename() const;
/*!
* Retrieves whether the test option was set. This is a general option which can be
* used for quick testing purposes to activate/decactivate a certain setting.
*
* @return True iff the test option was set.
*/
bool isTestSet() const;
// The name of the module. // The name of the module.
static const std::string moduleName; static const std::string moduleName;
@ -54,6 +62,7 @@ namespace storm {
static const std::string traceOptionName; static const std::string traceOptionName;
static const std::string logfileOptionName; static const std::string logfileOptionName;
static const std::string logfileOptionShortName; static const std::string logfileOptionShortName;
static const std::string testOptionName;
}; };
} // namespace modules } // namespace modules

Loading…
Cancel
Save