builder options for labeling overlapping guards

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;
+        }
+
     }
 }

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;