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 #include +#include #include @@ -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 labelings; + + /*! + * Generate a unique, previously unused label from the given prefix string. + */ + std::string generateUniqueLabel(const std::string& prefix) const; + }; } // namespace sparse