mCRL2
Loading...
Searching...
No Matches
mcrl2::lps::explorer< Stochastic, Timed, Specification > Class Template Reference

#include <explorer.h>

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

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::GlobalThreadSafeindexed_set_for_states_type
 

Public Member Functions

 explorer (const Specification &lpsspec, const explorer_options &options_)
 
 ~explorer ()=default
 
const data::data_expression_listinitial_state () const
 
const data::rewriterget_rewriter () const
 
std::list< transitionout_edges (const state &s)
 
std::list< transitionout_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_typemake_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_typestate_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::term_appl< data::data_expression > &key, data::enumerator_algorithm<> &enumerator, data::enumerator_identifier_generator &id_generator, ReportTransition report_transition=ReportTransition())
 
template<typename SummandSequence >
std::list< transitionout_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< stategenerate_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_symboladd_real_operators (std::set< data::function_symbol > s) const
 
std::unique_ptr< todo_setmake_todo_set (const state &init)
 
template<typename ForwardIterator >
std::unique_ptr< todo_setmake_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::variablem_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_summandm_regular_summands
 
std::vector< explorer_summandm_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_expressiontimed_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_stateIs invoked when a state is encountered for the first time.
examine_transitionIs invoked on every transition.
start_stateIs invoked on a state right before its outgoing transitions are being explored.
finish_stateIs 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::term_appl< data::data_expression > &  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: