mcrl2::lps::state_probability_pair

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.

Parameters:

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

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.

state_probability_pair(const state_probability_pair &p) = default

Copy constructor;.

Parameters:

• p The state probability pair to be copied.

state_probability_pair(state_probability_pair &&p) = default