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

#include <probabilistic_lts.h>

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

Public Types
using	super = lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >

using	probabilistic_state_t = PROBABILISTIC_STATE_T
	The type of probabilistic labels.

using	state_label_t = typename super::state_label_t

using	action_label_t = typename super::action_label_t

using	base_t = typename super::base_t

using	states_size_type = typename super::states_size_type

using	labels_size_type = typename super::labels_size_type

using	transitions_size_type = typename super::transitions_size_type

Public Types inherited from mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >
using	state_label_t = STATE_LABEL_T
	The type of state labels.

using	action_label_t = ACTION_LABEL_T
	The type of action labels.

using	base_t = LTS_BASE
	The type of the used lts base.

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

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

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

Public Member Functions
	probabilistic_lts ()=default
	Creates an empty LTS.

	probabilistic_lts (const probabilistic_lts &other)=default
	Standard copy constructor.

	probabilistic_lts (probabilistic_lts &&other)=default
	Standard move constructor.

probabilistic_lts &	operator= (const probabilistic_lts &other)=default
	Standard assignment operator.

probabilistic_lts &	operator= (probabilistic_lts &&other)=default
	Standard assignment move operator.

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

void	swap (probabilistic_lts &other) noexcept
	Swap this lts with the supplied supplied LTS.

const PROBABILISTIC_STATE_T &	initial_probabilistic_state () const
	Gets the initial state number of this LTS.

void	set_initial_probabilistic_state (const PROBABILISTIC_STATE_T &state)
	Sets the probabilistic initial state number of this LTS.

labels_size_type	num_probabilistic_states () const
	Gets the number of probabilistic states of this LTS.

states_size_type	add_probabilistic_state (const PROBABILISTIC_STATE_T &s)
	Adds a probabilistic state to this LTS.

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.

void	set_probabilistic_state (const states_size_type index, const PROBABILISTIC_STATE_T &s)
	Sets the probabilistic label corresponding to some index.

const PROBABILISTIC_STATE_T &	probabilistic_state (const states_size_type index) const
	Gets the probabilistic label of an index.

void	clear_probabilistic_states ()
	Clear the probabilistic states in this probabilistic transitions system.

void	clear ()
	Clear the transitions system.

Public Member Functions inherited from mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >
	lts ()
	Creates an empty LTS.

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

	lts (lts &&)=default
	Move constructor. Defaulted to avoid expensive copies when an lts is moved.

lts &	operator= (lts &&)=default
	Move assignment operator. Defaulted to avoid expensive copies when an lts is moved.

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

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

void	swap (lts &l) noexcept
	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_transitions (const std::size_t n)
	Sets the number of transitions of this LTS and tries to shrink the datastructure.

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.

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	add_state_number_as_state_information ()
	Label each state with its state number.

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	rename_hidden_labels_to_tau ()
	Rename the hidden labels in the hidden label map explicitly in the lts.

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.

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

Static Public Attributes inherited from mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >
static constexpr bool	is_probabilistic_lts
	An indicator that this is not a probabilistic lts.

Protected Member Functions
states_size_type	initial_state () const

void	set_initial_state (const states_size_type s)

Protected Member Functions inherited from mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >
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
std::vector< PROBABILISTIC_STATE_T >	m_probabilistic_states

PROBABILISTIC_STATE_T	m_init_probabilistic_state

Protected Attributes inherited from mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >
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 PROBABILISTIC_STATE_T, class LTS_BASE>
class mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_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 42 of file probabilistic_lts.h.

Member Typedef Documentation

◆ action_label_t

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

using mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::action_label_t = typename super::action_label_t

Definition at line 53 of file probabilistic_lts.h.

◆ base_t

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

using mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::base_t = typename super::base_t

Definition at line 54 of file probabilistic_lts.h.

◆ labels_size_type

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

using mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::labels_size_type = typename super::labels_size_type

Definition at line 56 of file probabilistic_lts.h.

◆ probabilistic_state_t

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

using mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::probabilistic_state_t = PROBABILISTIC_STATE_T

The type of probabilistic labels.

Definition at line 50 of file probabilistic_lts.h.

◆ state_label_t

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

using mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::state_label_t = typename super::state_label_t

Definition at line 52 of file probabilistic_lts.h.

◆ states_size_type

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

using mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::states_size_type = typename super::states_size_type

Definition at line 55 of file probabilistic_lts.h.

◆ super

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

using mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::super = lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE>

Definition at line 46 of file probabilistic_lts.h.

◆ transitions_size_type

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

using mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::transitions_size_type = typename super::transitions_size_type

Definition at line 57 of file probabilistic_lts.h.

Constructor & Destructor Documentation

◆ probabilistic_lts() [1/3]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

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

default

Creates an empty LTS.

◆ probabilistic_lts() [2/3]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::probabilistic_lts ( const probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > & other )

default

Standard copy constructor.

Parameters

[in] other The LTS to copy.

◆ probabilistic_lts() [3/3]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::probabilistic_lts ( probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > && other )

