mCRL2
Loading...
Searching...
No Matches
mcrl2::lps::explorer< Stochastic, Timed, Specification > Member List

This is the complete list of members for mcrl2::lps::explorer< Stochastic, Timed, Specification >, including all inherited members.

abort() overridemcrl2::lps::explorer< Stochastic, Timed, Specification >inlinevirtual
add_real_operators(std::set< data::function_symbol > s) constmcrl2::lps::explorer< Stochastic, Timed, Specification >inlineprotected
check_enumerator_solution(const data::data_expression &p_expression, const explorer_summand &summand, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr) constmcrl2::lps::explorer< Stochastic, Timed, Specification >inlineprotected
compute_state(state &result, const DataExpressionSequence &v, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr) constmcrl2::lps::explorer< Stochastic, Timed, Specification >inlineprotected
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) constmcrl2::lps::explorer< Stochastic, Timed, Specification >inlineprotected
confluent_summands() constmcrl2::lps::explorer< Stochastic, Timed, Specification >inline
construct_rewriter(const Specification &lpsspec, bool remove_unused_rewrite_rules)mcrl2::lps::explorer< Stochastic, Timed, Specification >inlineprotected
enumerator_element typedefmcrl2::lps::explorer< Stochastic, Timed, Specification >protected
explorer(const Specification &lpsspec, const explorer_options &options_)mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
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)mcrl2::lps::explorer< Stochastic, Timed, Specification >inlineprotected
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())mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
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())mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
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())mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
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())mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
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())mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
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())mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
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)mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
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())mcrl2::lps::explorer< Stochastic, Timed, Specification >inlineprotected
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())mcrl2::lps::explorer< Stochastic, Timed, Specification >inlineprotected
generate_transitions(const state &d0, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::enumerator_algorithm<> &enumerator, data::enumerator_identifier_generator &id_generator)mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
generate_transitions(const state &d0)mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
generate_transitions(const data::data_expression_list &init, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr)mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
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)mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
get_rewriter() constmcrl2::lps::explorer< Stochastic, Timed, Specification >inline
global_cachemcrl2::lps::explorer< Stochastic, Timed, Specification >protected
indexed_set_for_states_type typedefmcrl2::lps::explorer< Stochastic, Timed, Specification >
initial_state() constmcrl2::lps::explorer< Stochastic, Timed, Specification >inline
is_confluent_tau(const multi_action &a)mcrl2::lps::explorer< Stochastic, Timed, Specification >inlineprotected
is_stochasticmcrl2::lps::explorer< Stochastic, Timed, Specification >static
is_timedmcrl2::lps::explorer< Stochastic, Timed, Specification >static
less_equal(const data::data_expression &t0, const data::data_expression &t1, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr) constmcrl2::lps::explorer< Stochastic, Timed, Specification >inlineprotected
m_confluent_summandsmcrl2::lps::explorer< Stochastic, Timed, Specification >protected
m_discoveredmcrl2::lps::explorer< Stochastic, Timed, Specification >protected
m_exclusive_state_accessmcrl2::lps::explorer< Stochastic, Timed, Specification >protected
m_global_enumeratormcrl2::lps::explorer< Stochastic, Timed, Specification >protected
m_global_id_generatormcrl2::lps::explorer< Stochastic, Timed, Specification >protected
m_global_lpsspecmcrl2::lps::explorer< Stochastic, Timed, Specification >protected
m_global_rewrmcrl2::lps::explorer< Stochastic, Timed, Specification >protected
m_global_sigmamcrl2::lps::explorer< Stochastic, Timed, Specification >mutableprotected
m_initial_distributionmcrl2::lps::explorer< Stochastic, Timed, Specification >protected
m_initial_statemcrl2::lps::explorer< Stochastic, Timed, Specification >protected
m_must_abortmcrl2::lps::explorer< Stochastic, Timed, Specification >protected
m_nmcrl2::lps::explorer< Stochastic, Timed, Specification >protected
m_optionsmcrl2::lps::explorer< Stochastic, Timed, Specification >protected
m_process_parametersmcrl2::lps::explorer< Stochastic, Timed, Specification >protected
m_recursivemcrl2::lps::explorer< Stochastic, Timed, Specification >protected
m_regular_summandsmcrl2::lps::explorer< Stochastic, Timed, Specification >protected
make_state(const state &s) constmcrl2::lps::explorer< Stochastic, Timed, Specification >inline
make_state(const stochastic_state &s) constmcrl2::lps::explorer< Stochastic, Timed, Specification >inline
make_timed_state(state &result, const state &s, const data::data_expression &t) constmcrl2::lps::explorer< Stochastic, Timed, Specification >inline
make_todo_set(const state &init)mcrl2::lps::explorer< Stochastic, Timed, Specification >inlineprotected
make_todo_set(ForwardIterator first, ForwardIterator last)mcrl2::lps::explorer< Stochastic, Timed, Specification >inlineprotected
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)mcrl2::lps::explorer< Stochastic, Timed, Specification >inlineprotected
out_edges(const state &s)mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
out_edges(const state &s, const std::size_t summand_index)mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
preprocess(const Specification &lpsspec)mcrl2::lps::explorer< Stochastic, Timed, Specification >inlineprotected
process_parameter_values(data::mutable_indexed_substitution<> &sigma) constmcrl2::lps::explorer< Stochastic, Timed, Specification >inline
process_parameter_values() constmcrl2::lps::explorer< Stochastic, Timed, Specification >inline
process_parameters() constmcrl2::lps::explorer< Stochastic, Timed, Specification >inline
regular_summands() constmcrl2::lps::explorer< Stochastic, Timed, Specification >inline
rewrite_action(const lps::multi_action &a, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr) constmcrl2::lps::explorer< Stochastic, Timed, Specification >inlineprotected
set_process_parameter_values(const data::data_expression_list &values, data::mutable_indexed_substitution<> &sigma)mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
set_process_parameter_values(const data::data_expression_list &values)mcrl2::lps::explorer< Stochastic, Timed, Specification >inline
state_index_type typedefmcrl2::lps::explorer< Stochastic, Timed, Specification >
state_map() constmcrl2::lps::explorer< Stochastic, Timed, Specification >inline
state_type typedefmcrl2::lps::explorer< Stochastic, Timed, Specification >
timed_statemcrl2::lps::explorer< Stochastic, Timed, Specification >mutableprotected
~explorer()=defaultmcrl2::lps::explorer< Stochastic, Timed, Specification >