mcrl2::lts::detail::nondeterminism_detector< Explorer > Class Template Reference

#include <state_space_generator.h>

Public Member Functions
	nondeterminism_detector (trace_constructor< Explorer > &trace_constructor_, const std::string &filename_prefix_, const std::size_t number_of_threads, std::size_t max_trace_count=0)
void	start_state (std::size_t thread_index)
bool	detect_nondeterminism (const lps::state &s0, std::size_t s0_index, const lps::multi_action &a, const lps::state &s1, std::size_t thread_index)

Protected Attributes
trace_constructor< Explorer > &	m_trace_constructor
const std::string &	filename_prefix
std::vector< std::map< lps::multi_action, lps::state > >	m_transitions_vec
std::size_t	m_trace_count = 0
std::size_t	m_max_trace_count

Detailed Description

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

Definition at line 310 of file state_space_generator.h.

Constructor & Destructor Documentation

nondeterminism_detector()

template<typename Explorer >

mcrl2::lts::detail::nondeterminism_detector< Explorer >::nondeterminism_detector ( trace_constructor< Explorer > &  trace_constructor_, const std::string &  filename_prefix_, const std::size_t  number_of_threads, std::size_t  max_trace_count = 0  )

inline

Definition at line 320 of file state_space_generator.h.

Member Function Documentation

detect_nondeterminism()

template<typename Explorer >

bool mcrl2::lts::detail::nondeterminism_detector< Explorer >::detect_nondeterminism ( const lps::state &  s0, std::size_t  s0_index, const lps::multi_action &  a, const lps::state &  s1, std::size_t  thread_index  )

inline

Definition at line 340 of file state_space_generator.h.

start_state()

template<typename Explorer >

void mcrl2::lts::detail::nondeterminism_detector< Explorer >::start_state ( std::size_t  thread_index )

inline

Definition at line 334 of file state_space_generator.h.

Member Data Documentation

filename_prefix

template<typename Explorer >

const std::string& mcrl2::lts::detail::nondeterminism_detector< Explorer >::filename_prefix

protected

Definition at line 314 of file state_space_generator.h.

m_max_trace_count

template<typename Explorer >

std::size_t mcrl2::lts::detail::nondeterminism_detector< Explorer >::m_max_trace_count

protected

Definition at line 317 of file state_space_generator.h.

m_trace_constructor

template<typename Explorer >

trace_constructor<Explorer>& mcrl2::lts::detail::nondeterminism_detector< Explorer >::m_trace_constructor

protected

Definition at line 313 of file state_space_generator.h.

m_trace_count

template<typename Explorer >

std::size_t mcrl2::lts::detail::nondeterminism_detector< Explorer >::m_trace_count = 0

protected

Definition at line 316 of file state_space_generator.h.

m_transitions_vec

template<typename Explorer >

std::vector<std::map<lps::multi_action, lps::state> > mcrl2::lts::detail::nondeterminism_detector< Explorer >::m_transitions_vec

protected

Definition at line 315 of file state_space_generator.h.

---

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

• lts/include/mcrl2/lts/state_space_generator.h