This class manages the labeling of the state space with a number of (atomic) labels. More...

#include <StateLabeling.h>

Inheritance diagram for storm::models::sparse::StateLabeling:

Collaboration diagram for storm::models::sparse::StateLabeling:

Public Member Functions
	StateLabeling (uint_fast64_t stateCount=0)
	Constructs an empty labeling for the given number of states.

	StateLabeling (StateLabeling const &other)=default

	StateLabeling (ItemLabeling const &other)

	StateLabeling (ItemLabeling const &&other)

StateLabeling &	operator= (StateLabeling const &other)=default

virtual bool	isStateLabeling () const override

bool	operator== (StateLabeling const &other) const
	Checks whether the two labelings are equal.

StateLabeling	getSubLabeling (storm::storage::BitVector const &states) const
	Retrieves the sub labeling that represents the same labeling as the current one for all selected states.

std::set< std::string >	getLabelsOfState (storm::storage::sparse::state_type state) const
	Retrieves the set of labels attached to the given state.

void	addLabelToState (std::string const &label, storm::storage::sparse::state_type state)
	Adds a label to a given state.

void	removeLabelFromState (std::string const &label, storm::storage::sparse::state_type state)
	Removes a label from a given state.

bool	getStateHasLabel (std::string const &label, storm::storage::sparse::state_type state) const
	Checks whether a given state is labeled with the given label.

storm::storage::BitVector const &	getStates (std::string const &label) const
	Returns the labeling of states associated with the given label.

void	setStates (std::string const &label, storage::BitVector const &labeling)
	Sets the labeling of states associated with the given label.

void	setStates (std::string const &label, storage::BitVector &&labeling)
	Sets the labeling of states associated with the given label.

Public Member Functions inherited from storm::models::sparse::ItemLabeling
	ItemLabeling (uint64_t itemCount=0)
	Constructs an empty labeling for the given number of items.

	ItemLabeling (ItemLabeling const &other)=default

ItemLabeling &	operator= (ItemLabeling const &other)=default

virtual	~ItemLabeling ()=default

virtual bool	isChoiceLabeling () const

StateLabeling const &	asStateLabeling () const

StateLabeling &	asStateLabeling ()

ChoiceLabeling const &	asChoiceLabeling () const

ChoiceLabeling &	asChoiceLabeling ()

bool	operator== (ItemLabeling const &other) const
	Checks whether the two labelings are equal.

void	addLabel (std::string const &label)
	Adds a new label to the labelings.

void	removeLabel (std::string const &label)
	Removes a label from the labelings.

std::set< std::string >	getLabels () const
	Retrieves the set of labels contained in this labeling.

void	addLabel (std::string const &label, storage::BitVector const &labeling)
	Creates a new label and attaches it to the given items.

void	addLabel (std::string const &label, storage::BitVector &&labeling)
	Creates a new label and attaches it to the given items.

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::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.

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	getNumberOfLabels () const
	Returns the number of labels managed by this object.

std::size_t	getNumberOfItems () const
	Returns the number of items managed by this object.

void	permuteItems (std::vector< uint64_t > const &inversePermutation)

virtual std::size_t	hash () const

void	printLabelingInformationToStream (std::ostream &out=std::cout) const
	Prints information about the labeling to the specified stream.

void	printCompleteLabelingInformationToStream (std::ostream &out=std::cout) const
	Prints the complete labeling to the specified stream.

Friends
std::ostream &	operator<< (std::ostream &out, StateLabeling const &labeling)

Additional Inherited Members
Protected Member Functions inherited from storm::models::sparse::ItemLabeling
ItemLabeling	getSubLabeling (storm::storage::BitVector const &items) const
	Retrieves the sub labeling that represents the same labeling as the current one for all selected items.

virtual std::set< std::string >	getLabelsOfItem (uint64_t item) const
	Retrieves the set of labels attached to the given item.

virtual bool	getItemHasLabel (std::string const &label, uint64_t item) const
	Checks whether a given item is labeled with the given label.

virtual storm::storage::BitVector const &	getItems (std::string const &label) const
	Returns the labeling of items associated with the given label.

virtual void	setItems (std::string const &label, storage::BitVector const &labeling)
	Sets the labeling of items associated with the given label.

virtual void	setItems (std::string const &label, storage::BitVector &&labeling)
	Sets 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.

virtual void	removeLabelFromItem (std::string const &label, uint64_t item)
	Removes a label from a given item.

std::string	generateUniqueLabel (const std::string &prefix) const
	Generate a unique, previously unused label from the given prefix string.

Protected Attributes inherited from storm::models::sparse::ItemLabeling
uint64_t	itemCount

std::unordered_map< std::string, uint64_t >	nameToLabelingIndexMap

std::vector< storm::storage::BitVector >	labelings

Detailed Description

This class manages the labeling of the state space with a number of (atomic) labels.

Definition at line 19 of file StateLabeling.h.

Constructor & Destructor Documentation

◆ StateLabeling() [1/4]

storm::models::sparse::StateLabeling::StateLabeling ( uint_fast64_t stateCount = 0 )

