mcrl2::lts::detail::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	BLC_gj_counter_t
class	block_bunch_dnj_counter_t
class	block_counter_t
	counters for a block More...
class	block_dnj_counter_t
class	block_gj_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	state_gj_counter_t
class	trans_counter_t
class	trans_dnj_counter_t
class	trans_gj_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 , refine_partition_until_it_becomes_stable__find_splitter ,   BLOCK_gj_MIN , splitB__update_BLC_of_smaller_subblock , BLOCK_gj_MAX = splitB__update_BLC_of_smaller_subblock , split_block_B_into_R_and_BminR__carry_out_split ,   STATE_gj_MIN = split_block_B_into_R_and_BminR__carry_out_split , split_block_B_into_R_and_BminR__skip_over_state , simple_splitB__find_bottom_state , simple_splitB__find_predecessors_of_R_or_U_state ,   multiple_swap_states_in_block__account_for_swap_in_aborted_block , multiple_swap_states_in_block__swap_state_in_small_block , simple_splitB_R__find_predecessors , STATE_gj_MIN_TEMP = simple_splitB_R__find_predecessors ,   simple_splitB_U__find_predecessors , STATE_gj_MAX_TEMP = simple_splitB_U__find_predecessors , stabilizeB__prepare_block , stabilizeB__distribute_states_over_Phat ,   create_initial_partition__set_start_incoming_transitions , STATE_gj_MAX = create_initial_partition__set_start_incoming_transitions , refine_partition_until_it_becomes_stable__prepare_cosplit , BLC_gj_MIN = refine_partition_until_it_becomes_stable__prepare_cosplit ,   refine_partition_until_it_becomes_stable__correct_end_of_calM , refine_partition_until_it_becomes_stable__execute_main_split , four_way_splitB__handle_transitions_in_main_splitter , BLC_gj_MAX = four_way_splitB__handle_transitions_in_main_splitter ,   simple_splitB__handle_transition_from_R_or_U_state , TRANS_gj_MIN = simple_splitB__handle_transition_from_R_or_U_state , simple_splitB__handle_transition_to_R_or_U_state , refine_partition_until_it_becomes_stable__find_cotransition ,   order_BLC_transitions__sort_transition , simple_splitB_R__handle_transition_from_R_state , TRANS_gj_MIN_TEMP = simple_splitB_R__handle_transition_from_R_state , simple_splitB_R__handle_transition_to_R_state ,   simple_splitB_U__handle_transition_to_U_state , simple_splitB_U__handle_transition_from_potential_U_state , TRANS_gj_MAX_TEMP = simple_splitB_U__handle_transition_from_potential_U_state , simple_splitB__test_outgoing_transitions_found_new_bottom_state ,   splitB__unmark_transitions_out_of_new_bottom_block , splitB__unmark_transitions_out_of_new_bottom_block_afterwards , stabilizeB__initialize_Qhat , stabilizeB__initialize_Qhat_afterwards ,   stabilizeB__main_loop , stabilizeB__main_loop_afterwards , create_initial_partition__refine_block , TRANS_gj_MAX = create_initial_partition__refine_block }
	Type for complexity budget counters. More...
enum	result_type { complexity_ok = 77655 , complexity_print = 54854 , complexity_error = 81956 }

Static Public Member Functions
static int	ilog2 (state_type size)
	calculate the base-2 logarithm, rounded down
static void	wait (trans_type units=1)
	do some work that cannot be assigned directly
static void	check_waiting_cycles ()
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 void	print_grand_totals ()
	print grand total of work in the coroutines (to measure overhead)

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

Static Private Member Functions
static void	finalise_work_units (trans_type units=1)
static void	cancel_work_units (trans_type units=1)

Static Private Attributes
static signed_trans_type	sensible_work = 0
	counter to register the work balance for coroutines
static trans_type	no_of_waiting_cycles = 0
	the number of waiting cycles that have been done in the current accounting period
static bool	cannot_wait_before_reset = false
	indicates whether waiting cycles are allowed
static trans_type	sensible_work_grand_total = 0
	the number of useful steps in the course of the whole algorithm
static trans_type	cancelled_work_grand_total = 0
	the number of cancelled steps (in aborted coroutines) in the course of the whole algorithm
static trans_type	no_of_waiting_cycles_grand_total = 0
	the number of waiting cycles in the course of the whole algorithm

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 137 of file check_complexity.h.

Member Enumeration Documentation

counter_type

