mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::detail::lts_fsm_base Class Reference

#include <lts_fsm.h>

Inheritance diagram for mcrl2::lts::detail::lts_fsm_base:
mcrl2::lts::lts< state_label_fsm, action_label_string, detail::lts_fsm_base > mcrl2::lts::lts_fsm_t

Public Types

typedef mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fractionprobabilistic_state
 
typedef mcrl2::lps::state_probability_pair< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fractionstate_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

◆ state_probability_pair

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]nameThe variable name of the added parameter.
[in]sortThe 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]idxThe parameter index.
[in]sString 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]iThe 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_indexThe index for this parameter.
[in]element_indexThe 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]idxThe 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]lThe 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: