LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - check_complexity.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 216 259 83.4 %
Date: 2020-07-11 00:44:39 Functions: 57 57 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/detail/check_complexity.h
      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()`.  (The file
      52             : /// liblts_bisim_gjkw.cpp contains wrapper functions `blue_is_smaller()` and
      53             : /// `red_is_smaller()` that call `finalise_work()` and `cancel_work()`.)
      54             : /// After all temporary work has been handled, call `check_temporary_work()` to
      55             : /// compare the amount of sensible work with the amount of cancelled work.
      56             : ///
      57             : /// If the work could be assigned to one of several counters (in particular, to
      58             : /// any one transition out of a set of transitions), I recommend to assign it
      59             : /// to all of them;  otherwise, it may happen that a later excess of the time
      60             : /// budget goes unnoticed because too few counters were advanced.
      61             : /// This, however, poses some difficulties when using temporary counters: a
      62             : /// single unit of work should be assigned to multiple counters, but added to
      63             : /// the balance between sensible and superfluous work only once.  A variant of
      64             : /// `add_work()`, namely `add_work_notemporary()`, can be called in that case:
      65             : /// it assigns a special value `DONT_COUNT_TEMPORARY` to a temporary counter
      66             : /// meaning that it should be disregarded in the calculation of the balance.
      67             : ///
      68             : /// \author David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands
      69             : 
      70             : #ifndef _CHECK_COMPLEXITY_H
      71             : #define _CHECK_COMPLEXITY_H
      72             : 
      73             : #include <cstring>       // for std::size_t and std::memset()
      74             : #include <cassert>
      75             : #include <cmath>         // for std::log2()
      76             : #include <climits>       // for CHAR_BIT and SIZE_MAX
      77             : 
      78             : #include "mcrl2/utilities/logger.h"
      79             : 
      80             : 
      81             : namespace mcrl2
      82             : {
      83             : namespace lts
      84             : {
      85             : namespace detail
      86             : {
      87             : 
      88             : /// \brief type used to store state (numbers and) counts
      89             : /// \details defined here because this is the most basic #include header that
      90             : /// uses it.
      91             : typedef std::size_t state_type;
      92             : #define STATE_TYPE_MIN ((state_type) 0)
      93             : #define STATE_TYPE_MAX SIZE_MAX
      94             : 
      95             : /// \brief type used to store transition (numbers and) counts
      96             : /// \details defined here because this is the most basic #include header that
      97             : /// uses it.
      98             : typedef std::size_t trans_type;
      99             : #define TRANS_TYPE_MIN ((trans_type) 0)
     100             : #define TRANS_TYPE_MAX SIZE_MAX
     101             : 
     102             : #ifndef NDEBUG
     103             : 
     104             : /// \brief type used to store differences between transition counters
     105             : typedef std::ptrdiff_t signed_trans_type;
     106             : 
     107             : namespace bisim_gjkw
     108             : {
     109             : 
     110             : /// \brief class for time complexity checks
     111             : /// \details The class stores (as static members) the global counters needed
     112             : /// for checking time complexity budgets.
     113             : ///
     114             : /// It could almost be defined as a namespace because all members are static.
     115             : /// Still, just a few members are private.
     116             : class check_complexity
     117             : {
     118             :   public:
     119             :     /// \brief Type for complexity budget counters
     120             :     /// \details The enumeration constants defined by this type are used to
     121             :     /// distinguish the many counters that the time budget check uses.
     122             :     /// There are counters assigned to blocks, states, B_to_C slices, and
     123             :     /// transitions.  Counters assigned to a block are regarded as if the work
     124             :     /// would be registered with every state in the block.  Counters assigned
     125             :     /// to a B_to_C slice are regarded as if the work would be registered with
     126             :     /// every transition in the slice.  (These conventions are important when
     127             :     /// splitting a block or a B_to_C slice.)
     128             :     enum counter_type
     129             :     {
     130             :         // block counters: every state in the block is regarded as visited.  In
     131             :         // this way, every state is ``visited'' O(log n) times.
     132             :         // Invariant: block->constln()->size() << (counter value) <= n
     133             :         while_C_contains_a_nontrivial_constellation_2_4 = 0,
     134             :                 BLOCK_MIN = while_C_contains_a_nontrivial_constellation_2_4,
     135             : 
     136             :         // If a loop runs over every state of a block exactly once, we simplify
     137             :         // the task of updating the counters by making the corresponding loop
     138             :         // counter a block counter:
     139             :         for_all_s_in_SpB_2_10,
     140             :             // Invariant of the following block counters:
     141             :             // block->size() << (counter value) <= n
     142             :         Move_Blue_or_Red_to_a_new_block_NewB_pointer_3_29,
     143             :         Move_Blue_or_Red_to_a_new_block_states_3_29,
     144             :         for_all_s_in_NewB_3_31,
     145             :                 BLOCK_MAX = for_all_s_in_NewB_3_31,
     146             : 
     147             :         // state counters: every state is visited O(log n) times
     148             :         // Invariant: s->block->size() << (counter value) <= n
     149             :         Move_Blue_or_Red_to_a_new_block_NewB_swap_3_29,
     150             :                 STATE_MIN = Move_Blue_or_Red_to_a_new_block_NewB_swap_3_29,
     151             : 
     152             :         // The following counters are used when one refines a block:  the first
     153             :         // group is used to store the amount of work that (a posteriori) turns
     154             :         // out to be useful.  After that, there are two groups of counters to
     155             :         // store temporary work.
     156             :         refine_bottom_state_3_6l,
     157             :         refine_visited_state_3_15,
     158             : 
     159             :         // temporary state counters (blue):
     160             :         while_Test_is_not_empty_3_6l_s_is_blue_3_11l,
     161             :                 STATE_MIN_TEMP = while_Test_is_not_empty_3_6l_s_is_blue_3_11l,
     162             :         while_Blue_contains_unvisited_states_3_15l,
     163             : 
     164             :         // temporary state counters (red):
     165             :         while_Red_contains_unvisited_states_3_15r,
     166             :                 STATE_MAX_TEMP = while_Red_contains_unvisited_states_3_15r,
     167             : 
     168             :         // new bottom state counters: every state is visited once
     169             :         // Invariant: if s is a non-bottom state, the counter is 0;
     170             :         // otherwise, the counter is 0 or 1.
     171             :         for_all_bottom_states_s_in_RfnB_4_8,
     172             :             // the next counter is used to count the work done on a virtual
     173             :             // self-loop in line 4.15 (the new bottom state is regarded as red
     174             :             // because it is in the splitter, but there is no transition to the
     175             :             // splitter).
     176             :         for_all_old_bottom_states_s_in_RedB_selfloop_4_15,
     177             :                 STATE_MAX = for_all_old_bottom_states_s_in_RedB_selfloop_4_15,
     178             : 
     179             :         // B_to_C_descriptor counters: every transition in the B_to_C-slice is
     180             :         // regarded as visited.  In this way, every transition is ``visited''
     181             :         // O(log n) times.
     182             :         // Invariant: to_constln()->size() << (counter value) <= n
     183             :         for_all_refinable_blocks_RfnB_2_20,
     184             :                 B_TO_C_MIN = for_all_refinable_blocks_RfnB_2_20,
     185             : 
     186             :         // If a loop runs over every transition in a B_to_C slice exactly once,
     187             :         // we simplify the task of updating the counters by making the
     188             :         // corresponding loop counter a B_to_C counter:
     189             :         Register_that_inert_transitions_from_s_go_to_NewC_B_to_C_2_17,
     190             :         // the following counter is also meant for temporary work.
     191             :         // Sometimes, after separating the new bottom states from the old ones,
     192             :         // a constellation is reachable from the block of the new bottom
     193             :         // states, but only from non-bottom states in this block.  In that
     194             :         // case, it cannot yet be determined which state will be a new bottom
     195             :         // state.  Then, the work is assigned temporarily to the B_to_C slice,
     196             :         // until some new bottom state is found to which to assign it.
     197             :         for_all_constellations_C_not_in_R_from_RfnB_4_4,
     198             :                B_TO_C_MIN_TEMP=for_all_constellations_C_not_in_R_from_RfnB_4_4,
     199             :                B_TO_C_MAX_TEMP=for_all_constellations_C_not_in_R_from_RfnB_4_4,
     200             :                B_TO_C_MAX = for_all_constellations_C_not_in_R_from_RfnB_4_4,
     201             : 
     202             :         // transition counters: every transition is visited O(log n) times
     203             :             // counters for transitions into the splitter NewC
     204             :             // Invariant: target->constln()->size() << (counter value) <= n
     205             :         for_all_s_prime_in_pred_s_2_11,
     206             :                 TRANS_MIN = for_all_s_prime_in_pred_s_2_11,
     207             :         Register_that_inert_transitions_from_s_go_to_NewC_succ_2_17,
     208             :         Register_that_inert_transitions_from_s_go_to_NewC_swap_2_17,
     209             :         refine_outgoing_transition_to_marked_state_3_6l,
     210             : 
     211             :             // counters for outgoing transitions
     212             :             // Invariant: source->block->size() << (counter value) <= n
     213             :         refine_outgoing_transition_3_6_or_23l,
     214             :         Move_Blue_or_Red_to_a_new_block_succ_3_29,
     215             :         for_all_s_prime_in_succ_s_3_32r,
     216             : 
     217             :             // counters for incoming transitions
     218             :             // Invariant: target->block->size() << (counter value) <= n
     219             :         refine_incoming_transition_3_18,
     220             :         for_all_s_prime_in_pred_s_3_32l,
     221             : 
     222             :         // temporary transition counters for refine: similar to the temporary
     223             :         // counters for states, we have a first group to store the work done
     224             :         // for the smaller half, and temporary counters to store the work until
     225             :         // it becomes clear which half wins.
     226             :             // Because we have to sort the transitions into those to NewC, the
     227             :             // outgoing and the incoming transitions, these counters are
     228             :             // distributed above.  The counters used to store the work done for
     229             :             // the smaller half are: refine_outgoing_transition_3_6_or_23l,
     230             :             // refine_outgoing_transition_to_marked_state_3_6l and
     231             :             // refine_incoming_transition_3_18.
     232             : 
     233             :         // temporary transition counters (blue):
     234             :         while_Test_is_not_empty_3_6l_s_is_red_3_9l,
     235             :                 TRANS_MIN_TEMP = while_Test_is_not_empty_3_6l_s_is_red_3_9l,
     236             :         while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing,
     237             :         for_all_s_prime_in_pred_s_setminus_Red_3_18l,
     238             :             // The work in the following counter is assigned to red (new
     239             :             // bottom) states if the blue block is smaller!
     240             :         if___s_prime_has_transition_to_SpC_3_23l,
     241             : 
     242             :         // temporary transition counters (red):
     243             :         while_FromRed_is_not_empty_3_6r,
     244             :         for_all_s_prime_in_pred_s_3_18r,
     245             :                 TRANS_MAX_TEMP = for_all_s_prime_in_pred_s_3_18r,
     246             : 
     247             :         // new bottom transition counters: every transition is visited once
     248             :         // Invariant: If source is a non-bottom state, the counter is 0;
     249             :         // otherwise, the counter is 0 or 1.
     250             :         refine_outgoing_transition_postprocess_new_bottom_3_6l,
     251             :         refine_outgoing_transition_from_new_bottom_3_23l,
     252             :             // For the following counters, we have an ``a priori'' and an ``a
     253             :             // posteriori'' variant.  The reason is, as explained with the
     254             :             // B_to_C slice counters, that sometimes a constellation is
     255             :             // reachable from the block of new bottom states but it is not yet
     256             :             // clear which of the source states will become a new bottom state.
     257             :             // In that case, the ``a posteriori'' counters are used.  Later,
     258             :             // the same block and the same constellation may be refined another
     259             :             // time, but now with known new bottom states; then, the ``a
     260             :             // priori'' counters are used.
     261             :         for_all_transitions_from_bottom_states_a_priori_4_4,
     262             :         for_all_transitions_from_bottom_states_a_posteriori_4_4,
     263             :         for_all_transitions_that_need_postproc_a_priori_4_12,
     264             :         for_all_transitions_that_need_postproc_a_posteriori_4_12,
     265             :         for_all_old_bottom_states_s_in_RedB_4_15,
     266             :                 TRANS_MAX = for_all_old_bottom_states_s_in_RedB_4_15,
     267             : 
     268             :         /*-------------- counters for the bisim_jgkw algorithm --------------*/
     269             : 
     270             :         // block counters
     271             :             // Block counters are used to assign some work to each state in the
     272             :             // block (and possibly, by transitivity, each incoming or outgoing
     273             :             // transition of the block).
     274             :         split_off_block,
     275             :                     BLOCK_dnj_MIN = split_off_block,
     276             :         adapt_transitions_for_new_block,
     277             :         create_initial_partition,
     278             :                     BLOCK_dnj_MAX = create_initial_partition,
     279             : 
     280             :         // state counters
     281             :             // If every state of a block is handled by some loop, we
     282             :             // abbreviate the counter to a block counter.
     283             :         split__find_predecessors_of_R_or_U_state,
     284             :                     STATE_dnj_MIN = split__find_predecessors_of_R_or_U_state,
     285             : 
     286             :         // temporary state counters (U-coroutine):
     287             :         split_U__find_predecessors_of_U_state,
     288             :                     STATE_dnj_MIN_TEMP = split_U__find_predecessors_of_U_state,
     289             : 
     290             :         // temporary state counters (R-coroutine):
     291             :         split_R__find_predecessors_of_R_state,
     292             :                     STATE_dnj_MAX_TEMP = split_R__find_predecessors_of_R_state,
     293             :         handle_new_noninert_transns,
     294             :                     STATE_dnj_MAX = handle_new_noninert_transns,
     295             : 
     296             :         // bunch counters (only for small bunches, i. e. bunches that have been
     297             :         // split off from a large bunch)
     298             :         refine_partition_until_stable__find_pred,
     299             :                     BUNCH_dnj_MIN = refine_partition_until_stable__find_pred,
     300             :                     BUNCH_dnj_MAX = refine_partition_until_stable__find_pred,
     301             : 
     302             :         // block_bunch-slice counters (only for block_bunch-slices that are
     303             :         // part of a small bunch)
     304             :         refine_partition_until_stable__stabilize,
     305             :                   BLOCK_BUNCH_dnj_MIN=refine_partition_until_stable__stabilize,
     306             :         refine_partition_until_stable__stabilize_for_large_splitter,
     307             :         handle_new_noninert_transns__make_unstable_temp,
     308             :                     BLOCK_BUNCH_dnj_MIN_TEMP =
     309             :                                handle_new_noninert_transns__make_unstable_temp,
     310             :                     BLOCK_BUNCH_dnj_MAX_TEMP =
     311             :                                handle_new_noninert_transns__make_unstable_temp,
     312             :                     BLOCK_BUNCH_dnj_MAX =
     313             :                                handle_new_noninert_transns__make_unstable_temp,
     314             : 
     315             :         // transition counters
     316             :             // If every transition of a state is handled by some loop, we
     317             :             // abbreviate the counter to a state counter (and possibly, by
     318             :             // transitivity, to a block counter).
     319             :         move_out_slice_to_new_block, // source block size
     320             :                     TRANS_dnj_MIN = move_out_slice_to_new_block,
     321             :         split__handle_transition_from_R_or_U_state, // source block size
     322             :         split__handle_transition_to_R_or_U_state, // target block size
     323             : 
     324             :         // temporary transition counters (U-coroutine):
     325             :         split_U__handle_transition_to_U_state, // target block size
     326             :                     TRANS_dnj_MIN_TEMP = split_U__handle_transition_to_U_state,
     327             :         split_U__test_noninert_transitions, // R: new bottom;
     328             :                                             // U: source block size
     329             : 
     330             :         // temporary transition counters (R-coroutine):
     331             :         split_R__handle_transition_from_R_state, // source block size
     332             :         split_R__handle_transition_to_R_state, // target block size
     333             :                     TRANS_dnj_MAX_TEMP = split_R__handle_transition_to_R_state,
     334             : 
     335             :         // transition counters for new bottom states:
     336             :         split__test_noninert_transitions_found_new_bottom_state,
     337             :         handle_new_noninert_transns__make_unstable_a_priori,
     338             :         handle_new_noninert_transns__make_unstable_a_posteriori,
     339             :         refine_partition_until_stable__stabilize_new_noninert_a_priori,
     340             :         refine_partition_until_stable__stabilize_new_noninert_a_posteriori,
     341             :             TRANS_dnj_MAX =
     342             :              refine_partition_until_stable__stabilize_new_noninert_a_posteriori
     343             :     };
     344             : 
     345             :     /// \brief special value for temporary work without changing the balance
     346             :     #define DONT_COUNT_TEMPORARY (std::numeric_limits<unsigned char>::max()-1)
     347             : 
     348             :     /// \brief value of floor(log2(n)) for easy access
     349             :     /// \details This variable has to be set by `init()` before counting work
     350             :     /// can begin.
     351             :     static unsigned char log_n;
     352             : 
     353             :     /// \brief calculate the base-2 logarithm, rounded down
     354             :     /// \details The function cannot be constexpr because std::log2() may have
     355             :     /// the side effect of setting `errno`.
     356      179435 :     static int ilog2(state_type size)
     357             :     {
     358             :         #ifdef __GNUC__
     359             :             if constexpr (sizeof(unsigned) == sizeof(size))
     360             :             {
     361             :                 return sizeof(size) * CHAR_BIT - 1 - __builtin_clz(size);
     362             :             }
     363             :             else if constexpr (sizeof(unsigned long) == sizeof(size))
     364             :             {
     365      179435 :                 return sizeof(size) * CHAR_BIT - 1 - __builtin_clzl(size);
     366             :             }
     367             :             else if constexpr(sizeof(unsigned long long) == sizeof(size))
     368             :             {
     369             :                 return sizeof(size) * CHAR_BIT - 1 - __builtin_clzll(size);
     370             :             }
     371             :         //#elif defined(_MSC_VER)
     372             :         //    if constexpr (sizeof(long) == sizeof(size))
     373             :         //    {
     374             :         //        long result;
     375             :         //        _BitScanReverse(result, size);
     376             :         //        return result - 1;
     377             :         //    }
     378             :         //    else if constexpr(sizeof(__int64) == sizeof(size))
     379             :         //    {
     380             :         //        long result;
     381             :         //        _BitScanReverse64(result, size);
     382             :         //        return result - 1;
     383             :         //    }
     384             :         #endif
     385             :         return (int) std::log2(size);
     386             :     }
     387             : 
     388             :   private:
     389             :     /// \brief counter to register the work balance for coroutines
     390             :     /// \details Sensible work will be counted positively, and cancelled work
     391             :     /// negatively.
     392             :     static signed_trans_type sensible_work;
     393             : 
     394             :   public:
     395             :     /// \brief printable names of the counter types (for error messages)
     396             :     static const char *work_names[TRANS_dnj_MAX - BLOCK_MIN + 1];
     397             : 
     398             :     /// \brief check that not too much superfluous work has been done
     399             :     /// \details After having moved all temporary work counters to the normal
     400             :     /// counters, this function can be used to ensure that not too much
     401             :     /// temporary work is cancelled.
     402        1561 :     static void check_temporary_work()
     403             :     {
     404        1561 :         assert(-1 <= sensible_work);
     405        1561 :         sensible_work = 0;
     406        1561 :     }
     407             : 
     408             :     /// \brief subset of counters (to be associated with a state or transition)
     409             :     template <enum counter_type FirstCounter, enum counter_type LastCounter,
     410             :                   enum counter_type FirstTempCounter =
     411             :                                          (enum counter_type) (LastCounter + 1),
     412             :                   enum counter_type FirstPostprocessCounter = FirstTempCounter>
     413             :     class counter_t
     414             :     {
     415             :         static_assert(FirstCounter < FirstTempCounter);
     416             :         static_assert(FirstTempCounter <= FirstPostprocessCounter);
     417             :         static_assert(FirstPostprocessCounter <=
     418             :                                         (enum counter_type) (LastCounter + 1));
     419             :       public:
     420             :         /// \brief actual space to store the counters
     421             :         unsigned char counters[LastCounter - FirstCounter + 1];
     422             : 
     423             :         /// \brief cancel temporary work
     424             :         /// \details The function registers that all counters from `first` to
     425             :         /// `last` (inclusive) are counting superfluous work.  It adds them to
     426             :         /// the pool of superfluous work.
     427             :         /// \param ctr  temporary counter whose work is superfluous
     428             :         /// \returns false  iff some counter was too large.  In that case, also
     429             :         ///                 the beginning of an error message is printed.
     430             :         ///                 The function should be called through the macro
     431             :         ///                 `mCRL2complexity()`, because that macro will print
     432             :         ///                 the remainder of the error message as needed.
     433       40888 :         bool cancel_work(enum counter_type const ctr)
     434             :         {
     435       40888 :             assert(FirstTempCounter <= ctr);
     436       40888 :             assert(ctr < FirstPostprocessCounter);
     437       28425 :             if ((FirstTempCounter != TRANS_MIN_TEMP &&
     438       28425 :                  FirstTempCounter != TRANS_dnj_MIN_TEMP) ||
     439       28425 :                           DONT_COUNT_TEMPORARY != counters[ctr - FirstCounter])
     440             :             {
     441       40887 :                 assert(counters[ctr - FirstCounter] <= 1);
     442       40887 :                 sensible_work -= counters[ctr - FirstCounter];
     443             :             }
     444       40888 :             counters[ctr - FirstCounter] = 0;
     445       40888 :             return true;
     446             :         }
     447             : 
     448             : 
     449             :         /// \brief move temporary work to its final counter
     450             :         /// \details The function moves work from a temporary counter to a
     451             :         /// normal counter.  It also checks that the normal counter does not
     452             :         /// get too large.
     453             :         /// \param from       temporary counter from where work is moved
     454             :         /// \param to         normal counter to which work is moved
     455             :         /// \param max_value  maximal allowed value to the normal counter.  The
     456             :         ///                   old value of the counter should be strictly
     457             :         ///                   smaller.
     458             :         /// \returns false  iff the counter was too large.  In that case, also
     459             :         ///                 the beginning of an error message is printed.
     460             :         ///                 The function should be called through the macro
     461             :         ///                 `mCRL2complexity()`, because that macro will print
     462             :         ///                 the remainder of the error message as needed.
     463       17923 :         bool finalise_work(enum counter_type const from,
     464             :                           enum counter_type const to, unsigned const max_value)
     465             :         {
     466             :             // assert(...) -- see move_work().
     467       15790 :             if ((FirstTempCounter != TRANS_MIN_TEMP &&
     468       15790 :                  FirstTempCounter != TRANS_dnj_MIN_TEMP) ||
     469       15790 :                          DONT_COUNT_TEMPORARY != counters[from - FirstCounter])
     470             :             {
     471       17918 :                 sensible_work += counters[from - FirstCounter];
     472             :             }
     473             :             else
     474             :             {
     475           5 :                 counters[from - FirstCounter] = 1;
     476             :             }
     477       17923 :             return move_work(from, to, max_value);
     478             :         }
     479             : 
     480             : 
     481             :         /// \brief constructor, initializes all counters to 0
     482       11578 :         counter_t()
     483             :         {
     484       11578 :             std::memset(counters, '\0', sizeof(counters));
     485       11578 :         }
     486             : 
     487             : 
     488             :         /// \brief register work with some counter
     489             :         /// \details The function increases a work counter to a larger value.
     490             :         /// It is also checked that the counter does not get too large.
     491             :         /// The function is normally called through the macro
     492             :         /// `mCRL2complexity()`.
     493             :         /// \param ctr        counter with which work is registered
     494             :         /// \param max_value  maximal allowed value of the counter.  The old
     495             :         ///                   value of the counter should be strictly smaller.
     496             :         /// \returns false  iff the counter was too large.  In that case, also
     497             :         ///                 the beginning of an error message is printed.
     498             :         ///                 The function should be called through the macro
     499             :         ///                 `mCRL2complexity()`, because that macro will print
     500             :         ///                 the remainder of the error message as needed.
     501       13488 :         bool add_work(enum counter_type const ctr, unsigned const max_value)
     502             :         {
     503       13488 :             assert(FirstCounter <= ctr);
     504       13488 :             assert(ctr <= LastCounter);
     505       13488 :             assert(max_value <= (ctr < FirstTempCounter ? log_n : 1U));
     506       13488 :             if (counters[ctr - FirstCounter] >= max_value)
     507             :             {
     508           0 :                 mCRL2log(log::error) << "Error 1: counter \""
     509           0 :                         << work_names[ctr - BLOCK_MIN] << "\" exceeded "
     510           0 :                                     "maximum value (" << max_value << ") for ";
     511           0 :                 return false;
     512             :             }
     513       13488 :             counters[ctr - FirstCounter] = max_value;
     514       13488 :             return true;
     515             :         }
     516             : 
     517             : 
     518             :         /// \brief move temporary work to another counter
     519             :         /// \details The function moves work from a temporary counter to
     520             :         /// another temporary or a normal counter.  It also checks that the new
     521             :         /// counter does not get too large.
     522             :         /// The function is normally called through the macro
     523             :         /// `mCRL2complexity()`.
     524             :         /// \param from       temporary counter from where work is moved
     525             :         /// \param to         (temporary or normal) counter to which work is
     526             :         ///                   moved
     527             :         /// \param max_value  maximal allowed value to the normal counter.  The
     528             :         ///                   old value of the counter should be strictly
     529             :         ///                   smaller.
     530             :         /// \returns false  iff the new counter was too large.  In that case,
     531             :         ///                 also the beginning of an error message is printed.
     532             :         ///                 The function should be called through the macro
     533             :         ///                 `mCRL2complexity()`, because that macro will print
     534             :         ///                 the remainder of the error message as needed.
     535       17923 :         bool move_work(enum counter_type const from,
     536             :                           enum counter_type const to, unsigned const max_value)
     537             :         {
     538       17923 :             assert(FirstTempCounter <= from);
     539       17923 :             assert(from < FirstPostprocessCounter);
     540       17923 :             assert(FirstCounter <= to);
     541       17923 :             assert(to <= LastCounter);
     542       17923 :             assert(max_value <= (to < FirstTempCounter ? log_n : 1U));
     543       17923 :             if (0 == counters[from - FirstCounter])  return true;
     544        1772 :             if (counters[to - FirstCounter] >= max_value)
     545             :             {
     546           0 :                 mCRL2log(log::error) << "Error 2: counter \""
     547           0 :                         << work_names[to - BLOCK_MIN] << "\" exceeded "
     548           0 :                                     "maximum value (" << max_value << ") for ";
     549           0 :                 return false;
     550             :             }
     551             :             /*
     552             :             if ((FirstTempCounter == TRANS_MIN_TEMP ||
     553             :                  FirstTempCounter == TRANS_dnj_MIN_TEMP) &&
     554             :                     FirstTempCounter <= to && to < FirstPostprocessCounter &&
     555             :                          DONT_COUNT_TEMPORARY == counters[from - FirstCounter])
     556             :             {
     557             :                 assert(1 == max_value);
     558             :                 // the next assertion is always satisfied if 1 == max_value.
     559             :                 // assert(0 == counters[to - FirstCounter]);
     560             :                 counters[to - FirstCounter] = DONT_COUNT_TEMPORARY;
     561             :             }
     562             :             else
     563             :             */
     564             :             {
     565        1772 :                 counters[to - FirstCounter] = max_value;
     566        1772 :                 assert(1 == counters[from - FirstCounter]);
     567             :             }
     568        1772 :             counters[from - FirstCounter] = 0;
     569        1772 :             return true;
     570             :         }
     571             :     };
     572             : 
     573             : 
     574             :     // usage of the functions below: as soon as the block is refined, one
     575             :     // has to call state_counter_t::blue_is_smaller() or state_counter_t::
     576             :     // red_is_smaller() for every state in the old and new block.  Also, one
     577             :     // needs to call trans_counter_t::blue_is_smaller() or trans_counter_t::
     578             :     // red_is_smaller() for every incoming and outgoing transition in the old
     579             :     // and new block.  (Inert transitions need to be handled only once.)  After
     580             :     // that, one calls check_temporary_work() to verify that not too much
     581             :     // work was done on the larger block.
     582             : 
     583             :     /// \brief counters for a block
     584             :     /// \details The counters stored with a block are meant to be assigned to
     585             :     /// each state in the block.  This means that the counter values need to be
     586             :     /// copied when the block is split.
     587         556 :     class block_counter_t : public counter_t<BLOCK_MIN, BLOCK_MAX>
     588             :     {
     589             :       public:
     590             :         /// \brief ensures there is no orphaned temporary work counter
     591             :         /// \details When a refinement has finished, all work registered with
     592             :         /// temporary counters should have been moved to normal counters.  This
     593             :         /// function verifies this property.
     594             :         /// The function additionally ensures that no work counter exceeds its
     595             :         /// maximal allowed value, based on the size of the block or its
     596             :         /// constellation.  (The size of the constellation is the unit used for
     597             :         /// counters related to [blocks in the] splitter constellation;  the
     598             :         /// size of the block is used for other counters.)
     599             :         /// \param max_C  ilog2(n) - ilog2(size of constellation)
     600             :         /// \param max_B  ilog2(n) - ilog2(size of block)
     601             :         /// \returns false  iff some temporary counter was nonzero.  In that
     602             :         ///                 case, also the beginning of an error message is
     603             :         ///                 printed.  The function should be called through the
     604             :         ///                 macro `mCRL2complexity()`, because that macro will
     605             :         ///                 print the remainder of the error message as needed.
     606       10406 :         bool no_temporary_work(unsigned const max_C, unsigned const max_B)
     607             :         {
     608       10406 :             assert(max_C <= max_B);
     609       31218 :             for (enum counter_type ctr = BLOCK_MIN;
     610       31218 :                        ctr < Move_Blue_or_Red_to_a_new_block_NewB_pointer_3_29;
     611       20812 :                                            ctr = (enum counter_type) (ctr + 1))
     612             :             {
     613       20812 :                 assert(counters[ctr - BLOCK_MIN] <= max_C);
     614       20812 :                 counters[ctr - BLOCK_MIN] = max_C;
     615             :             }
     616       10406 :             assert(max_B <= log_n);
     617       41624 :             for (enum counter_type ctr =
     618             :                          Move_Blue_or_Red_to_a_new_block_NewB_pointer_3_29;
     619       72842 :                          ctr <= BLOCK_MAX; ctr = (enum counter_type) (ctr + 1))
     620             :             {
     621       31218 :                 assert(counters[ctr - BLOCK_MIN] <= max_B);
     622       31218 :                 counters[ctr - BLOCK_MIN] = max_B;
     623             :             }
     624       10406 :             return true;
     625             :         }
     626             :     };
     627             : 
     628             :     /// \brief counters for a B_to_C slice
     629             :     /// \details The counters stored with a B_to_C slice are meant to be
     630             :     /// assigned to each transition in the slice.  This means that the counter
     631             :     /// values need to be copied when the slice is split.
     632        1334 :     class B_to_C_counter_t : public counter_t<B_TO_C_MIN, B_TO_C_MAX,
     633             :                     B_TO_C_MIN_TEMP, (enum counter_type) (B_TO_C_MAX_TEMP + 1)>
     634             :     {
     635             :       public:
     636             :         /// \brief ensures there is no orphaned temporary work counter
     637             :         /// \details When a refinement has finished, all work registered with
     638             :         /// temporary counters should have been moved to normal counters.  This
     639             :         /// function verifies this property.
     640             :         /// The function additionally ensures that no work counter exceeds its
     641             :         /// maximal allowed value, based on the size of the target
     642             :         /// constellation.
     643             :         /// \param max_targetC  ilog2(n) - ilog2(size of target constellation)
     644             :         /// \returns false  iff some temporary counter was nonzero.  In that
     645             :         ///                 case, also the beginning of an error message is
     646             :         ///                 printed.  The function should be called through the
     647             :         ///                 macro `mCRL2complexity()`, because that macro will
     648             :         ///                 print the remainder of the error message as needed.
     649       14116 :         bool no_temporary_work(unsigned const max_targetC)
     650             :         {
     651       14116 :             assert(max_targetC <= log_n);
     652       42348 :             for (enum counter_type ctr = B_TO_C_MIN;
     653       70580 :                     ctr < B_TO_C_MIN_TEMP; ctr = (enum counter_type) (ctr + 1))
     654             :             {
     655       28232 :                 assert(counters[ctr - B_TO_C_MIN] <= max_targetC);
     656       28232 :                 counters[ctr - B_TO_C_MIN] = max_targetC;
     657             :             }
     658       28232 :             for (enum counter_type ctr = B_TO_C_MIN_TEMP;
     659       42348 :                    ctr <= B_TO_C_MAX_TEMP; ctr = (enum counter_type) (ctr + 1))
     660             :             {
     661       14116 :                 if (counters[ctr - B_TO_C_MIN] > 0)
     662             :                 {
     663           0 :                     mCRL2log(log::error) << "Error 3: counter \""
     664             :                         << work_names[ctr - BLOCK_MIN] << "\" exceeded "
     665           0 :                                             "maximum value (" << 0 << ") for ";
     666           0 :                     return false;
     667             :                 }
     668             :             }
     669             :             static_assert(B_TO_C_MAX_TEMP == B_TO_C_MAX);
     670       14116 :             return true;
     671             :         }
     672             : 
     673             : 
     674             :         /// \brief returns the _temporary_ counter associated with line 4.4
     675             :         /// \details The counter associated with line 4.4 is used when some
     676             :         /// constellation is reachable from a block containing new bottom
     677             :         /// states but it is not yet clear which states are the new bottom
     678             :         /// states that can reach the constellation.  Then, the work is
     679             :         /// temporarily assigned to the B_to_C slice until it has become clear
     680             :         /// to which new bottom states it can be assigned.
     681             :         ///
     682             :         /// We cannot use the normal mechanism of `move_work()` here because
     683             :         /// the normal counters are transition counters, not B_to_C slice
     684             :         /// counters.
     685             :         ///
     686             :         /// This function helps to decide whether the work still needs to be
     687             :         /// moved from the temporary counter to a normal counter.
     688             :         /// \returns the value of the _temporary_ counter associated with
     689             :         ///          line 4.4
     690          66 :         unsigned char get_work_counter_4_4() const
     691             :         {
     692             :             return counters[for_all_constellations_C_not_in_R_from_RfnB_4_4 -
     693          66 :                                                                    B_TO_C_MIN];
     694             :         }
     695             : 
     696             : 
     697             :         /// \brief sets the temporary counter associated with line 4.4 to zero
     698             :         /// \details The counter associated with line 4.4 is needed when some
     699             :         /// constellation is reachable from a block containing new bottom
     700             :         /// states but it is not yet clear which states are the new bottom
     701             :         /// states that can reach the constellation.  Then, the work is
     702             :         /// temporarily assigned to the B_to_C slice until it has become clear
     703             :         /// to which new bottom states it has to be assigned.
     704             :         ///
     705             :         /// We cannot use the normal mechanism of `move_work()` here because
     706             :         /// the normal counters are transition counters, not B_to_C slice
     707             :         /// counters.
     708             :         ///
     709             :         /// This function resets the temporary work counter and is meant to be
     710             :         /// called as soon as the work can be assigned to normal counters.
     711           3 :         void reset_work_counter_4_4()
     712             :         {
     713             :             counters[for_all_constellations_C_not_in_R_from_RfnB_4_4 -
     714           3 :                                                                B_TO_C_MIN] = 0;
     715           3 :         }
     716             :     };
     717         982 :     class state_counter_t : public counter_t<STATE_MIN, STATE_MAX,
     718             :                       STATE_MIN_TEMP, (enum counter_type) (STATE_MAX_TEMP + 1)>
     719             :     {
     720             :       public:
     721             :         /// \brief ensures there is no orphaned temporary work counter
     722             :         /// \details When a refinement has finished, all work registered with
     723             :         /// temporary counters should have been moved to normal counters.
     724             :         /// Further, there should not be any work ascribed to bottom-state
     725             :         /// counters in non-bottom states, but only to (new) bottom states.
     726             :         /// This function verifies these properties.  It also sets all counters
     727             :         /// for bottom states to 1 so that later no more work can be assigned
     728             :         /// to them.
     729             :         /// The function additionally ensures that no work counter exceeds its
     730             :         /// maximal allowed value, based on the size of the block of which the
     731             :         /// state is a member.
     732             :         /// \param max_B    log2(n) - log2(size of the block containing this
     733             :         ///                 state)
     734             :         /// \param bottom   `true` iff the state to which these counters belong
     735             :         ///                 is a bottom state
     736             :         /// \returns false  iff some temporary counter or some bottom-state
     737             :         ///                 counter of a non-bottom state was nonzero.  In that
     738             :         ///                 case, also the beginning of an error message is
     739             :         ///                 printed.  The function should be called through the
     740             :         ///                 macro `mCRL2complexity()`, because that macro will
     741             :         ///                 print the remainder of the error message as needed.
     742       26233 :         bool no_temporary_work(unsigned const max_B, bool const bottom)
     743             :         {
     744       26233 :             assert(max_B <= log_n);
     745      104932 :             for (enum counter_type ctr = STATE_MIN;
     746      183631 :                      ctr < STATE_MIN_TEMP; ctr = (enum counter_type) (ctr + 1))
     747             :             {
     748       78699 :                 assert(counters[ctr - STATE_MIN] <= max_B);
     749       78699 :                 counters[ctr - STATE_MIN] = max_B;
     750             :             }
     751             : 
     752             :             // temporary state counters must be zero:
     753      104932 :             for (enum counter_type ctr = STATE_MIN_TEMP;
     754      183631 :                     ctr <= STATE_MAX_TEMP; ctr = (enum counter_type) (ctr + 1))
     755             :             {
     756       78699 :                 if (counters[ctr - STATE_MIN] > 0)
     757             :                 {
     758           0 :                     mCRL2log(log::error) << "Error 4: counter \""
     759             :                         << work_names[ctr - BLOCK_MIN] << "\" exceeded "
     760           0 :                                             "maximum value (" << 0 << ") for ";
     761           0 :                     return false;
     762             :                 }
     763             :             }
     764             :             // bottom state counters must be 0 for non-bottom states and 1 for
     765             :             // bottom states:
     766             :             // assert((unsigned) bottom <= 1);
     767       78699 :             for(enum counter_type ctr = (enum counter_type) (STATE_MAX_TEMP+1);
     768      131165 :                         ctr <= STATE_MAX ; ctr = (enum counter_type) (ctr + 1))
     769             :             {
     770       52466 :                 if (counters[ctr - STATE_MIN] > (unsigned) bottom)
     771             :                 {
     772           0 :                     mCRL2log(log::error) << "Error 5: counter \""
     773             :                         << work_names[ctr - BLOCK_MIN] << "\" exceeded "
     774           0 :                             "maximum value (" << (unsigned) bottom << ") for ";
     775           0 :                     return false;
     776             :                 }
     777       52466 :                 counters[ctr - STATE_MIN] = (unsigned) bottom;
     778             :             }
     779       26233 :             return true;
     780             :         }
     781             :     };
     782        1116 :     class trans_counter_t : public counter_t<TRANS_MIN, TRANS_MAX,
     783             :                       TRANS_MIN_TEMP, (enum counter_type) (TRANS_MAX_TEMP + 1)>
     784             :     {
     785             :       public:
     786             :         /// \brief ensures there is no orphaned temporary work counter
     787             :         /// \details When a refinement has finished, all work registered with
     788             :         /// temporary counters should have been moved to normal counters.
     789             :         /// Further, there should not be any work ascribed to bottom-state
     790             :         /// counters in transitions from non-bottom states, but only to
     791             :         /// transitions from (new) bottom states.  This function verifies these
     792             :         /// properties.  It also sets all counters for bottom states to 1 so
     793             :         /// that later no more work can be assigned to them.
     794             :         /// The function additionally ensures that no work counter exceeds its
     795             :         /// maximal allowed value, based on the size of the source block,
     796             :         /// target block or target constellation.  (The constellation size is
     797             :         /// the relevant unit for counters that are related to transitions into
     798             :         /// the splitter, which is the constellation `NewC`.  The block size is
     799             :         /// the unit for counters that are related to refinements.  Because
     800             :         /// some parts of a refinement look at incoming transitions of the
     801             :         /// refined block and others at outgoing transitions, we need two block
     802             :         /// sizes.)
     803             :         /// \param max_sourceB    the maximum allowed value for work counters
     804             :         ///                       based on the source state of the transition
     805             :         /// \param max_targetC    the maximum allowed value for work counters
     806             :         ///                       based on the target constellation
     807             :         /// \param max_targetB    the maximum allowed value for work counters
     808             :         ///                       based on the target block
     809             :         /// \param source_bottom  `true` iff the transition to which these
     810             :         ///                       counters belong starts in a bottom state
     811             :         /// \returns false  iff some temporary counter or some bottom-state
     812             :         ///                 counter of a transition with non-bottom source was
     813             :         ///                 nonzero.  In that case, also the beginning of an
     814             :         ///                 error message is printed.  The function should be
     815             :         ///                 called through the macro `mCRL2complexity()`,
     816             :         ///                 because that macro will print the remainder of the
     817             :         ///                 error message as needed.
     818       33225 :         bool no_temporary_work(unsigned const max_sourceB,
     819             :                           unsigned const max_targetC,
     820             :                           unsigned const max_targetB, bool const source_bottom)
     821             :         {
     822       33225 :             assert(max_targetC <= max_targetB);
     823      166125 :             for (enum counter_type ctr = TRANS_MIN;
     824      166125 :                                    ctr < refine_outgoing_transition_3_6_or_23l;
     825      132900 :                                            ctr = (enum counter_type) (ctr + 1))
     826             :             {
     827      132900 :                 assert(counters[ctr - TRANS_MIN] <= max_targetC);
     828      132900 :                 counters[ctr - TRANS_MIN] = max_targetC;
     829             :             }
     830       33225 :             assert(max_sourceB <= log_n);
     831      132900 :             for (enum counter_type ctr = refine_outgoing_transition_3_6_or_23l;
     832      132900 :                                          ctr < refine_incoming_transition_3_18;
     833       99675 :                                            ctr = (enum counter_type) (ctr + 1))
     834             :             {
     835       99675 :                 assert(counters[ctr - TRANS_MIN] <= max_sourceB);
     836       99675 :                 counters[ctr - TRANS_MIN] = max_sourceB;
     837             :             }
     838       33225 :             assert(max_targetB <= log_n);
     839       99675 :             for (enum counter_type ctr = refine_incoming_transition_3_18;
     840      166125 :                      ctr < TRANS_MIN_TEMP; ctr = (enum counter_type) (ctr + 1))
     841             :             {
     842       66450 :                 assert(counters[ctr - TRANS_MIN] <= max_targetB);
     843       66450 :                 counters[ctr - TRANS_MIN] = max_targetB;
     844             :             }
     845             :             // temporary transition counters must be zero
     846      232575 :             for (enum counter_type ctr = TRANS_MIN_TEMP;
     847      431925 :                      ctr <= TRANS_MAX_TEMP; ctr = (enum counter_type)(ctr + 1))
     848             :             {
     849      199350 :                 if (counters[ctr - TRANS_MIN] > 0)
     850             :                 {
     851           0 :                     mCRL2log(log::error) << "Error 6: counter \""
     852             :                         << work_names[ctr - BLOCK_MIN] << "\" exceeded "
     853           0 :                                             "maximum value (" << 0 << ") for ";
     854           0 :                     return false;
     855             :                 }
     856             :             }
     857             :             // bottom state counters must be 0 for transitions from non-bottom
     858             :             // states and 1 for other transitions
     859             :             assert((unsigned) source_bottom <= 1);
     860      265800 :             for(enum counter_type ctr = (enum counter_type) (TRANS_MAX_TEMP+1);
     861      498375 :                         ctr <= TRANS_MAX ; ctr = (enum counter_type) (ctr + 1))
     862             :             {
     863      232575 :                 if (counters[ctr - TRANS_MIN] > (unsigned) source_bottom)
     864             :                 {
     865           0 :                     mCRL2log(log::error) << "Error 7: counter \""
     866             :                         << work_names[ctr - BLOCK_MIN] << "\" exceeded "
     867           0 :                      "maximum value (" << (unsigned) source_bottom << ") for ";
     868           0 :                     return false;
     869             :                 }
     870      232575 :                 counters[ctr - TRANS_MIN] = (unsigned) source_bottom;
     871             :             }
     872       33225 :             return true;
     873             :         }
     874             : 
     875             : 
     876             :         /// \brief register work with some temporary counter without changing
     877             :         /// the balance between sensible and superfluous work
     878             :         /// \details The function increases a temporary work counter.  It is
     879             :         /// also checked that the counter does not get too large.  This variant
     880             :         /// of `add_work()` should be used if one wants to assign a single step
     881             :         /// of work to multiple temporary counters of transitions:  for one of
     882             :         /// them, the normal `add_work()` is called, and for the others
     883             :         /// `add_work_notemporary()`.
     884             :         /// \param ctr        counter with which work is registered
     885             :         /// \param max_value  maximal allowed value of the counter.  The old
     886             :         ///                   value of the counter should be strictly smaller.
     887             :         ///                   (Because it is a temporary counter, only `1` is
     888             :         ///                   sensible.)
     889             :         /// \returns false  iff the counter was too large.  In that case, also
     890             :         ///                 the beginning of an error message is printed.
     891             :         ///                 The function should be called through the macro
     892             :         ///                 `mCRL2complexity()`, because that macro will print
     893             :         ///                 the remainder of the error message as needed.
     894          31 :         bool add_work_notemporary(enum counter_type const ctr,
     895             :                                                       unsigned const max_value)
     896             :         {
     897          31 :             if (TRANS_MIN_TEMP > ctr || ctr > TRANS_MAX_TEMP)
     898             :             {
     899          27 :                 return add_work(ctr, max_value);
     900             :             }
     901             : 
     902           4 :             assert(1 == max_value);
     903           4 :             if (0 == counters[ctr - TRANS_MIN])
     904             :             {
     905           4 :                 counters[ctr - TRANS_MIN] = DONT_COUNT_TEMPORARY;
     906           4 :                 return true;
     907             :             }
     908             : 
     909           0 :             mCRL2log(log::error) << "Error 8: counter \""
     910             :                         << work_names[ctr - BLOCK_MIN] << "\" exceeded "
     911           0 :                                     "maximum value (" << max_value << ") for ";
     912           0 :             return false;
     913             :         }
     914             :     };
     915             : 
     916             :     /*----------------- class specialisations for bisim_dnj -----------------*/
     917             : 
     918         848 :     class block_dnj_counter_t : public counter_t<BLOCK_dnj_MIN, BLOCK_dnj_MAX,
     919             :                                                       create_initial_partition>
     920             :     {
     921             :       public:
     922             :         /// \brief ensures there is no orphaned temporary work counter
     923             :         /// \details When a refinement has finished, all work registered with
     924             :         /// temporary counters should have been moved to normal counters.  This
     925             :         /// function verifies this property.
     926             :         /// The function additionally ensures that no work counter exceeds its
     927             :         /// maximal allowed value, based on the size of the block or its
     928             :         /// constellation.  (The size of the constellation is the unit used for
     929             :         /// counters related to [blocks in the] splitter constellation;  the
     930             :         /// size of the block is used for other counters.)
     931             :         /// \param max_block ilog2(n^2) - ilog2(size of block)
     932             :         /// \returns false  iff some temporary counter was nonzero.  In that
     933             :         ///                 case, also the beginning of an error message is
     934             :         ///                 printed.  The function should be called through the
     935             :         ///                 macro `mCRL2complexity()`, because that macro will
     936             :         ///                 print the remainder of the error message as needed.
     937        6764 :         bool no_temporary_work(unsigned const max_block)
     938             :         {
     939        6764 :             assert((log_n + 1U) / 2U <= max_block);
     940        6764 :             if (max_block > log_n)
     941             :             {
     942           0 :                     mCRL2log(log::error) << "Error 14: max_block == "
     943           0 :                                          << max_block << " exceeded log_n == "
     944           0 :                                          << (unsigned) log_n << " for ";
     945           0 :                     return false;
     946             :             }
     947        6764 :             assert(max_block <= log_n);
     948       20292 :             for (enum counter_type ctr = BLOCK_dnj_MIN;
     949       20292 :                                 ctr < create_initial_partition;
     950       13528 :                                            ctr = (enum counter_type) (ctr + 1))
     951             :             {
     952       13528 :                 assert(counters[ctr - BLOCK_dnj_MIN] <= max_block);
     953       13528 :                 counters[ctr - BLOCK_dnj_MIN] = max_block;
     954             :             }
     955       13528 :             for (enum counter_type ctr = create_initial_partition;
     956       20292 :                      ctr <= BLOCK_dnj_MAX; ctr = (enum counter_type) (ctr + 1))
     957             :             {
     958        6764 :                 assert(counters[ctr - BLOCK_dnj_MIN] <= 1);
     959        6764 :                 counters[ctr - BLOCK_dnj_MIN] = 1;
     960             :             }
     961        6764 :             return true;
     962             :         }
     963             :     };
     964             : 
     965        1494 :     class state_dnj_counter_t : public counter_t<STATE_dnj_MIN, STATE_dnj_MAX,
     966             :               STATE_dnj_MIN_TEMP, (enum counter_type) (STATE_dnj_MAX_TEMP + 1)>
     967             :     {
     968             :       public:
     969             :         /// \brief ensures there is no orphaned temporary work counter
     970             :         /// \details When a refinement has finished, all work registered with
     971             :         /// temporary counters should have been moved to normal counters.  This
     972             :         /// function verifies this property.
     973             :         /// The function additionally ensures that no work counter exceeds its
     974             :         /// maximal allowed value, based on the size of the block or its
     975             :         /// constellation.  (The size of the constellation is the unit used for
     976             :         /// counters related to [blocks in the] splitter constellation;  the
     977             :         /// size of the block is used for other counters.)
     978             :         /// \param max_block ilog2(n^2) - ilog2(size of block)
     979             :         /// \returns false  iff some temporary counter was nonzero.  In that
     980             :         ///                 case, also the beginning of an error message is
     981             :         ///                 printed.  The function should be called through the
     982             :         ///                 macro `mCRL2complexity()`, because that macro will
     983             :         ///                 print the remainder of the error message as needed.
     984       16141 :         bool no_temporary_work(unsigned const max_block, bool const bottom)
     985             :         {
     986       16141 :             assert((log_n + 1U) / 2U <= max_block);
     987       16141 :             assert(max_block <= log_n);
     988       32282 :             for (enum counter_type ctr = STATE_dnj_MIN;
     989       48423 :                  ctr < STATE_dnj_MIN_TEMP; ctr = (enum counter_type) (ctr + 1))
     990             :             {
     991       16141 :                 assert(counters[ctr - STATE_dnj_MIN] <= max_block);
     992       16141 :                 counters[ctr - STATE_dnj_MIN] = max_block;
     993             :             }
     994       48423 :             for (enum counter_type ctr = STATE_dnj_MIN_TEMP;
     995       80705 :                 ctr <= STATE_dnj_MAX_TEMP; ctr = (enum counter_type) (ctr + 1))
     996             :             {
     997       32282 :                 assert(counters[ctr - STATE_dnj_MIN] <= 0);
     998             :             }
     999             :             // assert((unsigned) bottom <= 1);
    1000       32282 :             for (enum counter_type ctr =
    1001             :                     (enum counter_type) (STATE_dnj_MAX_TEMP + 1);
    1002       48423 :                      ctr <= STATE_dnj_MAX; ctr = (enum counter_type) (ctr + 1))
    1003             :             {
    1004       16141 :                 assert(counters[ctr - STATE_dnj_MIN] <= (unsigned) bottom);
    1005       16141 :                 counters[ctr - STATE_dnj_MIN] = (unsigned) bottom;
    1006             :             }
    1007       16141 :             return true;
    1008             :         }
    1009             :     };
    1010             : 
    1011        1112 :     class bunch_dnj_counter_t : public counter_t<BUNCH_dnj_MIN, BUNCH_dnj_MAX>
    1012             :     {
    1013             :       public:
    1014             :         /// \brief ensures there is no orphaned temporary work counter
    1015             :         /// \details When a refinement has finished, all work registered with
    1016             :         /// temporary counters should have been moved to normal counters.  This
    1017             :         /// function verifies this property.
    1018             :         /// The function additionally ensures that no work counter exceeds its
    1019             :         /// maximal allowed value, based on the size of the block or its
    1020             :         /// constellation.  (The size of the constellation is the unit used for
    1021             :         /// counters related to [blocks in the] splitter constellation;  the
    1022             :         /// size of the block is used for other counters.)
    1023             :         /// \param max_bunch ilog2(n^2) - ilog2(size of bunch)
    1024             :         /// \returns false  iff some temporary counter was nonzero.  In that
    1025             :         ///                 case, also the beginning of an error message is
    1026             :         ///                 printed.  The function should be called through the
    1027             :         ///                 macro `mCRL2complexity()`, because that macro will
    1028             :         ///                 print the remainder of the error message as needed.
    1029        8583 :         bool no_temporary_work(unsigned const max_bunch)
    1030             :         {
    1031        8583 :             assert(max_bunch <= log_n);
    1032       17166 :             for (enum counter_type ctr = BUNCH_dnj_MIN;
    1033       25749 :                      ctr <= BUNCH_dnj_MAX; ctr = (enum counter_type) (ctr + 1))
    1034             :             {
    1035        8583 :                 assert(counters[ctr - BUNCH_dnj_MIN] <= max_bunch);
    1036        8583 :                 counters[ctr - BUNCH_dnj_MIN] = max_bunch;
    1037             :             }
    1038        8583 :             return true;
    1039             :         }
    1040             :     };
    1041             : 
    1042        1744 :     class block_bunch_dnj_counter_t : public counter_t<BLOCK_BUNCH_dnj_MIN,
    1043             :                         BLOCK_BUNCH_dnj_MAX, BLOCK_BUNCH_dnj_MIN_TEMP,
    1044             :                             (enum counter_type) (BLOCK_BUNCH_dnj_MAX_TEMP + 1)>
    1045             :     {
    1046             :       public:
    1047             :         /// \brief ensures there is no orphaned temporary work counter
    1048             :         /// \details When a refinement has finished, all work registered with
    1049             :         /// temporary counters should have been moved to normal counters.  This
    1050             :         /// function verifies this property.
    1051             :         /// The function additionally ensures that no work counter exceeds its
    1052             :         /// maximal allowed value, based on the size of the block or its
    1053             :         /// constellation.  (The size of the constellation is the unit used for
    1054             :         /// counters related to [blocks in the] splitter constellation;  the
    1055             :         /// size of the block is used for other counters.)
    1056             :         /// \param max_bunch ilog2(n^2) - ilog2(size of bunch)
    1057             :         /// \returns false  iff some temporary counter was nonzero.  In that
    1058             :         ///                 case, also the beginning of an error message is
    1059             :         ///                 printed.  The function should be called through the
    1060             :         ///                 macro `mCRL2complexity()`, because that macro will
    1061             :         ///                 print the remainder of the error message as needed.
    1062       12742 :         bool no_temporary_work(unsigned const max_bunch)
    1063             :         {
    1064       12742 :             assert(max_bunch <= log_n);
    1065       38226 :             for (enum counter_type ctr = BLOCK_BUNCH_dnj_MIN;
    1066       38226 :                             ctr < BLOCK_BUNCH_dnj_MIN_TEMP;
    1067       25484 :                                            ctr = (enum counter_type) (ctr + 1))
    1068             :             {
    1069       25484 :                 if (counters[ctr - BLOCK_BUNCH_dnj_MIN] > max_bunch)
    1070             :                 {
    1071           0 :                     mCRL2log(log::error) << "Error 12: counter \""
    1072             :                         << work_names[ctr - BLOCK_MIN] << "\" exceeded "
    1073           0 :                         "maximum value (" << (unsigned) max_bunch << ") for ";
    1074           0 :                     return false;
    1075             :                 }
    1076       25484 :                 assert(counters[ctr - BLOCK_BUNCH_dnj_MIN] <= max_bunch);
    1077       25484 :                 counters[ctr - BLOCK_BUNCH_dnj_MIN] = max_bunch;
    1078             :             }
    1079       25484 :             for (enum counter_type ctr = BLOCK_BUNCH_dnj_MIN_TEMP;
    1080       38226 :                ctr <= BLOCK_BUNCH_dnj_MAX; ctr = (enum counter_type) (ctr + 1))
    1081             :             {
    1082       12742 :                 if (counters[ctr - BLOCK_BUNCH_dnj_MIN] > 0)
    1083             :                 {
    1084           0 :                     mCRL2log(log::error) << "Error 13: counter \""
    1085             :                         << work_names[ctr - BLOCK_MIN] << "\" exceeded "
    1086           0 :                         "maximum value (" << (unsigned) 0 << ") for ";
    1087           0 :                     return false;
    1088             :                 }
    1089       12742 :                 assert(counters[ctr - BLOCK_BUNCH_dnj_MIN] <= 0);
    1090             :             }
    1091             :             static_assert(BLOCK_BUNCH_dnj_MAX_TEMP == BLOCK_BUNCH_dnj_MAX);
    1092       12742 :             return true;
    1093             :         }
    1094             : 
    1095         889 :         bool has_temporary_work()
    1096             :         {
    1097             :             static_assert(BLOCK_BUNCH_dnj_MIN_TEMP==BLOCK_BUNCH_dnj_MAX_TEMP);
    1098         889 :             return counters[BLOCK_BUNCH_dnj_MIN_TEMP-BLOCK_BUNCH_dnj_MIN] > 0;
    1099             :         }
    1100           4 :         void reset_temporary_work()
    1101             :         {
    1102             :             static_assert(BLOCK_BUNCH_dnj_MIN_TEMP==BLOCK_BUNCH_dnj_MAX_TEMP);
    1103           4 :             counters[BLOCK_BUNCH_dnj_MIN_TEMP - BLOCK_BUNCH_dnj_MIN] = 0;
    1104           4 :         }
    1105             :     };
    1106             : 
    1107        2392 :     class trans_dnj_counter_t : public counter_t<TRANS_dnj_MIN, TRANS_dnj_MAX,
    1108             :               TRANS_dnj_MIN_TEMP, (enum counter_type) (TRANS_dnj_MAX_TEMP + 1)>
    1109             :     {
    1110             :       public:
    1111             :         /// \brief ensures there is no orphaned temporary work counter
    1112             :         /// \details When a refinement has finished, all work registered with
    1113             :         /// temporary counters should have been moved to normal counters.  This
    1114             :         /// function verifies this property.
    1115             :         /// The function additionally ensures that no work counter exceeds its
    1116             :         /// maximal allowed value, based on the size of the block or its
    1117             :         /// constellation.  (The size of the constellation is the unit used for
    1118             :         /// counters related to [blocks in the] splitter constellation;  the
    1119             :         /// size of the block is used for other counters.)
    1120             :         /// \param max_source_block  ilog2(n) - ilog2(size of source block)
    1121             :         /// \param max_target_block  ilog2(n) - ilog2(size of target block)
    1122             :         /// \param bottom true iff the transition source is a bottom state
    1123             :         /// \returns false  iff some temporary counter was nonzero.  In that
    1124             :         ///                 case, also the beginning of an error message is
    1125             :         ///                 printed.  The function should be called through the
    1126             :         ///                 macro `mCRL2complexity()`, because that macro will
    1127             :         ///                 print the remainder of the error message as needed.
    1128       30215 :         bool no_temporary_work(unsigned const max_source_block,
    1129             :                             unsigned const max_target_block, bool const bottom)
    1130             :         {
    1131       30215 :             assert((log_n + 1U) / 2U <= max_source_block);
    1132       30215 :             assert(max_source_block <= log_n);
    1133       90645 :             for (enum counter_type ctr = TRANS_dnj_MIN;
    1134       90645 :                         ctr < split__handle_transition_to_R_or_U_state;
    1135       60430 :                                            ctr = (enum counter_type) (ctr + 1))
    1136             :             {
    1137       60430 :                 assert(counters[ctr - TRANS_dnj_MIN] <= max_source_block);
    1138       60430 :                 counters[ctr - TRANS_dnj_MIN] = max_source_block;
    1139             :             }
    1140       30215 :             assert((log_n + 1U) / 2U <= max_target_block);
    1141       30215 :             assert(max_target_block <= log_n);
    1142       60430 :             for(enum counter_type ctr=split__handle_transition_to_R_or_U_state;
    1143       60430 :                         ctr < TRANS_dnj_MIN_TEMP;
    1144       30215 :                                            ctr = (enum counter_type) (ctr + 1))
    1145             :             {
    1146       30215 :                 assert(counters[ctr - TRANS_dnj_MIN] <= max_target_block);
    1147       30215 :                 counters[ctr - TRANS_dnj_MIN] = max_target_block;
    1148             :             }
    1149      151075 :             for (enum counter_type ctr = TRANS_dnj_MIN_TEMP;
    1150      271935 :                 ctr <= TRANS_dnj_MAX_TEMP; ctr = (enum counter_type) (ctr + 1))
    1151             :             {
    1152      120860 :                 assert(counters[ctr - TRANS_dnj_MIN] <= 0);
    1153             :             }
    1154             :             // assert((unsigned) bottom <= 1);
    1155      181290 :             for (enum counter_type ctr =
    1156             :                     (enum counter_type) (TRANS_dnj_MAX_TEMP + 1);
    1157      332365 :                      ctr <= TRANS_dnj_MAX; ctr = (enum counter_type) (ctr + 1))
    1158             :             {
    1159      151075 :                 if (counters[ctr - TRANS_dnj_MIN] > (unsigned) bottom)
    1160             :                 {
    1161           0 :                     mCRL2log(log::error) << "Error 11: counter \""
    1162             :                         << work_names[ctr - BLOCK_MIN] << "\" exceeded "
    1163           0 :                             "maximum value (" << (unsigned) bottom << ") for ";
    1164           0 :                     return false;
    1165             :                 }
    1166      151075 :                 counters[ctr - TRANS_dnj_MIN] = (unsigned) bottom;
    1167             :             }
    1168       30215 :             return true;
    1169             :         }
    1170             : 
    1171             :         /// \brief register work with some temporary counter without changing
    1172             :         /// the balance between sensible and superfluous work
    1173             :         /// \details The function increases a temporary work counter.  It is
    1174             :         /// also checked that the counter does not get too large.  This variant
    1175             :         /// of `add_work()` should be used if one wants to assign a single step
    1176             :         /// of work to multiple temporary counters of transitions:  for one of
    1177             :         /// them, the normal `add_work()` is called, and for the others
    1178             :         /// `add_work_notemporary()`.
    1179             :         /// \param ctr        counter with which work is registered
    1180             :         /// \param max_value  maximal allowed value of the counter.  The old
    1181             :         ///                   value of the counter should be strictly smaller.
    1182             :         ///                   (Because it is a temporary counter, only `1` is
    1183             :         ///                   sensible.)
    1184             :         /// \returns false  iff the counter was too large.  In that case, also
    1185             :         ///                 the beginning of an error message is printed.
    1186             :         ///                 The function should be called through the macro
    1187             :         ///                 `mCRL2complexity()`, because that macro will print
    1188             :         ///                 the remainder of the error message as needed.
    1189           2 :         bool add_work_notemporary(enum counter_type const ctr,
    1190             :                                                       unsigned const max_value)
    1191             :         {
    1192           2 :             if (TRANS_dnj_MIN_TEMP > ctr || ctr > TRANS_dnj_MAX_TEMP)
    1193             :             {
    1194           0 :                 return add_work(ctr, max_value);
    1195             :             }
    1196             : 
    1197           2 :             assert(1 == max_value);
    1198           2 :             if (0 == counters[ctr - TRANS_dnj_MIN])
    1199             :             {
    1200           2 :                 counters[ctr - TRANS_dnj_MIN] = DONT_COUNT_TEMPORARY;
    1201           2 :                 return true;
    1202             :             }
    1203             : 
    1204           0 :             mCRL2log(log::error) << "Error 9: counter \""
    1205             :                         << work_names[ctr - BLOCK_MIN] << "\" exceeded "
    1206           0 :                                     "maximum value (" << max_value << ") for ";
    1207           0 :             return false;
    1208             :         }
    1209             :     };
    1210             : 
    1211             :     #if 0
    1212             :         /// \brief prints a message for each counter, for debugging purposes
    1213             :         /// \details The function can be called, e. g., from
    1214             :         /// `check_complexity::init()`.  However, as it is not
    1215             :         /// actually called, it is disabled by default.
    1216             :         static void test_work_names();
    1217             :     #endif
    1218             : 
    1219             : 
    1220             :     /// \brief starts counting for a new refinement run
    1221             :     /// \details Before any work can be counted, `init()` should be called to
    1222             :     /// set the size of the state space to the appropriate value.
    1223             :     /// \param n  size of the state space
    1224         229 :     static void init(state_type n)
    1225             :     {
    1226             :         #if 0
    1227             :             // as debugging measure:
    1228             :             test_work_names();
    1229             :         #endif
    1230             : 
    1231         229 :         log_n = ilog2(n);
    1232         229 :         assert(0 == sensible_work);     sensible_work = 0;
    1233         229 :     }
    1234             : 
    1235             : 
    1236             :     /// \brief Assigns work to a counter and checks for errors
    1237             :     /// \details Many functions that assign work to a counter actually return
    1238             :     /// `true` if everything is ok and `false` if the counter was too large.
    1239             :     /// In the latter case, they also print the start of an error message
    1240             :     /// (``Counter ... too large''), but as they do not know to which larger
    1241             :     /// unit (state, transition etc.) the counter belongs, this macro prints
    1242             :     /// the end of the error message and aborts the program with a return code
    1243             :     /// indicating failure.
    1244             :     ///
    1245             :     /// If debugging is off, the macro is translated to do nothing.
    1246             :     /// \param unit   the unit to which work is assigned
    1247             :     /// \param call   a function call that assigns work to a counter of `unit`
    1248             :     #define mCRL2complexity(unit, call, ...)                                  \
    1249             :             do                                                                \
    1250             :             {                                                                 \
    1251             :                 if (!((unit)->work_counter. call ))                           \
    1252             :                 {                                                             \
    1253             :                     mCRL2log(log::error)<<(unit)->debug_id(__VA_ARGS__)<<'\n';\
    1254             :                     exit(EXIT_FAILURE);                                       \
    1255             :                 }                                                             \
    1256             :                 /* else                                                       \
    1257             :                 {                                                             \
    1258             :                     mCRL2log(log::debug, "bisim_dnj") << "mCRL2complexity("   \
    1259             :                          << (unit)->debug_id(__VA_ARGS__) << ", " #call ")\n";\
    1260             :                 } */                                                          \
    1261             :             }                                                                 \
    1262             :             while (0)
    1263             : 
    1264             : };
    1265             : 
    1266             : } // end namespace bisim_gjkw
    1267             : 
    1268             : #else // ifndef NDEBUG
    1269             : 
    1270             :     #define mCRL2complexity(unit, call, ...) /* ignore unit and call */
    1271             : 
    1272             : #endif // ifndef NDEBUG
    1273             : 
    1274             : } // end namespace detail
    1275             : } // end namespace lts
    1276             : } // end namespace mcrl2
    1277             : 
    1278             : #endif // ifndef _COUNT_ITERATIONS_H

Generated by: LCOV version 1.13