#include <explorer.h>

Inheritance diagram for mcrl2::lps::explorer< Stochastic, Timed, Specification >:

Classes
struct	transition

Public Types
using	state_type = typename std::conditional< Stochastic, stochastic_state, state >::type

using	state_index_type = typename std::conditional< Stochastic, std::list< std::size_t >, std::size_t >::type

typedef atermpp::indexed_set< state, mcrl2::utilities::detail::GlobalThreadSafe >	indexed_set_for_states_type

Public Member Functions
	explorer (const Specification &lpsspec, const explorer_options &options_)

	~explorer ()=default

const data::data_expression_list &	initial_state () const

const data::rewriter &	get_rewriter () const

std::list< transition >	out_edges (const state &s)

std::list< transition >	out_edges (const state &s, const std::size_t summand_index)

void	make_timed_state (state &result, const state &s, const data::data_expression &t) const

state_type	make_state (const state &s) const

const state_type &	make_state (const stochastic_state &s) const

template<typename StateType , typename SummandSequence , typename DiscoverState = utilities::skip, typename ExamineTransition = utilities::skip, typename StartState = utilities::skip, typename FinishState = utilities::skip, typename DiscoverInitialState = utilities::skip>
void	generate_state_space_thread (std::unique_ptr< todo_set > &todo, const std::size_t thread_index, std::atomic< std::size_t > &number_of_active_processes, std::atomic< std::size_t > &number_of_idle_processes, const SummandSequence &regular_summands, const SummandSequence &confluent_summands, indexed_set_for_states_type &discovered, DiscoverState discover_state, ExamineTransition examine_transition, StartState start_state, FinishState finish_state, data::rewriter thread_rewr, data::mutable_indexed_substitution<> thread_sigma)

template<typename StateType , typename SummandSequence , typename DiscoverState = utilities::skip, typename ExamineTransition = utilities::skip, typename StartState = utilities::skip, typename FinishState = utilities::skip, typename DiscoverInitialState = utilities::skip>
void	generate_state_space (bool recursive, const StateType &s0, const SummandSequence &regular_summands, const SummandSequence &confluent_summands, indexed_set_for_states_type &discovered, DiscoverState discover_state=DiscoverState(), ExamineTransition examine_transition=ExamineTransition(), StartState start_state=StartState(), FinishState finish_state=FinishState(), DiscoverInitialState discover_initial_state=DiscoverInitialState())

template<typename DiscoverState = utilities::skip, typename ExamineTransition = utilities::skip, typename StartState = utilities::skip, typename FinishState = utilities::skip, typename DiscoverInitialState = utilities::skip>
void	generate_state_space (bool recursive, DiscoverState discover_state=DiscoverState(), ExamineTransition examine_transition=ExamineTransition(), StartState start_state=StartState(), FinishState finish_state=FinishState(), DiscoverInitialState discover_initial_state=DiscoverInitialState())
	Generates the state space, and reports all discovered states and transitions by means of callback functions.

std::vector< std::pair< lps::multi_action, state_type > >	generate_transitions (const state &d0, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::enumerator_algorithm<> &enumerator, data::enumerator_identifier_generator &id_generator)
	Generates outgoing transitions for a given state.

std::vector< std::pair< lps::multi_action, state_type > >	generate_transitions (const state &d0)
	Generates outgoing transitions for a given state, using the global substitution, rewriter, enumerator and id_generator.

std::vector< std::pair< lps::multi_action, state > >	generate_transitions (const data::data_expression_list &init, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr)
	Generates outgoing transitions for a given state.

std::vector< std::pair< lps::multi_action, state_type > >	generate_transitions (const data::data_expression_list &init, std::size_t i, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::data_expression &condition, state_type &d0, data::enumerator_algorithm<> &enumerator, data::enumerator_identifier_generator &id_generator)
	Generates outgoing transitions for a given state, reachable via the summand with index i.

template<typename SummandSequence , typename DiscoverState = utilities::skip, typename ExamineTransition = utilities::skip, typename TreeEdge = utilities::skip, typename BackEdge = utilities::skip, typename ForwardOrCrossEdge = utilities::skip, typename FinishState = utilities::skip>
void	generate_state_space_dfs_recursive (const state &s0, std::unordered_set< state > gray, std::unordered_set< state > &discovered, const SummandSequence &regular_summands, const SummandSequence &confluent_summands, DiscoverState discover_state=DiscoverState(), ExamineTransition examine_transition=ExamineTransition(), TreeEdge tree_edge=TreeEdge(), BackEdge back_edge=BackEdge(), ForwardOrCrossEdge forward_or_cross_edge=ForwardOrCrossEdge(), FinishState finish_state=FinishState())

