mCRL2
Loading...
Searching...
No Matches
Public Member Functions | Static Public Member Functions | Protected Attributes | List of all members
mcrl2::lts::stochastic_lts_lts_builder Class Reference

#include <stochastic_lts_builder.h>

Inheritance diagram for mcrl2::lts::stochastic_lts_lts_builder:
mcrl2::lts::stochastic_lts_builder mcrl2::lts::stochastic_lts_fsm_builder

Public Member Functions

 stochastic_lts_lts_builder (const data::data_specification &dataspec, const process::action_label_list &action_labels, const data::variable_list &process_parameters, bool discard_state_labels=false)
 
void set_initial_state (const std::list< std::size_t > &targets, const std::vector< data::data_expression > &probabilities) override
 
void add_transition (std::size_t from, const lps::multi_action &a, const std::list< std::size_t > &targets, const std::vector< data::data_expression > &probabilities, const std::size_t number_of_threads) override
 
void finalize (const indexed_set_for_states_type &state_map, bool timed) override
 
void save (const std::string &filename) override
 
- Public Member Functions inherited from mcrl2::lts::stochastic_lts_builder
 stochastic_lts_builder ()
 
std::size_t add_action (const lps::multi_action &a)
 
virtual void set_initial_state (const std::list< std::size_t > &targets, const std::vector< data::data_expression > &probabilities)=0
 
virtual void add_transition (std::size_t from, const lps::multi_action &a, const std::list< std::size_t > &targets, const std::vector< data::data_expression > &probabilities, const std::size_t number_of_threads=1)=0
 
virtual void finalize (const indexed_set_for_states_type &state_map, bool timed)=0
 
virtual void save (const std::string &filename)=0
 
virtual ~stochastic_lts_builder ()=default
 

Static Public Member Functions

static probabilistic_state< std::size_t, lps::probabilistic_data_expression > make_probabilistic_state (const std::list< std::size_t > &targets, const std::vector< data::data_expression > &probabilities)
 

Protected Attributes

probabilistic_lts_lts_t m_lts
 
bool m_discard_state_labels = false
 
probabilistic_state< std::size_t, lps::probabilistic_data_expression > m_initial_state
 
std::mutex m_exclusive_transition_access
 

Additional Inherited Members

- Public Types inherited from mcrl2::lts::stochastic_lts_builder
typedef atermpp::indexed_set< lps::state, mcrl2::utilities::detail::GlobalThreadSafe > indexed_set_for_states_type
 
- Public Attributes inherited from mcrl2::lts::stochastic_lts_builder
utilities::unordered_map_large< lps::multi_action, std::size_t > m_actions
 

Detailed Description

Definition at line 190 of file stochastic_lts_builder.h.

Constructor & Destructor Documentation

◆ stochastic_lts_lts_builder()

mcrl2::lts::stochastic_lts_lts_builder::stochastic_lts_lts_builder ( const data::data_specification &  dataspec,
const process::action_label_list &  action_labels,
const data::variable_list &  process_parameters,
bool  discard_state_labels = false 
)
inline

Definition at line 199 of file stochastic_lts_builder.h.

Member Function Documentation

◆ add_transition()

void mcrl2::lts::stochastic_lts_lts_builder::add_transition ( std::size_t  from,
const lps::multi_action &  a,
const std::list< std::size_t > &  targets,
const std::vector< data::data_expression > &  probabilities,
const std::size_t  number_of_threads 
)
inlineoverridevirtual

Implements mcrl2::lts::stochastic_lts_builder.

Definition at line 240 of file stochastic_lts_builder.h.

◆ finalize()

void mcrl2::lts::stochastic_lts_lts_builder::finalize ( const indexed_set_for_states_type &  state_map,
bool  timed 
)
inlineoverridevirtual

Implements mcrl2::lts::stochastic_lts_builder.

Definition at line 252 of file stochastic_lts_builder.h.

◆ make_probabilistic_state()

static probabilistic_state< std::size_t, lps::probabilistic_data_expression > mcrl2::lts::stochastic_lts_lts_builder::make_probabilistic_state ( const std::list< std::size_t > &  targets,
const std::vector< data::data_expression > &  probabilities 
)
inlinestatic

Definition at line 213 of file stochastic_lts_builder.h.

◆ save()

void mcrl2::lts::stochastic_lts_lts_builder::save ( const std::string &  filename)
inlineoverridevirtual

Implements mcrl2::lts::stochastic_lts_builder.

Definition at line 285 of file stochastic_lts_builder.h.

◆ set_initial_state()

void mcrl2::lts::stochastic_lts_lts_builder::set_initial_state ( const std::list< std::size_t > &  targets,
const std::vector< data::data_expression > &  probabilities 
)
inlineoverridevirtual

Implements mcrl2::lts::stochastic_lts_builder.

Definition at line 234 of file stochastic_lts_builder.h.

Member Data Documentation

◆ m_discard_state_labels

bool mcrl2::lts::stochastic_lts_lts_builder::m_discard_state_labels = false
protected

Definition at line 194 of file stochastic_lts_builder.h.

◆ m_exclusive_transition_access

std::mutex mcrl2::lts::stochastic_lts_lts_builder::m_exclusive_transition_access
protected

Definition at line 196 of file stochastic_lts_builder.h.

◆ m_initial_state

probabilistic_state<std::size_t, lps::probabilistic_data_expression> mcrl2::lts::stochastic_lts_lts_builder::m_initial_state
protected

Definition at line 195 of file stochastic_lts_builder.h.

◆ m_lts

probabilistic_lts_lts_t mcrl2::lts::stochastic_lts_lts_builder::m_lts
protected

Definition at line 193 of file stochastic_lts_builder.h.

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