A class that contains a labelled transition system. More...

#include <lts.h>

Inheritance diagram for mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >:

Public Types
typedef STATE_LABEL_T	state_label_t
	The type of state labels.

typedef ACTION_LABEL_T	action_label_t
	The type of action labels.

typedef LTS_BASE	base_t
	The type of the used lts base.

typedef std::vector< STATE_LABEL_T >::size_type	states_size_type
	The sort that contains the indices of states.

typedef std::vector< ACTION_LABEL_T >::size_type	labels_size_type
	The sort that represents the indices of labels.

typedef std::vector< transition >::size_type	transitions_size_type
	The sort that contains indices of transitions.

Public Member Functions
	lts ()
	Creates an empty LTS.

	lts (const lts &l)
	Creates a copy of the supplied LTS.

lts &	operator= (const lts &l)
	Standard assignment operator.

bool	operator== (const lts &other) const
	Standard equality operator.

void	swap (lts &l)
	Swap this lts with the supplied supplied LTS.

states_size_type	num_states () const
	Gets the number of states of this LTS.

std::vector< STATE_LABEL_T > &	state_labels ()
	Provides the state labels of an LTS.

const std::vector< STATE_LABEL_T > &	state_labels () const
	Provides the state labels of an LTS.

states_size_type	num_state_labels () const
	Gets the number of state labels of this LTS.

void	set_num_states (const states_size_type n, const bool has_state_labels=true)
	Sets the number of states of this LTS.

transitions_size_type	num_transitions () const
	Gets the number of transitions of this LTS.

void	set_num_action_labels (const labels_size_type n)
	Sets the number of action labels of this LTS.

labels_size_type	num_action_labels () const
	Gets the number of action labels of this LTS.

states_size_type	initial_state () const
	Gets the initial state number of this LTS.

void	set_initial_state (const states_size_type state)
	Sets the initial state number of this LTS.

states_size_type	add_state (const STATE_LABEL_T &label=STATE_LABEL_T())
	Adds a state to this LTS.

labels_size_type	add_action (const ACTION_LABEL_T &label)
	Adds an action with a label to this LTS.

const labels_size_type	tau_label_index () const
	Provide the index of the label that represents tau.

void	set_state_label (const states_size_type state, const STATE_LABEL_T &label)
	Sets the label of a state.

const std::vector< ACTION_LABEL_T > &	action_labels () const
	The action labels in this lts.

void	set_action_label (const labels_size_type action, const ACTION_LABEL_T &label)
	Sets the label of an action.

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.

std::set< labels_size_type > &	hidden_label_set ()
	Returns the hidden label set that tells for each label what its corresponding hidden label is.

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.

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.

STATE_LABEL_T	state_label (const states_size_type state) const
	Gets the label of a state.

bool	is_probabilistic (const states_size_type state) const
	Gets the label of a state.

ACTION_LABEL_T	action_label (const labels_size_type action) const
	Gets the label of an action.

void	clear_transitions (const std::size_t n=0)
	Clear the transitions of an lts.

void	clear_actions ()
	Clear the action labels of an lts.

void	clear_state_labels ()
	Clear the labels of an lts.

void	clear ()
	Clear the transitions system.

const std::vector< transition > &	get_transitions () const
	Gets a const reference to the vector of transitions of the current lts.

std::vector< transition > &	get_transitions ()
	Gets a reference to the vector of transitions of the current lts.

void	add_transition (const transition &t)
	Add a transition to the lts.

bool	is_tau (labels_size_type action) const
	Checks whether an action is a tau action.

void	record_hidden_actions (const std::vector< std::string > &tau_actions)
	Records all actions with a string that occurs in tau_actions internally.

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.

bool	has_state_info () const
	Checks whether this LTS has state values associated with its states.

bool	has_action_info () const
	Checks whether this LTS has labels associated with its actions, which are numbers.

Public Member Functions inherited from mcrl2::lts::lts_default_base
lts_type	type ()
	Provides the type of this lts, in casu lts_none.

void	swap (lts_default_base &)
	Standard swap function.

bool	operator== (const lts_default_base &) const
	Standard equality function.

Static Public Attributes
static constexpr bool	is_probabilistic_lts =false
	An indicator that this is not a probabilistic lts.

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)