template<typename DiscoverState = utilities::skip, typename ExamineTransition = utilities::skip, typename TreeEdge = utilities::skip, typename BackEdge = utilities::skip, typename ForwardOrCrossEdge = utilities::skip, typename FinishState = utilities::skip>
void	generate_state_space_dfs_recursive (bool recursive, DiscoverState discover_state=DiscoverState(), ExamineTransition examine_transition=ExamineTransition(), TreeEdge tree_edge=TreeEdge(), BackEdge back_edge=BackEdge(), ForwardOrCrossEdge forward_or_cross_edge=ForwardOrCrossEdge(), FinishState finish_state=FinishState())

template<typename SummandSequence , typename DiscoverState = utilities::skip, typename ExamineTransition = utilities::skip, typename TreeEdge = utilities::skip, typename BackEdge = utilities::skip, typename ForwardOrCrossEdge = utilities::skip, typename FinishState = utilities::skip>
void	generate_state_space_dfs_iterative (const state &s0, std::unordered_set< state > &discovered, const SummandSequence &regular_summands, const SummandSequence &confluent_summands, DiscoverState discover_state=DiscoverState(), ExamineTransition examine_transition=ExamineTransition(), TreeEdge tree_edge=TreeEdge(), BackEdge back_edge=BackEdge(), ForwardOrCrossEdge forward_or_cross_edge=ForwardOrCrossEdge(), FinishState finish_state=FinishState())

template<typename DiscoverState = utilities::skip, typename ExamineTransition = utilities::skip, typename TreeEdge = utilities::skip, typename BackEdge = utilities::skip, typename ForwardOrCrossEdge = utilities::skip, typename FinishState = utilities::skip>
void	generate_state_space_dfs_iterative (bool recursive, DiscoverState discover_state=DiscoverState(), ExamineTransition examine_transition=ExamineTransition(), TreeEdge tree_edge=TreeEdge(), BackEdge back_edge=BackEdge(), ForwardOrCrossEdge forward_or_cross_edge=ForwardOrCrossEdge(), FinishState finish_state=FinishState())

void	abort () override
	Abort the state space generation.

const indexed_set_for_states_type &	state_map () const
	Returns a mapping containing all discovered states.

const std::vector< explorer_summand > &	regular_summands () const

const std::vector< explorer_summand > &	confluent_summands () const

const std::vector< data::variable > &	process_parameters () const

data::data_expression_list	process_parameter_values (data::mutable_indexed_substitution<> &sigma) const

data::data_expression_list	process_parameter_values () const
	Process parameter values for use in a single thread.

void	set_process_parameter_values (const data::data_expression_list &values, data::mutable_indexed_substitution<> &sigma)

void	set_process_parameter_values (const data::data_expression_list &values)

virtual void	abort ()=0

Static Public Attributes
static constexpr bool	is_stochastic = Stochastic

static constexpr bool	is_timed = Timed

Protected Types
using	enumerator_element = data::enumerator_list_element_with_substitution<>

Protected Member Functions
Specification	preprocess (const Specification &lpsspec)

bool	less_equal (const data::data_expression &t0, const data::data_expression &t1, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr) const

template<typename SummandSequence >
state	find_representative (state &u0, const SummandSequence &summands, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::enumerator_algorithm<> &enumerator, data::enumerator_identifier_generator &id_generator)

template<typename DataExpressionSequence >
void	compute_state (state &result, const DataExpressionSequence &v, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr) const

template<typename DataExpressionSequence >
void	compute_stochastic_state (stochastic_state &result, const stochastic_distribution &distribution, const DataExpressionSequence &next_state, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::enumerator_algorithm<> &enumerator) const

lps::multi_action	rewrite_action (const lps::multi_action &a, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr) const
	Rewrite action a, and put it back in place.

void	check_enumerator_solution (const data::data_expression &p_expression, const explorer_summand &summand, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr) const

template<typename SummandSequence , typename ReportTransition = utilities::skip>
void	generate_transitions (const explorer_summand &summand, const SummandSequence &confluent_summands, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::data_expression &condition, state_type &s1, atermpp::aterm key, data::enumerator_algorithm<> &enumerator, data::enumerator_identifier_generator &id_generator, ReportTransition report_transition=ReportTransition())

template<typename SummandSequence >
std::list< transition >	out_edges (const state &s, const SummandSequence &regular_summands, const SummandSequence &confluent_summands, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::enumerator_algorithm<> &enumerator, data::enumerator_identifier_generator &id_generator)

template<typename SummandSequence >
std::vector< state >	generate_successors (const state &s0, const SummandSequence &summands, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::enumerator_algorithm<> &enumerator, data::enumerator_identifier_generator &id_generator, const SummandSequence &confluent_summands=SummandSequence())

std::set< data::function_symbol >	add_real_operators (std::set< data::function_symbol > s) const

std::unique_ptr< todo_set >	make_todo_set (const state &init)

template<typename ForwardIterator >
std::unique_ptr< todo_set >	make_todo_set (ForwardIterator first, ForwardIterator last)

data::rewriter	construct_rewriter (const Specification &lpsspec, bool remove_unused_rewrite_rules)

bool	is_confluent_tau (const multi_action &a)

Protected Attributes
const explorer_options	m_options

