A class that contains a probabilistic state. More...

#include <probabilistic_state.h>

Public Types
typedef lps::state_probability_pair< STATE, PROBABILITY >	state_probability_pair

typedef STATE	state_t

typedef PROBABILITY	probability_t

typedef std::vector< state_probability_pair >::iterator	iterator

typedef std::vector< state_probability_pair >::const_iterator	const_iterator

typedef std::vector< state_probability_pair >::reverse_iterator	reverse_iterator

typedef std::vector< state_probability_pair >::const_reverse_iterator	const_reverse_iterator

Public Member Functions
	probabilistic_state ()
	Default constructor.

	probabilistic_state (const STATE &s)
	Constructor of a probabilistic state from a non probabilistic state.

	probabilistic_state (const probabilistic_state &other)
	Copy constructor.

probabilistic_state &	operator= (const probabilistic_state &other)
	Copy assignment constructor.

template<class STATE_PROBABILITY_PAIR_ITERATOR >
	probabilistic_state (const STATE_PROBABILITY_PAIR_ITERATOR begin, const STATE_PROBABILITY_PAIR_ITERATOR end)
	Creates a probabilistic state on the basis of state_probability_pairs.

bool	operator== (const probabilistic_state &other) const
	Standard equality operator.

bool	operator!= (const probabilistic_state &other) const
	Standard equality operator.

void	swap (probabilistic_state &other)
	Swap this probabilistic state.

void	construct_internal_vector_representation ()
	Guarantee that this probabilistic state is internally stored as a vector, such that begin/end, cbegin/cend and size are properly defined.

void	set (const STATE &s)
	Set this probabilistic state to a single state with probability one.

STATE	get () const
	Get a probabilistic state if is is simple, i.e., consists of a single state.

void	add (const STATE &s, const PROBABILITY &p)
	Add a state with a probability to the probabilistic state.

void	shrink_to_fit ()
	If a probabilistic state is ready, shrinking it to minimal size might be useful to reduce its memory usage. A requirement is that the sum of the probabilities must be one.

std::size_t	size () const
	Gets the number of probabilistic states in the vector representation of this state. If the state is stored as a simple number this size returns 0. So, 0 means that there is one state, which should then be obtained using get(). If the size is larger than 0 the state is stored in a vector, and it must be accessed throught the iterators begin() and n.

void	clear ()
	Makes the probabilistic state empty.

const_iterator	begin () const
	Gets an iterator over pairs of state and probability. This can only be used when the state is stored internally as a vector.

const_iterator	end () const
	Gets the end iterator over pairs of state and probability.

iterator	begin ()
	Gets an iterator over pairs of state and probability. This can only be used if the state is internally stored as a vector.

iterator	end ()
	Gets the end iterator over pairs of state and probability.

const_reverse_iterator	rbegin () const
	Gets a reverse iterator over pairs of state and probability. This can only be used when the state is stored internally as a vector.

const_reverse_iterator	rend () const
	Gets the reverse end iterator over pairs of state and probability.

reverse_iterator	rbegin ()
	Gets a reverse iterator over pairs of state and probability. This can only be used if the state is internally stored as a vector.

reverse_iterator	rend ()
	Gets the reverse end iterator over pairs of state and probability.

Protected Attributes
STATE	m_single_state

std::vector< state_probability_pair >	m_probabilistic_state

Detailed Description

template<class STATE, class PROBABILITY>
class mcrl2::lts::probabilistic_state< STATE, PROBABILITY >

A class that contains a probabilistic state.

A probabilistic state is essentially a sequence of pairs of a state and a probability. The probability indicates the likelyhood with which that particular state can be reached. The sum of all probabilities in a probabilistic state is one. Internally, it is either stored as single state, or as a vector of states. When using a probabilistic state, a user should be aware which of the two internal representations are used. After calling "construct_internal_vector_representation" it is guaranteed that the state is stored as a vector, and iterators over begin/end, and cbegin/cend can be used.

Definition at line 48 of file probabilistic_state.h.

Member Typedef Documentation

◆ const_iterator

template<class STATE , class PROBABILITY >

typedef std::vector<state_probability_pair>::const_iterator mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::const_iterator

Definition at line 58 of file probabilistic_state.h.

◆ const_reverse_iterator

template<class STATE , class PROBABILITY >

typedef std::vector<state_probability_pair>::const_reverse_iterator mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::const_reverse_iterator

Definition at line 60 of file probabilistic_state.h.

◆ iterator

template<class STATE , class PROBABILITY >

typedef std::vector<state_probability_pair>::iterator mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::iterator

Definition at line 57 of file probabilistic_state.h.

◆ probability_t

template<class STATE , class PROBABILITY >

typedef PROBABILITY mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::probability_t

