mCRL2
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Protected Attributes | List of all members
mcrl2::lts::detail::divergence_detector< Explorer > Class Template Reference

#include <state_space_generator.h>

Public Types

using state_type = typename Explorer::state_type
 
using state_index_type = typename Explorer::state_index_type
 
using last_discovered_type = std::conditional_t< Explorer::is_stochastic, std::forward_list< lps::state >, lps::state >
 

Public Member Functions

 divergence_detector (Explorer &explorer_, const std::set< core::identifier_string > &actions, const std::string &filename_prefix_, std::size_t max_trace_count)
 
bool detect_divergence (const lps::state &s, std::size_t s_index, trace_constructor< Explorer > &global_trace_constructor, bool dfs_recursive=false)
 

Protected Attributes

Explorer & explorer
 
const std::string & filename_prefix
 
trace_constructor< Explorer > m_local_trace_constructor
 
utilities::unordered_map< lps::state, std::size_t > m_divergent_states
 
std::vector< lps::explorer_summand > m_regular_summands
 
std::vector< lps::explorer_summand > m_confluent_summands
 
std::size_t m_trace_count = 0
 
std::size_t m_max_trace_count
 
std::mutex divergence_detector_mutex
 

Detailed Description

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

Definition at line 374 of file state_space_generator.h.

Member Typedef Documentation

◆ last_discovered_type

template<typename Explorer >
using mcrl2::lts::detail::divergence_detector< Explorer >::last_discovered_type = std::conditional_t<Explorer::is_stochastic, std::forward_list<lps::state>, lps::state>

Definition at line 381 of file state_space_generator.h.

◆ state_index_type

template<typename Explorer >
using mcrl2::lts::detail::divergence_detector< Explorer >::state_index_type = typename Explorer::state_index_type

Definition at line 378 of file state_space_generator.h.

◆ state_type

template<typename Explorer >
using mcrl2::lts::detail::divergence_detector< Explorer >::state_type = typename Explorer::state_type

Definition at line 377 of file state_space_generator.h.

Constructor & Destructor Documentation

◆ divergence_detector()

template<typename Explorer >
mcrl2::lts::detail::divergence_detector< Explorer >::divergence_detector ( Explorer &  explorer_,
const std::set< core::identifier_string > &  actions,
const std::string &  filename_prefix_,
std::size_t  max_trace_count 
)
inline

Definition at line 395 of file state_space_generator.h.

Member Function Documentation

◆ detect_divergence()

template<typename Explorer >
bool mcrl2::lts::detail::divergence_detector< Explorer >::detect_divergence ( const lps::state &  s,
std::size_t  s_index,
trace_constructor< Explorer > &  global_trace_constructor,
bool  dfs_recursive = false 
)
inline

Definition at line 438 of file state_space_generator.h.

Member Data Documentation

◆ divergence_detector_mutex

template<typename Explorer >
std::mutex mcrl2::lts::detail::divergence_detector< Explorer >::divergence_detector_mutex
protected

Definition at line 392 of file state_space_generator.h.

◆ explorer

template<typename Explorer >
Explorer& mcrl2::lts::detail::divergence_detector< Explorer >::explorer
protected

Definition at line 384 of file state_space_generator.h.

◆ filename_prefix

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

Definition at line 385 of file state_space_generator.h.

◆ m_confluent_summands

template<typename Explorer >
std::vector<lps::explorer_summand> mcrl2::lts::detail::divergence_detector< Explorer >::m_confluent_summands
protected

Definition at line 389 of file state_space_generator.h.

◆ m_divergent_states

template<typename Explorer >
utilities::unordered_map<lps::state, std::size_t> mcrl2::lts::detail::divergence_detector< Explorer >::m_divergent_states
protected

Definition at line 387 of file state_space_generator.h.

◆ m_local_trace_constructor

template<typename Explorer >
trace_constructor<Explorer> mcrl2::lts::detail::divergence_detector< Explorer >::m_local_trace_constructor
protected

Definition at line 386 of file state_space_generator.h.

◆ m_max_trace_count

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

Definition at line 391 of file state_space_generator.h.

◆ m_regular_summands

template<typename Explorer >
std::vector<lps::explorer_summand> mcrl2::lts::detail::divergence_detector< Explorer >::m_regular_summands
protected

Definition at line 388 of file state_space_generator.h.

◆ m_trace_count

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

Definition at line 390 of file state_space_generator.h.

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