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 action_label_t

typedef for super::action_label_t

type base_t

typedef for super::base_t

type labels_size_type

typedef for super::labels_size_type

type probabilistic_state_t

typedef for PROBABILISTIC_STATE_T

The type of probabilistic labels.

type state_label_t

typedef for super::state_label_t

type states_size_type

typedef for super::states_size_type

type super
type transitions_size_type

typedef for super::transitions_size_type

Protected attributes¶

PROBABILISTIC_STATE_T m_init_probabilistic_state
std::vector<PROBABILISTIC_STATE_T> 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()

Creates an empty LTS.

probabilistic_lts(const probabilistic_lts &l)

Creates a copy of the supplied LTS.

Parameters:

• l 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 &l)

Swap this lts with the supplied supplied LTS.

Parameters:

• l The LTS to swap.