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 mcrl2::lts::lts::action_label_t

typedef for ACTION_LABEL_T

The type of action labels.

type mcrl2::lts::lts::base_t

typedef for LTS_BASE

The type of the used lts base.

type mcrl2::lts::lts::labels_size_type

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

The sort that represents the indices of labels.

type mcrl2::lts::lts::state_label_t

typedef for STATE_LABEL_T

The type of state labels.

type mcrl2::lts::lts::states_size_type

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

The sort that contains the indices of states.

type mcrl2::lts::lts::transitions_size_type

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

The sort that contains indices of transitions.

public-static-attrib

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

An indicator that this is not a probabilistic lts.

Protected attributes

std::vector<ACTION_LABEL_T> mcrl2::lts::lts::m_action_labels
std::set<labels_size_type> mcrl2::lts::lts::m_hidden_label_set
states_size_type mcrl2::lts::lts::m_init_state
states_size_type mcrl2::lts::lts::m_nstates
std::vector<STATE_LABEL_T> mcrl2::lts::lts::m_state_labels
std::vector<transition> mcrl2::lts::lts::m_transitions

Protected member functions

void rename_labels(const std::map<labels_size_type, labels_size_type> &action_rename_map)
void store_action_label_to_be_renamed(const ACTION_LABEL_T &a, const labels_size_type i, std::map<labels_size_type, labels_size_type> &action_rename_map)

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.

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

Rename actions in the lts by hiding the actions in the vector tau_actions.

Multiactions can be partially renamed. I.e. a|b becomes a if b is hidden. In such a case the new action a is mapped onto an existing action a; if such a label a does not exist, the action label a|b is renamed to a.

Parameters:

  • tau_actions Vector with strings indicating which actions must be transformed to tau’s
labels_size_type apply_hidden_label_map(const labels_size_type action) const

If the action label is registered hidden, it returns tau, otherwise the original 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.

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.

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.

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.
std::set<labels_size_type> &hidden_label_set()

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

Returns: The hidden action set

const std::set<labels_size_type> &hidden_label_set() const

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

Returns: The hidden action set

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.

lts &operator=(const lts &l)

Standard assignment operator.

Parameters:

  • l The lts to be assigned.
bool operator==(const lts &other) const

Standard equality operator.

Parameters:

  • other The lts to compare with.
void record_hidden_actions(const std::vector<std::string> &tau_actions)

Records all actions with a string that occurs in tau_actions internally.

In case actions are partially hidden, e.g. action a is hidden in a|b b is the result. If b is an existing label with index j, and a|b had index i, every i is replaced by j. If there was no action b yet, the action label a|b is replaced by the action label b. Essential for the correctness is that hiding an action repeatedly in a multiaction, has the same effect as hiding it once, which is a property of hiding actions.

Parameters:

  • tau_actions Vector with strings indicating which actions must be transformed to tau’s
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_set(const std::set<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.
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: const_tau_label_index, which is 0, i.e. the index of the label tau.