Added settings for non-Markovian state elimination

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>();
         }
 
     }

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

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