mCRL2
|
This is the complete list of members for mcrl2::lps::explorer< Stochastic, Timed, Specification >, including all inherited members.
abort() override | mcrl2::lps::explorer< Stochastic, Timed, Specification > | inlinevirtual |
add_real_operators(std::set< data::function_symbol > s) const | mcrl2::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) const | mcrl2::lps::explorer< Stochastic, Timed, Specification > | inlineprotected |
compute_state(state &result, const DataExpressionSequence &v, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr) const | mcrl2::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) const | mcrl2::lps::explorer< Stochastic, Timed, Specification > | inlineprotected |
confluent_summands() const | mcrl2::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 typedef | mcrl2::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 ®ular_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 ®ular_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 ®ular_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 ®ular_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() const | mcrl2::lps::explorer< Stochastic, Timed, Specification > | inline |
global_cache | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
indexed_set_for_states_type typedef | mcrl2::lps::explorer< Stochastic, Timed, Specification > | |
initial_state() const | mcrl2::lps::explorer< Stochastic, Timed, Specification > | inline |
is_confluent_tau(const multi_action &a) | mcrl2::lps::explorer< Stochastic, Timed, Specification > | inlineprotected |
is_stochastic | mcrl2::lps::explorer< Stochastic, Timed, Specification > | static |
is_timed | mcrl2::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) const | mcrl2::lps::explorer< Stochastic, Timed, Specification > | inlineprotected |
m_confluent_summands | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
m_discovered | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
m_exclusive_state_access | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
m_global_enumerator | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
m_global_id_generator | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
m_global_lpsspec | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
m_global_rewr | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
m_global_sigma | mcrl2::lps::explorer< Stochastic, Timed, Specification > | mutableprotected |
m_initial_distribution | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
m_initial_state | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
m_must_abort | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
m_n | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
m_options | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
m_process_parameters | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
m_recursive | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
m_regular_summands | mcrl2::lps::explorer< Stochastic, Timed, Specification > | protected |
make_state(const state &s) const | mcrl2::lps::explorer< Stochastic, Timed, Specification > | inline |
make_state(const stochastic_state &s) const | mcrl2::lps::explorer< Stochastic, Timed, Specification > | inline |
make_timed_state(state &result, const state &s, const data::data_expression &t) const | mcrl2::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 ®ular_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) const | mcrl2::lps::explorer< Stochastic, Timed, Specification > | inline |
process_parameter_values() const | mcrl2::lps::explorer< Stochastic, Timed, Specification > | inline |
process_parameters() const | mcrl2::lps::explorer< Stochastic, Timed, Specification > | inline |
regular_summands() const | mcrl2::lps::explorer< Stochastic, Timed, Specification > | inline |
rewrite_action(const lps::multi_action &a, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr) const | mcrl2::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 typedef | mcrl2::lps::explorer< Stochastic, Timed, Specification > | |
state_map() const | mcrl2::lps::explorer< Stochastic, Timed, Specification > | inline |
state_type typedef | mcrl2::lps::explorer< Stochastic, Timed, Specification > | |
timed_state | mcrl2::lps::explorer< Stochastic, Timed, Specification > | mutableprotected |
~explorer()=default | mcrl2::lps::explorer< Stochastic, Timed, Specification > |