Definition at line 56 of file probabilistic_state.h.

◆ reverse_iterator

template<class STATE , class PROBABILITY >

typedef std::vector<state_probability_pair>::reverse_iterator mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::reverse_iterator

Definition at line 59 of file probabilistic_state.h.

◆ state_probability_pair

template<class STATE , class PROBABILITY >

typedef lps::state_probability_pair< STATE, PROBABILITY > mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::state_probability_pair

Definition at line 54 of file probabilistic_state.h.

◆ state_t

template<class STATE , class PROBABILITY >

typedef STATE mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::state_t

Definition at line 55 of file probabilistic_state.h.

Constructor & Destructor Documentation

◆ probabilistic_state() [1/4]

template<class STATE , class PROBABILITY >

mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::probabilistic_state ( )

inline

Default constructor.

Definition at line 73 of file probabilistic_state.h.

◆ probabilistic_state() [2/4]

template<class STATE , class PROBABILITY >

mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::probabilistic_state ( const STATE & s )

inlineexplicit

Constructor of a probabilistic state from a non probabilistic state.

Parameters

[in] s A state.

Returns: The generated probabilistic state.

Definition at line 82 of file probabilistic_state.h.

◆ probabilistic_state() [3/4]

template<class STATE , class PROBABILITY >

mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::probabilistic_state ( const probabilistic_state< STATE, PROBABILITY > & other )

inline

Copy constructor.

Definition at line 88 of file probabilistic_state.h.

◆ probabilistic_state() [4/4]

template<class STATE , class PROBABILITY >

template<class STATE_PROBABILITY_PAIR_ITERATOR >

mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::probabilistic_state	(	const STATE_PROBABILITY_PAIR_ITERATOR	begin,
		const STATE_PROBABILITY_PAIR_ITERATOR	end
	)

inline

Creates a probabilistic state on the basis of state_probability_pairs.

Parameters

[in]	begin	Iterator to the first state_probability_pair.
[in]	end	Iterator to the last state_probability_pair.

Returns: Resulting probabilistic state.

Definition at line 109 of file probabilistic_state.h.

Member Function Documentation

◆ add()

template<class STATE , class PROBABILITY >

void mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::add	(	const STATE &	s,
		const PROBABILITY &	p
	)

inline

Add a state with a probability to the probabilistic state.

Parameters

[in]	s	The state to be added.
[in]	p	The probability of this state.

Definition at line 214 of file probabilistic_state.h.

◆ begin() [1/2]

template<class STATE , class PROBABILITY >

iterator mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::begin ( )

inline

Gets an iterator over pairs of state and probability. This can only be used if the state is internally stored as a vector.

Returns: The iterator pointing at the first state probability pair.

Definition at line 277 of file probabilistic_state.h.

◆ begin() [2/2]

template<class STATE , class PROBABILITY >

const_iterator mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::begin ( ) const

inline

Gets an iterator over pairs of state and probability. This can only be used when the state is stored internally as a vector.

Returns: The iterator pointing at the first state probability pair.

Definition at line 263 of file probabilistic_state.h.

◆ clear()

template<class STATE , class PROBABILITY >

void mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::clear ( )

inline

Makes the probabilistic state empty.

Definition at line 254 of file probabilistic_state.h.

◆ construct_internal_vector_representation()

template<class STATE , class PROBABILITY >

void mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::construct_internal_vector_representation ( )

inline

Guarantee that this probabilistic state is internally stored as a vector, such that begin/end, cbegin/cend and size are properly defined.

Definition at line 171 of file probabilistic_state.h.

◆ end() [1/2]

template<class STATE , class PROBABILITY >

iterator mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::end ( )

inline

Gets the end iterator over pairs of state and probability.

Returns: The iterator pointing beyond the last state probability pair in a probabilistic state.

Definition at line 284 of file probabilistic_state.h.

◆ end() [2/2]

template<class STATE , class PROBABILITY >

const_iterator mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::end ( ) const

inline

Gets the end iterator over pairs of state and probability.

Returns: The iterator pointing beyond the last state probability pair in a probabilistic state.

Definition at line 270 of file probabilistic_state.h.

◆ get()

template<class STATE , class PROBABILITY >

STATE mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::get ( ) const

inline

Get a probabilistic state if is is simple, i.e., consists of a single state.

It is assumed that the given state probability pair does not have any element.

Parameters

[in] s The state.

Definition at line 195 of file probabilistic_state.h.

◆ operator!=()

template<class STATE , class PROBABILITY >

bool mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::operator!= ( const probabilistic_state< STATE, PROBABILITY > & other ) const

inline

Standard equality operator.

Returns: Returns true iff the probabilistic states are equal.

