From 193bddbd113c8edf6c47ba591fe4f351ae28ca24 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Wed, 8 Apr 2020 22:42:03 -0700
Subject: [PATCH] add overlapping guards label via command line

---
 src/storm-cli-utilities/model-handling.h     | 5 +++++
 src/storm/settings/modules/BuildSettings.cpp | 6 ++++++
 src/storm/settings/modules/BuildSettings.h   | 7 ++++++-
 3 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index e6508c190..334480cbf 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -448,6 +448,11 @@ namespace storm {
                 options.setBuildAllLabels(true);
                 options.setBuildAllRewardModels(true);
             }
+
+            if (buildSettings.isAddOverlappingGuardsLabelSet()) {
+                options.setAddOverlappingGuardsLabel(true);
+            }
+
             return storm::api::buildSparseModel<ValueType>(input.model.get(), options, useJit, storm::settings::getModule<storm::settings::modules::JitBuilderSettings>().isDoctorSet());
         }
         
diff --git a/src/storm/settings/modules/BuildSettings.cpp b/src/storm/settings/modules/BuildSettings.cpp
index 3d1852ba5..7ef3c894c 100644
--- a/src/storm/settings/modules/BuildSettings.cpp
+++ b/src/storm/settings/modules/BuildSettings.cpp
@@ -33,6 +33,7 @@ namespace storm {
             const std::string buildChoiceOriginsOptionName = "buildchoiceorig";
             const std::string buildStateValuationsOptionName = "buildstateval";
             const std::string buildOutOfBoundsStateOptionName = "buildoutofboundsstate";
+            const std::string buildOverlappingGuardsLabelOptionName = "overlappingguardslabel";
             const std::string bitsForUnboundedVariablesOptionName = "int-bits";
 
             BuildSettings::BuildSettings() : ModuleSettings(moduleName) {
@@ -51,6 +52,7 @@ namespace storm {
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, buildOutOfBoundsStateOptionName, false, "If set, a state for out-of-bounds valuations is added").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, buildOverlappingGuardsLabelOptionName, false, "For states where multiple guards are enabled, we add a label (for debugging DTMCs)").setIsAdvanced().build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, bitsForUnboundedVariablesOptionName, false, "Sets the number of bits that is used for unbounded integer variables.").setIsAdvanced()
                                         .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("number", "The number of bits.").addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedRangeValidatorExcluding(0,63)).setDefaultValueUnsignedInteger(32).build()).build());
             }
@@ -99,6 +101,10 @@ namespace storm {
                 return this->getOption(buildOutOfBoundsStateOptionName).getHasOptionBeenSet();
             }
 
+            bool BuildSettings::isAddOverlappingGuardsLabelSet() const {
+                return this->getOption(buildOverlappingGuardsLabelOptionName).getHasOptionBeenSet();
+            }
+
             storm::builder::ExplorationOrder BuildSettings::getExplorationOrder() const {
                 std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString();
                 if (explorationOrderAsString == "dfs") {
diff --git a/src/storm/settings/modules/BuildSettings.h b/src/storm/settings/modules/BuildSettings.h
index 3cce0a705..10ae675e3 100644
--- a/src/storm/settings/modules/BuildSettings.h
+++ b/src/storm/settings/modules/BuildSettings.h
@@ -99,7 +99,12 @@ namespace storm {
                  * @return
                  */
                 bool isBuildOutOfBoundsStateSet() const;
-                
+
+                /*!
+                 * Retrieves whether to build the overlapping label
+                 */
+                 bool isAddOverlappingGuardsLabelSet() const;
+
                 /*!
                  * Retrieves the number of bits that should be used to represent unbounded integer variables
                  * @return