data::mutable_indexed_substitution	m_global_sigma

data::rewriter	m_global_rewr

data::enumerator_algorithm	m_global_enumerator

data::enumerator_identifier_generator	m_global_id_generator

Specification	m_global_lpsspec

std::mutex	m_exclusive_state_access

std::vector< data::variable >	m_process_parameters

std::size_t	m_n

data::data_expression_list	m_initial_state

lps::stochastic_distribution	m_initial_distribution

bool	m_recursive = false

std::vector< explorer_summand >	m_regular_summands

std::vector< explorer_summand >	m_confluent_summands

volatile std::atomic< bool >	m_must_abort = false

summand_cache_map	global_cache

indexed_set_for_states_type	m_discovered

std::vector< data::data_expression >	timed_state

Detailed Description

template<bool Stochastic, bool Timed, typename Specification>
class mcrl2::lps::explorer< Stochastic, Timed, Specification >

Definition at line 447 of file explorer.h.

Member Typedef Documentation

◆ enumerator_element

template<bool Stochastic, bool Timed, typename Specification >

using mcrl2::lps::explorer< Stochastic, Timed, Specification >::enumerator_element = data::enumerator_list_element_with_substitution<>

protected

Definition at line 469 of file explorer.h.

◆ indexed_set_for_states_type

template<bool Stochastic, bool Timed, typename Specification >

typedef atermpp::indexed_set<state, mcrl2::utilities::detail::GlobalThreadSafe> mcrl2::lps::explorer< Stochastic, Timed, Specification >::indexed_set_for_states_type

Definition at line 455 of file explorer.h.

◆ state_index_type

template<bool Stochastic, bool Timed, typename Specification >

using mcrl2::lps::explorer< Stochastic, Timed, Specification >::state_index_type = typename std::conditional<Stochastic, std::list<std::size_t>, std::size_t>::type

Definition at line 451 of file explorer.h.

◆ state_type

template<bool Stochastic, bool Timed, typename Specification >

using mcrl2::lps::explorer< Stochastic, Timed, Specification >::state_type = typename std::conditional<Stochastic, stochastic_state, state>::type

Definition at line 450 of file explorer.h.

Constructor & Destructor Documentation

◆ explorer()

template<bool Stochastic, bool Timed, typename Specification >

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

inline

Definition at line 988 of file explorer.h.

◆ ~explorer()

template<bool Stochastic, bool Timed, typename Specification >

mcrl2::lps::explorer< Stochastic, Timed, Specification >::~explorer ( )

default

Member Function Documentation

◆ abort()

template<bool Stochastic, bool Timed, typename Specification >

void mcrl2::lps::explorer< Stochastic, Timed, Specification >::abort ( )

inlineoverridevirtual

Abort the state space generation.

Implements mcrl2::lps::abortable.

Definition at line 1742 of file explorer.h.

◆ add_real_operators()

template<bool Stochastic, bool Timed, typename Specification >

std::set< data::function_symbol > mcrl2::lps::explorer< Stochastic, Timed, Specification >::add_real_operators ( std::set< data::function_symbol > s ) const

inlineprotected

Definition at line 928 of file explorer.h.

◆ check_enumerator_solution()

template<bool Stochastic, bool Timed, typename Specification >

void mcrl2::lps::explorer< Stochastic, Timed, Specification >::check_enumerator_solution	(	const data::data_expression &	p_expression,
		const explorer_summand &	summand,
		data::mutable_indexed_substitution<> &	sigma,
		data::rewriter &	rewr
	)		const

inlineprotected

Definition at line 625 of file explorer.h.

◆ compute_state()

template<bool Stochastic, bool Timed, typename Specification >

template<typename DataExpressionSequence >

void mcrl2::lps::explorer< Stochastic, Timed, Specification >::compute_state	(	state &	result,
		const DataExpressionSequence &	v,
		data::mutable_indexed_substitution<> &	sigma,
		data::rewriter &	rewr
	)		const

inlineprotected

Definition at line 547 of file explorer.h.

◆ compute_stochastic_state()

template<bool Stochastic, bool Timed, typename Specification >

template<typename DataExpressionSequence >

void mcrl2::lps::explorer< Stochastic, Timed, Specification >::compute_stochastic_state	(	stochastic_state &	result,
		const stochastic_distribution &	distribution,
		const DataExpressionSequence &	next_state,
		data::mutable_indexed_substitution<> &	sigma,
		data::rewriter &	rewr,
		data::enumerator_algorithm<> &	enumerator
	)		const

inlineprotected

Definition at line 559 of file explorer.h.

◆ confluent_summands()

template<bool Stochastic, bool Timed, typename Specification >

const std::vector< explorer_summand > & mcrl2::lps::explorer< Stochastic, Timed, Specification >::confluent_summands ( ) const

inline

Definition at line 1758 of file explorer.h.

◆ construct_rewriter()

template<bool Stochastic, bool Timed, typename Specification >

