mcrl2::lts::lts

Include file:

#include "mcrl2/lts/lts.h
class mcrl2::lts::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 ACTION_LABEL_T

The type of action labels.

type base_t

typedef for LTS_BASE

The type of the used lts base.

type labels_size_type

typedef for std::vector< ACTION_LABEL_T >::size_type

The sort that represents the indices of labels.

type state_label_t

typedef for STATE_LABEL_T

The type of state labels.

type states_size_type

typedef for std::vector< STATE_LABEL_T >::size_type

The sort that contains the indices of states.

type transitions_size_type

typedef for std::vector< transition >::size_type

The sort that contains indices of transitions.

Protected attributes

std::vector<ACTION_LABEL_T> m_action_labels
std::map<labels_size_type, labels_size_type> m_hidden_label_map
states_size_type m_init_state
states_size_type m_nstates
std::vector<STATE_LABEL_T> m_state_labels
std::vector<transition> m_transitions

Public member functions

ACTION_LABEL_T action_label(const labels_size_type action) const

Gets the label of an action.

Parameters:

  • action The number of the action.

Returns: The label of the action.

const std::vector<ACTION_LABEL_T> &action_labels() const

The action labels in this lts.

Returns: The action labels of this lts.

labels_size_type add_action(const ACTION_LABEL_T &label)

Adds an action with a label to this LTS.

It is not checked whether this action label already exists.

Parameters:

  • label The label of the label.

Returns: The number of the added label.

states_size_type add_state(const STATE_LABEL_T &label = STATE_LABEL_T())

Adds a state to this LTS.

It is not checked whether the added state already exists.

Parameters:

  • label The label of the state. If one state has a state label, all states must have state labels. If no state label is given, it must be the case that no state has a label.

Returns: The number of the added state label.

void add_transition(const transition &t)

Add a transition to the lts.

The transition can be added, even if there are not (yet) valid state and action labels for it.

labels_size_type apply_hidden_label_map(const labels_size_type action) const

Gives for an action label its corresponding hidden action label.

Parameters:

  • action The index of an action label.

Returns: The index of the corresponding action label in which actions are hidden.

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_actions()

Clear the action labels of an lts.

This removes the action labels of an lts. It also resets the information regarding to what actions labels are tau. It will not change the number of action labels.

void clear_state_labels()

Clear the labels of an lts.

This removes the action labels of an lts. It does not change the number of state labels

void clear_transitions(const std::size_t n = 0)

Clear the transitions of an lts.

Parameters:

  • n An optional parameter that indicates how many transitions are to be expected. This is used to set the reserved size of a vector, to prevent unnecessary resizing.

This resets the transition vector in an lts, but leaves other related items, such as state or action labels untouched.

const std::vector<transition> &get_transitions() const

Gets a const reference to the vector of transitions of the current lts.

As this vector can be huge, it is adviced to avoid to copy this vector.

Returns: A const reference to the vector.

std::vector<transition> &get_transitions()

Gets a reference to the vector of transitions of the current lts.

As this vector can be huge, it is adviced to avoid to copy this vector.

Returns: A reference to the vector.

bool has_action_info() const

Checks whether this LTS has labels associated with its actions, which are numbers.

Returns: * true if the LTS has values for labels;

  • false otherwise.
bool has_state_info() const

Checks whether this LTS has state values associated with its states.

Returns: * true if the LTS has state information;

  • false otherwise.
const std::map<labels_size_type, labels_size_type> &hidden_label_map() const

Returns the hidden label map that tells for each label what its corresponding hidden label is.

Returns: The hidden action map

std::map<labels_size_type, labels_size_type> &hidden_label_map()

Returns the hidden label map that tells for each label what its corresponding hidden label is.

Returns: The hidden action map

void hide_actions(const std::vector<std::string> &tau_actions)

Sets all actions with a string that occurs in tau_actions to tau.

After hiding actions, it checks whether action labels are equal and merges actions with the same labels in the lts.

Parameters:

  • tau_actions Vector with strings indicating which actions must be transformed to tau’s
states_size_type initial_state() const

Gets the initial state number of this LTS.

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

bool is_probabilistic(const states_size_type state) const

Gets the label of a state.

Parameters:

  • state The number of the state.

Returns: The label of the state.

bool is_tau(labels_size_type action) const

Checks whether an action is a tau action.

Parameters:

  • action The number of the action.

Returns: * true if the action is a tau action;

  • false otherwise.
lts()

Creates an empty LTS.

lts(const lts &l)

Creates a copy of the supplied LTS.

Parameters:

  • l The LTS to copy.
labels_size_type num_action_labels() const

Gets the number of action labels of this LTS.

Returns: The number of action labels of this LTS.

states_size_type num_state_labels() const

Gets the number of state labels of this LTS.

As states do not need to have state labels, the number of state labels can differ from the number of states.

Returns: The number of state labels of this LTS.

states_size_type num_states() const

Gets the number of states of this LTS.

Returns: The number of states of this LTS.

transitions_size_type num_transitions() const

Gets the number of transitions of this LTS.

Returns: The number of transitions of this LTS.

void set_action_label(const labels_size_type action, const ACTION_LABEL_T &label)

Sets the label of an action.

Parameters:

  • action The number of the action.
  • label The label that will be assigned to the action.
void set_hidden_label_map(const std::map<labels_size_type, labels_size_type> &m)

Sets the hidden label map that tells for each label what its corresponding hidden label is.

Parameters:

  • m The new hidden label map.
void set_initial_state(const states_size_type state)

Sets the initial state number of this LTS.

Parameters:

  • state The number of the state that will become the initial state.
void set_num_action_labels(const labels_size_type n)

Sets the number of action labels of this LTS.

If space is reserved for new action labels, these are set to the default action label.

void set_num_states(const states_size_type n, const bool has_state_labels = true)

Sets the number of states of this LTS.

Parameters:

  • n The number of states of this LTS.
  • has_state_labels If true state labels are initialised
void set_state_label(const states_size_type state, const STATE_LABEL_T &label)

Sets the label of a state.

Parameters:

  • state The number of the state.
  • label The label that will be assigned to the state.
void sort_transitions(transition_sort_style ts = src_lbl_tgt)

Sorts the transitions using a sort style.

Parameters:

  • ts The sort style to use.

Note

Deprecated

STATE_LABEL_T state_label(const states_size_type state) const

Gets the label of a state.

Parameters:

  • state The number of the state.

Returns: The label of the state.

std::vector<STATE_LABEL_T> &state_labels()

Provides the state labels of an LTS.

Returns: A reference to the state label vector of the LTS.

const std::vector<STATE_LABEL_T> &state_labels() const

Provides the state labels of an LTS.

Returns: A reference to the state label vector of the LTS.

void swap(lts &l)

Swap this lts with the supplied supplied LTS.

Parameters:

  • l The LTS to swap.
const labels_size_type tau_label_index() const

Provide the index of the label that represents tau.

Returns: 0, i.e. the index of the label tau.