Protected Attributes
states_size_type	m_nstates

states_size_type	m_init_state

std::vector< transition >	m_transitions

std::vector< STATE_LABEL_T >	m_state_labels

std::vector< ACTION_LABEL_T >	m_action_labels

std::set< labels_size_type >	m_hidden_label_set

Detailed Description

template<class STATE_LABEL_T, class ACTION_LABEL_T, class LTS_BASE = lts_default_base>
class mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >

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.

Definition at line 82 of file lts.h.

Member Typedef Documentation

◆ action_label_t

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

typedef ACTION_LABEL_T mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::action_label_t

The type of action labels.

Definition at line 92 of file lts.h.

◆ base_t

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

typedef LTS_BASE mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::base_t

The type of the used lts base.

Definition at line 96 of file lts.h.

◆ labels_size_type

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

typedef std::vector<ACTION_LABEL_T>::size_type mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::labels_size_type

The sort that represents the indices of labels.

Definition at line 104 of file lts.h.

◆ state_label_t

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

typedef STATE_LABEL_T mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::state_label_t

The type of state labels.

Definition at line 88 of file lts.h.

◆ states_size_type

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

typedef std::vector<STATE_LABEL_T>::size_type mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::states_size_type

The sort that contains the indices of states.

Definition at line 100 of file lts.h.

◆ transitions_size_type

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

typedef std::vector<transition>::size_type mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::transitions_size_type

The sort that contains indices of transitions.

Definition at line 108 of file lts.h.

Constructor & Destructor Documentation

◆ lts() [1/2]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::lts ( )

inline

Creates an empty LTS.

Definition at line 172 of file lts.h.

◆ lts() [2/2]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::lts ( const lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > & l )

inline

Creates a copy of the supplied LTS.

Parameters

[in] l The LTS to copy.

Definition at line 180 of file lts.h.

Member Function Documentation

◆ action_label()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

ACTION_LABEL_T mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::action_label ( const labels_size_type action ) const

inline

Gets the label of an action.

Parameters

[in] action The number of the action.

Returns: The label of the action.

Definition at line 470 of file lts.h.

◆ action_labels()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

const std::vector< ACTION_LABEL_T > & mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::action_labels ( ) const

inline

The action labels in this lts.

Returns: The action labels of this lts.

Definition at line 393 of file lts.h.

◆ add_action()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

labels_size_type mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::add_action ( const ACTION_LABEL_T & label )

inline

Adds an action with a label to this LTS.

It is not checked whether this action label already exists.

Parameters

[in] label The label of the label.

Returns: The number of the added label.

Definition at line 361 of file lts.h.

◆ add_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

states_size_type mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::add_state ( const STATE_LABEL_T & label = STATE_LABEL_T() )

inline

Adds a state to this LTS.

It is not checked whether the added state already exists.

Parameters

[in] 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.

Definition at line 347 of file lts.h.

◆ add_transition()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::add_transition ( const transition & t )

inline

Add a transition to the lts.

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

Definition at line 544 of file lts.h.

◆ apply_hidden_actions()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::apply_hidden_actions ( const std::vector< std::string > & tau_actions )

inline

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

[in] tau_actions Vector with strings indicating which actions must be transformed to tau's

Definition at line 609 of file lts.h.

◆ apply_hidden_label_map()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

labels_size_type mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::apply_hidden_label_map ( const labels_size_type action ) const

inline

If the action label is registered hidden, it returns tau, otherwise the original label.

Parameters

[in] action The index of an action label.

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

Definition at line 438 of file lts.h.

◆ clear()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::clear ( )

inline

Clear the transitions system.

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

Definition at line 514 of file lts.h.

◆ clear_actions()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::clear_actions ( )

inline

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.

Definition at line 495 of file lts.h.

◆ clear_state_labels()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::clear_state_labels ( )

inline

Clear the labels of an lts.

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

Definition at line 506 of file lts.h.

◆ clear_transitions()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::clear_transitions ( const std::size_t n = 0 )

inline

Clear the transitions of an lts.

Parameters

[in] 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.

Definition at line 484 of file lts.h.

◆ get_transitions() [1/2]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

std::vector< transition > & mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::get_transitions ( )

inline

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.

