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.

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

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.

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

const_iterator begin() const

Gets an iterator over pairs of state and probability.

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

void clear()

Makes the probabilistic state empty.

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.

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 &s)

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 &s)

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 labels of this LTS.

Returns: The number of action labels of this LTS.

void swap(probabilistic_state &s)

Swap this probabilistic state.

Parameters:

  • s A probabilistic state.