mcrl2::lts::detail::divergence_detector

Include file:

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

Public types

type mcrl2::lts::detail::divergence_detector::last_discovered_type

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

type mcrl2::lts::detail::divergence_detector::state_index_type

typedef for typename Explorer::state_index_type

type mcrl2::lts::detail::divergence_detector::state_type

typedef for typename Explorer::state_type

Protected attributes

Explorer &mcrl2::lts::detail::divergence_detector::explorer
const std::string &mcrl2::lts::detail::divergence_detector::filename_prefix
std::vector<lps::explorer_summand> mcrl2::lts::detail::divergence_detector::m_confluent_summands
utilities::unordered_map<lps::state, std::size_t> mcrl2::lts::detail::divergence_detector::m_divergent_states
trace_constructor<Explorer> mcrl2::lts::detail::divergence_detector::m_local_trace_constructor
std::size_t mcrl2::lts::detail::divergence_detector::m_max_trace_count
std::vector<lps::explorer_summand> mcrl2::lts::detail::divergence_detector::m_regular_summands
std::size_t mcrl2::lts::detail::divergence_detector::m_trace_count

Public member functions

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