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

std::mutex mcrl2::lts::detail::divergence_detector::divergence_detector_mutex

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)