69 uint64_t labelIndex = labelIt->second;
79 it.second = labelIndex;
87 "The item count of the two labelings does not match: " << this->itemCount <<
" vs. " << other.
itemCount <<
".");
88 for (
auto const& label : other.
getLabels()) {
98 std::set<std::string> result;
100 result.insert(labelIndexPair.first);
106 std::set<std::string> result;
109 result.insert(labelIndexPair.first);
116 STORM_LOG_THROW(inversePermutation.size() ==
itemCount, storm::exceptions::InvalidArgumentException,
"Permutation does not match number of items");
117 std::vector<storm::storage::BitVector> newLabelings;
119 newLabelings.push_back(source.permute(inversePermutation));
122 this->labelings = newLabelings;
128 "Labeling vector has invalid size. Expected: " <<
itemCount <<
" Actual: " << labeling.
size());
136 "Labeling vector has invalid size. Expected: " <<
itemCount <<
" Actual: " << labeling.size());
138 labelings.emplace_back(std::move(labeling));
166 "Item " << item <<
" does not have label '" << label <<
"'.");
172 "The label '" << label <<
"' is invalid for the labeling of the model.");
186 "The label " << label <<
" is invalid for the labeling of the model.");
192 "The label " << label <<
" is invalid for the labeling of the model.");
199 "The label " << label <<
" is invalid for the labeling of the model.");
200 STORM_LOG_THROW(labeling.size() ==
itemCount, storm::exceptions::InvalidArgumentException,
"Labeling vector has invalid size.");
207 out <<
" * " << labelIndexPair.first <<
" -> " << this->
labelings[labelIndexPair.second].getNumberOfSetBits() <<
" item(s)\n";
214 out <<
"Label '" << label.first <<
"': ";
215 for (
auto index : this->
labelings[label.second]) {
238 label = prefix +
"_" + std::to_string(i);
This class manages the labeling of the choice space with a number of (atomic) labels.
virtual std::size_t hash() const
virtual std::set< std::string > getLabelsOfItem(uint64_t item) const
Retrieves the set of labels attached to the given item.
virtual void setItems(std::string const &label, storage::BitVector const &labeling)
Sets the labeling of items associated with the given 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.
std::set< std::string > getLabels() const
Retrieves the set of labels contained in this labeling.
ItemLabeling(uint64_t itemCount=0)
Constructs an empty labeling for the given number of items.
virtual bool isChoiceLabeling() const
virtual bool getItemHasLabel(std::string const &label, uint64_t item) const
Checks whether a given item is labeled with the given label.
void addLabel(std::string const &label)
Adds a new label to the labelings.
void permuteItems(std::vector< uint64_t > const &inversePermutation)
ChoiceLabeling const & asChoiceLabeling() const
void join(ItemLabeling const &other)
Adds all labels from the other labeling to this labeling.
bool containsLabel(std::string const &label) const
Checks whether a label is registered within this labeling.
std::size_t getNumberOfItems() const
Returns the number of items managed by this object.
void removeLabel(std::string const &label)
Removes a label from the labelings.
void printCompleteLabelingInformationToStream(std::ostream &out=std::cout) const
Prints the complete labeling to the specified stream.
virtual bool isStateLabeling() const
std::unordered_map< std::string, uint64_t > nameToLabelingIndexMap
StateLabeling const & asStateLabeling() const
virtual storm::storage::BitVector const & getItems(std::string const &label) const
Returns the labeling of items associated with the given label.
virtual void addLabelToItem(std::string const &label, uint64_t item)
Adds a label to a given item.
bool operator==(ItemLabeling const &other) const
Checks whether the two labelings are equal.
void printLabelingInformationToStream(std::ostream &out=std::cout) const
Prints information about the labeling to the specified stream.
std::vector< storm::storage::BitVector > labelings
virtual void removeLabelFromItem(std::string const &label, uint64_t item)
Removes a label from a given item.
std::size_t getNumberOfLabels() const
Returns the number of labels managed by this object.
std::string generateUniqueLabel(const std::string &prefix) const
Generate a unique, previously unused label from the given prefix string.
ItemLabeling getSubItemLabeling(storm::storage::BitVector const &items) const
Retrieves the sub labeling that represents the same labeling as the current one for all selected item...
friend std::ostream & operator<<(std::ostream &out, ItemLabeling const &labeling)
This class manages the labeling of the state space with a number of (atomic) labels.
A bit vector that is internally represented as a vector of 64-bit values.
uint64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
size_t size() const
Retrieves the number of bits this bit vector can store.
#define STORM_LOG_THROW(cond, exception, message)