mcrl2::lts::detail::divergence_detector

Include file:

#include "mcrl2/lts/state_space_generator-cpp17.h
class mcrl2::lts::detail::divergence_detector

Public types

type last_discovered_type

typedef for typename std::conditional< Explorer::is_stochastic, std::forward_list< lps::state >, lps::state >::type

type state_index_type

typedef for typename Explorer::state_index_type

type state_type

typedef for typename Explorer::state_type

Protected attributes

lps::explorer &explorer
Explorer &explorer
const std::string &filename_prefix
std::vector<lps::explorer_summand> m_confluent_summands
std::unordered_map<lps::state, std::size_t> m_divergent_states
trace_constructor m_local_trace_constructor
trace_constructor<Explorer> m_local_trace_constructor
std::size_t m_max_trace_count
std::vector<lps::explorer_summand> m_regular_summands
bool m_timed
std::size_t m_trace_count

Public member functions

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