Include file:

#include "mcrl2/lps/state_probability_pair.h
class mcrl2::lps::state_probability_pair

Protected attributes

PROBABILITY mcrl2::lps::state_probability_pair::m_probability
STATE mcrl2::lps::state_probability_pair::m_state

Public member functions

state_probability_pair &operator=(const state_probability_pair &p) = default

Standard assignment.


  • p The state probability pair to be assigned.

Returns: A reference to the assigned object.

state_probability_pair &operator=(state_probability_pair &&p) = default
bool operator==(const state_probability_pair &other) const

Standard equality operator.

Returns: Returns true iff the probabilistic states are equal.

PROBABILITY &probability()

Set the probability in a state probability pair.

const PROBABILITY &probability() const

get the probability from a state proability pair.

STATE &state()

Get the state in a state probability pair.

const STATE &state() const

Get the state from a state probability pair.

state_probability_pair(const STATE &state, const PROBABILITY &probability)



  • state The state.
  • probability The probability of the occurrence of this state.
state_probability_pair(const state_probability_pair &p) = default

Copy constructor;.


  • p The state probability pair to be copied.
state_probability_pair(state_probability_pair &&p) = default