mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::detail::bisim_gjkw::check_complexity Class Reference

class for time complexity checks More...

#include <check_complexity.h>

Classes

class  B_to_C_counter_t
 counters for a B_to_C slice More...
 
class  block_bunch_dnj_counter_t
 
class  block_counter_t
 counters for a block More...
 
class  block_dnj_counter_t
 
class  bunch_dnj_counter_t
 
class  counter_t
 subset of counters (to be associated with a state or transition) More...
 
class  state_counter_t
 
class  state_dnj_counter_t
 
class  trans_counter_t
 
class  trans_dnj_counter_t
 

Public Types

enum  counter_type {
  while_C_contains_a_nontrivial_constellation_2_4 = 0 , BLOCK_MIN = while_C_contains_a_nontrivial_constellation_2_4 , for_all_s_in_SpB_2_10 , Move_Blue_or_Red_to_a_new_block_NewB_pointer_3_29 ,
  Move_Blue_or_Red_to_a_new_block_states_3_29 , for_all_s_in_NewB_3_31 , BLOCK_MAX = for_all_s_in_NewB_3_31 , Move_Blue_or_Red_to_a_new_block_NewB_swap_3_29 ,
  STATE_MIN = Move_Blue_or_Red_to_a_new_block_NewB_swap_3_29 , refine_bottom_state_3_6l , refine_visited_state_3_15 , while_Test_is_not_empty_3_6l_s_is_blue_3_11l ,
  STATE_MIN_TEMP = while_Test_is_not_empty_3_6l_s_is_blue_3_11l , while_Blue_contains_unvisited_states_3_15l , while_Red_contains_unvisited_states_3_15r , STATE_MAX_TEMP = while_Red_contains_unvisited_states_3_15r ,
  for_all_bottom_states_s_in_RfnB_4_8 , for_all_old_bottom_states_s_in_RedB_selfloop_4_15 , STATE_MAX = for_all_old_bottom_states_s_in_RedB_selfloop_4_15 , for_all_refinable_blocks_RfnB_2_20 ,
  B_TO_C_MIN = for_all_refinable_blocks_RfnB_2_20 , Register_that_inert_transitions_from_s_go_to_NewC_B_to_C_2_17 , for_all_constellations_C_not_in_R_from_RfnB_4_4 , B_TO_C_MIN_TEMP =for_all_constellations_C_not_in_R_from_RfnB_4_4 ,
  B_TO_C_MAX_TEMP =for_all_constellations_C_not_in_R_from_RfnB_4_4 , B_TO_C_MAX = for_all_constellations_C_not_in_R_from_RfnB_4_4 , for_all_s_prime_in_pred_s_2_11 , TRANS_MIN = for_all_s_prime_in_pred_s_2_11 ,
  Register_that_inert_transitions_from_s_go_to_NewC_succ_2_17 , Register_that_inert_transitions_from_s_go_to_NewC_swap_2_17 , refine_outgoing_transition_to_marked_state_3_6l , refine_outgoing_transition_3_6_or_23l ,
  Move_Blue_or_Red_to_a_new_block_succ_3_29 , for_all_s_prime_in_succ_s_3_32r , refine_incoming_transition_3_18 , for_all_s_prime_in_pred_s_3_32l ,
  while_Test_is_not_empty_3_6l_s_is_red_3_9l , TRANS_MIN_TEMP = while_Test_is_not_empty_3_6l_s_is_red_3_9l , while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing , for_all_s_prime_in_pred_s_setminus_Red_3_18l ,
  if___s_prime_has_transition_to_SpC_3_23l , while_FromRed_is_not_empty_3_6r , for_all_s_prime_in_pred_s_3_18r , TRANS_MAX_TEMP = for_all_s_prime_in_pred_s_3_18r ,
  refine_outgoing_transition_postprocess_new_bottom_3_6l , refine_outgoing_transition_from_new_bottom_3_23l , for_all_transitions_from_bottom_states_a_priori_4_4 , for_all_transitions_from_bottom_states_a_posteriori_4_4 ,
  for_all_transitions_that_need_postproc_a_priori_4_12 , for_all_transitions_that_need_postproc_a_posteriori_4_12 , for_all_old_bottom_states_s_in_RedB_4_15 , TRANS_MAX = for_all_old_bottom_states_s_in_RedB_4_15 ,
  split_off_block , BLOCK_dnj_MIN = split_off_block , adapt_transitions_for_new_block , create_initial_partition ,
  BLOCK_dnj_MAX = create_initial_partition , split__find_predecessors_of_R_or_U_state , STATE_dnj_MIN = split__find_predecessors_of_R_or_U_state , split_U__find_predecessors_of_U_state ,
  STATE_dnj_MIN_TEMP = split_U__find_predecessors_of_U_state , split_R__find_predecessors_of_R_state , STATE_dnj_MAX_TEMP = split_R__find_predecessors_of_R_state , handle_new_noninert_transns ,
  STATE_dnj_MAX = handle_new_noninert_transns , refine_partition_until_stable__find_pred , BUNCH_dnj_MIN = refine_partition_until_stable__find_pred , BUNCH_dnj_MAX = refine_partition_until_stable__find_pred ,
  refine_partition_until_stable__stabilize , BLOCK_BUNCH_dnj_MIN =refine_partition_until_stable__stabilize , refine_partition_until_stable__stabilize_for_large_splitter , handle_new_noninert_transns__make_unstable_temp ,
  BLOCK_BUNCH_dnj_MIN_TEMP , BLOCK_BUNCH_dnj_MAX_TEMP , BLOCK_BUNCH_dnj_MAX , move_out_slice_to_new_block ,
  TRANS_dnj_MIN = move_out_slice_to_new_block , split__handle_transition_from_R_or_U_state , split__handle_transition_to_R_or_U_state , split_U__handle_transition_to_U_state ,
  TRANS_dnj_MIN_TEMP = split_U__handle_transition_to_U_state , split_U__test_noninert_transitions , split_R__handle_transition_from_R_state , split_R__handle_transition_to_R_state ,
  TRANS_dnj_MAX_TEMP = split_R__handle_transition_to_R_state , split__test_noninert_transitions_found_new_bottom_state , handle_new_noninert_transns__make_unstable_a_priori , handle_new_noninert_transns__make_unstable_a_posteriori ,
  refine_partition_until_stable__stabilize_new_noninert_a_priori , refine_partition_until_stable__stabilize_new_noninert_a_posteriori , TRANS_dnj_MAX
}
 Type for complexity budget counters. More...
 

