mcrl2::lps::state_probability_pair

Include file:

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

Protected attributes

PROBABILITY m_probability
STATE m_state

Public member functions

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

Standard assignment.

Parameters:

  • p The state probability pair to be assigned.

Returns: A reference to the assigned object.

bool operator==(const state_probability_pair &other) const

Standard equality operator.

Returns: Returns true iff the probabilistic states are equal.

const PROBABILITY &probability() const

get the probability from a state proability pair.

PROBABILITY &probability()

Set the probability in a state probability pair.

const STATE &state() const

Get the state from a state probability pair.

STATE &state()

Get the state in a state probability pair.

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

constructor.

Parameters:

  • state The state.
  • probability The probability of the occurrence of this state.