item labelling class

src/storm/models/sparse/ChoiceLabeling.cpp

@@ -0,0 +1,85 @@
+#include "ChoiceLabeling.h"
+
+
+
+#include "storm/exceptions/OutOfRangeException.h"
+#include "storm/exceptions/InvalidArgumentException.h"
+
+
+namespace storm {
+    namespace models {
+        namespace sparse {
+            ChoiceLabeling::ChoiceLabeling(uint_fast64_t choiceCount) : ItemLabeling(choiceCount) {
+                // Intentionally left empty.
+            }
+
+            ChoiceLabeling::ChoiceLabeling(ItemLabeling const& itemLab) : ItemLabeling(itemLab) {
+                // Intentionally left empty.
+            }
+
+            ChoiceLabeling::ChoiceLabeling(ItemLabeling const&& itemLab) : ItemLabeling(itemLab) {
+                // Intentionally left empty.
+            }
+
+
+            bool ChoiceLabeling::operator==(ChoiceLabeling const& other) const {
+                if (itemCount != other.itemCount) {
+                    return false;
+                }
+                if (this->getNumberOfLabels() != other.getNumberOfLabels()) {
+                    return false;
+                }
+                for (auto const& labelIndexPair : this->nameToLabelingIndexMap) {
+                    if (!other.containsLabel(labelIndexPair.first)) {
+                        return false;
+                    }
+                    if (labelings[labelIndexPair.second] != other.getChoices(labelIndexPair.first)) {
+                        return false;
+                    }
+                }
+                return true;
+            }
+
+
+
+            ChoiceLabeling ChoiceLabeling::getSubLabeling(storm::storage::BitVector const& choices) const {
+                return ChoiceLabeling(ItemLabeling::getSubLabeling(choices));
+            }
+
+
+
+            std::set<std::string> ChoiceLabeling::getLabelsOfChoice(uint64_t choice) const {
+                return this->getLabelsOfItem(choice);
+            }
+
+
+            void ChoiceLabeling::addLabelToChoice(std::string const& label,uint64_t choice) {
+                this->addLabelToChoice(label, choice);
+            }
+
+            bool ChoiceLabeling::getChoiceHasLabel(std::string const& label, uint64_t choice) const {
+                return this->getItemHasLabel(label, choice);
+            }
+
+
+            storm::storage::BitVector const& ChoiceLabeling::getChoices(std::string const& label) const {
+                return this->getItems(label);
+            }
+
+            void ChoiceLabeling::setChoices(std::string const& label, storage::BitVector const& labeling) {
+                this->setItems(label, labeling);
+            }
+
+            void ChoiceLabeling::setChoices(std::string const& label, storage::BitVector&& labeling) {
+                this->setItems(label, labeling);
+            }
+
+
+            std::ostream& operator<<(std::ostream& out, ChoiceLabeling const& labeling) {
+                labeling.printLabelingInformationToStream(out);
+                return out;
+            }
+
+        }
+    }
+}

src/storm/models/sparse/ChoiceLabeling.h

@@ -0,0 +1,102 @@
+#pragma once
+
+#include "storm/models/sparse/ItemLabeling.h"
+
+
+namespace storm {
+    namespace models {
+        namespace sparse {
+
+            /*!
+             * This class manages the labeling of the choice space with a number of (atomic) labels.
+             */
+            class ChoiceLabeling : public ItemLabeling {
+            public:
+                /*!
+                 * Constructs an empty labeling for the given number of choices.
+                 *
+                 * @param choiceCount The number of choices for which this labeling can hold the labels.
+                 */
+                ChoiceLabeling(uint_fast64_t choiceCount = 0);
+
+                ChoiceLabeling(ChoiceLabeling const& other) = default;
+                ChoiceLabeling(ItemLabeling const& other);
+                ChoiceLabeling(ItemLabeling const&& other);
+                ChoiceLabeling& operator=(ChoiceLabeling const& other) = default;
+
+
+                /*!
+                 * Checks whether the two labelings are equal.
+                 *
+                 * @param other The labeling with which the current one is compared.
+                 * @return True iff the labelings are equal.
+                 */
+                bool operator==(ChoiceLabeling const& other) const;
+
+                /*!
+                 * Retrieves the sub labeling that represents the same labeling as the current one for all selected choices.
+                 *
+                 * @param choices The selected set of choices.
+                 */
+                ChoiceLabeling getSubLabeling(storm::storage::BitVector const& choices) const;
+
+
+                /*!
+                 * Retrieves the set of labels attached to the given choice.
+                 *
+                 * @param choice The choice for which to retrieve the labels.
+                 * @return The labels attached to the given choice.
+                 */
+                std::set<std::string> getLabelsOfChoice(uint64_t choice) const;
+
+
+
+                /*!
+                 * Adds a label to a given choice.
+                 *
+                 * @param label The name of the label to add.
+                 * @param choice The index of the choice to label.
+                 */
+                void addLabelToChoice(std::string const& label, uint64_t choice);
+
+                /*!
+                 * Checks whether a given choice is labeled with the given label.
+                 *
+                 * @param label The name of the label.
+                 * @param choice The index of the choice to check.
+                 * @return True if the node is labeled with the label, false otherwise.
+                 */
+                bool getChoiceHasLabel(std::string const& label, uint64_t choice) const;
+
+
+                /*!
+                 * Returns the labeling of choices associated with the given label.
+                 *
+                 * @param label The name of the label.
+                 * @return A bit vector that represents the labeling of the choices with the given label.
+                 */
+                storm::storage::BitVector const& getChoices(std::string const& label) const;
+
+                /*!
+                 * Sets the labeling of choices associated with the given label.
+                 *
+                 * @param label The name of the label.
+                 * @param labeling A bit vector that represents the set of choices that will get this label.
+                 */
+                void setChoices(std::string const& label, storage::BitVector const& labeling);