From 3696e1373688e1bac9b7cc3488d4f8773dd158f2 Mon Sep 17 00:00:00 2001
From: Joachim Klein <joachim.klein@automata.tools>
Date: Mon, 24 Aug 2020 22:24:57 +0200
Subject: [PATCH] (DA) ItemLabeling: addUniqueLabel, generateUniqueLabel

For model-automaton product constructions, we would like to add
automatically generated labels to the result, so we need a way to
ensure that we can get those without clashing with existing labels.
---
 src/storm/models/sparse/ItemLabeling.cpp | 24 ++++++++++++++++++++
 src/storm/models/sparse/ItemLabeling.h   | 29 ++++++++++++++++++++++++
 2 files changed, 53 insertions(+)

diff --git a/src/storm/models/sparse/ItemLabeling.cpp b/src/storm/models/sparse/ItemLabeling.cpp
index 329c961c8..47db00e3c 100644
--- a/src/storm/models/sparse/ItemLabeling.cpp
+++ b/src/storm/models/sparse/ItemLabeling.cpp
@@ -137,6 +137,18 @@ namespace storm {
                 labelings.emplace_back(std::move(labeling));
             }
 
+            std::string ItemLabeling::addUniqueLabel(std::string const& prefix, storage::BitVector const& labeling) {
+                std::string label = generateUniqueLabel(prefix);
+                addLabel(label, labeling);
+                return label;
+            }
+
+            std::string ItemLabeling::addUniqueLabel(std::string const& prefix, storage::BitVector const&& labeling) {
+                std::string label = generateUniqueLabel(prefix);
+                addLabel(label, labeling);
+                return label;
+            }
+
             bool ItemLabeling::containsLabel(std::string const& label) const {
                 return nameToLabelingIndexMap.find(label) != nameToLabelingIndexMap.end();
             }
@@ -210,6 +222,18 @@ namespace storm {
                 return out;
             }
 
+            std::string ItemLabeling::generateUniqueLabel(const std::string& prefix) const {
+                if (!containsLabel(prefix)) {
+                    return prefix;
+                }
+                unsigned int i = 0;
+                std::string label;
+                do {
+                    label = prefix + "_" + std::to_string(i);
+                } while (containsLabel(label));
+                return label;
+            }
+
         }
     }
 }
diff --git a/src/storm/models/sparse/ItemLabeling.h b/src/storm/models/sparse/ItemLabeling.h
index 43a5b9f21..9c386de85 100644
--- a/src/storm/models/sparse/ItemLabeling.h
+++ b/src/storm/models/sparse/ItemLabeling.h
@@ -3,6 +3,7 @@
 
 #include <unordered_map>
 #include <set>
+#include <string>
 #include <ostream>
 
 
@@ -90,6 +91,28 @@ namespace storm {
                  */
                 void addLabel(std::string const& label, storage::BitVector&& labeling);
 
+                /*!
+                 * Creates a new label with a unique name, derived from the prefix,
+                 * and attaches it to the given items. Note that the dimension of given labeling must
+                 * match the number of items for which this item labeling is valid.
+                 *
+                 * @param prefix A prefix to use for the new label.
+                 * @param labeling A bit vector that indicates whether or not the new label is attached to a item.
+                 * @return the new label
+                 */
+                std::string addUniqueLabel(std::string const& prefix, storage::BitVector const& labeling);
+
+                /*!
+                 * Creates a new label with a unique name, derived from the prefix,
+                 * and attaches it to the given items. Note that the dimension of given labeling must
+                 * match the number of items for which this item labeling is valid.
+                 *
+                 * @param prefix A prefix to use for the new label.
+                 * @param labeling A bit vector that indicates whether or not the new label is attached to a item.
+                 * @return the new label
+                 */
+                std::string addUniqueLabel(std::string const& prefix, storage::BitVector const&& labeling);
+
                 /*!
                  * Adds all labels from the other labeling to this labeling.
                  * It is assumed that both labelings have the same itemcount.
@@ -217,6 +240,12 @@ namespace storm {
 
                 // A vector that holds the labeling for all known labels.
                 std::vector<storm::storage::BitVector> labelings;
+
+                /*!
+                 * Generate a unique, previously unused label from the given prefix string.
+                 */
+                std::string generateUniqueLabel(const std::string& prefix) const;
+
             };
 
         } // namespace sparse