From 91bbe85a0768731e5befe958cd7ecd5ac5c06d57 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Wed, 16 May 2018 22:55:34 +0200
Subject: [PATCH] builder options for labeling overlapping guards

---
 src/storm/builder/BuilderOptions.cpp | 11 ++++++++++-
 src/storm/builder/BuilderOptions.h   | 12 +++++++++++-
 2 files changed, 21 insertions(+), 2 deletions(-)

diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp
index 33152ca36..d4d729d21 100644
--- a/src/storm/builder/BuilderOptions.cpp
+++ b/src/storm/builder/BuilderOptions.cpp
@@ -36,7 +36,7 @@ namespace storm {
             return boost::get<storm::expressions::Expression>(labelOrExpression);
         }
         
-        BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false), addOutOfBoundsState(false), showProgress(false), showProgressDelay(0) {
+        BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false), addOverlappingGuardsLabel(false), addOutOfBoundsState(false), showProgress(false), showProgressDelay(0) {
             // Intentionally left empty.
         }
         
@@ -164,6 +164,10 @@ namespace storm {
             return addOutOfBoundsState;
         }
 
+        bool BuilderOptions::isAddOverlappingGuardLabelSet() const {
+            return addOverlappingGuardsLabel;
+        }
+
         BuilderOptions& BuilderOptions::setBuildAllRewardModels(bool newValue) {
             buildAllRewardModels = newValue;
             return *this;
@@ -238,5 +242,10 @@ namespace storm {
             return *this;
         }
 
+        BuilderOptions& BuilderOptions::setAddOverlappingGuardsLabel(bool newValue) {
+            addOverlappingGuardsLabel = newValue;
+            return *this;
+        }
+
     }
 }
diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h
index c6106172b..904d45de6 100644
--- a/src/storm/builder/BuilderOptions.h
+++ b/src/storm/builder/BuilderOptions.h
@@ -108,6 +108,7 @@ namespace storm {
             bool isExplorationChecksSet() const;
             bool isShowProgressSet() const;
             bool isAddOutOfBoundsStateSet() const;
+            bool isAddOverlappingGuardLabelSet() const;
             uint64_t getShowProgressDelay() const;
 
             /**
@@ -164,6 +165,12 @@ namespace storm {
              */
             BuilderOptions& setAddOutOfBoundsState(bool newValue = true);
 
+            /**
+             * Should a state be labelled for overlapping guards
+             * @param newValue the new value (default true)
+             */
+            BuilderOptions& setAddOverlappingGuardsLabel(bool newValue = true);
+
 
         private:
             /// A flag that indicates whether all reward models are to be built. In this case, the reward model names are
@@ -194,10 +201,13 @@ namespace storm {
             // A flag that indicates whether or not to generate the information from which parts of the model specification
             // each choice originates.
             bool buildChoiceOrigins;
-            
+
             /// A flag that stores whether exploration checks are to be performed.
             bool explorationChecks;
 
+            /// A flag for states with overlapping guards
+            bool addOverlappingGuardsLabel;
+
             /// A flag indicating that the an additional state for out of bounds should be created.
             bool addOutOfBoundsState;