mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::detail::action_detector< Explorer > Class Template Reference

#include <state_space_generator.h>

Public Member Functions

template<typename Specification >
 action_detector (const Specification &lpsspec, trace_constructor< Explorer > &trace_constructor_, const std::set< core::identifier_string > &trace_actions_, const std::set< lps::multi_action > &trace_multiactions_, const std::string &filename_prefix_, std::size_t max_trace_count)
 
bool detect_action (const lps::state &s0, std::size_t s0_index, const lps::multi_action &a, const lps::state &s1, std::size_t summand_index)
 

Protected Member Functions

bool match_action (const lps::action_summand &summand) const
 
bool match_summand (std::size_t i) const
 
std::string create_filename (const lps::multi_action &a)
 

Protected Attributes

const std::set< core::identifier_string > & trace_actions
 
const std::set< lps::multi_action > & trace_multiactions
 
trace_constructor< Explorer > & m_trace_constructor
 
const std::string & filename_prefix
 
std::vector< bool > summand_matches
 
std::size_t m_trace_count = 0
 
std::size_t m_max_trace_count
 

Detailed Description

template<typename Explorer>
class mcrl2::lts::detail::action_detector< Explorer >

Definition at line 171 of file state_space_generator.h.

Constructor & Destructor Documentation

◆ action_detector()

template<typename Explorer >
template<typename Specification >
mcrl2::lts::detail::action_detector< Explorer >::action_detector ( const Specification &  lpsspec,
trace_constructor< Explorer > &  trace_constructor_,
const std::set< core::identifier_string > &  trace_actions_,
const std::set< lps::multi_action > &  trace_multiactions_,
const std::string &  filename_prefix_,
std::size_t  max_trace_count 
)
inline

Definition at line 221 of file state_space_generator.h.

Member Function Documentation

◆ create_filename()

template<typename Explorer >
std::string mcrl2::lts::detail::action_detector< Explorer >::create_filename ( const lps::multi_action a)
inlineprotected

Definition at line 200 of file state_space_generator.h.

◆ detect_action()

template<typename Explorer >
bool mcrl2::lts::detail::action_detector< Explorer >::detect_action ( const lps::state s0,
std::size_t  s0_index,
const lps::multi_action a,
const lps::state s1,
std::size_t  summand_index 
)
inline

Definition at line 244 of file state_space_generator.h.

◆ match_action()

template<typename Explorer >
bool mcrl2::lts::detail::action_detector< Explorer >::match_action ( const lps::action_summand summand) const
inlineprotected

Definition at line 182 of file state_space_generator.h.

◆ match_summand()

template<typename Explorer >
bool mcrl2::lts::detail::action_detector< Explorer >::match_summand ( std::size_t  i) const
inlineprotected

Definition at line 195 of file state_space_generator.h.

Member Data Documentation

◆ filename_prefix

template<typename Explorer >
const std::string& mcrl2::lts::detail::action_detector< Explorer >::filename_prefix
protected

Definition at line 177 of file state_space_generator.h.

◆ m_max_trace_count

template<typename Explorer >
std::size_t mcrl2::lts::detail::action_detector< Explorer >::m_max_trace_count
protected

Definition at line 180 of file state_space_generator.h.

◆ m_trace_constructor

template<typename Explorer >
trace_constructor<Explorer>& mcrl2::lts::detail::action_detector< Explorer >::m_trace_constructor
protected

Definition at line 176 of file state_space_generator.h.

◆ m_trace_count

template<typename Explorer >
std::size_t mcrl2::lts::detail::action_detector< Explorer >::m_trace_count = 0
protected

Definition at line 179 of file state_space_generator.h.

◆ summand_matches

template<typename Explorer >
std::vector<bool> mcrl2::lts::detail::action_detector< Explorer >::summand_matches
protected

Definition at line 178 of file state_space_generator.h.

◆ trace_actions

template<typename Explorer >
const std::set<core::identifier_string>& mcrl2::lts::detail::action_detector< Explorer >::trace_actions
protected

Definition at line 174 of file state_space_generator.h.

◆ trace_multiactions

template<typename Explorer >
const std::set<lps::multi_action>& mcrl2::lts::detail::action_detector< Explorer >::trace_multiactions
protected

Definition at line 175 of file state_space_generator.h.


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