data::rewriter mcrl2::lps::explorer< Stochastic, Timed, Specification >::construct_rewriter	(	const Specification &	lpsspec,
		bool	remove_unused_rewrite_rules
	)

inlineprotected

Definition at line 960 of file explorer.h.

◆ find_representative()

template<bool Stochastic, bool Timed, typename Specification >

template<typename SummandSequence >

state mcrl2::lps::explorer< Stochastic, Timed, Specification >::find_representative	(	state &	u0,
		const SummandSequence &	summands,
		data::mutable_indexed_substitution<> &	sigma,
		data::rewriter &	rewr,
		data::enumerator_algorithm<> &	enumerator,
		data::enumerator_identifier_generator &	id_generator
	)

inlineprotected

Definition at line 528 of file explorer.h.

◆ generate_state_space() [1/2]

template<bool Stochastic, bool Timed, typename Specification >

template<typename StateType , typename SummandSequence , typename DiscoverState = utilities::skip, typename ExamineTransition = utilities::skip, typename StartState = utilities::skip, typename FinishState = utilities::skip, typename DiscoverInitialState = utilities::skip>

void mcrl2::lps::explorer< Stochastic, Timed, Specification >::generate_state_space	(	bool	recursive,
		const StateType &	s0,
		const SummandSequence &	regular_summands,
		const SummandSequence &	confluent_summands,
		indexed_set_for_states_type &	discovered,
		DiscoverState	discover_state = `DiscoverState()`,
		ExamineTransition	examine_transition = `ExamineTransition()`,
		StartState	start_state = `StartState()`,
		FinishState	finish_state = `FinishState()`,
		DiscoverInitialState	discover_initial_state = `DiscoverInitialState()`
	)

inline

Definition at line 1267 of file explorer.h.

◆ generate_state_space() [2/2]

template<bool Stochastic, bool Timed, typename Specification >

template<typename DiscoverState = utilities::skip, typename ExamineTransition = utilities::skip, typename StartState = utilities::skip, typename FinishState = utilities::skip, typename DiscoverInitialState = utilities::skip>

void mcrl2::lps::explorer< Stochastic, Timed, Specification >::generate_state_space	(	bool	recursive,
		DiscoverState	discover_state = `DiscoverState()`,
		ExamineTransition	examine_transition = `ExamineTransition()`,
		StartState	start_state = `StartState()`,
		FinishState	finish_state = `FinishState()`,
		DiscoverInitialState	discover_initial_state = `DiscoverInitialState()`
	)

inline

Generates the state space, and reports all discovered states and transitions by means of callback functions.

Parameters

discover_state	Is invoked when a state is encountered for the first time.
examine_transition	Is invoked on every transition.
start_state	Is invoked on a state right before its outgoing transitions are being explored.
finish_state	Is invoked on a state after all of its outgoing transitions have been explored.

Definition at line 1375 of file explorer.h.

◆ generate_state_space_dfs_iterative() [1/2]

template<bool Stochastic, bool Timed, typename Specification >

template<typename DiscoverState = utilities::skip, typename ExamineTransition = utilities::skip, typename TreeEdge = utilities::skip, typename BackEdge = utilities::skip, typename ForwardOrCrossEdge = utilities::skip, typename FinishState = utilities::skip>

void mcrl2::lps::explorer< Stochastic, Timed, Specification >::generate_state_space_dfs_iterative	(	bool	recursive,
		DiscoverState	discover_state = `DiscoverState()`,
		ExamineTransition	examine_transition = `ExamineTransition()`,
		TreeEdge	tree_edge = `TreeEdge()`,
		BackEdge	back_edge = `BackEdge()`,
		ForwardOrCrossEdge	forward_or_cross_edge = `ForwardOrCrossEdge()`,
		FinishState	finish_state = `FinishState()`
	)

inline

Definition at line 1714 of file explorer.h.

◆ generate_state_space_dfs_iterative() [2/2]

template<bool Stochastic, bool Timed, typename Specification >

template<typename SummandSequence , typename DiscoverState = utilities::skip, typename ExamineTransition = utilities::skip, typename TreeEdge = utilities::skip, typename BackEdge = utilities::skip, typename ForwardOrCrossEdge = utilities::skip, typename FinishState = utilities::skip>

void mcrl2::lps::explorer< Stochastic, Timed, Specification >::generate_state_space_dfs_iterative	(	const state &	s0,
		std::unordered_set< state > &	discovered,
		const SummandSequence &	regular_summands,
		const SummandSequence &	confluent_summands,
		DiscoverState	discover_state = `DiscoverState()`,
		ExamineTransition	examine_transition = `ExamineTransition()`,
		TreeEdge	tree_edge = `TreeEdge()`,
		BackEdge	back_edge = `BackEdge()`,
		ForwardOrCrossEdge	forward_or_cross_edge = `ForwardOrCrossEdge()`,
		FinishState	finish_state = `FinishState()`
	)

inline

Definition at line 1625 of file explorer.h.

