mcrl2::lts::probabilistic_lts

Include file:

#include "mcrl2/lts/probabilistic_lts.h
class mcrl2::lts::probabilistic_lts

A class that contains a labelled transition system.

The state labels and action labels can be any type. Essentially, a labelled transition system consists of a vector of transitions. Each transition is a triple of three numbers <from, label, to>. For these numbers, there can be associated state labels (for ‘from’ and ‘to’), and action labels (for ‘label’). But it is also possible, that no state or action labels are provided. For all action labels it is maintained whether this action label is an internal ‘tau’ action. This can be indicated for each action label separately. Finally, the number of states is recalled as a separate variable.

Public types

type mcrl2::lts::probabilistic_lts::action_label_t

typedef for super::action_label_t

type mcrl2::lts::probabilistic_lts::base_t

typedef for super::base_t

type mcrl2::lts::probabilistic_lts::labels_size_type

typedef for super::labels_size_type

type mcrl2::lts::probabilistic_lts::probabilistic_state_t

typedef for PROBABILISTIC_STATE_T

The type of probabilistic labels.

type mcrl2::lts::probabilistic_lts::state_label_t

typedef for super::state_label_t

type mcrl2::lts::probabilistic_lts::states_size_type

typedef for super::states_size_type

type mcrl2::lts::probabilistic_lts::super

typedef for lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >

type mcrl2::lts::probabilistic_lts::transitions_size_type

typedef for super::transitions_size_type

public-static-attrib

constexpr bool mcrl2::lts::probabilistic_lts::is_probabilistic_lts

An indicator that this is a probabilistic lts.

Protected attributes

PROBABILISTIC_STATE_T mcrl2::lts::probabilistic_lts::m_init_probabilistic_state
std::vector<PROBABILISTIC_STATE_T> mcrl2::lts::probabilistic_lts::m_probabilistic_states

Protected member functions

states_size_type initial_state() const
void set_initial_state(const states_size_type s)

Public member functions

states_size_type add_and_reset_probabilistic_state(PROBABILISTIC_STATE_T &s)

Adds a probabilistic state to this LTS and resets the state to empty.

This is more efficient than using add_probabilistic state, as this variant does not copy the probabilistic state. It is not checked whether this probabilistic state already exists.

Parameters:

  • s The probabilistic state.

Returns: The index of the added probabilistic state.

states_size_type add_probabilistic_state(const PROBABILISTIC_STATE_T &s)

Adds a probabilistic state to this LTS.

It is not checked whether this probabilistic state already exists.

Parameters:

  • s The probabilistic state.

Returns: The index of the added probabilistic.

void clear()

Clear the transitions system.

The state values, action values and transitions are reset. The number of states, actions and transitions are set to 0.

void clear_probabilistic_states()

Clear the probabilistic states in this probabilistic transitions system.

const PROBABILISTIC_STATE_T &initial_probabilistic_state() const

Gets the initial state number of this LTS.

Returns: The number of the initial state of this LTS.

labels_size_type num_probabilistic_states() const

Gets the number of probabilistic states of this LTS.

Returns: The number of action labels of this LTS.

probabilistic_lts &operator=(const probabilistic_lts &other) = default

Standard assignment operator.

Parameters:

  • other The LTS to assign.
probabilistic_lts &operator=(probabilistic_lts &&other) = default

Standard assignment move operator.

Parameters:

  • other The LTS to assign.
bool operator==(const probabilistic_lts &other) const

Standard equality operator.

Parameters:

  • other The LTS to compare this probabilistic lts with.
probabilistic_lts()

Creates an empty LTS.

probabilistic_lts(const probabilistic_lts &other) = default

Standard copy constructor.

Parameters:

  • other The LTS to copy.
probabilistic_lts(probabilistic_lts &&other) = default

Standard move constructor.

Parameters:

  • other The LTS to copy.
const PROBABILISTIC_STATE_T &probabilistic_state(const states_size_type index) const

Gets the probabilistic label of an index.

Parameters:

  • index The index of an action.

Returns: The probabilistic state belonging to the index.

void set_initial_probabilistic_state(const PROBABILISTIC_STATE_T &state)

Sets the probabilistic initial state number of this LTS.

Parameters:

  • state The number of the state that will become the initial state.
void set_probabilistic_state(const states_size_type index, const PROBABILISTIC_STATE_T &s)

Sets the probabilistic label corresponding to some index.

Parameters:

  • index The index of the state.
  • s The new probabilistic state belonging to this index.
void swap(probabilistic_lts &other)

Swap this lts with the supplied supplied LTS.

Parameters:

  • l The LTS to swap.