LCOV - code coverage report
Current view: top level - lts/source - check_complexity.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 1 1 100.0 %
Date: 2019-09-14 00:54:39 Functions: 2 2 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands
       2             : //
       3             : // Copyright: see the accompanying file COPYING or copy at
       4             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       5             : //
       6             : // Distributed under the Boost Software License, Version 1.0.
       7             : // (See accompanying file LICENSE_1_0.txt or copy at
       8             : // http://www.boost.org/LICENSE_1_0.txt)
       9             : 
      10             : /// \file lts/source/check_complexity.cpp
      11             : ///
      12             : /// \brief helper class for time complexity checks during test runs
      13             : ///
      14             : /// \details We use the class in this file to check whether the overall time
      15             : /// complexity fits in O(m log n).  Although it is difficult to test this in
      16             : /// general because of the constant factor in the definition of the O()
      17             : /// notation, it is often possible to give a (rather tight) upper bound on the
      18             : /// number of iterations of most loops.
      19             : ///
      20             : /// The principle of time measurement with this file is:  the work done in
      21             : /// every loop body is assigned to a state or a transition.  Every state and
      22             : /// every transition gets a counter for every loop body which is assigned
      23             : /// to it.  When the loop body is executed, the corresponding counter is
      24             : /// increased.  When increasing a counter, a new value is assigned, based on
      25             : /// the logarithm of the size of the corresponding block (or constellation).
      26             : /// If the new value is not actually larger than the old one, an error is
      27             : /// raised.  The new value never is allowed to become larger than log2(n), so
      28             : /// we have:  For every counter, its value is increased at most log2(n) times,
      29             : /// and therefore no more than log2(n) steps (of a certain kind) can be
      30             : /// assigned to any single state or transition.
      31             : ///
      32             : /// Note that an ``increase'' is by at least 1, but it may be more than 1.  If
      33             : /// one always increases to the maximal allowed value, it is ensured that a
      34             : /// very small block found early will only incur work that corresponds to its
      35             : /// own size (and not to the size of the block from which it was split off).
      36             : ///
      37             : /// To assign work to some unit, write `mCRL2complexity(unit, add_work(counter
      38             : /// type, new counter value));`  The `unit` is a state or transition;  the
      39             : /// `counter type` is a value of `enum check_complexity::counter_type` defined
      40             : /// below; the `new counter value` typically is `check_complexity::log_n -
      41             : /// check_complexity::ilog2(block size)`.
      42             : ///
      43             : /// For coroutines, there is an additional provision: work can temporarily be
      44             : /// recorded in some special counters.  As soon as it becomes clear which
      45             : /// coroutine (the one handling red states or the one handling blue states, in
      46             : /// our case) is faster, its counters are transferred to normal counters and
      47             : /// the counters of the other coroutine are cancelled.  It is checked that not
      48             : /// too many counters are cancelled.
      49             : ///
      50             : /// To transfer work from a temporary to a normal counter, one uses
      51             : /// `finalise_work()`.  To cancel counters, use `cancel_work()`.  These
      52             : /// functions are not normally called directly, but through `red_is_smaller()`
      53             : /// or `blue_is_smaller()`:  If the red subblock is smaller, call
      54             : /// `red_is_smaller(temporary counter, normal counter, new counter value)` for
      55             : /// each state and each transition of the block that was refined;  if the blue
      56             : /// subblock is smaller, call `blue_is_smaller(...)`.
      57             : /// After all temporary work has been handled, call `check_temporary_work()` to
      58             : /// compare the amount of sensible work with the amount of cancelled work.
      59             : ///
      60             : /// If the work could be assigned to one of several counters, I recommend to
      61             : /// assign it to all of them;  otherwise, it may happen that a later excess of
      62             : /// the time budget goes unnoticed because too few counters were advanced.
      63             : /// This, however, poses some difficulties when using temporary counters: a
      64             : /// single unit of work should be assigned to multiple counters, but added to
      65             : /// the balance between sensible and superfluous work only once.  A variant of
      66             : /// `add_work()`, namely `add_work_notemporary()`, can be called in that case:
      67             : /// it assigns a special value `DONT_COUNT_TEMPORARY` to a temporary counter
      68             : /// meaning that it should be disregarded in the calculation of the balance.
      69             : ///
      70             : /// \author David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands
      71             : 
      72             : 
      73             : #include "mcrl2/lts/detail/check_complexity.h"
      74             : 
      75             : namespace mcrl2
      76             : {
      77             : namespace lts
      78             : {
      79             : namespace detail
      80             : {
      81             : namespace bisim_gjkw
      82             : {
      83             : 
      84             : #ifndef NDEBUG
      85             : 
      86             : /// \brief binary logarithm of the state space size, rounded down
      87             : unsigned char check_complexity::log_n = '\0';
      88             : 
      89             : /// \brief the number of useful steps in the last refinement
      90             : signed_state_type check_complexity::sensible_work = 0;
      91             : 
      92             : /// \brief names for complexity counters
      93             : /// \details Every complexity counter (defined in check_complexity.h)
      94             : /// corresponds to a loop in one of the places of the algorithm.  Here, an
      95             : /// English description of that place is given, together with the line number
      96             : /// in the pseudocode in the article [Groote/Jansen/Keiren/Wijs: An O(m log n)
      97             : /// algorithm for computing stuttering equivalence and branching bisimulation.
      98             : /// Accepted for publication in ACM TOCL 2017].
      99             : const char *check_complexity::work_names[TRANS_dnj_MAX - BLOCK_MIN + 1] =
     100             : {
     101             :     // block counters
     102             :     "2.4: while C contains a nontrivial constellation",
     103             :     "2.10: for all s in SpB",
     104             :     "3.29: Move Blue/Red to a new block NewB (set pointers to new block)",
     105             :     "3.29: Move Blue/Red to a new block NewB (for all states s in NewB)",
     106             :     "3.31: for all s in NewB",
     107             : 
     108             :     // state counters
     109             :     "3.29: Move Blue/Red to a new block NewB (swap states)",
     110             : 
     111             :     "3.6l: refine bottom state",
     112             :     "3.15: refine visited state",
     113             : 
     114             :     // temporary state counters (blue):
     115             :     "3.6l: while Test is not empty (3.11l: s is blue)",
     116             :     "3.15l: while Blue contains unvisited states",
     117             : 
     118             :     // temporary state counters (red):
     119             :     "3.15r: while Red contains unvisited states",
     120             : 
     121             :     // new bottom state counters: every state is visited once
     122             :     "4.8: for all bottom states s in RfnB",
     123             :     "4.15: for all old bottom states s in RedB (self-loop)",
     124             :     
     125             :     // B_to_C_descriptor counters
     126             :     "2.20: for all refinable blocks RfnB",
     127             :     "2.17: Register that inert transitions from s go to NewC (B_to_C)",
     128             :     "4.4: for all constellations C not in R reachable from RfnB",
     129             : 
     130             :     // transition counters: every transition is visited O(log n) times
     131             :     "2.11: for all s_prime in in(s)",
     132             :     "2.17: Register that inert transitions from s go to NewC (out)",
     133             :     "2.17: Register that inert transitions from s go to NewC (swap "
     134             :                                                                 "transitions)",
     135             :     "3.6l: refine outgoing transition to marked state",
     136             : 
     137             :     "3.6/3.23l: refine outgoing transition",
     138             :     "3.29: Move Blue/Red to a new block NewB (for all transitions in out(s))",
     139             :     "3.32r: for all s_prime in out(s)",
     140             : 
     141             :     "3.18: refine incoming transition",
     142             :     "3.32l: for all s_prime in in(s)",
     143             : 
     144             :     // temporary transition counters (blue):
     145             :     "3.6l: while Test is not empty (3.9l: s is red)",
     146             :     "3.6l: while Test is not empty (3.9l: s is red) during postprocessing",
     147             :     "3.18l: for all s_prime in in(s) \\ Red",
     148             :     "3.23l: if ... s_prime has no transition to SpC",
     149             : 
     150             :     // temporary transition counters (red):
     151             :     "3.6r: while FromRed is not empty",
     152             :     "3.18r: for all s_prime in in(s)",
     153             : 
     154             :     // new bottom transition counters: every transition is visited once
     155             :     "3.6l: refine outgoing transition (called from PostprocessNewBottom)",
     156             :     "3.23l: refine outgoing transition (state is new bottom state)",
     157             :     "4.4: for all transitions from new bottom states (a priori)",
     158             :     "4.4: for all transitions from new bottom states (a posteriori)",
     159             :     "4.12: for all blocks B with transitions to SpC that need postprocessing "
     160             :                                                                   "(a priori)",
     161             :     "4.12: for all blocks B with transitions to SpC that need postprocessing "
     162             :                                                               "(a posteriori)",
     163             :     "4.15: for all old bottom states s in RedB",
     164             : 
     165             :     /*---------------- counters for the bisim_dnj algorithm ----------------*/
     166             : 
     167             :     // block counters
     168             :     "split_off_block()",
     169             :     "adapt_transitions_for_new_block()",
     170             :     "create_initial_partition()",
     171             : 
     172             :     // state counters
     173             :     "refine(), find predecessors of a red or blue state",
     174             :     "refine(), while blue coroutine runs, find predecessors of a blue state",
     175             :     "refine(), while red coroutine runs, find predecessors of a red state",
     176             :     "prepare_for_postprocessing()",
     177             : 
     178             :     // bunch counters (only for small bunches, i. e. bunches that have been
     179             :     // split off from a large bunch)
     180             :     "refine_partition_until_it_becomes_stable(), find predecessors",
     181             : 
     182             :     // block_bunch-slice counters (only for block_bunch-slices that are
     183             :     // part of a small bunch)
     184             :     "refine_partition_until_it_becomes_stable(), stabilize",
     185             :     "refine_partition_until_it_becomes_stable(), stabilize for large splitter",
     186             :     "second_move_transition_to_new_bunch()",
     187             :     "prepare_for_postprocessing(), make block_bunch-slice without bottom "
     188             :                                          "states unstable (temporary counter)",
     189             : 
     190             :     // transition counters
     191             :     "move_out_slice_to_new_block()",
     192             :     "refine(), handle a transition from a red or blue state",
     193             :     "refine(), handle a transition to a red or blue state",
     194             :     "refine(), handle a transition in the small splitter",
     195             :     "refine(), while blue coroutine runs, handle a transition in the small "
     196             :                                                                     "splitter",
     197             :     "refine(), while blue coroutine runs, handle a transition to a blue state",
     198             :     "refine(), while blue coroutine runs, slow test",
     199             :     "refine(), while red coroutine runs, handle a transition from a red state",
     200             :     "refine(), while red coroutine runs, handle a transition to a red state",
     201             :     "refine(), the slow test found a red state",
     202             :     "prepare_for_postprocessing(), make block_bunch-slice with bottom states "
     203             :                                                                     "unstable",
     204             :     "prepare_for_postprocessing(), make block_bunch-slice without bottom "
     205             :                                              "states unstable (final counter)",
     206             :     "postprocess_new_noninert(), sort",
     207             :     "postprocess_new_noninert(), stabilize block with bottom states",
     208             :     "postprocess_new_noninert(), stabilize block without bottom states"
     209             : };
     210             : 
     211             : 
     212             : #if 0
     213             : /// \brief helper macro for check_complexity::test_work_names()
     214             : #define test_work_name(var, ctr)                                              \
     215             :         do                                                                    \
     216             :         {                                                                     \
     217             :             assert((var) == ctr);                                             \
     218             :             mCRL2log(log::debug, "bisim_gjkw") << "work_names[" #ctr "] = \"" \
     219             :                                                 << work_names[ctr] << "\".\n";\
     220             :             (var) = (enum counter_type) ((var) + 1);                          \
     221             :         }                                                                     \
     222             :         while (0)
     223             : 
     224             : 
     225             : /// \brief prints a message for each counter, for debugging purposes
     226             : /// \details The function prints, for each counter, the enum constant and the
     227             : /// string associated with these counters.  The function is intended to be used
     228             : /// for debugging:  a programmer can check the output of the function and see
     229             : /// whether each enum constant is similar to the string stored in that
     230             : /// position.  If no, confusing error messages about time budget overruns may
     231             : /// be printed.
     232             : ///
     233             : /// The function is not currently called.  A typical place where a call could
     234             : /// be inserted is in check_complexity::init() in check_complexity.h.
     235             : void check_complexity::test_work_names()
     236             : {
     237             :     enum check_complexity::counter_type i = BLOCK_MIN;
     238             :     // block counters
     239             :     assert(check_complexity::BLOCK_MIN == i);
     240             :     test_work_name(i, while_C_contains_a_nontrivial_constellation_2_4);
     241             :     test_work_name(i, for_all_s_in_SpB_2_10);
     242             :     test_work_name(i, Move_Blue_or_Red_to_a_new_block_NewB_pointer_3_29);
     243             :     test_work_name(i, Move_Blue_or_Red_to_a_new_block_states_3_29);
     244             :     test_work_name(i, for_all_s_in_NewB_3_31);
     245             :     assert(check_complexity::BLOCK_MAX + 1 == i);
     246             : 
     247             :     // state counters
     248             :     assert(check_complexity::STATE_MIN == i);
     249             :     test_work_name(i, Move_Blue_or_Red_to_a_new_block_NewB_swap_3_29);
     250             :     test_work_name(i, refine_bottom_state_3_6l);
     251             :     test_work_name(i, refine_visited_state_3_15);
     252             : 
     253             :     // temporary state counters (blue):
     254             :     test_work_name(i, while_Test_is_not_empty_3_6l_s_is_blue_3_11l);
     255             :     test_work_name(i, while_Blue_contains_unvisited_states_3_15l);
     256             : 
     257             :     // temporary state counters (red):
     258             :     test_work_name(i, while_Red_contains_unvisited_states_3_15r);
     259             : 
     260             :     // new bottom state counters
     261             :     test_work_name(i, for_all_bottom_states_s_in_RfnB_4_8);
     262             :     test_work_name(i, for_all_old_bottom_states_s_in_RedB_selfloop_4_15);
     263             :     assert(check_complexity::STATE_MAX + 1 == i);
     264             : 
     265             :     // B_to_C_descriptor counters
     266             :     assert(check_complexity::B_TO_C_MIN == i);
     267             :     test_work_name(i, for_all_refinable_blocks_RfnB_2_20);
     268             :     test_work_name(i,
     269             :                 Register_that_inert_transitions_from_s_go_to_NewC_B_to_C_2_17);
     270             :     // temporary B_to_C_descriptor counters
     271             :     test_work_name(i, for_all_constellations_C_not_in_R_from_RfnB_4_4);
     272             :     assert(check_complexity::B_TO_C_MAX + 1 == i);
     273             : 
     274             :     // transition counters
     275             :     assert(check_complexity::TRANS_MIN == i);
     276             :     test_work_name(i, for_all_s_prime_in_pred_s_2_11);
     277             :     test_work_name(i,
     278             :                   Register_that_inert_transitions_from_s_go_to_NewC_succ_2_17);
     279             :     test_work_name(i,
     280             :                   Register_that_inert_transitions_from_s_go_to_NewC_swap_2_17);
     281             :     test_work_name(i, refine_outgoing_transition_to_marked_state_3_6l);
     282             : 
     283             :     test_work_name(i, refine_outgoing_transition_3_6_or_23l);
     284             :     test_work_name(i, Move_Blue_or_Red_to_a_new_block_succ_3_29);
     285             :     test_work_name(i, for_all_s_prime_in_succ_s_3_32r);
     286             : 
     287             :     test_work_name(i, refine_incoming_transition_3_18);
     288             :     test_work_name(i, for_all_s_prime_in_pred_s_3_32l);
     289             : 
     290             :     // temporary transition counters (blue):
     291             :     assert(check_complexity::TRANS_MIN_TEMP == i);
     292             :     test_work_name(i, while_Test_is_not_empty_3_6l_s_is_red_3_9l);
     293             :     test_work_name(i,
     294             :                     while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing);
     295             :     test_work_name(i, for_all_s_prime_in_pred_s_setminus_Red_3_18l);
     296             :     test_work_name(i, if___s_prime_has_transition_to_SpC_3_23l);
     297             : 
     298             :     // temporary transition counters (red):
     299             :     test_work_name(i, while_FromRed_is_not_empty_3_6r);
     300             :     test_work_name(i, for_all_s_prime_in_pred_s_3_18r);
     301             :     assert(check_complexity::TRANS_MAX_TEMP + 1 == i);
     302             : 
     303             :     // new bottom transition counters
     304             :     test_work_name(i, refine_outgoing_transition_postprocess_new_bottom_3_6l);
     305             :     test_work_name(i, refine_outgoing_transition_from_new_bottom_3_23l);
     306             :     test_work_name(i, for_all_transitions_from_bottom_states_a_priori_4_4);
     307             :     test_work_name(i, for_all_transitions_from_bottom_states_a_posteriori_4_4);
     308             :     test_work_name(i, for_all_transitions_that_need_postproc_a_priori_4_12);
     309             :     test_work_name(i,for_all_transitions_that_need_postproc_a_posteriori_4_12);
     310             :     test_work_name(i, for_all_old_bottom_states_s_in_RedB_4_15);
     311             :     assert(check_complexity::TRANS_MAX + 1 == i);
     312             : 
     313             :     /*---------------- counters for the bisim_dnj algorithm ----------------*/
     314             : 
     315             :     // block counters
     316             :     assert(check_complexity::BLOCK_dnj_MIN == i);
     317             :     test_work_name(i, split_off_block);
     318             :     test_work_name(i, adapt_transitions_for_new_block);
     319             :     test_work_name(i, create_initial_partition);
     320             :     assert(check_complexity::BLOCK_dnj_MAX + 1 == i);
     321             : 
     322             :     // state counters
     323             :     assert(check_complexity::STATE_dnj_MIN == i);
     324             :     test_work_name(i, refine__find_predecessors_of_red_or_blue_state);
     325             :     assert(check_complexity::STATE_dnj_MIN_TEMP == i);
     326             :     test_work_name(i, refine_blue__find_predecessors_of_blue_state);
     327             :     test_work_name(i, refine_red__find_predecessors_of_red_state);
     328             :     assert(check_complexity::STATE_dnj_MAX_TEMP + 1 == i);
     329             :     test_work_name(i, prepare_for_postprocessing);
     330             :     assert(check_complexity::STATE_dnj_MAX + 1 == i);
     331             : 
     332             :     // bunch counters (only for small bunches, i. e. bunches that have been
     333             :     // split off from a large bunch)
     334             :     assert(check_complexity::BUNCH_dnj_MIN == i);
     335             :     test_work_name(i, refine_partition_until_it_becomes_stable__find_pred);
     336             :     assert(check_complexity::BUNCH_dnj_MAX + 1 == i);
     337             : 
     338             :     // block_bunch-slice counters (only for block_bunch-slices that are
     339             :     // part of a small bunch)
     340             :     assert(check_complexity::BLOCK_BUNCH_dnj_MIN == i);
     341             :     test_work_name(i, refine_partition_until_it_becomes_stable__stabilize);
     342             :     test_work_name(i,
     343             :        refine_partition_until_it_becomes_stable__stabilize_for_large_splitter);
     344             :     test_work_name(i, second_move_transition_to_new_bunch);
     345             :     assert(check_complexity::BLOCK_BUNCH_dnj_MIN_TEMP == i);
     346             :     test_work_name(i, prepare_for_postprocessing__make_unstable_temp);
     347             :     assert(check_complexity::BLOCK_BUNCH_dnj_MAX_TEMP + 1 == i);
     348             :     assert(check_complexity::BLOCK_BUNCH_dnj_MAX + 1 == i);
     349             : 
     350             :     // transition counters
     351             :     assert(check_complexity::TRANS_dnj_MIN == i);
     352             :     test_work_name(i, move_out_slice_to_new_block);
     353             :     test_work_name(i, refine__handle_transition_from_red_or_blue_state);
     354             :     test_work_name(i, refine__handle_transition_to_red_or_blue_state);
     355             :     test_work_name(i, refine__handle_transition_in_FromRed);
     356             :     assert(check_complexity::TRANS_dnj_MIN_TEMP == i);
     357             :     test_work_name(i, refine_blue__handle_transition_in_FromRed);
     358             :     test_work_name(i, refine_blue__handle_transition_to_blue_state);
     359             :     test_work_name(i, refine_blue__slow_test);
     360             :     test_work_name(i, refine_red__handle_transition_from_red_state);
     361             :     test_work_name(i, refine_red__handle_transition_to_red_state);
     362             :     assert(check_complexity::TRANS_dnj_MAX_TEMP + 1 == i);
     363             :     test_work_name(i, refine__slow_test_found_red_state);
     364             :     test_work_name(i, prepare_for_postprocessing__make_unstable_a_priori);
     365             :     test_work_name(i, prepare_for_postprocessing__make_unstable_a_posteriori);
     366             :     test_work_name(i, postprocess_new_noninert__sort);
     367             :     test_work_name(i, postprocess_new_noninert__stabilize_a_priori);
     368             :     test_work_name(i, postprocess_new_noninert__stabilize_a_posteriori);
     369             :     assert(check_complexity::TRANS_dnj_MAX + 1 == i);
     370             : 
     371             :     exit(EXIT_SUCCESS);
     372             : }
     373             : #endif // #if 0
     374             : 
     375             : #endif // #ifndef NDEBUG
     376             : 
     377             : } // end namespace bisim_gjkw
     378             : } // end namespace detail
     379             : } // end namespace lts
     380          21 : } // end namespace mcrl2

Generated by: LCOV version 1.12