◆ generate_state_space_dfs_recursive() [1/2]

template<bool Stochastic, bool Timed, typename Specification >

template<typename DiscoverState = utilities::skip, typename ExamineTransition = utilities::skip, typename TreeEdge = utilities::skip, typename BackEdge = utilities::skip, typename ForwardOrCrossEdge = utilities::skip, typename FinishState = utilities::skip>

void mcrl2::lps::explorer< Stochastic, Timed, Specification >::generate_state_space_dfs_recursive	(	bool	recursive,
		DiscoverState	discover_state = `DiscoverState()`,
		ExamineTransition	examine_transition = `ExamineTransition()`,
		TreeEdge	tree_edge = `TreeEdge()`,
		BackEdge	back_edge = `BackEdge()`,
		ForwardOrCrossEdge	forward_or_cross_edge = `ForwardOrCrossEdge()`,
		FinishState	finish_state = `FinishState()`
	)

inline

Definition at line 1586 of file explorer.h.

◆ generate_state_space_dfs_recursive() [2/2]

template<bool Stochastic, bool Timed, typename Specification >

template<typename SummandSequence , typename DiscoverState = utilities::skip, typename ExamineTransition = utilities::skip, typename TreeEdge = utilities::skip, typename BackEdge = utilities::skip, typename ForwardOrCrossEdge = utilities::skip, typename FinishState = utilities::skip>

void mcrl2::lps::explorer< Stochastic, Timed, Specification >::generate_state_space_dfs_recursive	(	const state &	s0,
		std::unordered_set< state >	gray,
		std::unordered_set< state > &	discovered,
		const SummandSequence &	regular_summands,
		const SummandSequence &	confluent_summands,
		DiscoverState	discover_state = `DiscoverState()`,
		ExamineTransition	examine_transition = `ExamineTransition()`,
		TreeEdge	tree_edge = `TreeEdge()`,
		BackEdge	back_edge = `BackEdge()`,
		ForwardOrCrossEdge	forward_or_cross_edge = `ForwardOrCrossEdge()`,
		FinishState	finish_state = `FinishState()`
	)

inline

Definition at line 1506 of file explorer.h.

◆ generate_state_space_thread()

template<bool Stochastic, bool Timed, typename Specification >

template<typename StateType , typename SummandSequence , typename DiscoverState = utilities::skip, typename ExamineTransition = utilities::skip, typename StartState = utilities::skip, typename FinishState = utilities::skip, typename DiscoverInitialState = utilities::skip>

void mcrl2::lps::explorer< Stochastic, Timed, Specification >::generate_state_space_thread	(	std::unique_ptr< todo_set > &	todo,
		const std::size_t	thread_index,
		std::atomic< std::size_t > &	number_of_active_processes,
		std::atomic< std::size_t > &	number_of_idle_processes,
		const SummandSequence &	regular_summands,
		const SummandSequence &	confluent_summands,
		indexed_set_for_states_type &	discovered,
		DiscoverState	discover_state,
		ExamineTransition	examine_transition,
		StartState	start_state,
		FinishState	finish_state,
		data::rewriter	thread_rewr,
		data::mutable_indexed_substitution<>	thread_sigma
	)

inline

XXXX Nodig??

Definition at line 1086 of file explorer.h.

◆ generate_successors()

template<bool Stochastic, bool Timed, typename Specification >

template<typename SummandSequence >

std::vector< state > mcrl2::lps::explorer< Stochastic, Timed, Specification >::generate_successors	(	const state &	s0,
		const SummandSequence &	summands,
		data::mutable_indexed_substitution<> &	sigma,
		data::rewriter &	rewr,
		data::enumerator_algorithm<> &	enumerator,
		data::enumerator_identifier_generator &	id_generator,
		const SummandSequence &	confluent_summands = `SummandSequence()`
	)

inlineprotected

Definition at line 889 of file explorer.h.

◆ generate_transitions() [1/5]

template<bool Stochastic, bool Timed, typename Specification >

std::vector< std::pair< lps::multi_action, state > > mcrl2::lps::explorer< Stochastic, Timed, Specification >::generate_transitions	(	const data::data_expression_list &	init,
		data::mutable_indexed_substitution<> &	sigma,
		data::rewriter &	rewr
	)

inline

Generates outgoing transitions for a given state.

Definition at line 1451 of file explorer.h.

◆ generate_transitions() [2/5]

template<bool Stochastic, bool Timed, typename Specification >

std::vector< std::pair< lps::multi_action, state_type > > mcrl2::lps::explorer< Stochastic, Timed, Specification >::generate_transitions	(	const data::data_expression_list &	init,
		std::size_t	i,
		data::mutable_indexed_substitution<> &	sigma,
		data::rewriter &	rewr,
		data::data_expression &	condition,
		state_type &	d0,
		data::enumerator_algorithm<> &	enumerator,
		data::enumerator_identifier_generator &	id_generator
	)

inline

Generates outgoing transitions for a given state, reachable via the summand with index i.