Definition at line 535 of file lts.h.

◆ get_transitions() [2/2]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

const std::vector< transition > & mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::get_transitions ( ) const

inline

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.

Definition at line 526 of file lts.h.

◆ has_action_info()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

bool mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::has_action_info ( ) const

inline

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

Return values

true	if the LTS has values for labels;
false	otherwise.

Definition at line 645 of file lts.h.

◆ has_state_info()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

bool mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::has_state_info ( ) const

inline

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

Return values

true	if the LTS has state information;
false	otherwise.

Definition at line 636 of file lts.h.

◆ hidden_label_set() [1/2]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

std::set< labels_size_type > & mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::hidden_label_set ( )

inline

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

Returns: The hidden action set

Definition at line 422 of file lts.h.

◆ hidden_label_set() [2/2]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

const std::set< labels_size_type > & mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::hidden_label_set ( ) const

inline

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

Returns: The hidden action set

Definition at line 414 of file lts.h.

◆ initial_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

states_size_type mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::initial_state ( ) const

inline

Gets the initial state number of this LTS.

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

Definition at line 326 of file lts.h.

◆ is_probabilistic()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

bool mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::is_probabilistic ( const states_size_type state ) const

inline

Gets the label of a state.

Parameters

[in] state The number of the state.

Returns: The label of the state.

Definition at line 460 of file lts.h.

◆ is_tau()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

bool mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::is_tau ( labels_size_type action ) const

inline

Checks whether an action is a tau action.

Parameters

[in] action The number of the action.

Return values

true	if the action is a tau action;
false	otherwise.

Definition at line 553 of file lts.h.

◆ num_action_labels()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

labels_size_type mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::num_action_labels ( ) const

inline

Gets the number of action labels of this LTS.

Returns: The number of action labels of this LTS.

Definition at line 318 of file lts.h.

◆ num_state_labels()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

states_size_type mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::num_state_labels ( ) const

inline

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.

Definition at line 271 of file lts.h.

◆ num_states()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

states_size_type mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::num_states ( ) const

inline

Gets the number of states of this LTS.

Returns: The number of states of this LTS.

Definition at line 245 of file lts.h.

◆ num_transitions()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

transitions_size_type mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::num_transitions ( ) const

inline

Gets the number of transitions of this LTS.

Returns: The number of transitions of this LTS.

Definition at line 302 of file lts.h.

◆ operator=()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

lts & mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::operator= ( const lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > & l )

inline

Standard assignment operator.

Parameters

[in] l The lts to be assigned.

Definition at line 194 of file lts.h.

◆ operator==()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

bool mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::operator== ( const lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > & other ) const

inline

Standard equality operator.

Parameters

[in] other The lts to compare with.

Definition at line 209 of file lts.h.

◆ record_hidden_actions()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::record_hidden_actions ( const std::vector< std::string > & tau_actions )

inline

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

[in] tau_actions Vector with strings indicating which actions must be transformed to tau's

Definition at line 570 of file lts.h.

◆ rename_labels()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::rename_labels ( const std::map< labels_size_type, labels_size_type > & action_rename_map )

inlineprotected

Definition at line 127 of file lts.h.

◆ set_action_label()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::set_action_label	(	const labels_size_type	action,
		const ACTION_LABEL_T &	label
	)

inline

Sets the label of an action.

Parameters

[in]	action	The number of the action.
[in]	label	The label that will be assigned to the action.

Definition at line 402 of file lts.h.

◆ set_hidden_label_set()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::set_hidden_label_set ( const std::set< labels_size_type > & m )

inline

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

Parameters

[in] m The new hidden label map.

Definition at line 430 of file lts.h.

◆ set_initial_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::set_initial_state ( const states_size_type state )

inline

Sets the initial state number of this LTS.

Parameters

[in] state The number of the state that will become the initial state.

Definition at line 334 of file lts.h.

◆ set_num_action_labels()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::set_num_action_labels ( const labels_size_type n )

inline

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.

Definition at line 310 of file lts.h.

◆ set_num_states()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::set_num_states	(	const states_size_type	n,
		const bool	has_state_labels = `true`
	)

inline

Sets the number of states of this LTS.

Parameters

