mCRL2
Loading...
Searching...
No Matches
Public Member Functions | Public Attributes | List of all members
mcrl2::lts::detail::fsm_builder Struct Reference

#include <fsm_builder.h>

Public Member Functions

 fsm_builder (probabilistic_lts_fsm_t &fsm_)
 
void start ()
 
std::size_t find_maximal_state_index (const lts_fsm_base::probabilistic_state &distribution)
 
void add_transition (const std::string &source, const std::string &target, const std::string &label)
 
void add_state (const std::vector< std::size_t > &values)
 
void add_parameter (const std::string &name, const std::string &cardinality, const std::string &sort, const std::vector< std::string > &domain_values)
 
void add_initial_distribution (const std::string &distribution)
 
void write_parameters ()
 
void finish ()
 

Public Attributes

probabilistic_lts_fsm_t & fsm
 
std::vector< fsm_parameter > parameters
 
std::map< std::string, std::size_t > labels
 
bool m_initial_state_is_set
 

Detailed Description

Definition at line 202 of file fsm_builder.h.

Constructor & Destructor Documentation

◆ fsm_builder()

mcrl2::lts::detail::fsm_builder::fsm_builder ( probabilistic_lts_fsm_t &  fsm_)
inlineexplicit

Definition at line 204 of file fsm_builder.h.

Member Function Documentation

◆ add_initial_distribution()

void mcrl2::lts::detail::fsm_builder::add_initial_distribution ( const std::string &  distribution)
inline

Definition at line 285 of file fsm_builder.h.

◆ add_parameter()

void mcrl2::lts::detail::fsm_builder::add_parameter ( const std::string &  name,
const std::string &  cardinality,
const std::string &  sort,
const std::vector< std::string > &  domain_values 
)
inline

Definition at line 280 of file fsm_builder.h.

◆ add_state()

void mcrl2::lts::detail::fsm_builder::add_state ( const std::vector< std::size_t > &  values)
inline

Definition at line 275 of file fsm_builder.h.

◆ add_transition()

void mcrl2::lts::detail::fsm_builder::add_transition ( const std::string &  source,
const std::string &  target,
const std::string &  label 
)
inline

Definition at line 247 of file fsm_builder.h.

◆ find_maximal_state_index()

std::size_t mcrl2::lts::detail::fsm_builder::find_maximal_state_index ( const lts_fsm_base::probabilistic_state &  distribution)
inline

Definition at line 230 of file fsm_builder.h.

◆ finish()

void mcrl2::lts::detail::fsm_builder::finish ( )
inline

Definition at line 317 of file fsm_builder.h.

◆ start()

void mcrl2::lts::detail::fsm_builder::start ( )
inline

Definition at line 222 of file fsm_builder.h.

◆ write_parameters()

void mcrl2::lts::detail::fsm_builder::write_parameters ( )
inline

Definition at line 300 of file fsm_builder.h.

Member Data Documentation

◆ fsm

probabilistic_lts_fsm_t& mcrl2::lts::detail::fsm_builder::fsm

Definition at line 210 of file fsm_builder.h.

◆ labels

std::map<std::string, std::size_t> mcrl2::lts::detail::fsm_builder::labels

Definition at line 216 of file fsm_builder.h.

◆ m_initial_state_is_set

bool mcrl2::lts::detail::fsm_builder::m_initial_state_is_set

Definition at line 220 of file fsm_builder.h.

◆ parameters

std::vector<fsm_parameter> mcrl2::lts::detail::fsm_builder::parameters

Definition at line 213 of file fsm_builder.h.

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