Definition at line 155 of file probabilistic_state.h.

◆ operator=()

template<class STATE , class PROBABILITY >

probabilistic_state & mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::operator= ( const probabilistic_state< STATE, PROBABILITY > & other )

inline

Copy assignment constructor.

Definition at line 96 of file probabilistic_state.h.

◆ operator==()

template<class STATE , class PROBABILITY >

bool mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::operator== ( const probabilistic_state< STATE, PROBABILITY > & other ) const

inline

Standard equality operator.

Returns: Returns true iff the probabilistic states are equal.

Definition at line 120 of file probabilistic_state.h.

◆ rbegin() [1/2]

template<class STATE , class PROBABILITY >

reverse_iterator mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::rbegin ( )

inline

Gets a reverse iterator over pairs of state and probability. This can only be used if the state is internally stored as a vector.

Returns: The iterator pointing at the last state probability pair.

Definition at line 306 of file probabilistic_state.h.

◆ rbegin() [2/2]

template<class STATE , class PROBABILITY >

const_reverse_iterator mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::rbegin ( ) const

inline

Gets a reverse iterator over pairs of state and probability. This can only be used when the state is stored internally as a vector.

Returns: The iterator pointing at the last state probability pair.

Definition at line 292 of file probabilistic_state.h.

◆ rend() [1/2]

template<class STATE , class PROBABILITY >

reverse_iterator mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::rend ( )

inline

Gets the reverse end iterator over pairs of state and probability.

Returns: The iterator pointing before the first state probability pair in a probabilistic state.

Definition at line 313 of file probabilistic_state.h.

◆ rend() [2/2]

template<class STATE , class PROBABILITY >

const_reverse_iterator mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::rend ( ) const

inline

Gets the reverse end iterator over pairs of state and probability.

Returns: The iterator pointing before the first state probability pair in a probabilistic state.

Definition at line 299 of file probabilistic_state.h.

◆ set()

template<class STATE , class PROBABILITY >

void mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::set ( const STATE & s )

inline

Set this probabilistic state to a single state with probability one.

It is assumed that the given state probability pair does not have any element.

Parameters

[in] s The state.

Definition at line 185 of file probabilistic_state.h.

◆ shrink_to_fit()

template<class STATE , class PROBABILITY >

void mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::shrink_to_fit ( )

inline

If a probabilistic state is ready, shrinking it to minimal size might be useful to reduce its memory usage. A requirement is that the sum of the probabilities must be one.

Definition at line 223 of file probabilistic_state.h.

◆ size()

template<class STATE , class PROBABILITY >

std::size_t mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::size ( ) const

inline

Gets the number of probabilistic states in the vector representation of this state. If the state is stored as a simple number this size returns 0. So, 0 means that there is one state, which should then be obtained using get(). If the size is larger than 0 the state is stored in a vector, and it must be accessed throught the iterators begin() and n.

Returns: The number of probabilistic states, where 0 means there is one simple state.

Definition at line 247 of file probabilistic_state.h.

◆ swap()

template<class STATE , class PROBABILITY >

void mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::swap ( probabilistic_state< STATE, PROBABILITY > & other )

inline

Swap this probabilistic state.

Parameters

[in] s A probabilistic state.

Definition at line 162 of file probabilistic_state.h.

Member Data Documentation

◆ m_probabilistic_state

template<class STATE , class PROBABILITY >

std::vector<state_probability_pair> mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::m_probabilistic_state

protected

Definition at line 66 of file probabilistic_state.h.

◆ m_single_state

template<class STATE , class PROBABILITY >

STATE mcrl2::lts::probabilistic_state< STATE, PROBABILITY >::m_single_state

protected

Definition at line 64 of file probabilistic_state.h.

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

lts/include/mcrl2/lts/probabilistic_state.h

Public Types

Public Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ const_iterator

◆ const_reverse_iterator

◆ iterator

◆ probability_t

◆ reverse_iterator

◆ state_probability_pair

◆ state_t

Constructor & Destructor Documentation

◆ probabilistic_state() [1/4]

◆ probabilistic_state() [2/4]

◆ probabilistic_state() [3/4]

◆ probabilistic_state() [4/4]

Member Function Documentation

◆ add()

◆ begin() [1/2]

◆ begin() [2/2]

◆ clear()

◆ construct_internal_vector_representation()

◆ end() [1/2]

◆ end() [2/2]

◆ get()

◆ operator!=()

◆ operator=()

◆ operator==()

◆ rbegin() [1/2]

◆ rbegin() [2/2]

◆ rend() [1/2]

◆ rend() [2/2]

◆ set()

◆ shrink_to_fit()

◆ size()

◆ swap()

Member Data Documentation

◆ m_probabilistic_state

◆ m_single_state