mcrl2::lts::probabilistic_state

Include file:

#include "mcrl2/lts/probabilistic_state.h

class mcrl2::lts::probabilistic_state

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.

Public types

type mcrl2::lts::probabilistic_state::const_iterator

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

type mcrl2::lts::probabilistic_state::iterator

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

type mcrl2::lts::probabilistic_state::probability_t

typedef for PROBABILITY

type mcrl2::lts::probabilistic_state::state_probability_pair

typedef for lps::state_probability_pair< STATE, PROBABILITY >

type mcrl2::lts::probabilistic_state::state_t

typedef for STATE

Protected attributes

std::vector<state_probability_pair> mcrl2::lts::probabilistic_state::m_probabilistic_state

STATE mcrl2::lts::probabilistic_state::m_single_state

Public member functions

void add(const STATE &s, const PROBABILITY &p)

Add a state with a probability to the probabilistic state.

Parameters:

• s The state to be added.
• p The probability of this state.

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.

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

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.

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

void clear()

Makes the probabilistic state empty.

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.

iterator end()

Gets the end iterator over pairs of state and probability.

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

const_iterator end() const

Gets the end iterator over pairs of state and probability.

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

STATE get() const

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:

• s The state.

bool operator!=(const probabilistic_state &other) const

Standard equality operator.

Returns: Returns true iff the probabilistic states are equal.

probabilistic_state &operator=(const probabilistic_state &other)

Copy assignment constructor.

bool operator==(const probabilistic_state &other) const

Standard equality operator.

Returns: Returns true iff the probabilistic states are equal.

probabilistic_state()

Default constructor.

probabilistic_state(const probabilistic_state &other)

Copy constructor.

probabilistic_state(const STATE &s)

Constructor of a probabilistic state from a non probabilistic state.

Parameters:

• s A state.

Returns: The generated probabilistic state.

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.

Parameters:

• begin Iterator to the first state_probability_pair.
• end Iterator to the last state_probability_pair.

Returns: Resulting probabilistic state.

void set(const STATE &s)

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:

• s The 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.

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

void swap(probabilistic_state &other)

Swap this probabilistic state.

Parameters:

• s A probabilistic state.