enum mcrl2::lts::detail::check_complexity::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
refine_partition_until_it_becomes_stable__find_splitter
BLOCK_gj_MIN
splitB__update_BLC_of_smaller_subblock
BLOCK_gj_MAX
split_block_B_into_R_and_BminR__carry_out_split
STATE_gj_MIN
split_block_B_into_R_and_BminR__skip_over_state
simple_splitB__find_bottom_state
simple_splitB__find_predecessors_of_R_or_U_state
multiple_swap_states_in_block__account_for_swap_in_aborted_block
multiple_swap_states_in_block__swap_state_in_small_block
simple_splitB_R__find_predecessors
STATE_gj_MIN_TEMP
simple_splitB_U__find_predecessors
STATE_gj_MAX_TEMP
stabilizeB__prepare_block
stabilizeB__distribute_states_over_Phat
create_initial_partition__set_start_incoming_transitions
STATE_gj_MAX
refine_partition_until_it_becomes_stable__prepare_cosplit
BLC_gj_MIN
refine_partition_until_it_becomes_stable__correct_end_of_calM
refine_partition_until_it_becomes_stable__execute_main_split
four_way_splitB__handle_transitions_in_main_splitter
BLC_gj_MAX
simple_splitB__handle_transition_from_R_or_U_state
TRANS_gj_MIN
simple_splitB__handle_transition_to_R_or_U_state
refine_partition_until_it_becomes_stable__find_cotransition
order_BLC_transitions__sort_transition
simple_splitB_R__handle_transition_from_R_state
TRANS_gj_MIN_TEMP
simple_splitB_R__handle_transition_to_R_state
simple_splitB_U__handle_transition_to_U_state
simple_splitB_U__handle_transition_from_potential_U_state
TRANS_gj_MAX_TEMP
simple_splitB__test_outgoing_transitions_found_new_bottom_state
splitB__unmark_transitions_out_of_new_bottom_block
splitB__unmark_transitions_out_of_new_bottom_block_afterwards
stabilizeB__initialize_Qhat
stabilizeB__initialize_Qhat_afterwards
stabilizeB__main_loop
stabilizeB__main_loop_afterwards
create_initial_partition__refine_block
TRANS_gj_MAX

Definition at line 149 of file check_complexity.h.

result_type

enum mcrl2::lts::detail::check_complexity::result_type

Enumerator
complexity_ok
complexity_print
complexity_error

Definition at line 464 of file check_complexity.h.

Member Function Documentation

cancel_work_units()

static void mcrl2::lts::detail::check_complexity::cancel_work_units ( trans_type  units = 1 )

inlinestaticprivate

Definition at line 562 of file check_complexity.h.

check_temporary_work()

static void mcrl2::lts::detail::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 575 of file check_complexity.h.

check_waiting_cycles()

static void mcrl2::lts::detail::check_complexity::check_waiting_cycles ( )

inlinestatic

Definition at line 543 of file check_complexity.h.

finalise_work_units()

static void mcrl2::lts::detail::check_complexity::finalise_work_units ( trans_type  units = 1 )

inlinestaticprivate

Definition at line 554 of file check_complexity.h.

ilog2()

static int mcrl2::lts::detail::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 479 of file check_complexity.h.

init()

static void mcrl2::lts::detail::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

n	size of the state space

Definition at line 1858 of file check_complexity.h.

print_grand_totals()

static void mcrl2::lts::detail::check_complexity::print_grand_totals ( )

inlinestatic

print grand total of work in the coroutines (to measure overhead)

Definition at line 1878 of file check_complexity.h.

wait()

static void mcrl2::lts::detail::check_complexity::wait ( trans_type  units = 1 )

inlinestatic

do some work that cannot be assigned directly

This is meant for a coroutine that has nothing to do currently; in particular, it cannot do sensible work on a state or transition.

Definition at line 534 of file check_complexity.h.

Member Data Documentation

cancelled_work_grand_total

trans_type mcrl2::lts::detail::check_complexity::cancelled_work_grand_total = 0

staticprivate

the number of cancelled steps (in aborted coroutines) in the course of the whole algorithm

Definition at line 521 of file check_complexity.h.

cannot_wait_before_reset

bool mcrl2::lts::detail::check_complexity::cannot_wait_before_reset = false

staticprivate

indicates whether waiting cycles are allowed

During finalising all counters of an accounting period, there is a point when waiting cycles are measured (by calling the function check_waiting_cycles()); from that moment until the balance is reset (using check_temporary_work()) one cannot insert waiting cycles. This boolean is used to check for the restriction.

Definition at line 518 of file check_complexity.h.

log_n

unsigned char mcrl2::lts::detail::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 474 of file check_complexity.h.

no_of_waiting_cycles

trans_type mcrl2::lts::detail::check_complexity::no_of_waiting_cycles = 0

staticprivate

the number of waiting cycles that have been done in the current accounting period

After finalising all counters of an accounting period, the number of waiting cycles should not exceed the sensible work. However, in contrast to cancelled work, it is not subtracted from the balance.

Definition at line 517 of file check_complexity.h.

no_of_waiting_cycles_grand_total

trans_type mcrl2::lts::detail::check_complexity::no_of_waiting_cycles_grand_total = 0

staticprivate

the number of waiting cycles in the course of the whole algorithm

Definition at line 522 of file check_complexity.h.

sensible_work

signed_trans_type mcrl2::lts::detail::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 516 of file check_complexity.h.

sensible_work_grand_total

trans_type mcrl2::lts::detail::check_complexity::sensible_work_grand_total = 0

staticprivate

the number of useful steps in the course of the whole algorithm

Definition at line 520 of file check_complexity.h.

work_names

const char * mcrl2::lts::detail::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 527 of file check_complexity.h.

---

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

• lts/include/mcrl2/lts/detail/check_complexity.h
• lts/source/check_complexity.cpp