[in]	n	The number of states of this LTS.
[in]	has_state_labels	If true state labels are initialised

Definition at line 280 of file lts.h.

◆ set_state_label()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::set_state_label	(	const states_size_type	state,
		const STATE_LABEL_T &	label
	)

inline

Sets the label of a state.

Parameters

[in]	state	The number of the state.
[in]	label	The label that will be assigned to the state.

Definition at line 384 of file lts.h.

◆ state_label()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

STATE_LABEL_T mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::state_label ( const states_size_type state ) const

inline

Gets the label of a state.

Parameters

[in] state The number of the state.

Returns: The label of the state.

Definition at line 450 of file lts.h.

◆ state_labels() [1/2]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

std::vector< STATE_LABEL_T > & mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::state_labels ( )

inline

Provides the state labels of an LTS.

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

Definition at line 253 of file lts.h.

◆ state_labels() [2/2]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

const std::vector< STATE_LABEL_T > & mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::state_labels ( ) const

inline

Provides the state labels of an LTS.

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

Definition at line 261 of file lts.h.

◆ store_action_label_to_be_renamed()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::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
	)

inlineprotected

Definition at line 146 of file lts.h.

◆ swap()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

void mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::swap ( lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > & l )

inline

Swap this lts with the supplied supplied LTS.

Parameters

[in] l The LTS to swap.

Definition at line 222 of file lts.h.

◆ tau_label_index()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

const labels_size_type mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::tau_label_index ( ) const

inline

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.

Definition at line 376 of file lts.h.

Member Data Documentation

◆ is_probabilistic_lts

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

constexpr bool mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::is_probabilistic_lts =false

staticconstexpr

An indicator that this is not a probabilistic lts.

Definition at line 112 of file lts.h.

◆ m_action_labels

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

std::vector<ACTION_LABEL_T> mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::m_action_labels

protected

Definition at line 120 of file lts.h.

◆ m_hidden_label_set

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

std::set<labels_size_type> mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::m_hidden_label_set

protected

Definition at line 124 of file lts.h.

◆ m_init_state

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

states_size_type mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::m_init_state

protected

Definition at line 117 of file lts.h.

◆ m_nstates

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

states_size_type mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::m_nstates

protected

Definition at line 116 of file lts.h.

◆ m_state_labels

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

std::vector<STATE_LABEL_T> mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::m_state_labels

protected

Definition at line 119 of file lts.h.

◆ m_transitions

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE = lts_default_base>

std::vector<transition> mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >::m_transitions

protected

Definition at line 118 of file lts.h.

The documentation for this class was generated from the following file:

lts/include/mcrl2/lts/lts.h

Public Types

Public Member Functions

Static Public Attributes

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ action_label_t

◆ base_t

◆ labels_size_type

◆ state_label_t

◆ states_size_type

◆ transitions_size_type

Constructor & Destructor Documentation

◆ lts() [1/2]

◆ lts() [2/2]

Member Function Documentation

◆ action_label()

◆ action_labels()

◆ add_action()

◆ add_state()

◆ add_transition()

◆ apply_hidden_actions()

◆ apply_hidden_label_map()

◆ clear()

◆ clear_actions()

◆ clear_state_labels()

◆ clear_transitions()

◆ get_transitions() [1/2]

◆ get_transitions() [2/2]

◆ has_action_info()

◆ has_state_info()

◆ hidden_label_set() [1/2]

◆ hidden_label_set() [2/2]

◆ initial_state()

◆ is_probabilistic()

◆ is_tau()

◆ num_action_labels()

◆ num_state_labels()

◆ num_states()

◆ num_transitions()

◆ operator=()

◆ operator==()

◆ record_hidden_actions()

◆ rename_labels()

◆ set_action_label()

◆ set_hidden_label_set()

◆ set_initial_state()

◆ set_num_action_labels()

◆ set_num_states()

◆ set_state_label()

◆ state_label()

◆ state_labels() [1/2]

◆ state_labels() [2/2]

◆ store_action_label_to_be_renamed()

◆ swap()

◆ tau_label_index()

Member Data Documentation

◆ is_probabilistic_lts

◆ m_action_labels

◆ m_hidden_label_set

◆ m_init_state

◆ m_nstates

◆ m_state_labels

◆ m_transitions