Definition at line 1462 of file explorer.h.

◆ generate_transitions() [3/5]

template<bool Stochastic, bool Timed, typename Specification >

template<typename SummandSequence , typename ReportTransition = utilities::skip>

void mcrl2::lps::explorer< Stochastic, Timed, Specification >::generate_transitions	(	const explorer_summand &	summand,
		const SummandSequence &	confluent_summands,
		data::mutable_indexed_substitution<> &	sigma,
		data::rewriter &	rewr,
		data::data_expression &	condition,
		state_type &	s1,
		atermpp::aterm	key,
		data::enumerator_algorithm<> &	enumerator,
		data::enumerator_identifier_generator &	id_generator,
		ReportTransition	report_transition = `ReportTransition()`
	)

inlineprotected

Definition at line 646 of file explorer.h.

◆ generate_transitions() [4/5]

template<bool Stochastic, bool Timed, typename Specification >

std::vector< std::pair< lps::multi_action, state_type > > mcrl2::lps::explorer< Stochastic, Timed, Specification >::generate_transitions ( const state & d0 )

inline

Generates outgoing transitions for a given state, using the global substitution, rewriter, enumerator and id_generator.

This function is not suitable to be used in parallel threads, but can only be used for pre or post processing.

Definition at line 1443 of file explorer.h.

◆ generate_transitions() [5/5]

template<bool Stochastic, bool Timed, typename Specification >

std::vector< std::pair< lps::multi_action, state_type > > mcrl2::lps::explorer< Stochastic, Timed, Specification >::generate_transitions	(	const state &	d0,
		data::mutable_indexed_substitution<> &	sigma,
		data::rewriter &	rewr,
		data::enumerator_algorithm<> &	enumerator,
		data::enumerator_identifier_generator &	id_generator
	)

inline

Generates outgoing transitions for a given state.

Definition at line 1406 of file explorer.h.

◆ get_rewriter()

template<bool Stochastic, bool Timed, typename Specification >

const data::rewriter & mcrl2::lps::explorer< Stochastic, Timed, Specification >::get_rewriter ( ) const

inline

Definition at line 1028 of file explorer.h.

◆ initial_state()

template<bool Stochastic, bool Timed, typename Specification >

const data::data_expression_list & mcrl2::lps::explorer< Stochastic, Timed, Specification >::initial_state ( ) const

inline

Definition at line 1022 of file explorer.h.

◆ is_confluent_tau()

template<bool Stochastic, bool Timed, typename Specification >

bool mcrl2::lps::explorer< Stochastic, Timed, Specification >::is_confluent_tau ( const multi_action & a )

inlineprotected

Definition at line 974 of file explorer.h.

◆ less_equal()

template<bool Stochastic, bool Timed, typename Specification >

bool mcrl2::lps::explorer< Stochastic, Timed, Specification >::less_equal	(	const data::data_expression &	t0,
		const data::data_expression &	t1,
		data::mutable_indexed_substitution<> &	sigma,
		data::rewriter &	rewr
	)		const

inlineprotected

Definition at line 518 of file explorer.h.

◆ make_state() [1/2]

template<bool Stochastic, bool Timed, typename Specification >

state_type mcrl2::lps::explorer< Stochastic, Timed, Specification >::make_state ( const state & s ) const

inline

Definition at line 1060 of file explorer.h.

◆ make_state() [2/2]

template<bool Stochastic, bool Timed, typename Specification >

const state_type & mcrl2::lps::explorer< Stochastic, Timed, Specification >::make_state ( const stochastic_state & s ) const

inline

Definition at line 1072 of file explorer.h.

◆ make_timed_state()

template<bool Stochastic, bool Timed, typename Specification >

void mcrl2::lps::explorer< Stochastic, Timed, Specification >::make_timed_state	(	state &	result,
		const state &	s,
		const data::data_expression &	t
	)		const

inline

Definition at line 1053 of file explorer.h.

◆ make_todo_set() [1/2]

template<bool Stochastic, bool Timed, typename Specification >

std::unique_ptr< todo_set > mcrl2::lps::explorer< Stochastic, Timed, Specification >::make_todo_set ( const state & init )

inlineprotected

Definition at line 937 of file explorer.h.

◆ make_todo_set() [2/2]

template<bool Stochastic, bool Timed, typename Specification >

template<typename ForwardIterator >

std::unique_ptr< todo_set > mcrl2::lps::explorer< Stochastic, Timed, Specification >::make_todo_set	(	ForwardIterator	first,
		ForwardIterator	last
	)

inlineprotected

Definition at line 949 of file explorer.h.

◆ out_edges() [1/3]

template<bool Stochastic, bool Timed, typename Specification >

std::list< transition > mcrl2::lps::explorer< Stochastic, Timed, Specification >::out_edges ( const state & s )

inline

Definition at line 1035 of file explorer.h.

◆ out_edges() [2/3]

template<bool Stochastic, bool Timed, typename Specification >