Static Public Member Functions

static int ilog2 (state_type size)
 calculate the base-2 logarithm, rounded down
 
static void check_temporary_work ()
 check that not too much superfluous work has been done
 
static void init (state_type n)
 starts counting for a new refinement run
 

Static Public Attributes

static unsigned char log_n = '\0'
 value of floor(log2(n)) for easy access
 
static const char * work_names [TRANS_dnj_MAX - BLOCK_MIN+1]
 printable names of the counter types (for error messages)
 

Static Private Attributes

static signed_trans_type sensible_work = 0
 counter to register the work balance for coroutines
 

Detailed Description

class for time complexity checks

The class stores (as static members) the global counters needed for checking time complexity budgets.

It could almost be defined as a namespace because all members are static. Still, just a few members are private.

Definition at line 116 of file check_complexity.h.

Member Enumeration Documentation

◆ counter_type

Type for complexity budget counters.

The enumeration constants defined by this type are used to distinguish the many counters that the time budget check uses. There are counters assigned to blocks, states, B_to_C slices, and transitions. Counters assigned to a block are regarded as if the work would be registered with every state in the block. Counters assigned to a B_to_C slice are regarded as if the work would be registered with every transition in the slice. (These conventions are important when splitting a block or a B_to_C slice.)

Enumerator
while_C_contains_a_nontrivial_constellation_2_4 
BLOCK_MIN 
for_all_s_in_SpB_2_10 
Move_Blue_or_Red_to_a_new_block_NewB_pointer_3_29 
Move_Blue_or_Red_to_a_new_block_states_3_29 
for_all_s_in_NewB_3_31 
BLOCK_MAX 
Move_Blue_or_Red_to_a_new_block_NewB_swap_3_29 
STATE_MIN 
refine_bottom_state_3_6l 
refine_visited_state_3_15 
while_Test_is_not_empty_3_6l_s_is_blue_3_11l 
STATE_MIN_TEMP 
while_Blue_contains_unvisited_states_3_15l 
while_Red_contains_unvisited_states_3_15r 
STATE_MAX_TEMP 
for_all_bottom_states_s_in_RfnB_4_8 
for_all_old_bottom_states_s_in_RedB_selfloop_4_15 
STATE_MAX 
for_all_refinable_blocks_RfnB_2_20 
B_TO_C_MIN 
Register_that_inert_transitions_from_s_go_to_NewC_B_to_C_2_17 
for_all_constellations_C_not_in_R_from_RfnB_4_4 
B_TO_C_MIN_TEMP 
B_TO_C_MAX_TEMP 
B_TO_C_MAX 
for_all_s_prime_in_pred_s_2_11 
TRANS_MIN 
Register_that_inert_transitions_from_s_go_to_NewC_succ_2_17 
Register_that_inert_transitions_from_s_go_to_NewC_swap_2_17 
refine_outgoing_transition_to_marked_state_3_6l 
refine_outgoing_transition_3_6_or_23l 
Move_Blue_or_Red_to_a_new_block_succ_3_29 
for_all_s_prime_in_succ_s_3_32r 
refine_incoming_transition_3_18 
for_all_s_prime_in_pred_s_3_32l 
while_Test_is_not_empty_3_6l_s_is_red_3_9l 
TRANS_MIN_TEMP 
while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing 
for_all_s_prime_in_pred_s_setminus_Red_3_18l 
if___s_prime_has_transition_to_SpC_3_23l 
while_FromRed_is_not_empty_3_6r 
for_all_s_prime_in_pred_s_3_18r 
TRANS_MAX_TEMP 
refine_outgoing_transition_postprocess_new_bottom_3_6l 
refine_outgoing_transition_from_new_bottom_3_23l 
for_all_transitions_from_bottom_states_a_priori_4_4 
for_all_transitions_from_bottom_states_a_posteriori_4_4 
for_all_transitions_that_need_postproc_a_priori_4_12 
for_all_transitions_that_need_postproc_a_posteriori_4_12 
for_all_old_bottom_states_s_in_RedB_4_15 
TRANS_MAX 
split_off_block 
BLOCK_dnj_MIN 
adapt_transitions_for_new_block 
create_initial_partition 
BLOCK_dnj_MAX 
split__find_predecessors_of_R_or_U_state 
STATE_dnj_MIN 
split_U__find_predecessors_of_U_state 
STATE_dnj_MIN_TEMP 
split_R__find_predecessors_of_R_state 
STATE_dnj_MAX_TEMP 
handle_new_noninert_transns 
STATE_dnj_MAX 
refine_partition_until_stable__find_pred 
BUNCH_dnj_MIN 
BUNCH_dnj_MAX 
refine_partition_until_stable__stabilize 
BLOCK_BUNCH_dnj_MIN 
refine_partition_until_stable__stabilize_for_large_splitter 
handle_new_noninert_transns__make_unstable_temp 
BLOCK_BUNCH_dnj_MIN_TEMP 
BLOCK_BUNCH_dnj_MAX_TEMP 
BLOCK_BUNCH_dnj_MAX 
move_out_slice_to_new_block 
TRANS_dnj_MIN 
split__handle_transition_from_R_or_U_state 
split__handle_transition_to_R_or_U_state 
split_U__handle_transition_to_U_state 
TRANS_dnj_MIN_TEMP 
split_U__test_noninert_transitions 
split_R__handle_transition_from_R_state 
split_R__handle_transition_to_R_state 
TRANS_dnj_MAX_TEMP 
split__test_noninert_transitions_found_new_bottom_state 
handle_new_noninert_transns__make_unstable_a_priori 
handle_new_noninert_transns__make_unstable_a_posteriori 
refine_partition_until_stable__stabilize_new_noninert_a_priori 
refine_partition_until_stable__stabilize_new_noninert_a_posteriori 
TRANS_dnj_MAX 

