mcrl2::lts::state_space_generator< Stochastic, Timed, Specification > Struct Template Reference

#include <state_space_generator.h>

Classes
struct	aligned_bool

Public Types
using	explorer_type = lps::explorer< Stochastic, Timed, Specification >
using	state_type = typename explorer_type::state_type

Public Member Functions
	state_space_generator (const Specification &lpsspec, const lps::explorer_options &options_)
bool	max_states_exceeded (const std::size_t thread_index)
template<typename LTSBuilder >
bool	explore (LTSBuilder &builder)

Public Attributes
const lps::explorer_options &	options
lps::explorer< Stochastic, Timed, Specification >	explorer
detail::trace_constructor< explorer_type >	m_trace_constructor
detail::action_detector< explorer_type >	m_action_detector
detail::deadlock_detector< explorer_type >	m_deadlock_detector
detail::nondeterminism_detector< explorer_type >	m_nondeterminism_detector
std::unique_ptr< detail::divergence_detector< explorer_type > >	m_divergence_detector
detail::progress_monitor	m_progress_monitor

Detailed Description

template<bool Stochastic, bool Timed, typename Specification>
struct mcrl2::lts::state_space_generator< Stochastic, Timed, Specification >

Definition at line 650 of file state_space_generator.h.

Member Typedef Documentation

explorer_type

template<bool Stochastic, bool Timed, typename Specification >

using mcrl2::lts::state_space_generator< Stochastic, Timed, Specification >::explorer_type = lps::explorer<Stochastic, Timed, Specification>

Definition at line 652 of file state_space_generator.h.

state_type

template<bool Stochastic, bool Timed, typename Specification >

using mcrl2::lts::state_space_generator< Stochastic, Timed, Specification >::state_type = typename explorer_type::state_type

Definition at line 653 of file state_space_generator.h.

Constructor & Destructor Documentation

state_space_generator()

template<bool Stochastic, bool Timed, typename Specification >

mcrl2::lts::state_space_generator< Stochastic, Timed, Specification >::state_space_generator ( const Specification &  lpsspec, const lps::explorer_options &  options_  )

inline

Definition at line 665 of file state_space_generator.h.

Member Function Documentation

explore()

template<bool Stochastic, bool Timed, typename Specification >

template<typename LTSBuilder >

bool mcrl2::lts::state_space_generator< Stochastic, Timed, Specification >::explore ( LTSBuilder &  builder )

inline

Definition at line 697 of file state_space_generator.h.

max_states_exceeded()

template<bool Stochastic, bool Timed, typename Specification >

bool mcrl2::lts::state_space_generator< Stochastic, Timed, Specification >::max_states_exceeded ( const std::size_t  thread_index )

inline

Definition at line 685 of file state_space_generator.h.

Member Data Documentation

explorer

template<bool Stochastic, bool Timed, typename Specification >

lps::explorer<Stochastic, Timed, Specification> mcrl2::lts::state_space_generator< Stochastic, Timed, Specification >::explorer

Definition at line 656 of file state_space_generator.h.

m_action_detector

template<bool Stochastic, bool Timed, typename Specification >

detail::action_detector<explorer_type> mcrl2::lts::state_space_generator< Stochastic, Timed, Specification >::m_action_detector

Definition at line 659 of file state_space_generator.h.

m_deadlock_detector

template<bool Stochastic, bool Timed, typename Specification >

detail::deadlock_detector<explorer_type> mcrl2::lts::state_space_generator< Stochastic, Timed, Specification >::m_deadlock_detector

Definition at line 660 of file state_space_generator.h.

m_divergence_detector

template<bool Stochastic, bool Timed, typename Specification >

std::unique_ptr<detail::divergence_detector<explorer_type> > mcrl2::lts::state_space_generator< Stochastic, Timed, Specification >::m_divergence_detector

Definition at line 662 of file state_space_generator.h.

m_nondeterminism_detector

template<bool Stochastic, bool Timed, typename Specification >

detail::nondeterminism_detector<explorer_type> mcrl2::lts::state_space_generator< Stochastic, Timed, Specification >::m_nondeterminism_detector

Definition at line 661 of file state_space_generator.h.

m_progress_monitor

template<bool Stochastic, bool Timed, typename Specification >

detail::progress_monitor mcrl2::lts::state_space_generator< Stochastic, Timed, Specification >::m_progress_monitor

Definition at line 663 of file state_space_generator.h.

m_trace_constructor

template<bool Stochastic, bool Timed, typename Specification >

detail::trace_constructor<explorer_type> mcrl2::lts::state_space_generator< Stochastic, Timed, Specification >::m_trace_constructor

Definition at line 657 of file state_space_generator.h.

options

template<bool Stochastic, bool Timed, typename Specification >

const lps::explorer_options& mcrl2::lts::state_space_generator< Stochastic, Timed, Specification >::options

Definition at line 655 of file state_space_generator.h.

---

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

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