default

Standard move constructor.

Parameters

[in] other The LTS to copy.

Member Function Documentation

◆ add_and_reset_probabilistic_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

states_size_type mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::add_and_reset_probabilistic_state ( PROBABILISTIC_STATE_T & s )

inline

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

[in] s The probabilistic state.

Returns: The index of the added probabilistic state.

Definition at line 162 of file probabilistic_lts.h.

◆ add_probabilistic_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

states_size_type mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::add_probabilistic_state ( const PROBABILISTIC_STATE_T & s )

inline

Adds a probabilistic state to this LTS.

It is not checked whether this probabilistic state already exists.

Parameters

[in] s The probabilistic state.

Returns: The index of the added probabilistic.

Definition at line 150 of file probabilistic_lts.h.

◆ clear()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

void mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_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 198 of file probabilistic_lts.h.

◆ clear_probabilistic_states()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

void mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::clear_probabilistic_states ( )

inline

Clear the probabilistic states in this probabilistic transitions system.

Definition at line 190 of file probabilistic_lts.h.

◆ initial_probabilistic_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

const PROBABILISTIC_STATE_T & mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::initial_probabilistic_state ( ) const

inline

Gets the initial state number of this LTS.

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

Definition at line 122 of file probabilistic_lts.h.

◆ initial_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

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

inlineprotected

Definition at line 69 of file probabilistic_lts.h.

◆ num_probabilistic_states()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

labels_size_type mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::num_probabilistic_states ( ) const

inline

Gets the number of probabilistic states of this LTS.

Returns: The number of action labels of this LTS.

Definition at line 141 of file probabilistic_lts.h.

◆ operator=() [1/2]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

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

default

Standard assignment operator.

Parameters

[in] other The LTS to assign.

◆ operator=() [2/2]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

probabilistic_lts & mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::operator= ( probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > && other )

default

Standard assignment move operator.

Parameters

[in] other The LTS to assign.

◆ operator==()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

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

inline

Standard equality operator.

Parameters

[in] other The LTS to compare this probabilistic lts with.

Definition at line 104 of file probabilistic_lts.h.

◆ probabilistic_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

const PROBABILISTIC_STATE_T & mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::probabilistic_state ( const states_size_type index ) const

inline

Gets the probabilistic label of an index.

Parameters

[in] index The index of an action.

Returns: The probabilistic state belonging to the index.

Definition at line 182 of file probabilistic_lts.h.

◆ set_initial_probabilistic_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

void mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::set_initial_probabilistic_state ( const PROBABILISTIC_STATE_T & state )

inline

Sets the probabilistic initial state number of this LTS.

Parameters

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

Definition at line 130 of file probabilistic_lts.h.

◆ set_initial_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

void mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::set_initial_state ( const states_size_type s )

inlineprotected

Definition at line 75 of file probabilistic_lts.h.

◆ set_probabilistic_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

void mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::set_probabilistic_state	(	const states_size_type	index,
		const PROBABILISTIC_STATE_T &	s
	)

inline

Sets the probabilistic label corresponding to some index.

Parameters

[in]	index	The index of the state.
[in]	s	The new probabilistic state belonging to this index.

Definition at line 173 of file probabilistic_lts.h.

◆ swap()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

void mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::swap ( probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > & other )

inlinenoexcept

Swap this lts with the supplied supplied LTS.

Parameters

[in] l The LTS to swap.

Definition at line 113 of file probabilistic_lts.h.

Member Data Documentation

◆ is_probabilistic_lts

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

constexpr bool mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::is_probabilistic_lts =true

staticconstexpr

An indicator that this is a probabilistic lts.

Definition at line 61 of file probabilistic_lts.h.

◆ m_init_probabilistic_state

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

PROBABILISTIC_STATE_T mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::m_init_probabilistic_state

protected

Definition at line 66 of file probabilistic_lts.h.

◆ m_probabilistic_states

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

std::vector<PROBABILISTIC_STATE_T> mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::m_probabilistic_states

protected

Definition at line 65 of file probabilistic_lts.h.

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

lts/include/mcrl2/lts/probabilistic_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

◆ probabilistic_state_t

◆ state_label_t

◆ states_size_type

◆ super

◆ transitions_size_type

Constructor & Destructor Documentation

◆ probabilistic_lts() [1/3]

◆ probabilistic_lts() [2/3]

◆ probabilistic_lts() [3/3]

Member Function Documentation

◆ add_and_reset_probabilistic_state()

◆ add_probabilistic_state()

◆ clear()

◆ clear_probabilistic_states()

◆ initial_probabilistic_state()

◆ initial_state()

◆ num_probabilistic_states()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ operator==()

◆ probabilistic_state()

◆ set_initial_probabilistic_state()

◆ set_initial_state()

◆ set_probabilistic_state()

◆ swap()

Member Data Documentation

◆ is_probabilistic_lts

◆ m_init_probabilistic_state

◆ m_probabilistic_states