#include <lts_fsm.h>

Inheritance diagram for mcrl2::lts::detail::lts_fsm_base:

Public Types
typedef mcrl2::lts::probabilistic_state< std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fraction >	probabilistic_state

typedef mcrl2::lps::state_probability_pair< std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fraction >	state_probability_pair

Public Member Functions
bool	operator== (const lts_fsm_base &other) const

lts_type	type () const
	The lts_type of this labelled transition system. In this case lts_fsm.

void	swap (lts_fsm_base &other)
	Standard swap function.

void	clear ()
	Clear the transitions system.

const std::vector< std::string > &	state_element_values (std::size_t idx) const
	Provides the vector of strings that correspond to the values of the number at position idx in a vector.

std::string	state_label_to_string (const state_label_fsm &l) const
	Pretty print a state value of this FSM.

std::size_t	add_state_element_value (std::size_t idx, const std::string &s)
	Adds a string to the state element values for the idx-th position in a state vector. Returns the number given to this string.

std::string	state_element_value (std::size_t parameter_index, std::size_t element_index) const
	Returns the element_index'th element for the parameter with index parameter_index.

std::vector< std::pair< std::string, std::string > >	process_parameters () const
	Return the parameters of the state vectors stored in this LTS.

std::pair< std::string, std::string >	process_parameter (std::size_t i) const
	Returns the i-th parameter of the state vectors stored in this LTS.

void	clear_process_parameters ()
	Clear the state parameters for this LTS.

void	add_process_parameter (const std::string &name, const std::string &sort)
	Set the state parameters for this LTS.

Protected Attributes
std::vector< std::vector< std::string > >	m_state_element_values
	state_element_values contain the values that can occur at the i-th position of a state label

std::vector< std::pair< std::string, std::string > >	m_parameters
	m_parameters contain the parameters corresponding to the consecutive elements of a state vector. A parameter consists of two strings: a variable name and a string indicating its sort.

Detailed Description

Definition at line 83 of file lts_fsm.h.

Member Typedef Documentation

◆ probabilistic_state

typedef mcrl2::lts::probabilistic_state<std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fraction> mcrl2::lts::detail::lts_fsm_base::probabilistic_state

Definition at line 86 of file lts_fsm.h.

◆ state_probability_pair

typedef mcrl2::lps::state_probability_pair<std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fraction> mcrl2::lts::detail::lts_fsm_base::state_probability_pair

Definition at line 87 of file lts_fsm.h.

Member Function Documentation

◆ add_process_parameter()

void mcrl2::lts::detail::lts_fsm_base::add_process_parameter	(	const std::string &	name,
		const std::string &	sort
	)

inline

Set the state parameters for this LTS.

Parameters

[in]	name	The variable name of the added parameter.
[in]	sort	The sort of the added parameter.

Definition at line 229 of file lts_fsm.h.

◆ add_state_element_value()

std::size_t mcrl2::lts::detail::lts_fsm_base::add_state_element_value	(	std::size_t	idx,
		const std::string &	s
	)

inline

Adds a string to the state element values for the idx-th position in a state vector. Returns the number given to this string.

Parameters

[in]	idx	The parameter index.
[in]	s	String to be added as value for the indicate parameter.

Returns: The index for the added parameter.

Definition at line 172 of file lts_fsm.h.

◆ clear()

void mcrl2::lts::detail::lts_fsm_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 128 of file lts_fsm.h.

◆ clear_process_parameters()

void mcrl2::lts::detail::lts_fsm_base::clear_process_parameters ( )

inline

Clear the state parameters for this LTS.

Definition at line 219 of file lts_fsm.h.

◆ operator==()

bool mcrl2::lts::detail::lts_fsm_base::operator== ( const lts_fsm_base & other ) const

inline

Definition at line 102 of file lts_fsm.h.

◆ process_parameter()

std::pair< std::string, std::string > mcrl2::lts::detail::lts_fsm_base::process_parameter ( std::size_t i ) const

inline

Returns the i-th parameter of the state vectors stored in this LTS.

Parameters

[in] i The index of the parameter.

Returns: The variable/sort of the state parameter at index i.

Definition at line 211 of file lts_fsm.h.

◆ process_parameters()

std::vector< std::pair< std::string, std::string > > mcrl2::lts::detail::lts_fsm_base::process_parameters ( ) const

inline

Return the parameters of the state vectors stored in this LTS.

Returns: The state parameters stored in this LTS.

Definition at line 202 of file lts_fsm.h.

◆ state_element_value()

std::string mcrl2::lts::detail::lts_fsm_base::state_element_value	(	std::size_t	parameter_index,
		std::size_t	element_index
	)		const

inline

Returns the element_index'th element for the parameter with index parameter_index.

If there are no values for the parameter_index, the element_index is transformed to a string, and this string is returned.

Parameters

[in]	parameter_index	The index for this parameter.
[in]	element_index	The index to the value string corresponding to this parameter.

Returns: The string corresponding to the two given indices.

Definition at line 187 of file lts_fsm.h.

◆ state_element_values()

const std::vector< std::string > & mcrl2::lts::detail::lts_fsm_base::state_element_values ( std::size_t idx ) const

inline

Provides the vector of strings that correspond to the values of the number at position idx in a vector.

Parameters

[in] idx The index of the parameter.

Returns: A vector containing strings representing the possible values that this parameter can have.

Definition at line 140 of file lts_fsm.h.

◆ state_label_to_string()

std::string mcrl2::lts::detail::lts_fsm_base::state_label_to_string ( const state_label_fsm & l ) const

inline

Pretty print a state value of this FSM.

The label l is printed as (t1,...,tn). It uses information from the lts.

Parameters

[in] l The state value to pretty print.

Returns: The pretty-printed representation of value.

Definition at line 150 of file lts_fsm.h.

◆ swap()

void mcrl2::lts::detail::lts_fsm_base::swap ( lts_fsm_base & other )

inline

Standard swap function.

Definition at line 117 of file lts_fsm.h.

◆ type()

lts_type mcrl2::lts::detail::lts_fsm_base::type ( ) const

inline

The lts_type of this labelled transition system. In this case lts_fsm.

Returns: Returns lts_fsm as type of this transition system.

Definition at line 111 of file lts_fsm.h.

Member Data Documentation

◆ m_parameters

std::vector< std::pair < std::string, std::string > > mcrl2::lts::detail::lts_fsm_base::m_parameters

protected

m_parameters contain the parameters corresponding to the consecutive elements of a state vector. A parameter consists of two strings: a variable name and a string indicating its sort.

Definition at line 98 of file lts_fsm.h.

◆ m_state_element_values

std::vector< std::vector < std::string > > mcrl2::lts::detail::lts_fsm_base::m_state_element_values

protected

state_element_values contain the values that can occur at the i-th position of a state label

Definition at line 93 of file lts_fsm.h.

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

lts/include/mcrl2/lts/lts_fsm.h

Public Types

Public Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ probabilistic_state

◆ state_probability_pair

Member Function Documentation

◆ add_process_parameter()

◆ add_state_element_value()

◆ clear()

◆ clear_process_parameters()

◆ operator==()

◆ process_parameter()

◆ process_parameters()

◆ state_element_value()

◆ state_element_values()

◆ state_label_to_string()

◆ swap()

◆ type()

Member Data Documentation

◆ m_parameters

◆ m_state_element_values