From 3f06a518694162c3fb2a47afed477b5f0fea0b4a Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Tue, 5 Apr 2016 16:31:57 +0200
Subject: [PATCH] Added test setting for quick activation/deactivation of test
 feature

Former-commit-id: a7bbfabcbe0b11be629209e18b40ec003b62cf67
---
 src/settings/modules/DebugSettings.cpp | 6 ++++++
 src/settings/modules/DebugSettings.h   | 9 +++++++++
 2 files changed, 15 insertions(+)

diff --git a/src/settings/modules/DebugSettings.cpp b/src/settings/modules/DebugSettings.cpp
index 16d035015..0f37e7ce7 100644
--- a/src/settings/modules/DebugSettings.cpp
+++ b/src/settings/modules/DebugSettings.cpp
@@ -15,12 +15,14 @@ namespace storm {
             const std::string DebugSettings::traceOptionName = "trace";
             const std::string DebugSettings::logfileOptionName = "logfile";
             const std::string DebugSettings::logfileOptionShortName = "l";
+            const std::string DebugSettings::testOptionName = "test";
  
             DebugSettings::DebugSettings() : ModuleSettings(moduleName) {
                 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());
+                this->addOption(storm::settings::OptionBuilder(moduleName, testOptionName, false, "Activate a test setting.").build());
             }
             
             bool DebugSettings::isDebugSet() const {
@@ -39,6 +41,10 @@ namespace storm {
                 return this->getOption(traceOptionName).getArgumentByName("filename").getValueAsString();
             }
             
+            bool DebugSettings::isTestSet() const {
+                return this->getOption(testOptionName).getHasOptionBeenSet();
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/DebugSettings.h b/src/settings/modules/DebugSettings.h
index f78a4e3a8..438017307 100644
--- a/src/settings/modules/DebugSettings.h
+++ b/src/settings/modules/DebugSettings.h
@@ -45,6 +45,14 @@ namespace storm {
                  */
                 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.
                 static const std::string moduleName;
                 
@@ -54,6 +62,7 @@ namespace storm {
                 static const std::string traceOptionName;
                 static const std::string logfileOptionName;
                 static const std::string logfileOptionShortName;
+                static const std::string testOptionName;
             };
             
         } // namespace modules