Reduced code duplications as suggested by SJ

moves-rwth · May 23, 2024 · e4d3cea · e4d3cea
1 parent 2390574
commit e4d3cea
Show file tree

Hide file tree

Showing 4 changed files with 25 additions and 32 deletions.
diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp
@@ -119,8 +119,7 @@ JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani
                 this->terminalStates.emplace_back(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second);
             } else {
                 // If it's a label, i.e. refers to a transient boolean variable we do some sanity checks first
-                if (expressionOrLabelAndBool.first.getLabel() != "init" && expressionOrLabelAndBool.first.getLabel() != "deadlock" &&
-                    expressionOrLabelAndBool.first.getLabel() != "unexplored") {
+                if (!this->isSpecialLabel(expressionOrLabelAndBool.first.getLabel())) {
                     STORM_LOG_THROW(this->model.getGlobalVariables().hasVariable(expressionOrLabelAndBool.first.getLabel()),
                                     storm::exceptions::InvalidArgumentException,
                                     "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'.");

diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp
@@ -210,45 +210,36 @@ storm::models::sparse::StateLabeling NextStateGenerator<ValueType, StateType>::l
         }
     }
 
-    if (!result.containsLabel("init")) {
-        // Also label the initial state with the special label "init".
-        result.addLabel("init");
-        for (auto index : initialStateIndices) {
-            result.addLabelToState("init", index);
-        }
-    }
-    if (!result.containsLabel("deadlock")) {
-        result.addLabel("deadlock");
-        for (auto index : deadlockStateIndices) {
-            result.addLabelToState("deadlock", index);
-        }
-    }
-    if (!result.containsLabel("unexplored") && !unexploredStateIndices.empty()) {
-        result.addLabel("unexplored");
-        for (auto index : unexploredStateIndices) {
-            result.addLabelToState("unexplored", index);
+    auto addSpecialLabel = [&result](std::string const& label, auto const& indices) {
+        if (!result.containsLabel(label)) {
+            result.addLabel(label);
+            for (auto index : indices) {
+                result.addLabelToState(label, index);
+            }
         }
-    }
-
+    };
+    addSpecialLabel("init", initialStateIndices);
+    addSpecialLabel("deadlock", deadlockStateIndices);
+    addSpecialLabel("unexplored", unexploredStateIndices);
     if (this->options.isAddOverlappingGuardLabelSet()) {
         STORM_LOG_THROW(!result.containsLabel("overlap_guards"), storm::exceptions::WrongFormatException,
                         "Label 'overlap_guards' is reserved when adding overlapping guard labels");
-        result.addLabel("overlap_guards");
-        for (auto index : overlappingGuardStates.get()) {
-            result.addLabelToState("overlap_guards", index);
-        }
+        addSpecialLabel("overlap_guards", overlappingGuardStates.get());
     }
-
     if (this->options.isAddOutOfBoundsStateSet() && stateStorage.stateToId.contains(outOfBoundsState)) {
         STORM_LOG_THROW(!result.containsLabel("out_of_bounds"), storm::exceptions::WrongFormatException,
                         "Label 'out_of_bounds' is reserved when adding out of bounds states.");
-        result.addLabel("out_of_bounds");
-        result.addLabelToState("out_of_bounds", stateStorage.stateToId.getValue(outOfBoundsState));
+        addSpecialLabel("out_of_bounds", std::vector{stateStorage.stateToId.getValue(outOfBoundsState)});
     }
 
     return result;
 }
 
+template<typename ValueType, typename StateType>
+bool NextStateGenerator<ValueType, StateType>::isSpecialLabel(std::string const& label) const {
+    return label == "init" || label == "deadlock" || label == "unexplored" || label == "overlap_guards" || label == "out_of_bounds";
+}
+
 template<typename ValueType, typename StateType>
 void NextStateGenerator<ValueType, StateType>::unpackTransientVariableValuesIntoEvaluator(CompressedState const&,
                                                                                           storm::expressions::ExpressionEvaluator<ValueType>&) const {

diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h
@@ -140,6 +140,11 @@ class NextStateGenerator {
     void remapStateIds(std::function<StateType(StateType const&)> const& remapping);
 
    protected:
+    /*!
+     * Checks if the input label has a special purpose (e.g. "init", "deadlock", "unexplored", "overlap_guards", "out_of_bounds").
+     */
+    bool isSpecialLabel(std::string const& label) const;
+
     /*!
      * Creates the state labeling for the given states using the provided labels and expressions.
      */

diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp
@@ -90,9 +90,7 @@ PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::pr
                         std::make_pair(this->program.getLabelExpression(expressionOrLabelAndBool.first.getLabel()), expressionOrLabelAndBool.second));
                 } else {
                     // If the label is not present in the program and is not a special one, we raise an error.
-                    STORM_LOG_THROW(expressionOrLabelAndBool.first.getLabel() == "init" || expressionOrLabelAndBool.first.getLabel() == "deadlock" ||
-                                        expressionOrLabelAndBool.first.getLabel() == "unexplored",
-                                    storm::exceptions::InvalidArgumentException,
+                    STORM_LOG_THROW(this->isSpecialLabel(expressionOrLabelAndBool.first.getLabel()), storm::exceptions::InvalidArgumentException,
                                     "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'.");
                 }
             }
@@ -829,7 +827,7 @@ storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateTyp
             if (program.hasLabel(labelName)) {
                 labels.push_back(std::make_pair(labelName, program.getLabelExpression(labelName)));
             } else {
-                STORM_LOG_THROW(labelName == "init" || labelName == "deadlock" || labelName == "unexplored", storm::exceptions::InvalidArgumentException,
+                STORM_LOG_THROW(this->isSpecialLabel("labelName"), storm::exceptions::InvalidArgumentException,
                                 "Cannot build labeling for unknown label '" << labelName << "'.");
             }
         }