Constructs an empty labeling for the given number of states.

Parameters

stateCount The number of states for which this labeling can hold the labels.

Definition at line 9 of file StateLabeling.cpp.

◆ StateLabeling() [2/4]

storm::models::sparse::StateLabeling::StateLabeling ( StateLabeling const & other )

default

◆ StateLabeling() [3/4]

storm::models::sparse::StateLabeling::StateLabeling ( ItemLabeling const & other )

Definition at line 13 of file StateLabeling.cpp.

◆ StateLabeling() [4/4]

storm::models::sparse::StateLabeling::StateLabeling ( ItemLabeling const && other )

Definition at line 17 of file StateLabeling.cpp.

Member Function Documentation

◆ addLabelToState()

void storm::models::sparse::StateLabeling::addLabelToState	(	std::string const &	label,
		storm::storage::sparse::state_type	state
	)

Adds a label to a given state.

Parameters

label	The name of the label to add.
state	The index of the state to label.

Definition at line 51 of file StateLabeling.cpp.

◆ getLabelsOfState()

std::set< std::string > storm::models::sparse::StateLabeling::getLabelsOfState ( storm::storage::sparse::state_type state ) const

Retrieves the set of labels attached to the given state.

Parameters

state The state for which to retrieve the labels.

Returns: The labels attached to the given state.

Definition at line 47 of file StateLabeling.cpp.

◆ getStateHasLabel()

bool storm::models::sparse::StateLabeling::getStateHasLabel	(	std::string const &	label,
		storm::storage::sparse::state_type	state
	)		const

Checks whether a given state is labeled with the given label.

Parameters

label	The name of the label.
state	The index of the state to check.

Returns: True if the node is labeled with the label, false otherwise.

Definition at line 59 of file StateLabeling.cpp.

◆ getStates()

storm::storage::BitVector const & storm::models::sparse::StateLabeling::getStates ( std::string const & label ) const

Returns the labeling of states associated with the given label.

Parameters

label The name of the label.

Returns: A bit vector that represents the labeling of the states with the given label.

Definition at line 63 of file StateLabeling.cpp.

◆ getSubLabeling()

StateLabeling storm::models::sparse::StateLabeling::getSubLabeling ( storm::storage::BitVector const & states ) const

Retrieves the sub labeling that represents the same labeling as the current one for all selected states.

Parameters

states The selected set of states.

Definition at line 43 of file StateLabeling.cpp.

◆ isStateLabeling()

bool storm::models::sparse::StateLabeling::isStateLabeling ( ) const

overridevirtual

Reimplemented from storm::models::sparse::ItemLabeling.

Definition at line 21 of file StateLabeling.cpp.

◆ operator=()

StateLabeling & storm::models::sparse::StateLabeling::operator= ( StateLabeling const & other )

default

◆ operator==()

bool storm::models::sparse::StateLabeling::operator== ( StateLabeling const & other ) const

Checks whether the two labelings are equal.

Parameters

other The labeling with which the current one is compared.

Returns: True iff the labelings are equal.

Definition at line 25 of file StateLabeling.cpp.

◆ removeLabelFromState()

void storm::models::sparse::StateLabeling::removeLabelFromState	(	std::string const &	label,
		storm::storage::sparse::state_type	state
	)

Removes a label from a given state.

Parameters

label	The name of the label to remove.
state	The index of the state.

Definition at line 55 of file StateLabeling.cpp.

◆ setStates() [1/2]

void storm::models::sparse::StateLabeling::setStates	(	std::string const &	label,
		storage::BitVector &&	labeling
	)

Sets the labeling of states associated with the given label.

Parameters

label	The name of the label.
labeling	A bit vector that represents the set of states that will get this label.

Definition at line 71 of file StateLabeling.cpp.

◆ setStates() [2/2]

void storm::models::sparse::StateLabeling::setStates	(	std::string const &	label,
		storage::BitVector const &	labeling
	)

Sets the labeling of states associated with the given label.

Parameters

label	The name of the label.
labeling	A bit vector that represents the set of states that will get this label.

Definition at line 67 of file StateLabeling.cpp.

Friends And Related Symbol Documentation

◆ operator<<

std::ostream & operator<<	(	std::ostream &	out,
		StateLabeling const &	labeling
	)

friend

Definition at line 75 of file StateLabeling.cpp.

The documentation for this class was generated from the following files:

src/storm/models/sparse/StateLabeling.h
src/storm/models/sparse/StateLabeling.cpp

Public Member Functions

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ StateLabeling() [1/4]

◆ StateLabeling() [2/4]

◆ StateLabeling() [3/4]

◆ StateLabeling() [4/4]

Member Function Documentation

◆ addLabelToState()

◆ getLabelsOfState()

◆ getStateHasLabel()

◆ getStates()

◆ getSubLabeling()

◆ isStateLabeling()

◆ operator=()

◆ operator==()

◆ removeLabelFromState()

◆ setStates() [1/2]

◆ setStates() [2/2]

Friends And Related Symbol Documentation

◆ operator<<