mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE > Member List

This is the complete list of members for mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >, including all inherited members.

accumulate_entries(std::vector< transition_index > &action_counter, const std::vector< label_index > &todo_stack) constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
bisim_partitioner_gj_lazy_BLC(LTS_TYPE &aut, const bool branching=false, const bool preserve_divergence=false)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inline
blocks_that_need_refinementmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >private
change_non_bottom_state_to_bottom_state(const fixed_vector< state_type_gj_lb >::iterator si)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
check_data_structures(const std::string &tag, const bool check_temporary_complexity_counters=true) constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
check_incoming_tau_transitions_become_noninert(block_type_lb &NewBotSt_block, state_in_block_pointer_lb *start_bottom, state_in_block_pointer_lb *const end_non_bottom)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
check_stability(const std::string &tag, const std::vector< std::pair< BLC_list_iterator, BLC_list_iterator > > *calM=nullptr, const std::pair< BLC_list_iterator, BLC_list_iterator > *calM_elt=nullptr, const constellation_type_lb *const old_constellation=null_constellation_lb, const constellation_type_lb *const new_constellation=null_constellation_lb) constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
check_transitions(const bool initialisation, const bool check_temporary_complexity_counters, const bool check_block_to_constellation=true) constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
clear_state_counters(std::vector< state_in_block_pointer_lb >::const_iterator begin, std::vector< state_in_block_pointer_lb >::const_iterator const end, block_type_lb &block)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
create_initial_partition()mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
create_new_block(state_in_block_pointer_lb *start_bottom_states, state_in_block_pointer_lb *const start_non_bottom_states, state_in_block_pointer_lb *const end_states, block_type_lb &old_block_index)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
display_BLC_list(const BLC_source_type &blc_src) constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
end_initial_partmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >
finalize_minimized_LTS()mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inline
four_way_splitB(block_that_needs_refinement_type &bri, constellation_type_lb *const old_constellation=null_constellation_lb, constellation_type_lb *const new_constellation=null_constellation_lb)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
get_eq_class(const state_index si) constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inline
in_same_class(state_index const s, state_index const t) constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inline
is_inert_during_init(const transition &t) constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
is_inert_during_init_if_branching(const transition &t) constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
label_or_divergence(const transition &t, const label_index divergent_label=-2) constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
m_autmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >
m_aut_apply_hidden_label_map(typename LTS_TYPE::labels_size_type l)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivatestatic
m_BLC_indicators_to_be_deletedmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >private
m_BLC_transitionsmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >
m_blocks_with_new_bottom_statesmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >private
m_branchingmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >private
m_non_trivial_constellationsmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >private
m_outgoing_transitionsmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >
m_preserve_divergencemcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >private
m_singleton_block_with_new_bottom_states_for_debugmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >private
m_statesmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >
m_states_in_blocksmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >
m_transitionsmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >
make_BLC_simple(block_type_lb &block_index, const bool mark_all_transitions_in_instable_BLC_sets=false, constellation_type_lb *const old_constellation=null_constellation_lb, constellation_type_lb *const new_constellation=null_constellation_lb)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
make_BLC_simple_split_off_part(BLC_source_type &BLC_source, state_in_block_pointer_lb *const splitpoint, const bool mark_all_transitions_in_instable_BLC_sets, constellation_type_lb *old_constellation, constellation_type_lb *const new_constellation, const int split_type=SPLIT_SMALLER)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
make_stable_and_move_to_start_of_BLC(BLC_source_type &from_blc_src, const simple_list< BLC_indicators_lb >::iterator splitter)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
mark_BLC_transition(const outgoing_transitions_it_lb out_pos)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
move_nonbottom_states_to(const todo_state_vector_lb &R, state_in_block_pointer_lb *to_pos, state_index new_block_bottom_size)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
multiple_swap_states_in_states_in_block(state_in_block_pointer_lb *pos1, state_in_block_pointer_lb *pos2, state_index count, const state_in_block_pointer_lb *assign_work_to, unsigned char const max_B, enum check_complexity::counter_type const ctr=check_complexity::multiple_swap_states_in_block_swap_state_in_small_block)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
next_target_constln_in_same_saC(state_in_block_pointer_lb const src, BLC_list_const_iterator const splitter_it) constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
no_of_BLC_source_setsmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >private
no_of_blocksmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >
no_of_constellationsmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >
no_of_new_bottom_statesmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >private
num_eq_classes() constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inline
number_of_states_in_block(const block_type_lb &B) constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
number_of_states_in_constellation(const constellation_type_lb &C) constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
print_data_structures(const std::string &header) constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
ptr(const transition &t) constmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
refine_partition_until_it_becomes_stable()mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
refine_super_BLC(BLC_indicators_lb &small_splitter, BLC_indicators_lb *const large_splitter=nullptr)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
select_and_remove_a_block_in_a_non_trivial_constellation()mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
set_of_states_type typedefmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >private
set_of_transitions_type typedefmcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >private
stabilizeB()mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
swap_in_the_doubly_linked_list_LBC_in_blocks_new_block(const transition_index ti, simple_list< BLC_indicators_lb >::iterator new_BLC_block, simple_list< BLC_indicators_lb >::iterator old_BLC_block, const bool mark_all_transitions_in_instable_BLC_sets=false)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
swap_in_the_doubly_linked_list_LBC_in_blocks_new_constellation(const transition_index ti, simple_list< BLC_indicators_lb >::iterator new_BLC_block, simple_list< BLC_indicators_lb >::iterator old_BLC_block)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
swap_states_in_states_in_block(state_in_block_pointer_lb *pos1, state_in_block_pointer_lb *pos2)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
swap_states_in_states_in_block_never_equal(state_in_block_pointer_lb *pos1, state_in_block_pointer_lb *pos2)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
swap_three_iterators_and_update_m_transitions(BLC_list_iterator i1, BLC_list_iterator i2, BLC_list_iterator i3)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
update_all_small_subblock_counters(state_in_block_pointer_lb *start_block, state_in_block_pointer_lb *end_block)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
update_small_subblock_counters(state_in_block_pointer_lb *start_blocks, state_in_block_pointer_lb *splitpoint, state_in_block_pointer_lb *end_blocks, const int split_type=SPLIT_SMALLER)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate
update_the_doubly_linked_list_LBC_new_constellation(block_type_lb &index_block_B, const transition &t, const transition_index ti)mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >inlineprivate