From 5aa19c9a58e8fd46a9a1da2910151ce2ba51b3dd Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Mon, 15 Jul 2019 17:38:19 +0200
Subject: [PATCH] Added settings for non-Markovian state elimination

---
 src/storm/settings/SettingsManager.cpp        |  2 +
 .../modules/TransformationSettings.cpp        | 49 ++++++++++++++++
 .../settings/modules/TransformationSettings.h | 56 +++++++++++++++++++
 3 files changed, 107 insertions(+)
 create mode 100644 src/storm/settings/modules/TransformationSettings.cpp
 create mode 100644 src/storm/settings/modules/TransformationSettings.h

diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp
index 69ad4a909..7f5ffc604 100644
--- a/src/storm/settings/SettingsManager.cpp
+++ b/src/storm/settings/SettingsManager.cpp
@@ -37,6 +37,7 @@
 #include "storm/settings/modules/JitBuilderSettings.h"
 #include "storm/settings/modules/MultiObjectiveSettings.h"
 #include "storm/settings/modules/MultiplierSettings.h"
+#include "storm/settings/modules/TransformationSettings.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/file.h"
 #include "storm/utility/string.h"
@@ -568,6 +569,7 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::JitBuilderSettings>();
             storm::settings::addModule<storm::settings::modules::MultiObjectiveSettings>();
             storm::settings::addModule<storm::settings::modules::MultiplierSettings>();
+            storm::settings::addModule<storm::settings::modules::TransformationSettings>();
         }
 
     }
diff --git a/src/storm/settings/modules/TransformationSettings.cpp b/src/storm/settings/modules/TransformationSettings.cpp
new file mode 100644
index 000000000..75b1c3daf
--- /dev/null
+++ b/src/storm/settings/modules/TransformationSettings.cpp
@@ -0,0 +1,49 @@
+#include "TransformationSettings.h"
+
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/exceptions/InvalidSettingsException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            const std::string TransformationSettings::moduleName = "transformation";
+
+            const std::string TransformationSettings::chainEliminationOptionName = "eliminate-chains";
+            const std::string TransformationSettings::ignoreLabelingOptionName = "ec-ignore-labeling";
+
+
+            TransformationSettings::TransformationSettings() : ModuleSettings(moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, chainEliminationOptionName, false,
+                                                               "If set, chains of non-Markovian states are eliminated if the resulting model is a Markov Automaton.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, ignoreLabelingOptionName, false,
+                                                               "If set, the elimination of chains ignores the labels for all non-Markovian states. This may cause wrong results.").build());
+            }
+
+            bool TransformationSettings::isChainEliminationSet() const {
+                return this->getOption(chainEliminationOptionName).getHasOptionBeenSet();
+            }
+
+            bool TransformationSettings::isIgnoreLabelingSet() const {
+                return this->getOption(ignoreLabelingOptionName).getHasOptionBeenSet();
+            }
+
+
+            bool TransformationSettings::check() const {
+                // Ensure that labeling preservation is only set if chain elimination is set
+                STORM_LOG_THROW(isChainEliminationSet() || !isIgnoreLabelingSet(),
+                                storm::exceptions::InvalidSettingsException,
+                                "Label preservation can only be chosen if chain elimination is applied.");
+
+                return true;
+            }
+
+            void TransformationSettings::finalize() {
+                //Intentionally left empty
+            }
+
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
diff --git a/src/storm/settings/modules/TransformationSettings.h b/src/storm/settings/modules/TransformationSettings.h
new file mode 100644
index 000000000..ba646c763
--- /dev/null
+++ b/src/storm/settings/modules/TransformationSettings.h
@@ -0,0 +1,56 @@
+#ifndef STORM_TRANSFORMATIONSETTINGS_H
+#define STORM_TRANSFORMATIONSETTINGS_H
+
+#include "storm-config.h"
+#include "storm/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            /*!
+             * This class represents the model transformer settings
+             */
+            class TransformationSettings : public ModuleSettings {
+            public:
+
+                /*!
+                 * Creates a new set of transformer settings.
+                 */
+                TransformationSettings();
+
+                /*!
+                 * Retrieves whether the option to eliminate chains of non-Markovian states was set.
+                 *
+                 * @return True if the option to eliminate chains of non-Markovian states was set.
+                 */
+                bool isChainEliminationSet() const;
+
+
+                /*!
+                 * Retrieves whether the preserve-labeling option for jani was set.
+                 *
+                 * @return True if the preserve-labeling option was set.
+                 */
+                bool isIgnoreLabelingSet() const;
+
+
+                bool check() const override;
+
+                void finalize() override;
+
+                // The name of the module.
+                static const std::string moduleName;
+
+            private:
+                // Define the string names of the options as constants.
+                static const std::string chainEliminationOptionName;
+                static const std::string ignoreLabelingOptionName;
+
+            };
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
+
+#endif //STORM_TRANSFORMATIONSETTINGS_H