From a2ed0fc4bf42fa615af5b481c98e08ba40ef09e1 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 28 Apr 2017 11:54:06 +0200 Subject: [PATCH] item labelling class --- src/storm/models/sparse/ChoiceLabeling.cpp | 85 ++++++++++ src/storm/models/sparse/ChoiceLabeling.h | 102 ++++++++++++ src/storm/models/sparse/ItemLabeling.cpp | 137 +++++++++++++++ src/storm/models/sparse/ItemLabeling.h | 185 +++++++++++++++++++++ src/storm/models/sparse/StateLabeling.cpp | 100 +++-------- src/storm/models/sparse/StateLabeling.h | 87 +--------- 6 files changed, 541 insertions(+), 155 deletions(-) create mode 100644 src/storm/models/sparse/ChoiceLabeling.cpp create mode 100644 src/storm/models/sparse/ChoiceLabeling.h create mode 100644 src/storm/models/sparse/ItemLabeling.cpp create mode 100644 src/storm/models/sparse/ItemLabeling.h diff --git a/src/storm/models/sparse/ChoiceLabeling.cpp b/src/storm/models/sparse/ChoiceLabeling.cpp new file mode 100644 index 000000000..96c6aeec0 --- /dev/null +++ b/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 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; + } + + } + } +} diff --git a/src/storm/models/sparse/ChoiceLabeling.h b/src/storm/models/sparse/ChoiceLabeling.h new file mode 100644 index 000000000..880133ee1 --- /dev/null +++ b/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 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); + + /*! + * 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&& labeling); + + friend std::ostream& operator<<(std::ostream& out, ChoiceLabeling const& labeling); + + }; + + } // namespace sparse + } // namespace models +} // namespace storm \ No newline at end of file diff --git a/src/storm/models/sparse/ItemLabeling.cpp b/src/storm/models/sparse/ItemLabeling.cpp new file mode 100644 index 000000000..455791d66 --- /dev/null +++ b/src/storm/models/sparse/ItemLabeling.cpp @@ -0,0 +1,137 @@ +#include "storm/models/sparse/ItemLabeling.h" + +#include "storm/exceptions/OutOfRangeException.h" +#include "storm/exceptions/InvalidArgumentException.h" + + +namespace storm { + namespace models { + namespace sparse { + ItemLabeling::ItemLabeling(uint_fast64_t itemCount) : itemCount(itemCount), nameToLabelingIndexMap(), labelings() { + // Intentionally left empty. + } + + bool ItemLabeling::operator==(ItemLabeling 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.getItems(labelIndexPair.first)) { + return false; + } + } + return true; + } + + ItemLabeling ItemLabeling::getSubLabeling(storm::storage::BitVector const& items) const { + ItemLabeling result(items.getNumberOfSetBits()); + for (auto const& labelIndexPair : nameToLabelingIndexMap) { + result.addLabel(labelIndexPair.first, labelings[labelIndexPair.second] % items); + } + return result; + } + + void ItemLabeling::addLabel(std::string const& label) { + addLabel(label, storage::BitVector(itemCount)); + } + + std::set ItemLabeling::getLabels() const { + std::set result; + for (auto const& labelIndexPair : this->nameToLabelingIndexMap) { + result.insert(labelIndexPair.first); + } + return result; + } + + std::set ItemLabeling::getLabelsOfItem(uint64_t item) const { + std::set result; + for (auto const& labelIndexPair : this->nameToLabelingIndexMap) { + if (this->getItemHasLabel(labelIndexPair.first, item)) { + result.insert(labelIndexPair.first); + } + } + return result; + } + + void ItemLabeling::addLabel(std::string const& label, storage::BitVector const& labeling) { + STORM_LOG_THROW(!this->containsLabel(label), storm::exceptions::InvalidArgumentException, "Label '" << label << "' already exists."); + STORM_LOG_THROW(labeling.size() == itemCount, storm::exceptions::InvalidArgumentException, "Labeling vector has invalid size. Expected: " << itemCount << " Actual: " << labeling.size()); + nameToLabelingIndexMap.emplace(label, labelings.size()); + labelings.push_back(labeling); + } + + void ItemLabeling::addLabel(std::string const& label, storage::BitVector&& labeling) { + STORM_LOG_THROW(!this->containsLabel(label), storm::exceptions::InvalidArgumentException, "Label '" << label << "' already exists."); + STORM_LOG_THROW(labeling.size() == itemCount, storm::exceptions::InvalidArgumentException, "Labeling vector has invalid size. Expected: " << itemCount << " Actual: " << labeling.size()); + nameToLabelingIndexMap.emplace(label, labelings.size()); + labelings.emplace_back(std::move(labeling)); + } + + bool ItemLabeling::containsLabel(std::string const& label) const { + return nameToLabelingIndexMap.find(label) != nameToLabelingIndexMap.end(); + } + + void ItemLabeling::addLabelToItem(std::string const& label, uint64_t item) { + STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::OutOfRangeException, "Label '" << label << "' unknown."); + STORM_LOG_THROW(item < itemCount, storm::exceptions::OutOfRangeException, "Item index out of range."); + this->labelings[nameToLabelingIndexMap.at(label)].set(item, true); + } + + bool ItemLabeling::getItemHasLabel(std::string const& label, uint64_t item) const { + STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::InvalidArgumentException, "The label '" << label << "' is invalid for the labeling of the model."); + return this->labelings[nameToLabelingIndexMap.at(label)].get(item); + } + + std::size_t ItemLabeling::getNumberOfLabels() const { + return labelings.size(); + } + + storm::storage::BitVector const& ItemLabeling::getItems(std::string const& label) const { + STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::InvalidArgumentException, "The label " << label << " is invalid for the labeling of the model."); + return this->labelings[nameToLabelingIndexMap.at(label)]; + } + + void ItemLabeling::setItems(std::string const& label, storage::BitVector const& labeling) { + STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::InvalidArgumentException, "The label " << label << " is invalid for the labeling of the model."); + STORM_LOG_THROW(labeling.size() == itemCount, storm::exceptions::InvalidArgumentException, "Labeling vector has invalid size."); + this->labelings[nameToLabelingIndexMap.at(label)] = labeling; + } + + void ItemLabeling::setItems(std::string const& label, storage::BitVector&& labeling) { + STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::InvalidArgumentException, "The label " << label << " is invalid for the labeling of the model."); + STORM_LOG_THROW(labeling.size() == itemCount, storm::exceptions::InvalidArgumentException, "Labeling vector has invalid size."); + this->labelings[nameToLabelingIndexMap.at(label)] = labeling; + } + + void ItemLabeling::printLabelingInformationToStream(std::ostream& out) const { + out << "Labels: \t" << this->getNumberOfLabels() << std::endl; + for (auto const& labelIndexPair : this->nameToLabelingIndexMap) { + out << " * " << labelIndexPair.first << " -> " << this->labelings[labelIndexPair.second].getNumberOfSetBits() << " item(s)" << std::endl; + } + } + + void ItemLabeling::printCompleteLabelingInformationToStream(std::ostream& out) const { + out << "Labels: \t" << this->getNumberOfLabels() << std::endl; + for (auto label : nameToLabelingIndexMap) { + out << "Label '" << label.first << "': "; + for (auto index : this->labelings[label.second]) { + out << index << " "; + } + out << std::endl; + } + } + + std::ostream& operator<<(std::ostream& out, ItemLabeling const& labeling) { + labeling.printLabelingInformationToStream(out); + return out; + } + + } + } +} diff --git a/src/storm/models/sparse/ItemLabeling.h b/src/storm/models/sparse/ItemLabeling.h new file mode 100644 index 000000000..57b52ff76 --- /dev/null +++ b/src/storm/models/sparse/ItemLabeling.h @@ -0,0 +1,185 @@ +#pragma once + + +#include +#include +#include + + + +#include "storm/storage/BitVector.h" +#include "storm/utility/macros.h" +#include "storm/utility/OsDetection.h" + +namespace storm { + namespace models { + namespace sparse { + + /*! + * A base class managing the labeling of items with a number of (atomic) labels. + */ + class ItemLabeling { + public: + /*! + * Constructs an empty labeling for the given number of items. + * + * @param itemCount The number of items for which this labeling can hold the labels. + */ + explicit ItemLabeling(uint64_t itemCount = 0); + + ItemLabeling(ItemLabeling const& other) = default; + ItemLabeling& operator=(ItemLabeling 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==(ItemLabeling const& other) const; + + + /*! + * Adds a new label to the labelings. Initially, no item is labeled with this label. + * + * @param label The name of the new label. + */ + void addLabel(std::string const& label); + + /*! + * Retrieves the set of labels contained in this labeling. + * + * @return The set of known labels. + */ + std::set getLabels() const; + + + + /*! + * Creates a new label 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 label The new label. + * @param labeling A bit vector that indicates whether or not the new label is attached to a item. + */ + void addLabel(std::string const& label, storage::BitVector const& labeling); + + /*! + * Creates a new label 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 label The new label. + * @param labeling A bit vector that indicates whether or not the new label is attached to a item. + */ + void addLabel(std::string const& label, storage::BitVector&& labeling); + + /*! + * Checks whether a label is registered within this labeling. + * + * @return True if the label is known, false otherwise. + */ + bool containsLabel(std::string const& label) const; + + + /*! + * Returns the number of labels managed by this object. + * + * @return The number of labels. + */ + std::size_t getNumberOfLabels() const; + + + + /*! + * Prints information about the labeling to the specified stream. + * + * @param out The stream the information is to be printed to. + */ + void printLabelingInformationToStream(std::ostream& out = std::cout) const; + + /*! + * Prints the complete labeling to the specified stream. + * + * @param out The stream the information is to be printed to. + */ + void printCompleteLabelingInformationToStream(std::ostream& out = std::cout) const; + + friend std::ostream& operator<<(std::ostream& out, ItemLabeling const& labeling); + + protected: + + /*! + * Retrieves the sub labeling that represents the same labeling as the current one for all selected items. + * + * @param items The selected set of items. + */ + ItemLabeling getSubLabeling(storm::storage::BitVector const& items) const; + + + /*! + * Retrieves the set of labels attached to the given item. + * + * @param item The item for which to retrieve the labels. + * @return The labels attached to the given item. + */ + virtual std::set getLabelsOfItem(uint64_t item) const; + + /*! + * Checks whether a given item is labeled with the given label. + * + * @param label The name of the label. + * @param item The index of the item to check. + * @return True if the node is labeled with the label, false otherwise. + */ + virtual bool getItemHasLabel(std::string const& label, uint64_t item) const; + + + /*! + * Returns the labeling of items associated with the given label. + * + * @param label The name of the label. + * @return A bit vector that represents the labeling of the items with the given label. + */ + virtual storm::storage::BitVector const& getItems(std::string const& label) const; + + /*! + * Sets the labeling of items associated with the given label. + * + * @param label The name of the label. + * @param labeling A bit vector that represents the set of items that will get this label. + */ + virtual void setItems(std::string const& label, storage::BitVector const& labeling); + + /*! + * Sets the labeling of items associated with the given label. + * + * @param label The name of the label. + * @param labeling A bit vector that represents the set of items that will get this label. + */ + virtual void setItems(std::string const& label, storage::BitVector&& labeling); + + /*! + * Adds a label to a given item. + * + * @param label The name of the label to add. + * @param item The index of the item to label. + */ + virtual void addLabelToItem(std::string const& label, uint64_t item); + + + + // The number of items for which this object can hold the labeling. + uint64_t itemCount; + + // A mapping from labels to the index of the corresponding bit vector in the vector. + std::unordered_map nameToLabelingIndexMap; + + // A vector that holds the labeling for all known labels. + std::vector labelings; + }; + + } // namespace sparse + } // namespace models +} // namespace storm + diff --git a/src/storm/models/sparse/StateLabeling.cpp b/src/storm/models/sparse/StateLabeling.cpp index c88a5f07e..43ade7bac 100644 --- a/src/storm/models/sparse/StateLabeling.cpp +++ b/src/storm/models/sparse/StateLabeling.cpp @@ -7,12 +7,21 @@ namespace storm { namespace models { namespace sparse { - StateLabeling::StateLabeling(uint_fast64_t stateCount) : stateCount(stateCount), nameToLabelingIndexMap(), labelings() { + StateLabeling::StateLabeling(uint_fast64_t stateCount) : ItemLabeling(stateCount) { // Intentionally left empty. } + + StateLabeling::StateLabeling(ItemLabeling const& itemLab) : ItemLabeling(itemLab) { + // Intentionally left empty. + } + + StateLabeling::StateLabeling(ItemLabeling const&& itemLab) : ItemLabeling(itemLab) { + // Intentionally left empty. + } + bool StateLabeling::operator==(StateLabeling const& other) const { - if (stateCount != other.stateCount) { + if (itemCount != other.itemCount) { return false; } if (this->getNumberOfLabels() != other.getNumberOfLabels()) { @@ -28,104 +37,41 @@ namespace storm { } return true; } + + StateLabeling StateLabeling::getSubLabeling(storm::storage::BitVector const& states) const { - StateLabeling result(states.getNumberOfSetBits()); - for (auto const& labelIndexPair : nameToLabelingIndexMap) { - result.addLabel(labelIndexPair.first, labelings[labelIndexPair.second] % states); - } - return result; - } - - void StateLabeling::addLabel(std::string const& label) { - addLabel(label, storage::BitVector(stateCount)); + return StateLabeling(ItemLabeling::getSubLabeling(states)); } - std::set StateLabeling::getLabels() const { - std::set result; - for (auto const& labelIndexPair : this->nameToLabelingIndexMap) { - result.insert(labelIndexPair.first); - } - return result; - } + std::set StateLabeling::getLabelsOfState(storm::storage::sparse::state_type state) const { - std::set result; - for (auto const& labelIndexPair : this->nameToLabelingIndexMap) { - if (this->getStateHasLabel(labelIndexPair.first, state)) { - result.insert(labelIndexPair.first); - } - } - return result; - } - - void StateLabeling::addLabel(std::string const& label, storage::BitVector const& labeling) { - STORM_LOG_THROW(!this->containsLabel(label), storm::exceptions::InvalidArgumentException, "Label '" << label << "' already exists."); - STORM_LOG_THROW(labeling.size() == stateCount, storm::exceptions::InvalidArgumentException, "Labeling vector has invalid size. Expected: " << stateCount << " Actual: " << labeling.size()); - nameToLabelingIndexMap.emplace(label, labelings.size()); - labelings.push_back(labeling); - } - - void StateLabeling::addLabel(std::string const& label, storage::BitVector&& labeling) { - STORM_LOG_THROW(!this->containsLabel(label), storm::exceptions::InvalidArgumentException, "Label '" << label << "' already exists."); - STORM_LOG_THROW(labeling.size() == stateCount, storm::exceptions::InvalidArgumentException, "Labeling vector has invalid size. Expected: " << stateCount << " Actual: " << labeling.size()); - nameToLabelingIndexMap.emplace(label, labelings.size()); - labelings.emplace_back(std::move(labeling)); - } - - bool StateLabeling::containsLabel(std::string const& label) const { - return nameToLabelingIndexMap.find(label) != nameToLabelingIndexMap.end(); + return ItemLabeling::getLabelsOfItem(state); } + void StateLabeling::addLabelToState(std::string const& label, storm::storage::sparse::state_type state) { - STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::OutOfRangeException, "Label '" << label << "' unknown."); - STORM_LOG_THROW(state < stateCount, storm::exceptions::OutOfRangeException, "State index out of range."); - this->labelings[nameToLabelingIndexMap.at(label)].set(state, true); + return ItemLabeling::addLabelToItem(label, state); } bool StateLabeling::getStateHasLabel(std::string const& label, storm::storage::sparse::state_type state) const { - STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::InvalidArgumentException, "The label '" << label << "' is invalid for the labeling of the model."); - return this->labelings[nameToLabelingIndexMap.at(label)].get(state); - } - - std::size_t StateLabeling::getNumberOfLabels() const { - return labelings.size(); + return ItemLabeling::getItemHasLabel(label, state); } + storm::storage::BitVector const& StateLabeling::getStates(std::string const& label) const { - STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::InvalidArgumentException, "The label " << label << " is invalid for the labeling of the model."); - return this->labelings[nameToLabelingIndexMap.at(label)]; + return ItemLabeling::getItems(label); } void StateLabeling::setStates(std::string const& label, storage::BitVector const& labeling) { - STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::InvalidArgumentException, "The label " << label << " is invalid for the labeling of the model."); - STORM_LOG_THROW(labeling.size() == stateCount, storm::exceptions::InvalidArgumentException, "Labeling vector has invalid size."); - this->labelings[nameToLabelingIndexMap.at(label)] = labeling; + ItemLabeling::setItems(label, labeling); } void StateLabeling::setStates(std::string const& label, storage::BitVector&& labeling) { - STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::InvalidArgumentException, "The label " << label << " is invalid for the labeling of the model."); - STORM_LOG_THROW(labeling.size() == stateCount, storm::exceptions::InvalidArgumentException, "Labeling vector has invalid size."); - this->labelings[nameToLabelingIndexMap.at(label)] = labeling; - } - - void StateLabeling::printLabelingInformationToStream(std::ostream& out) const { - out << "Labels: \t" << this->getNumberOfLabels() << std::endl; - for (auto const& labelIndexPair : this->nameToLabelingIndexMap) { - out << " * " << labelIndexPair.first << " -> " << this->labelings[labelIndexPair.second].getNumberOfSetBits() << " state(s)" << std::endl; - } + ItemLabeling::setItems(label, labeling); } - void StateLabeling::printCompleteLabelingInformationToStream(std::ostream& out) const { - out << "Labels: \t" << this->getNumberOfLabels() << std::endl; - for (auto label : nameToLabelingIndexMap) { - out << "Label '" << label.first << "': "; - for (auto index : this->labelings[label.second]) { - out << index << " "; - } - out << std::endl; - } - } std::ostream& operator<<(std::ostream& out, StateLabeling const& labeling) { labeling.printLabelingInformationToStream(out); diff --git a/src/storm/models/sparse/StateLabeling.h b/src/storm/models/sparse/StateLabeling.h index f66ea86b4..4639b108e 100644 --- a/src/storm/models/sparse/StateLabeling.h +++ b/src/storm/models/sparse/StateLabeling.h @@ -1,15 +1,14 @@ -#ifndef STORM_MODELS_SPARSE_STATELABELING_H_ -#define STORM_MODELS_SPARSE_STATELABELING_H_ +#pragma once #include #include #include +#include "storm/models/sparse/ItemLabeling.h" #include "storm/storage/sparse/StateType.h" #include "storm/storage/BitVector.h" #include "storm/utility/macros.h" -#include "storm/utility/OsDetection.h" namespace storm { @@ -19,7 +18,7 @@ namespace storm { /*! * This class manages the labeling of the state space with a number of (atomic) labels. */ - class StateLabeling { + class StateLabeling : public ItemLabeling { public: /*! * Constructs an empty labeling for the given number of states. @@ -29,13 +28,11 @@ namespace storm { StateLabeling(uint_fast64_t stateCount = 0); StateLabeling(StateLabeling const& other) = default; + StateLabeling(ItemLabeling const& other); + StateLabeling(ItemLabeling const&& other); StateLabeling& operator=(StateLabeling const& other) = default; -#ifndef WINDOWS - StateLabeling(StateLabeling&& StateLabeling) = default; - StateLabeling& operator=(StateLabeling&& other) = default; -#endif - + /*! * Checks whether the two labelings are equal. * @@ -51,20 +48,7 @@ namespace storm { */ StateLabeling getSubLabeling(storm::storage::BitVector const& states) const; - /*! - * Adds a new label to the labelings. Initially, no state is labeled with this label. - * - * @param label The name of the new label. - */ - void addLabel(std::string const& label); - - /*! - * Retrieves the set of labels contained in this labeling. - * - * @return The set of known labels. - */ - std::set getLabels() const; - + /*! * Retrieves the set of labels attached to the given state. * @@ -73,30 +57,7 @@ namespace storm { */ std::set getLabelsOfState(storm::storage::sparse::state_type state) const; - /*! - * Creates a new label and attaches it to the given states. Note that the dimension of given labeling must - * match the number of states for which this state labeling is valid. - * - * @param label The new label. - * @param labeling A bit vector that indicates whether or not the new label is attached to a state. - */ - void addLabel(std::string const& label, storage::BitVector const& labeling); - - /*! - * Creates a new label and attaches it to the given states. Note that the dimension of given labeling must - * match the number of states for which this state labeling is valid. - * - * @param label The new label. - * @param labeling A bit vector that indicates whether or not the new label is attached to a state. - */ - void addLabel(std::string const& label, storage::BitVector&& labeling); - - /*! - * Checks whether a label is registered within this labeling. - * - * @return True if the label is known, false otherwise. - */ - bool containsLabel(std::string const& label) const; + /*! * Adds a label to a given state. @@ -114,13 +75,7 @@ namespace storm { * @return True if the node is labeled with the label, false otherwise. */ bool getStateHasLabel(std::string const& label, storm::storage::sparse::state_type state) const; - - /*! - * Returns the number of labels managed by this object. - * - * @return The number of labels. - */ - std::size_t getNumberOfLabels() const; + /*! * Returns the labeling of states associated with the given label. @@ -145,36 +100,12 @@ namespace storm { * @param labeling A bit vector that represents the set of states that will get this label. */ void setStates(std::string const& label, storage::BitVector&& labeling); - - /*! - * Prints information about the labeling to the specified stream. - * - * @param out The stream the information is to be printed to. - */ - void printLabelingInformationToStream(std::ostream& out) const; - - /*! - * Prints the complete labeling to the specified stream. - * - * @param out The stream the information is to be printed to. - */ - void printCompleteLabelingInformationToStream(std::ostream& out) const; friend std::ostream& operator<<(std::ostream& out, StateLabeling const& labeling); - private: - // The number of states for which this object can hold the labeling. - uint_fast64_t stateCount; - - // A mapping from labels to the index of the corresponding bit vector in the vector. - std::unordered_map nameToLabelingIndexMap; - - // A vector that holds the labeling for all known labels. - std::vector labelings; }; } // namespace sparse } // namespace models } // namespace storm -#endif /* STORM_MODELS_SPARSE_STATELABELING_H_ */