std::list< transition > mcrl2::lps::explorer< Stochastic, Timed, Specification >::out_edges	(	const state &	s,
		const std::size_t	summand_index
	)

inline

Definition at line 1043 of file explorer.h.

◆ out_edges() [3/3]

template<bool Stochastic, bool Timed, typename Specification >

template<typename SummandSequence >

std::list< transition > mcrl2::lps::explorer< Stochastic, Timed, Specification >::out_edges	(	const state &	s,
		const SummandSequence &	regular_summands,
		const SummandSequence &	confluent_summands,
		data::mutable_indexed_substitution<> &	sigma,
		data::rewriter &	rewr,
		data::enumerator_algorithm<> &	enumerator,
		data::enumerator_identifier_generator &	id_generator
	)

inlineprotected

Definition at line 838 of file explorer.h.

◆ preprocess()

template<bool Stochastic, bool Timed, typename Specification >

Specification mcrl2::lps::explorer< Stochastic, Timed, Specification >::preprocess ( const Specification & lpsspec )

inlineprotected

Definition at line 500 of file explorer.h.

◆ process_parameter_values() [1/2]

template<bool Stochastic, bool Timed, typename Specification >

data::data_expression_list mcrl2::lps::explorer< Stochastic, Timed, Specification >::process_parameter_values ( ) const

inline

Process parameter values for use in a single thread.

Definition at line 1774 of file explorer.h.

◆ process_parameter_values() [2/2]

template<bool Stochastic, bool Timed, typename Specification >

data::data_expression_list mcrl2::lps::explorer< Stochastic, Timed, Specification >::process_parameter_values ( data::mutable_indexed_substitution<> & sigma ) const

inline

Definition at line 1768 of file explorer.h.

◆ process_parameters()

template<bool Stochastic, bool Timed, typename Specification >

const std::vector< data::variable > & mcrl2::lps::explorer< Stochastic, Timed, Specification >::process_parameters ( ) const

inline

Definition at line 1763 of file explorer.h.

◆ regular_summands()

template<bool Stochastic, bool Timed, typename Specification >

const std::vector< explorer_summand > & mcrl2::lps::explorer< Stochastic, Timed, Specification >::regular_summands ( ) const

inline

Definition at line 1753 of file explorer.h.

◆ rewrite_action()

template<bool Stochastic, bool Timed, typename Specification >

lps::multi_action mcrl2::lps::explorer< Stochastic, Timed, Specification >::rewrite_action	(	const lps::multi_action &	a,
		data::mutable_indexed_substitution<> &	sigma,
		data::rewriter &	rewr
	)		const

inlineprotected

Rewrite action a, and put it back in place.

Definition at line 598 of file explorer.h.

◆ set_process_parameter_values() [1/2]

template<bool Stochastic, bool Timed, typename Specification >

void mcrl2::lps::explorer< Stochastic, Timed, Specification >::set_process_parameter_values ( const data::data_expression_list & values )

inline

Definition at line 1784 of file explorer.h.

◆ set_process_parameter_values() [2/2]

template<bool Stochastic, bool Timed, typename Specification >

void mcrl2::lps::explorer< Stochastic, Timed, Specification >::set_process_parameter_values	(	const data::data_expression_list &	values,
		data::mutable_indexed_substitution<> &	sigma
	)

inline

Definition at line 1779 of file explorer.h.

◆ state_map()

template<bool Stochastic, bool Timed, typename Specification >

const indexed_set_for_states_type & mcrl2::lps::explorer< Stochastic, Timed, Specification >::state_map ( ) const

inline

Returns a mapping containing all discovered states.

Definition at line 1748 of file explorer.h.

Member Data Documentation

◆ global_cache

template<bool Stochastic, bool Timed, typename Specification >

summand_cache_map mcrl2::lps::explorer< Stochastic, Timed, Specification >::global_cache

protected

Definition at line 493 of file explorer.h.

◆ is_stochastic

template<bool Stochastic, bool Timed, typename Specification >

constexpr bool mcrl2::lps::explorer< Stochastic, Timed, Specification >::is_stochastic = Stochastic

staticconstexpr

Definition at line 452 of file explorer.h.

◆ is_timed

template<bool Stochastic, bool Timed, typename Specification >

constexpr bool mcrl2::lps::explorer< Stochastic, Timed, Specification >::is_timed = Timed

staticconstexpr

Definition at line 453 of file explorer.h.

◆ m_confluent_summands

template<bool Stochastic, bool Timed, typename Specification >

std::vector<explorer_summand> mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_confluent_summands

protected

Definition at line 488 of file explorer.h.

◆ m_discovered

template<bool Stochastic, bool Timed, typename Specification >

indexed_set_for_states_type mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_discovered

protected

Definition at line 495 of file explorer.h.

◆ m_exclusive_state_access

template<bool Stochastic, bool Timed, typename Specification >

std::mutex mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_exclusive_state_access

protected

Definition at line 480 of file explorer.h.

◆ m_global_enumerator