Definition at line 128 of file check_complexity.h.

Member Function Documentation

◆ check_temporary_work()

static void mcrl2::lts::detail::bisim_gjkw::check_complexity::check_temporary_work ( )
inlinestatic

check that not too much superfluous work has been done

After having moved all temporary work counters to the normal counters, this function can be used to ensure that not too much temporary work is cancelled.

Definition at line 402 of file check_complexity.h.

◆ ilog2()

static int mcrl2::lts::detail::bisim_gjkw::check_complexity::ilog2 ( state_type  size)
inlinestatic

calculate the base-2 logarithm, rounded down

The function cannot be constexpr because std::log2() may have the side effect of setting errno.

Definition at line 356 of file check_complexity.h.

◆ init()

static void mcrl2::lts::detail::bisim_gjkw::check_complexity::init ( state_type  n)
inlinestatic

starts counting for a new refinement run

Before any work can be counted, init() should be called to set the size of the state space to the appropriate value.

Parameters
nsize of the state space

Definition at line 1224 of file check_complexity.h.

Member Data Documentation

◆ log_n

unsigned char mcrl2::lts::detail::bisim_gjkw::check_complexity::log_n = '\0'
static

value of floor(log2(n)) for easy access

binary logarithm of the state space size, rounded down

This variable has to be set by init() before counting work can begin.

Definition at line 351 of file check_complexity.h.

◆ sensible_work

signed_trans_type mcrl2::lts::detail::bisim_gjkw::check_complexity::sensible_work = 0
staticprivate

counter to register the work balance for coroutines

the number of useful steps in the last refinement

Sensible work will be counted positively, and cancelled work negatively.

Definition at line 392 of file check_complexity.h.

◆ work_names

const char * mcrl2::lts::detail::bisim_gjkw::check_complexity::work_names
static

printable names of the counter types (for error messages)

names for complexity counters

Every complexity counter (defined in check_complexity.h) corresponds to a loop in one of the places of the algorithm. Here, an English description of that place is given, together with the line number in the pseudocode in the article [Groote/Jansen/Keiren/Wijs: An O(m log n) algorithm for computing stuttering equivalence and branching bisimulation. Accepted for publication in ACM TOCL 2017].

Definition at line 396 of file check_complexity.h.


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