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: 2021-05-13 00:46:59 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_trans_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_jgkw algorithm ----------------*/
     166             : 
     167             :     // block counters
     168             :     "split_off_block()",
     169             :     "adapt_transitions_for_new_block()",
     170             :     "create_initial_partition()",
     171             : 
     172             :     // state counters
     173             :     "split(), find predecessors of a state in the smaller subblock",
     174             :     "split(), while U-coroutine runs, find predecessors of a U-state",
     175             :     "split(), while R-coroutine runs, find predecessors of a R-state",
     176             :     "handle_new_noninert_transns()",
     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             :     "handle_new_noninert_transns(), make block_bunch-slice without bottom "
     187             :                                          "states unstable (temporary counter)",
     188             : 
     189             :     // transition counters
     190             :     "move_out_slice_to_new_block()",
     191             :     "split(), handle a transition from a state in the smaller subblock",
     192             :     "split(), handle a transition to a state in the smaller subblock",
     193             :     "split(), while U-coroutine runs, handle a transition to a U-state",
     194             :     "split(), while U-coroutine runs, test noninert outgoing transitions",
     195             :     "split(), while R-coroutine runs, handle a transition from a R-state",
     196             :     "split(), while R-coroutine runs, handle a transition to a R-state",
     197             :     "split(), the test for noninert transitions found a new bottom state",
     198             :     "handle_new_noninert_transns(), make block_bunch-slice with bottom states "
     199             :                                                                     "unstable",
     200             :     "handle_new_noninert_transns(), make block_bunch-slice without bottom "
     201             :                                              "states unstable (final counter)",
     202             :     "refine_partition_until_it_becomes_stable(), stabilize block with bottom "
     203             :                                         "states for new non-inert transitions",
     204             :     "refine_partition_until_it_becomes_stable(), stabilize block without "
     205             :                                   "bottom states for new non-inert transitions"
     206             : };
     207             : 
     208             : 
     209             : #if 0
     210             : /// \brief helper macro for check_complexity::test_work_names()
     211             : #define test_work_name(var, ctr)                                              \
     212             :         do                                                                    \
     213             :         {                                                                     \
     214             :             assert((var) == ctr);                                             \
     215             :             mCRL2log(log::debug, "bisim_gjkw") << "work_names[" #ctr "] = \"" \
     216             :                                                 << work_names[ctr] << "\".\n";\
     217             :             (var) = (enum counter_type) ((var) + 1);                          \
     218             :         }                                                                     \
     219             :         while (0)
     220             : 
     221             : 
     222             : /// \brief prints a message for each counter, for debugging purposes
     223             : /// \details The function prints, for each counter, the enum constant and the
     224             : /// string associated with these counters.  The function is intended to be used
     225             : /// for debugging:  a programmer can check the output of the function and see
     226             : /// whether each enum constant is similar to the string stored in that
     227             : /// position.  If no, confusing error messages about time budget overruns may
     228             : /// be printed.
     229             : ///
     230             : /// The function is not currently called.  A typical place where a call could
     231             : /// be inserted is in check_complexity::init() in check_complexity.h.
     232             : void check_complexity::test_work_names()
     233             : {
     234             :     enum check_complexity::counter_type i = BLOCK_MIN;
     235             :     // block counters
     236             :     assert(check_complexity::BLOCK_MIN == i);
     237             :     test_work_name(i, while_C_contains_a_nontrivial_constellation_2_4);
     238             :     test_work_name(i, for_all_s_in_SpB_2_10);
     239             :     test_work_name(i, Move_Blue_or_Red_to_a_new_block_NewB_pointer_3_29);
     240             :     test_work_name(i, Move_Blue_or_Red_to_a_new_block_states_3_29);
     241             :     test_work_name(i, for_all_s_in_NewB_3_31);
     242             :     assert(check_complexity::BLOCK_MAX + 1 == i);
     243             : 
     244             :     // state counters
     245             :     assert(check_complexity::STATE_MIN == i);
     246             :     test_work_name(i, Move_Blue_or_Red_to_a_new_block_NewB_swap_3_29);
     247             :     test_work_name(i, refine_bottom_state_3_6l);
     248             :     test_work_name(i, refine_visited_state_3_15);
     249             : 
     250             :     // temporary state counters (blue):
     251             :     test_work_name(i, while_Test_is_not_empty_3_6l_s_is_blue_3_11l);
     252             :     test_work_name(i, while_Blue_contains_unvisited_states_3_15l);
     253             : 
     254             :     // temporary state counters (red):
     255             :     test_work_name(i, while_Red_contains_unvisited_states_3_15r);
     256             : 
     257             :     // new bottom state counters
     258             :     test_work_name(i, for_all_bottom_states_s_in_RfnB_4_8);
     259             :     test_work_name(i, for_all_old_bottom_states_s_in_RedB_selfloop_4_15);
     260             :     assert(check_complexity::STATE_MAX + 1 == i);
     261             : 
     262             :     // B_to_C_descriptor counters
     263             :     assert(check_complexity::B_TO_C_MIN == i);
     264             :     test_work_name(i, for_all_refinable_blocks_RfnB_2_20);
     265             :     test_work_name(i,
     266             :                 Register_that_inert_transitions_from_s_go_to_NewC_B_to_C_2_17);
     267             :     // temporary B_to_C_descriptor counters
     268             :     test_work_name(i, for_all_constellations_C_not_in_R_from_RfnB_4_4);
     269             :     assert(check_complexity::B_TO_C_MAX + 1 == i);
     270             : 
     271             :     // transition counters
     272             :     assert(check_complexity::TRANS_MIN == i);
     273             :     test_work_name(i, for_all_s_prime_in_pred_s_2_11);
     274             :     test_work_name(i,
     275             :                   Register_that_inert_transitions_from_s_go_to_NewC_succ_2_17);
     276             :     test_work_name(i,
     277             :                   Register_that_inert_transitions_from_s_go_to_NewC_swap_2_17);
     278             :     test_work_name(i, refine_outgoing_transition_to_marked_state_3_6l);
     279             : 
     280             :     test_work_name(i, refine_outgoing_transition_3_6_or_23l);
     281             :     test_work_name(i, Move_Blue_or_Red_to_a_new_block_succ_3_29);
     282             :     test_work_name(i, for_all_s_prime_in_succ_s_3_32r);
     283             : 
     284             :     test_work_name(i, refine_incoming_transition_3_18);
     285             :     test_work_name(i, for_all_s_prime_in_pred_s_3_32l);
     286             : 
     287             :     // temporary transition counters (blue):
     288             :     assert(check_complexity::TRANS_MIN_TEMP == i);
     289             :     test_work_name(i, while_Test_is_not_empty_3_6l_s_is_red_3_9l);
     290             :     test_work_name(i,
     291             :                     while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing);
     292             :     test_work_name(i, for_all_s_prime_in_pred_s_setminus_Red_3_18l);
     293             :     test_work_name(i, if___s_prime_has_transition_to_SpC_3_23l);
     294             : 
     295             :     // temporary transition counters (red):
     296             :     test_work_name(i, while_FromRed_is_not_empty_3_6r);
     297             :     test_work_name(i, for_all_s_prime_in_pred_s_3_18r);
     298             :     assert(check_complexity::TRANS_MAX_TEMP + 1 == i);
     299             : 
     300             :     // new bottom transition counters
     301             :     test_work_name(i, refine_outgoing_transition_postprocess_new_bottom_3_6l);
     302             :     test_work_name(i, refine_outgoing_transition_from_new_bottom_3_23l);
     303             :     test_work_name(i, for_all_transitions_from_bottom_states_a_priori_4_4);
     304             :     test_work_name(i, for_all_transitions_from_bottom_states_a_posteriori_4_4);
     305             :     test_work_name(i, for_all_transitions_that_need_postproc_a_priori_4_12);
     306             :     test_work_name(i,for_all_transitions_that_need_postproc_a_posteriori_4_12);
     307             :     test_work_name(i, for_all_old_bottom_states_s_in_RedB_4_15);
     308             :     assert(check_complexity::TRANS_MAX + 1 == i);
     309             : 
     310             :     /*---------------- counters for the bisim_jgkw algorithm ----------------*/
     311             : 
     312             :     // block counters
     313             :     assert(check_complexity::BLOCK_dnj_MIN == i);
     314             :     test_work_name(i, split_off_block);
     315             :     test_work_name(i, adapt_transitions_for_new_block);
     316             :     test_work_name(i, create_initial_partition);
     317             :     assert(check_complexity::BLOCK_dnj_MAX + 1 == i);
     318             : 
     319             :     // state counters
     320             :     assert(check_complexity::STATE_dnj_MIN == i);
     321             :     test_work_name(i, split__find_predecessors_of_R_or_U_state);
     322             :     assert(check_complexity::STATE_dnj_MIN_TEMP == i);
     323             :     test_work_name(i, split_U__find_predecessors_of_U_state);
     324             :     test_work_name(i, split_R__find_predecessors_of_R_state);
     325             :     assert(check_complexity::STATE_dnj_MAX_TEMP + 1 == i);
     326             :     test_work_name(i, handle_new_noninert_transns);
     327             :     assert(check_complexity::STATE_dnj_MAX + 1 == i);
     328             : 
     329             :     // bunch counters (only for small bunches, i. e. bunches that have been
     330             :     // split off from a large bunch)
     331             :     assert(check_complexity::BUNCH_dnj_MIN == i);
     332             :     test_work_name(i, refine_partition_until_stable__find_pred);
     333             :     assert(check_complexity::BUNCH_dnj_MAX + 1 == i);
     334             : 
     335             :     // block_bunch-slice counters (only for block_bunch-slices that are
     336             :     // part of a small bunch)
     337             :     assert(check_complexity::BLOCK_BUNCH_dnj_MIN == i);
     338             :     test_work_name(i, refine_partition_until_stable__stabilize);
     339             :     test_work_name(i,
     340             :                   refine_partition_until_stable__stabilize_for_large_splitter);
     341             :     assert(check_complexity::BLOCK_BUNCH_dnj_MIN_TEMP == i);
     342             :     test_work_name(i, handle_new_noninert_transns__make_unstable_temp);
     343             :     assert(check_complexity::BLOCK_BUNCH_dnj_MAX_TEMP + 1 == i);
     344             :     assert(check_complexity::BLOCK_BUNCH_dnj_MAX + 1 == i);
     345             : 
     346             :     // transition counters
     347             :     assert(check_complexity::TRANS_dnj_MIN == i);
     348             :     test_work_name(i, move_out_slice_to_new_block);
     349             :     test_work_name(i, split__handle_transition_from_R_or_U_state);
     350             :     test_work_name(i, split__handle_transition_to_R_or_U_state);
     351             :     assert(check_complexity::TRANS_dnj_MIN_TEMP == i);
     352             :     test_work_name(i, split_U__handle_transition_to_U_state);
     353             :     test_work_name(i, split_U__test_noninert_transitions);
     354             :     test_work_name(i, split_R__handle_transition_from_R_state);
     355             :     test_work_name(i, split_R__handle_transition_to_R_state);
     356             :     assert(check_complexity::TRANS_dnj_MAX_TEMP + 1 == i);
     357             :     test_work_name(i, split__test_noninert_transitions_found_new_bottom_state);
     358             :     test_work_name(i, handle_new_noninert_transns__make_unstable_a_priori);
     359             :     test_work_name(i, handle_new_noninert_transns__make_unstable_a_posteriori);
     360             :     test_work_name(i,
     361             :                refine_partition_until_stable__stabilize_new_noninert_a_priori);
     362             :     test_work_name(i,
     363             :            refine_partition_until_stable__stabilize_new_noninert_a_posteriori);
     364             :     assert(check_complexity::TRANS_dnj_MAX + 1 == i);
     365             : 
     366             :     exit(EXIT_SUCCESS);
     367             : }
     368             : #endif // #if 0
     369             : 
     370             : #endif // #ifndef NDEBUG
     371             : 
     372             : } // end namespace bisim_gjkw
     373             : } // end namespace detail
     374             : } // end namespace lts
     375          21 : } // end namespace mcrl2

Generated by: LCOV version 1.13