template<bool Stochastic, bool Timed, typename Specification >

data::enumerator_algorithm mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_global_enumerator

protected

Definition at line 475 of file explorer.h.

◆ m_global_id_generator

template<bool Stochastic, bool Timed, typename Specification >

data::enumerator_identifier_generator mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_global_id_generator

protected

Definition at line 476 of file explorer.h.

◆ m_global_lpsspec

template<bool Stochastic, bool Timed, typename Specification >

Specification mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_global_lpsspec

protected

Definition at line 478 of file explorer.h.

◆ m_global_rewr

template<bool Stochastic, bool Timed, typename Specification >

data::rewriter mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_global_rewr

protected

Definition at line 474 of file explorer.h.

◆ m_global_sigma

template<bool Stochastic, bool Timed, typename Specification >

data::mutable_indexed_substitution mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_global_sigma

mutableprotected

Definition at line 473 of file explorer.h.

◆ m_initial_distribution

template<bool Stochastic, bool Timed, typename Specification >

lps::stochastic_distribution mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_initial_distribution

protected

Definition at line 485 of file explorer.h.

◆ m_initial_state

template<bool Stochastic, bool Timed, typename Specification >

data::data_expression_list mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_initial_state

protected

Definition at line 484 of file explorer.h.

◆ m_must_abort

template<bool Stochastic, bool Timed, typename Specification >

volatile std::atomic<bool> mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_must_abort = false

protected

Definition at line 490 of file explorer.h.

◆ m_n

template<bool Stochastic, bool Timed, typename Specification >

std::size_t mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_n

protected

Definition at line 483 of file explorer.h.

◆ m_options

template<bool Stochastic, bool Timed, typename Specification >

const explorer_options mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_options

protected

Definition at line 470 of file explorer.h.

◆ m_process_parameters

template<bool Stochastic, bool Timed, typename Specification >

std::vector<data::variable> mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_process_parameters

protected

Definition at line 482 of file explorer.h.

◆ m_recursive

template<bool Stochastic, bool Timed, typename Specification >

bool mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_recursive = false

protected

Definition at line 486 of file explorer.h.

◆ m_regular_summands

template<bool Stochastic, bool Timed, typename Specification >

std::vector<explorer_summand> mcrl2::lps::explorer< Stochastic, Timed, Specification >::m_regular_summands

protected

Definition at line 487 of file explorer.h.

◆ timed_state

template<bool Stochastic, bool Timed, typename Specification >

std::vector<data::data_expression> mcrl2::lps::explorer< Stochastic, Timed, Specification >::timed_state

mutableprotected

Definition at line 498 of file explorer.h.

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

lps/include/mcrl2/lps/explorer.h

Classes

Public Types

Public Member Functions

Static Public Attributes

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ enumerator_element

◆ indexed_set_for_states_type

◆ state_index_type

◆ state_type

Constructor & Destructor Documentation

◆ explorer()

◆ ~explorer()

Member Function Documentation

◆ abort()

◆ add_real_operators()

◆ check_enumerator_solution()

◆ compute_state()

◆ compute_stochastic_state()

◆ confluent_summands()

◆ construct_rewriter()

◆ find_representative()

◆ generate_state_space() [1/2]

◆ generate_state_space() [2/2]

◆ generate_state_space_dfs_iterative() [1/2]

◆ generate_state_space_dfs_iterative() [2/2]

◆ generate_state_space_dfs_recursive() [1/2]

◆ generate_state_space_dfs_recursive() [2/2]

◆ generate_state_space_thread()

◆ generate_successors()

◆ generate_transitions() [1/5]

◆ generate_transitions() [2/5]

◆ generate_transitions() [3/5]

◆ generate_transitions() [4/5]

◆ generate_transitions() [5/5]

◆ get_rewriter()

◆ initial_state()

◆ is_confluent_tau()

◆ less_equal()

◆ make_state() [1/2]

◆ make_state() [2/2]

◆ make_timed_state()

◆ make_todo_set() [1/2]

◆ make_todo_set() [2/2]

◆ out_edges() [1/3]

◆ out_edges() [2/3]

◆ out_edges() [3/3]

◆ preprocess()

◆ process_parameter_values() [1/2]

◆ process_parameter_values() [2/2]

◆ process_parameters()

◆ regular_summands()

◆ rewrite_action()

◆ set_process_parameter_values() [1/2]

◆ set_process_parameter_values() [2/2]

◆ state_map()

Member Data Documentation

◆ global_cache

◆ is_stochastic

◆ is_timed

◆ m_confluent_summands

◆ m_discovered

◆ m_exclusive_state_access

◆ m_global_enumerator

◆ m_global_id_generator

◆ m_global_lpsspec

◆ m_global_rewr

◆ m_global_sigma

◆ m_initial_distribution

◆ m_initial_state

◆ m_must_abort

◆ m_n

◆ m_options

◆ m_process_parameters

◆ m_recursive

◆ m_regular_summands

◆ timed_state