From debabb01bb8a9d365033ca36b593b989b7bddbb3 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Thu, 6 Feb 2020 14:54:48 +0100
Subject: [PATCH] cmd line arguments for hinting on the number of states added

---
 src/storm-dft/settings/DftSettings.cpp      |  2 +
 src/storm-pars/settings/ParsSettings.cpp    |  4 ++
 src/storm/settings/SettingsManager.cpp      |  2 +
 src/storm/settings/modules/HintSettings.cpp | 43 +++++++++++++++++++++
 src/storm/settings/modules/HintSettings.h   | 40 +++++++++++++++++++
 5 files changed, 91 insertions(+)
 create mode 100644 src/storm/settings/modules/HintSettings.cpp
 create mode 100644 src/storm/settings/modules/HintSettings.h

diff --git a/src/storm-dft/settings/DftSettings.cpp b/src/storm-dft/settings/DftSettings.cpp
index 4ff3e2aaf..a3d0bf4ed 100644
--- a/src/storm-dft/settings/DftSettings.cpp
+++ b/src/storm-dft/settings/DftSettings.cpp
@@ -24,6 +24,7 @@
 #include "storm-gspn/settings/modules/GSPNSettings.h"
 #include "storm-gspn/settings/modules/GSPNExportSettings.h"
 #include "storm/settings/modules/TransformationSettings.h"
+#include "storm/settings/modules/HintSettings.h"
 
 
 namespace storm {
@@ -39,6 +40,7 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::IOSettings>();
             storm::settings::addModule<storm::settings::modules::CoreSettings>();
             storm::settings::addModule<storm::settings::modules::TransformationSettings>();
+            storm::settings::addModule<storm::settings::modules::HintSettings>();
 
             storm::settings::addModule<storm::settings::modules::DebugSettings>();
             storm::settings::addModule<storm::settings::modules::ModelCheckerSettings>();
diff --git a/src/storm-pars/settings/ParsSettings.cpp b/src/storm-pars/settings/ParsSettings.cpp
index c0aab397d..36a16e33a 100644
--- a/src/storm-pars/settings/ParsSettings.cpp
+++ b/src/storm-pars/settings/ParsSettings.cpp
@@ -26,6 +26,8 @@
 #include "storm/settings/modules/JitBuilderSettings.h"
 #include "storm/settings/modules/MultiplierSettings.h"
 #include "storm/settings/modules/TransformationSettings.h"
+#include "storm/settings/modules/HintSettings.h"
+
 
 
 namespace storm {
@@ -57,6 +59,8 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::JitBuilderSettings>();
             storm::settings::addModule<storm::settings::modules::MultiplierSettings>();
             storm::settings::addModule<storm::settings::modules::TransformationSettings>();
+
+            storm::settings::addModule<storm::settings::modules::HintSettings>();
         }
     
     }
diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp
index 058d92d99..8e278fecb 100644
--- a/src/storm/settings/SettingsManager.cpp
+++ b/src/storm/settings/SettingsManager.cpp
@@ -39,6 +39,7 @@
 #include "storm/settings/modules/MultiObjectiveSettings.h"
 #include "storm/settings/modules/MultiplierSettings.h"
 #include "storm/settings/modules/TransformationSettings.h"
+#include "storm/settings/modules/HintSettings.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/file.h"
 #include "storm/utility/string.h"
@@ -670,6 +671,7 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::MultiObjectiveSettings>();
             storm::settings::addModule<storm::settings::modules::MultiplierSettings>();
             storm::settings::addModule<storm::settings::modules::TransformationSettings>();
+            storm::settings::addModule<storm::settings::modules::HintSettings>();
         }
 
     }
diff --git a/src/storm/settings/modules/HintSettings.cpp b/src/storm/settings/modules/HintSettings.cpp
new file mode 100644
index 000000000..4066c3fb1
--- /dev/null
+++ b/src/storm/settings/modules/HintSettings.cpp
@@ -0,0 +1,43 @@
+#include "storm/settings/modules/HintSettings.h"
+
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/exceptions/InvalidSettingsException.h"
+#include "storm/exceptions/IllegalArgumentValueException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            const std::string HintSettings::moduleName = "hints";
+
+            const std::string stateHintOption = "states";
+
+
+            HintSettings::HintSettings() : ModuleSettings(moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, stateHintOption, true,
+                                                               "Estimate of the number of reachable states").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("number", "size.").build()).build());
+
+            }
+
+            bool HintSettings::isNumberStatesSet() const {
+                return this->getOption(stateHintOption).getHasOptionBeenSet();
+            }
+
+            uint64_t HintSettings::getNumberStates() const {
+                return this->getOption(stateHintOption).getArgumentByName("number").getValueAsUnsignedInteger();
+            }
+
+            bool HintSettings::check() const {
+                return true;
+            }
+
+            void HintSettings::finalize() {
+                //Intentionally left empty
+            }
+
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
diff --git a/src/storm/settings/modules/HintSettings.h b/src/storm/settings/modules/HintSettings.h
new file mode 100644
index 000000000..459c83443
--- /dev/null
+++ b/src/storm/settings/modules/HintSettings.h
@@ -0,0 +1,40 @@
+#pragma once
+
+#include "storm-config.h"
+#include "storm/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            /*!
+             * This class represents the model transformer settings
+             */
+            class HintSettings : public ModuleSettings {
+            public:
+
+                /*!
+                 * Creates a new set of transformer settings.
+                 */
+                HintSettings();
+
+                /*!
+                 * Retrieves whether the option that estimates the number of states is set.
+                 */
+                bool isNumberStatesSet() const;
+
+                uint64_t getNumberStates() const;
+
+                bool check() const override;
+
+                void finalize() override;
+
+                // The name of the module.
+                static const std::string moduleName;
+
+            };
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
+