LCOV - code coverage report
Current view: top level - lts/source - liblts_bisim_gjkw.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 1163 1307 89.0 %
Date: 2020-09-16 00:45:56 Functions: 20 37 54.1 %
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 liblts_bisim_gjkw.cpp
      11             : ///
      12             : /// \brief O(m log n)-time stuttering equivalence algorithm
      13             : ///
      14             : /// \details This file implements the efficient partition refinement algorithm
      15             : /// by Groote / Jansen / Keiren / Wijs to calculate the stuttering equivalence
      16             : /// quotient of a Kripke structure.  (Labelled transition systems are converted
      17             : /// to Kripke structures before the main algorithm).
      18             : /// The file accompanies the planned publication in the ACM Trans. Comput. Log.
      19             : /// Log. special issue for TACAS 2016, to appear in 2017.
      20             : ///
      21             : /// \author David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands
      22             : 
      23             : #include "mcrl2/lts/detail/liblts_bisim_gjkw.h"
      24             : #include "mcrl2/lts/detail/coroutine.h"
      25             : #include "mcrl2/lts/lts_aut.h"
      26             : #include "mcrl2/lts/lts_fsm.h"
      27             : #include "mcrl2/lts/lts_utilities.h"
      28             : 
      29             : #define PARANOID_CHECK
      30             : 
      31             : namespace mcrl2
      32             : {
      33             : namespace lts
      34             : {
      35             : namespace detail
      36             : {
      37             : namespace bisim_gjkw
      38             : {
      39             : 
      40             : 
      41             : 
      42             : 
      43             : 
      44             : /* ************************************************************************* */
      45             : /*                                                                           */
      46             : /*                   R E F I N A B L E   P A R T I T I O N                   */
      47             : /*                                                                           */
      48             : /* ************************************************************************* */
      49             : 
      50             : 
      51             : 
      52             : 
      53             : 
      54             : block_t* block_t::refinable_first = nullptr;
      55             : state_type block_t::nr_of_blocks = 0;
      56             : constln_t* constln_t::nontrivial_first = nullptr;
      57             :                                                                                 #ifndef NDEBUG
      58             :                                                                                     // These variables are only accessed in debug mode.  In release mode,
      59             :                                                                                     // accessing them would lead to a linker error.
      60             :                                                                                     state_info_const_ptr state_info_entry::s_i_begin;
      61             :                                                                                     state_info_const_ptr state_info_entry::s_i_end;
      62             :                                                                                     permutation_const_iter_t block_t::perm_begin;
      63             :                                                                                 #endif
      64             : /// \brief refine the block (the blue subblock is smaller)
      65             : /// \details This function is called after a refinement function has found
      66             : /// that the blue subblock is the smaller one.  It creates a new block for
      67             : /// the blue states.
      68             : /// \param blue_nonbottom_end iterator past the last blue non-bottom state
      69             : /// \returns pointer to the new (blue) block
      70          57 : block_t* block_t::split_off_blue(permutation_iter_t const blue_nonbottom_end)
      71          57 : {                                                                               assert(unmarked_nonbottom_end() >= blue_nonbottom_end);
      72          57 :                                                                                 assert(unmarked_nonbottom_begin() <= blue_nonbottom_end);
      73          57 :                                                                                 assert(0 != unmarked_bottom_size());
      74             :     permutation_iter_t const splitpoint = blue_nonbottom_end +
      75          57 :                                                         unmarked_bottom_size(); assert(splitpoint < end());  assert(begin() < splitpoint);
      76             :                                                                                 #ifndef NDEBUG
      77         114 :                                                                                     unsigned const max_counter = check_complexity::log_n -
      78         114 :     /* It is not necessary to reset the nottoblue counters; these counters   */                   check_complexity::ilog2((state_type) (splitpoint - begin()));
      79          57 :     /* are anyway only valid for the maybe-blue states.                      */     assert((state_type) (splitpoint - begin()) <= size()/2);
      80             :                                                                                 #endif
      81         171 :     if (state_type swapcount = std::min(unmarked_bottom_size(),
      82         171 :                    (state_type) (marked_nonbottom_end() - blue_nonbottom_end));
      83             :                                                                 0 != swapcount)
      84             :     {
      85             :         // vector swap the states:
      86          39 :         permutation_iter_t pos1=blue_nonbottom_end, pos2=unmarked_bottom_end();
      87          39 :         state_info_ptr const temp = *pos1;
      88             :         for (;;)
      89             :         {
      90          85 :             --pos2;                                                             mCRL2complexity(*pos2, add_work(check_complexity::
      91             :                                                                                                Move_Blue_or_Red_to_a_new_block_NewB_swap_3_29, max_counter), );
      92          62 :             *pos1 = *pos2;
      93          62 :             (*pos1)->pos = pos1;
      94          62 :             ++pos1;
      95          62 :             if (0 == --swapcount)  break;
      96          23 :             *pos2 = *pos1;
      97          23 :             (*pos2)-> pos = pos2;
      98             :         }
      99          39 :         *pos2 = temp;
     100          39 :         (*pos2)->pos = pos2;
     101             :     }
     102             : 
     103             :     // create a new block for the blue states
     104          57 :     block_t* const NewB = new block_t(constln(), begin(), splitpoint);
     105             :                                                                                 #ifndef NDEBUG
     106          57 :                                                                                     NewB->work_counter = work_counter;
     107             :                                                                                 #endif
     108          57 :     if (BLOCK_NO_SEQNR != seqnr())
     109             :     {
     110          47 :         NewB->assign_seqnr();
     111             :     }
     112             :     // NewB->set_begin(begin());
     113          57 :     NewB->set_bottom_begin(blue_nonbottom_end);
     114          57 :     NewB->set_marked_nonbottom_begin(blue_nonbottom_end);
     115             :     // NewB->set_marked_bottom_begin(splitpoint);
     116          57 :     /* NewB->set_end(splitpoint);                                            */ assert(NewB->to_constln.empty());
     117          57 :     /* NewB->set_inert_begin(?);                                             */ mCRL2complexity(NewB, add_work(check_complexity::
     118             :     /* NewB->set_inert_end(?);                                               */             Move_Blue_or_Red_to_a_new_block_NewB_pointer_3_29, max_counter), );
     119         211 :     for(permutation_iter_t s_iter=NewB->begin(); NewB->end()!=s_iter; ++s_iter)
     120             :     {                                                                           // mCRL2complexity(*s_iter, ...) -- optimized to the above call.
     121         154 :         (*s_iter)->block = NewB;
     122             :     }
     123             : 
     124             :     // adapt the old block: it only keeps the red states
     125             :     // set_end(end());
     126          57 :     set_bottom_begin(marked_bottom_begin());
     127             :     // set_marked_bottom_begin(marked_bottom_begin());
     128          57 :     set_marked_nonbottom_begin(marked_bottom_begin());
     129          57 :     set_begin(splitpoint);
     130             : 
     131          57 :     constln()->make_nontrivial();
     132             : 
     133          57 :     return NewB;
     134             : }
     135             : 
     136             : /// \brief refine the block (the red subblock is smaller)
     137             : /// \details This function is called after a refinement function has found
     138             : /// that the red subblock is the smaller one.  It creates a new block for
     139             : /// the red states.
     140             : ///
     141             : /// Both `split_off_blue()` and `split_off_red()` unmark all states in the blue
     142             : /// subblock and mark all bottom states in the red subblock.  (This will help
     143             : /// the caller to distinguish old bottom states from new bottom states found
     144             : /// after `split_off_blue()` or `split_off_red()`, respectively.)  The two
     145             : /// functions use the same complexity counters because their operations belong
     146             : /// together.
     147             : /// \param red_nonbottom_begin iterator to the first red non-bottom state
     148             : /// \returns pointer to the new (red) block
     149         308 : block_t* block_t::split_off_red(permutation_iter_t const red_nonbottom_begin)
     150         308 : {                                                                               assert(marked_nonbottom_begin() == red_nonbottom_begin);
     151         308 :                                                                                 assert(marked_nonbottom_end() >= red_nonbottom_begin);
     152         308 :                                                                                 assert(0 != marked_size());
     153             :     permutation_iter_t const splitpoint = red_nonbottom_begin +
     154         308 :                                                         unmarked_bottom_size(); assert(begin() < splitpoint);  assert(splitpoint < end());
     155             :                                                                                 #ifndef NDEBUG
     156         616 :                                                                                     unsigned const max_counter = check_complexity::log_n -
     157         616 :     /* It is not necessary to reset the nottoblue counters; these counters   */                     check_complexity::ilog2((state_type) (end() - splitpoint));
     158         308 :     /* are anyway only valid for the maybe-blue states.                      */     assert((state_type) (end() - splitpoint) <= size() / 2);
     159             :                                                                                 #endif
     160         924 :     if (state_type swapcount = std::min(unmarked_bottom_size(),
     161         924 :                   (state_type) (marked_nonbottom_end() - red_nonbottom_begin));
     162             :                                                                 0 != swapcount)
     163             :     {
     164             :         // vector swap the states:
     165          55 :         permutation_iter_t pos1=red_nonbottom_begin,pos2=unmarked_bottom_end();
     166          55 :         state_info_ptr const temp = *pos1;
     167          57 :         for (;;)
     168         112 :         {                                                                       mCRL2complexity(*pos1, add_work(check_complexity::
     169             :                                                                                                Move_Blue_or_Red_to_a_new_block_NewB_swap_3_29, max_counter), );
     170         112 :             *pos1 = *--pos2;
     171         112 :             (*pos1)->pos = pos1;
     172         112 :             ++pos1;
     173         112 :             if (0 == --swapcount)  break;
     174          57 :             *pos2 = *pos1;
     175          57 :             (*pos2)->pos = pos2;
     176             :         }
     177          55 :         *pos2 = temp;
     178          55 :         (*pos2)->pos = pos2;
     179             :     }
     180             :     // create a new block for the red states
     181         308 :     block_t* const NewB = new block_t(constln(), splitpoint, end());
     182             :                                                                                 #ifndef NDEBUG
     183         308 :                                                                                     NewB->work_counter = work_counter;
     184             :                                                                                 #endif
     185         308 :     if (BLOCK_NO_SEQNR != seqnr())
     186             :     {
     187         177 :         NewB->assign_seqnr();
     188             :     }
     189             :     // NewB->set_end(end());
     190         308 :     NewB->set_marked_bottom_begin(marked_bottom_begin());
     191         308 :     NewB->set_bottom_begin(marked_bottom_begin());
     192         308 :     NewB->set_marked_nonbottom_begin(marked_bottom_begin());
     193         308 :     /* NewB->set_begin(splitpoint);                                          */ assert(NewB->to_constln.empty());
     194         308 :     /* NewB->set_inert_begin(?);                                             */ mCRL2complexity(NewB, add_work(check_complexity::
     195             :     /* NewB->set_inert_end(?);                                               */             Move_Blue_or_Red_to_a_new_block_NewB_pointer_3_29, max_counter), );
     196         842 :     for(permutation_iter_t s_iter=NewB->begin(); NewB->end()!=s_iter; ++s_iter)
     197             :     {                                                                           // mCRL2complexity(*s_iter, ...) -- optimized to the above call.
     198         534 :         (*s_iter)->block = NewB;
     199             :     }
     200             : 
     201             :     // adapt the old block: it only keeps the blue states
     202             :     // set_begin(begin());
     203         308 :     set_marked_nonbottom_begin(red_nonbottom_begin);
     204         308 :     set_bottom_begin(red_nonbottom_begin);
     205         308 :     set_marked_bottom_begin(splitpoint);
     206         308 :     set_end(splitpoint);
     207             : 
     208         308 :     constln()->make_nontrivial();
     209             : 
     210         308 :     return NewB;
     211             : }
     212             :                                                                                 #ifndef NDEBUG
     213             :                                                                                     /// \brief print a slice of the partition (typically a block)
     214             :                                                                                     /// \details If the slice indicated by the parameters is not empty, the
     215             :                                                                                     /// states in this slice will be printed.
     216             :                                                                                     /// \param message text printed as a title if the slice is not empty
     217             :                                                                                     /// \param B       block that is being printed (it is checked whether
     218             :                                                                                     ///                states belong to this block)
     219             :                                                                                     /// \param begin   iterator to the beginning of the slice
     220             :                                                                                     /// \param end     iterator past the end of the slice
     221           0 :                                                                                     void part_state_t::print_block(const char* const message,
     222             :                                                                                                                       const block_t* const B,
     223             :                                                                                                                       permutation_const_iter_t begin,
     224             :                                                                                                                       permutation_const_iter_t const end) const
     225             :                                                                                     {
     226           0 :                                                                                         if (0 != end - begin)
     227             :                                                                                         {
     228           0 :                                                                                             mCRL2log(log::debug, "bisim_gjkw") << "\t\t" << message
     229           0 :                                                                                                                            << (1 < end-begin ? "s:\n" : ":\n");
     230           0 :                                                                                             do
     231             :                                                                                             {
     232           0 :                                                                                                 mCRL2log(log::debug, "bisim_gjkw") << "\t\t\t"
     233           0 :                                                                                                                                        << (*begin)->debug_id();
     234           0 :                                                                                                 if (B != (*begin)->block)
     235             :                                                                                                 {
     236           0 :                                                                                                     mCRL2log(log::debug,"bisim_gjkw") << ", inconsistent: "
     237           0 :                                                                                                                    "points to " << (*begin)->block->debug_id();
     238             :                                                                                                 }
     239           0 :                                                                                                 if (begin != (*begin)->pos)
     240             :                                                                                                 {
     241           0 :                                                                                                     mCRL2log(log::debug, "bisim_gjkw")
     242           0 :                                                                                                                << ", inconsistent pointer to state_info_entry";
     243             :                                                                                                 }
     244           0 :                                                                                                 mCRL2log(log::debug, "bisim_gjkw") << '\n';
     245             :                                                                                             }
     246           0 :                                                                                             while (++begin != end);
     247             :                                                                                         }
     248           0 :                                                                                     }
     249             : 
     250             :                                                                                     /// \brief print the partition as a tree (per constellation and block)
     251             :                                                                                     /// \details The function prints all constellations (in order); for each
     252             :                                                                                     /// constellation it prints the blocks it consists of; and for each block,
     253             :                                                                                     /// it lists its states, separated into nonbottom and bottom states.
     254             :                                                                                     /// \param part_tr partition for the transitions
     255           0 :                                                                                     void part_state_t::print_part(const part_trans_t& part_tr) const
     256             :                                                                                     {
     257           0 :                                                                                         assert(permutation.begin() < permutation.end());
     258           0 :                                                                                         for (const constln_t* C = permutation.front()->constln(); ; )
     259             :                                                                                         {
     260           0 :                                                                                             mCRL2log(log::debug, "bisim_gjkw") << C->debug_id() << ":\n";
     261           0 :                                                                                             assert(C->begin() < C->end());
     262           0 :                                                                                             for (const block_t* B = (*C->begin())->block; ; )
     263             :                                                                                             {
     264           0 :                                                                                                 mCRL2log(log::debug, "bisim_gjkw") << "\t" << B->debug_id();
     265           0 :                                                                                                 if (C != B->constln())
     266             :                                                                                                 {
     267           0 :                                                                                                     mCRL2log(log::debug,"bisim_gjkw") << ", inconsistent: "
     268           0 :                                                                                                                       "points to " << B->constln()->debug_id();
     269             :                                                                                                 }
     270           0 :                                                                                                 mCRL2log(log::debug, "bisim_gjkw") << ":\n";
     271           0 :                                                                                                 print_block("Non-bottom state", B, B->nonbottom_begin(),
     272             :                                                                                                                                            B->nonbottom_end());
     273           0 :                                                                                                 print_block("Bottom state", B, B->bottom_begin(),
     274             :                                                                                                                                               B->bottom_end());
     275           0 :                                                                                                 mCRL2log(log::debug, "bisim_gjkw") << "\t\tThis block has ";
     276           0 :                                                                                                 if (B->inert_end() == part_tr.B_to_C_begin())
     277             :                                                                                                 {
     278           0 :                                                                                                     mCRL2log(log::debug, "bisim_gjkw")
     279           0 :                                                                                                                << "no transitions to its own constellation.\n";
     280           0 :                                                                                                     assert(B->inert_begin() == B->inert_end());
     281             :                                                                                                 }
     282             :                                                                                                 else
     283             :                                                                                                 {
     284           0 :                                                                                                     assert(B->inert_end() ==
     285             :                                                                                                                          B->inert_end()[-1].B_to_C_slice->end);
     286           0 :                                                                                                     assert(B->inert_end()[-1].B_to_C_slice->from_block() == B);
     287           0 :                                                                                                     assert(B->inert_end()[-1].B_to_C_slice->to_constln() == C);
     288           0 :                                                                                                     mCRL2log(log::debug, "bisim_gjkw") << B->inert_end() -
     289           0 :                                                                                                                          B->inert_end()[-1].B_to_C_slice->begin
     290           0 :                                                                                                     <<" transition(s) to its own constellation,\n\t\tof which "
     291           0 :                                                                                                                      << B->inert_end() - B->inert_begin()
     292           0 :                                                                                                                      << (1 == B->inert_end() - B->inert_begin()
     293           0 :                                                                                                                            ? " is inert.\n" : " are inert.\n");
     294             :                                                                                                 }
     295             :                                                                                                 // go to next block
     296           0 :                                                                                                 if (C->end() == B->end())  break;
     297           0 :                                                                                                 B = (*B->end())->block;
     298             :                                                                                             }
     299             :                                                                                             // go to next constellation
     300           0 :                                                                                             if (permutation.end() == C->end())  break;
     301           0 :                                                                                             C = (*C->end())->constln();
     302           0 :                                                                                         }
     303           0 :                                                                                     }
     304             : 
     305             :                                                                                     /// \brief print all transitions
     306             :                                                                                     /// \details For each state (in order), its outgoing transitions are
     307             :                                                                                     /// listed, sorted by goal constellation.  The function also indicates
     308             :                                                                                     /// where the current constellation pointer of the state points at.
     309           0 :                                                                                     void part_state_t::print_trans() const
     310             :                                                                                     {
     311             :                                                                                         fixed_vector<state_info_entry>::const_iterator const state_info_end =
     312           0 :                                                                                                                                           state_info.end() - 1;
     313           0 :                                                                                         for (fixed_vector<state_info_entry>::const_iterator state_iter =
     314           0 :                                                                                                 state_info.begin(); state_info_end != state_iter; ++state_iter)
     315             :                                                                                         {
     316             :                                                                                             // print transitions out of state
     317           0 :                                                                                             succ_const_iter_t succ_constln_iter = state_iter->succ_begin();
     318           0 :                                                                                             if (state_iter->succ_end() != succ_constln_iter)
     319             :                                                                                             {
     320           0 :                                                                                                 mCRL2log(log::debug, "bisim_gjkw") << state_iter->debug_id()
     321           0 :                                                                                                                                                       << ":\n";
     322           0 :                                                                                                 assert(state_iter->succ_begin() <=
     323             :                                                                                                                                state_iter->inert_succ_begin());
     324           0 :                                                                                                 assert(state_iter->inert_succ_begin() <=
     325             :                                                                                                                                  state_iter->inert_succ_end());
     326           0 :                                                                                                 assert(state_iter->succ_begin()==state_iter->inert_succ_begin()
     327             :                                                                                                     || *state_iter->inert_succ_begin()[-1].target->constln() <=
     328             :                                                                                                                                        *state_iter->constln());
     329           0 :                                                                                                 assert(state_iter->succ_begin()==state_iter->inert_succ_begin()
     330             :                                                                                                     || state_iter->inert_succ_begin()[-1].target->block !=
     331             :                                                                                                                                             state_iter->block);
     332           0 :                                                                                                 assert(state_iter->inert_succ_begin() ==
     333             :                                                                                                                                 state_iter->inert_succ_end() ||
     334             :                                                                                                           (state_iter->inert_succ_begin()->target->block ==
     335             :                                                                                                                                            state_iter->block &&
     336             :                                                                                                            state_iter->inert_succ_end()[-1].target->block ==
     337             :                                                                                                                                            state_iter->block));
     338           0 :                                                                                                 assert(state_iter->succ_end() == state_iter->inert_succ_end()||
     339             :                                                                                                              *state_iter->constln() <
     340             :                                                                                                              *state_iter->inert_succ_end()->target->constln());
     341           0 :                                                                                                 do
     342             :                                                                                                 {
     343             :                                                                                                     // print transitions to a constellation
     344           0 :                                                                                                     mCRL2log(log::debug, "bisim_gjkw") << "\ttransitions to "
     345           0 :                                                                                                             << succ_constln_iter->target->constln()->debug_id()
     346           0 :                                                                                                                                                       << ":\n";
     347           0 :                                                                                                     succ_const_iter_t s_iter = succ_constln_iter;
     348             :                                                                                                     // set succ_constln_iter to the end of the transitions to
     349             :                                                                                                     // this constellation
     350           0 :                                                                                                     succ_constln_iter=succ_entry::slice_end(succ_constln_iter);
     351           0 :                                                                                                     for ( ;s_iter != succ_constln_iter ;++s_iter)
     352             :                                                                                                     {
     353           0 :                                                                                                         mCRL2log(log::debug, "bisim_gjkw") << "\t\tto "
     354           0 :                                                                                                                                  << s_iter->target->debug_id();
     355           0 :                                                                                                         if (state_iter->inert_succ_begin() <= s_iter &&
     356           0 :                                                                                                                          s_iter < state_iter->inert_succ_end())
     357             :                                                                                                         {
     358           0 :                                                                                                             mCRL2log(log::debug, "bisim_gjkw") << " (inert)";
     359             :                                                                                                         }
     360           0 :                                                                                                         if (state_iter->current_constln() == s_iter)
     361             :                                                                                                         {
     362           0 :                                                                                                             mCRL2log(log::debug, "bisim_gjkw")
     363           0 :                                                                                                                                       << " <- current_constln";
     364             :                                                                                                         }
     365           0 :                                                                                                         mCRL2log(log::debug, "bisim_gjkw") << '\n';
     366           0 :                                                                                                         assert(s_iter->B_to_C->pred->succ == s_iter);
     367           0 :                                                                                                         assert(s_iter->B_to_C->pred->source == &*state_iter);
     368             :                                                                                                     }
     369             :                                                                                                 }
     370           0 : /* ************************************************************************* */                 while (state_iter->succ_end() != succ_constln_iter);
     371           0 : /*                                                                           */                 if (state_iter->current_constln() == state_iter->succ_end())
     372             : /*                           T R A N S I T I O N S                           */                 {
     373           0 : /*                                                                           */                     mCRL2log(log::debug, "bisim_gjkw")
     374           0 : /* ************************************************************************* */                                                  << "\t\t<- current_constln\n";
     375             :                                                                                                 }
     376             :                                                                                             }
     377             :                                                                                         }
     378           0 :                                                                                     }
     379             :                                                                                 #endif // ifndef NDEBUG
     380             : /// \brief handle the transitions from the splitter to its own constellation
     381             : /// \details split_inert_to_C splits the B_to_C slice of block SpB to its own
     382             : /// constellation into two slices: one for the inert and one for the non-inert
     383             : /// transitions.  It is called with SpB just after a constellation is split, as
     384             : /// the transitions from SpB to itself (= the inert transitions) now go to a
     385             : /// different constellation than the other transitions from SpB to its old
     386             : /// constellation.  It does, however, not adapt the other transition arrays to
     387             : /// reflect that noninert and inert transitions from block SpB would go to
     388             : /// different constellations.
     389             : ///
     390             : /// Its time complexity is O(1+min{|out_noninert(SpB-->C)|, |inert_out(SpB)|}).
     391             : /// \param SpB  pointer to the splitter block
     392         501 : void part_trans_t::split_inert_to_C(block_t* const SpB)
     393             : {
     394             :     // if there are no inert transitions
     395         501 :     if (SpB->inert_begin() == SpB->inert_end())
     396             :     {
     397         465 :         if (SpB->inert_end() != B_to_C.begin())
     398             :         {
     399             :             // There are noninert transitions from SpB to its old
     400             :             // constellation:  they all go to SpC.
     401         156 :             SpB->SetFromRed(SpB->inert_end()[-1].B_to_C_slice);
     402             :             // There are no more transitions from SpB to its own constellation
     403         156 :             SpB->set_inert_begin(B_to_C.begin());
     404         156 :             SpB->set_inert_end(B_to_C.begin());
     405             :         }
     406         954 :         return;
     407             :     }
     408          36 :     B_to_C_desc_iter_t const slice = SpB->inert_begin()->B_to_C_slice;
     409             :     // if all transitions are inert
     410          36 :     if (slice->begin == SpB->inert_begin())
     411             :     {
     412          24 :         return;
     413             :     }
     414             : 
     415             :     // now the slice actually has to be split
     416          12 :     B_to_C_desc_iter_t new_slice;
     417             :     // select the smaller number of swaps to decide which part should be the
     418             :     // new one:
     419          12 :     if(SpB->inert_begin() - slice->begin < slice->end - SpB->inert_begin())
     420             :     {
     421             :         // fewer noninert transitions
     422           2 :         SpB->to_constln.emplace_front(slice->begin, SpB->inert_begin());
     423           2 :         new_slice = SpB->to_constln.begin();
     424           2 :         /* SpB->SetFromRed(new_slice);                                       */ assert(new_slice->from_block() == SpB);
     425           2 :         slice->begin = SpB->inert_begin();
     426             :                                                                                 #ifndef NDEBUG
     427           2 :                                                                                     new_slice->work_counter = slice->work_counter;
     428             :                                                                                     // We actually change the pointers in the new slice (i. e. the pointers of
     429             :                                                                                     // the non-inert transitions) because there are fewer of them; however, we
     430             :                                                                                     // still have to assign this work to the inert transitions.
     431           2 :                                                                                     mCRL2complexity(slice, add_work(check_complexity::
     432             :                                                                                               Register_that_inert_transitions_from_s_go_to_NewC_B_to_C_2_17,
     433             :                                                                                               check_complexity::log_n-check_complexity::ilog2(SpB->size())), );
     434             :                                                                                 #endif
     435             :     }
     436             :     else
     437             :     {
     438             :         // fewer (or equal) inert transitions
     439          10 :         SpB->to_constln.emplace_back(SpB->inert_begin(), slice->end);
     440          10 :         new_slice = std::prev(SpB->to_constln.end());
     441          10 :         slice->end = SpB->inert_begin();
     442          10 :         SpB->SetFromRed(slice);
     443             :                                                                                 #ifndef NDEBUG
     444          10 :                                                                                     new_slice->work_counter = slice->work_counter;
     445          10 :                                                                                     mCRL2complexity(new_slice, add_work(check_complexity::
     446             :                                                                                               Register_that_inert_transitions_from_s_go_to_NewC_B_to_C_2_17,
     447             :                                                                                               check_complexity::log_n-check_complexity::ilog2(SpB->size())), );
     448             :                                                                                 #endif
     449             :     }
     450             :     // set the slice pointers of the smaller part to the new slice:
     451          51 :     for (B_to_C_iter_t iter = new_slice->begin; new_slice->end != iter; ++iter)
     452             :     {                                                                           // mCRL2complexity(...) -- optimized to the above calls.
     453          39 :                                                                                 assert(B_to_C.end() > iter);  assert(iter->pred->succ->B_to_C == iter);
     454          39 :         iter->B_to_C_slice = new_slice;
     455             :     }
     456             : }
     457             : 
     458             : 
     459             : /// \brief transition target is moved to a new constellation
     460             : /// \details part_trans_t::change_to_C has to be called after a transition
     461             : /// target has changed its constellation.  The member function will adapt the
     462             : /// transition data structure.  It assumes that the transition is non-inert and
     463             : /// that the new constellation does not (yet) have _inert_ incoming
     464             : /// transitions.  It returns the boundary between transitions to SpC and
     465             : /// transitions to NewC in the state's outgoing transition array.
     466             : /// \param pred_iter  transition that has to be changed
     467             : /// \param SpC        splitter constellation
     468             : /// \param NewC       new constellation, where the transition goes to now
     469             : /// \param first_transition_of_state  This is the first transition of the
     470             : ///                                   state, so a new constln slice is started.
     471             : /// \param first_transition_of_block  This is the first transition of the
     472             : ///                                   block, so a new B_to_C slice has to be
     473             : ///                                   allocated.
     474        1046 : succ_iter_t part_trans_t::change_to_C(pred_iter_t const pred_iter,              ONLY_IF_DEBUG( constln_t* const SpC, constln_t* const NewC, )
     475             :     bool const first_transition_of_state, bool const first_transition_of_block)
     476        1046 : {                                                                               assert(pred_iter<pred.end()); assert(pred_iter->succ->B_to_C->pred==pred_iter);
     477             :     // adapt the B_to_C array:
     478             :     // always move the transition to the beginning of the slice (this will make
     479             :     // it easier because inert transitions are stored at the end of a slice).
     480        1046 :     B_to_C_iter_t const old_B_to_C_pos = pred_iter->succ->B_to_C;
     481        1046 :     B_to_C_desc_iter_t const old_B_to_C_slice = old_B_to_C_pos->B_to_C_slice;
     482        1046 :     B_to_C_iter_t const new_B_to_C_pos = old_B_to_C_slice->begin;               assert(new_B_to_C_pos < B_to_C.end());
     483        1046 :     B_to_C_desc_iter_t new_B_to_C_slice;                                        assert(new_B_to_C_pos->pred->succ->B_to_C == new_B_to_C_pos);
     484        1046 :     if (first_transition_of_block)
     485             :     {
     486             :         // create a new slice in B_to_C for the transitions from RfnB to NewC
     487         624 :         block_t* const RfnB = pred_iter->source->block;
     488         624 :         RfnB->to_constln.emplace_back(new_B_to_C_pos, new_B_to_C_pos);
     489         624 :         new_B_to_C_slice = std::prev(RfnB->to_constln.end());
     490             :                                                                                 #ifndef NDEBUG
     491         624 :                                                                                     new_B_to_C_slice->work_counter = old_B_to_C_slice->work_counter;
     492             :                                                                                 #endif
     493         624 :         RfnB->SetFromRed(old_B_to_C_slice);
     494             :     }
     495             :     else
     496             :     {
     497         422 :         new_B_to_C_slice = new_B_to_C_pos[-1].B_to_C_slice;
     498             :     }
     499        1046 :     ++new_B_to_C_slice->end;
     500        1046 :     ++old_B_to_C_slice->begin;                                                  assert(new_B_to_C_slice->end == old_B_to_C_slice->begin);
     501        1046 :     if (old_B_to_C_slice->begin == old_B_to_C_slice->end)
     502             :     {
     503             :         // this was the last transition from RfnB to SpC
     504         242 :         block_t* const RfnB = pred_iter->source->block;
     505         242 :         if (RfnB->inert_end() == old_B_to_C_slice->begin)
     506          87 :         {                                                                       assert(RfnB->inert_begin() == RfnB->inert_end());
     507             :             // this was the last transition from RfnB to its own constellation
     508          87 :             RfnB->set_inert_begin(B_to_C.begin());
     509          87 :             RfnB->set_inert_end(B_to_C.begin());
     510         242 :         }                                                                       assert(RfnB->to_constln.begin() == old_B_to_C_slice);
     511         242 :         RfnB->to_constln.erase(old_B_to_C_slice);
     512             :     }
     513        1046 :     swap_B_to_C(pred_iter->succ, new_B_to_C_pos->pred->succ);
     514        1046 :     new_B_to_C_pos->B_to_C_slice = new_B_to_C_slice;
     515             :     // adapt the outgoing transition array:
     516             :     // move the transition to the beginning
     517        1046 :     succ_iter_t const old_out_pos = pred_iter->succ;                            assert(succ.end() > old_out_pos);
     518        1046 :                                                                                 assert(old_out_pos->B_to_C->pred->succ == old_out_pos);
     519        1046 :     /* move to beginning                                                     */ assert(*NewC < *SpC);
     520        1046 :     succ_iter_t const new_out_pos = old_out_pos->slice_begin();
     521        1046 :     swap_out(pred_iter, new_out_pos->B_to_C->pred);
     522        2092 :     if (succ_iter_t const old_slice_end = succ_entry::slice_end(old_out_pos);
     523        1046 :                                                old_slice_end > new_out_pos + 1)
     524             :     {
     525             :         // the following assignment might assign an illegal transition if the
     526             :         // old slice becomes empty -- but then it doesn't hurt, because it will
     527             :         // be overwritten below.  However, Visual Studio C complains.
     528         232 :         old_slice_end[-1].set_slice_begin_or_before_end(new_out_pos + 1);       assert(old_slice_end - 1 == new_out_pos->slice_begin_or_before_end());
     529             :     }                                                                           else
     530         814 :                                                                                 {   assert(old_slice_end - 1 == new_out_pos);
     531         814 :                                                                                     assert(old_slice_end-1==old_slice_end[-1].slice_begin_or_before_end());
     532             :                                                                                 }
     533        1046 :     if (first_transition_of_state)
     534             :     {
     535        1013 :         new_out_pos->set_slice_begin_or_before_end(new_out_pos);
     536             :     }
     537             :     else
     538          33 :     {                                                                           assert(pred_iter->source->current_constln() == new_out_pos);
     539          66 :         new_out_pos->set_slice_begin_or_before_end(
     540          33 :                                   new_out_pos[-1].slice_begin_or_before_end());
     541             :     }
     542        1046 :     return new_out_pos + 1;
     543             : }
     544             : 
     545             : 
     546             : /// \brief Split outgoing transitions of a state in the splitter
     547             : /// \details split_s_inert_out splits the outgoing transitions from s to its
     548             : /// own constellation into two:  the inert transitions become transitions to
     549             : /// the new constellation of which s is now part;  the non-inert transitions
     550             : /// remain transitions to OldC.
     551             : /// Its time complexity is O(1 + min { |out_\nottau(s)|, |out_\tau(s)| }).
     552             : /// \param s     state whose outgoing transitions need to be split
     553             : /// \param OldC  old constellation (of which the splitter was a part earlier)
     554             : /// \result true iff the state also has transitions to OldC
     555         949 : bool part_trans_t::split_s_inert_out(state_info_ptr s                           ONLY_IF_DEBUG( , constln_t* OldC )
     556             :                                                      )
     557             : {
     558         949 :     constln_t* NewC = s->constln();                                             assert(*NewC < *OldC); assert(NewC->sort_key + OldC->size() == OldC->sort_key);
     559         949 :                                                                                 assert(OldC->end() == NewC->begin() || NewC->end() == OldC->begin());
     560         949 :     succ_iter_t split = s->inert_succ_begin(), to_C_end = s->inert_succ_end();  assert(s->succ_begin() == to_C_end ||
     561             :                                                                                                           to_C_end[-1].slice_begin_or_before_end() < to_C_end);
     562        1898 :     succ_iter_t to_C_begin = s->succ_begin() == to_C_end ? to_C_end
     563         949 :                                     : to_C_end[-1].slice_begin_or_before_end();
     564             :         //< If s has no transitions to OldC at all, then to_C_begin may be the
     565             :         // beginning of the constln_slice for transitions to another
     566             :         // constellation.  We will check that later.
     567         949 :     bool result = to_C_begin < split;                                           assert(to_C_begin <= split);  assert(split <= to_C_end);
     568         949 :                                                                                 assert(succ.end() == split || split->B_to_C->pred->succ == split);
     569         949 :                                                                                 assert(succ.end() == to_C_end || to_C_end->B_to_C->pred->succ == to_C_end);
     570         949 :                                                                                 assert(succ.end() == to_C_begin ||
     571             :                                                                                                              to_C_begin->B_to_C->pred->succ == to_C_begin);
     572         949 :     if (!result)  ;
     573         701 :     else if (split < to_C_end)
     574             :     {
     575             :         // s has both inert and non-inert transitions
     576             :                                                                                 #ifndef NDEBUG
     577          56 :         /* the out-transitions of s also have to be swapped.                 */     unsigned const max_counter = check_complexity::log_n -
     578          56 :         /* Actually only B_to_C and the target need to be swapped, as the    */                                          check_complexity::ilog2(NewC->size());
     579          28 :         /* constln_slices are (still) identical.                             */     assert(*NewC < *OldC);
     580             :                                                                                 #endif
     581          28 :         trans_type swapcount = std::min(to_C_end - split, split - to_C_begin);
     582          28 :         split = to_C_end - split + to_C_begin;                                  assert(0 != swapcount);
     583             : 
     584          28 :         succ_iter_t pos1 = to_C_begin, pos2 = to_C_end;
     585          28 :         state_info_ptr temp_target = pos1->target;
     586          28 :         B_to_C_iter_t temp_B_to_C = pos1->B_to_C;
     587             :         for (;;)
     588             :         {
     589          28 :             --pos2;                                                             mCRL2complexity(pos2->B_to_C->pred, add_work(check_complexity::
     590             :                                                                                                Register_that_inert_transitions_from_s_go_to_NewC_swap_2_17,
     591             :                                                                                                                                                max_counter), );
     592          28 :             pos1->target = pos2->target;
     593          28 :             pos1->B_to_C = pos2->B_to_C;
     594          28 :             pos1->B_to_C->pred->succ = pos1;
     595          28 :             ++pos1;
     596          28 :             if (0 == --swapcount)  break;
     597           0 :             pos2->target = pos1->target;
     598           0 :             pos2->B_to_C = pos1->B_to_C;
     599           0 :             pos2->B_to_C->pred->succ = pos2;
     600             :         }
     601          28 :         pos2->target = temp_target;
     602          28 :         pos2->B_to_C = temp_B_to_C;
     603          28 :         pos2->B_to_C->pred->succ = pos2;
     604             : 
     605          28 :         s->set_inert_succ_begin_and_end(to_C_begin, split);                     assert(s->succ_begin() == s->inert_succ_begin() ||
     606             :                                                                                                          *s->inert_succ_begin()[-1].target->constln() < *NewC);
     607          28 :                                                                                 assert(s->inert_succ_begin()->target->block == s->block);
     608          28 :                                                                                 assert(s->inert_succ_end()[-1].target->block == s->block);
     609          28 :                                                                                 assert(s->inert_succ_end() < s->succ_end());
     610          28 :         /* set the pointer to the slice for the inert transitions.           */ assert(OldC == s->inert_succ_end()->target->constln());
     611          28 :         to_C_end[-1].set_slice_begin_or_before_end(split);
     612          28 :         split[-1].set_slice_begin_or_before_end(to_C_begin);
     613          30 :         for (succ_iter_t succ_iter = split - 1; to_C_begin != succ_iter; )
     614             :         {
     615           2 :             --succ_iter;                                                        mCRL2complexity(succ_iter->B_to_C->pred,add_work(bisim_gjkw::check_complexity::
     616             :                                                                                                Register_that_inert_transitions_from_s_go_to_NewC_succ_2_17,
     617             :                                                                                                                                                max_counter), );
     618           2 :                                                                                 assert(succ.end() > succ_iter);
     619           2 :                                                                                 assert(succ_iter->B_to_C->pred->succ == succ_iter);
     620           2 :             succ_iter->set_slice_begin_or_before_end(split - 1);
     621             :         }
     622             :     }
     623         673 :     else if (*to_C_begin->target->constln() > *NewC)
     624             :     {
     625             :         // s has (noninert) transitions to OldC, but no (inert)
     626         397 :         /* transitions to NewC.                                              */ assert(to_C_begin->target->constln() == OldC);
     627         397 :         s->set_inert_succ_begin_and_end(to_C_begin, to_C_begin);                assert(s->succ_begin() == s->inert_succ_begin() ||
     628             :                                                                                                          *s->inert_succ_begin()[-1].target->constln() < *NewC);
     629         397 :                                                                                 assert(s->succ_end() > s->inert_succ_end());  assert(to_C_end == split);
     630         397 :                                                                                 assert(OldC == s->inert_succ_end()->target->constln());
     631             :     }
     632             :     else
     633             :     {
     634             :         // s actually hasn't got transitions to OldC at all, so `result`
     635             :         // should not be true.
     636         276 :         result = false;
     637             :     }
     638             :                                                                                 #ifndef NDEBUG
     639         949 :                                                                                     if (succ_iter_t succ_iter = s->succ_begin(); succ_iter != s->succ_end())
     640             :                                                                                     {
     641         288 :                                                                                         do
     642             :                                                                                         {
     643        1220 :                                                                                             assert(succ_iter->B_to_C->pred->source == s);
     644             :                                                                                         }
     645        1220 :                                                                                         while (++succ_iter != s->succ_end());
     646         932 :                                                                                         assert(s->succ_begin() == s->inert_succ_begin() ||
     647             :                                                                                                          *s->inert_succ_begin()[-1].target->constln() < *NewC);
     648         932 :                                                                                         assert(s->inert_succ_begin() == s->inert_succ_end() ||
     649             :                                                                                                           (s->inert_succ_begin()->target->block == s->block &&
     650             :                                                                                                            s->inert_succ_end()[-1].target->block == s->block));
     651         932 :                                                                                         assert(s->inert_succ_end() == s->succ_end() ||
     652             :                                                                                                               *NewC < *s->inert_succ_end()->target->constln());
     653             :                                                                                     }
     654             :                                                                                 #endif // ifndef NDEBUG
     655         949 :     return result;
     656             : }
     657             : 
     658             : 
     659             : /// \brief handle B_to_C slices after a new blue block has been created
     660             : /// \details part_trans_t::new_blue_block_created splits the B_to_C-slices to
     661             : /// reflect that some transitions now start in the new block NewB.  They can no
     662             : /// longer be in the same slice as the transitions that start in the old block.
     663             : /// Its time complexity is O(1 + |out(NewB)|).
     664             : /// \param RfnB  the old block that has been refined (now the red subblock)
     665             : /// \param NewB  the new block (the blue subblock)
     666          57 : void part_trans_t::new_blue_block_created(block_t* const RfnB,
     667             :                                                            block_t* const NewB)
     668          57 : {                                                                               assert(RfnB->constln()==NewB->constln());  assert(NewB->end()==RfnB->begin());
     669          57 :     NewB->set_inert_begin_and_end(B_to_C.begin(), B_to_C.begin());
     670             :                                                                                 #ifndef NDEBUG
     671         114 :                                                                                     unsigned const max_counter = check_complexity::log_n -
     672         114 :                                                                                                                          check_complexity::ilog2(NewB->size());
     673          57 :                                                                                     mCRL2complexity(NewB, add_work(check_complexity::
     674             :     /* for all outgoing transitions of NewB                                  */                   Move_Blue_or_Red_to_a_new_block_states_3_29, max_counter), );
     675             :                                                                                 #endif
     676         211 :     for(permutation_iter_t s_iter=NewB->begin(); NewB->end()!=s_iter; ++s_iter)
     677             :     {                                                                           // mCRL2complexity(*s_iter, ...) -- optimized to the above call
     678         367 :         for (succ_iter_t succ_iter = (*s_iter)->succ_begin();
     679         367 :                                (*s_iter)->succ_end() != succ_iter; ++succ_iter)
     680         213 :         {                                                                       mCRL2complexity(succ_iter->B_to_C->pred,add_work(check_complexity::
     681             :                                                                                                     Move_Blue_or_Red_to_a_new_block_succ_3_29, max_counter), );
     682         213 :             /* Move the transition to a new slice:                           */ assert(succ.end()>succ_iter); assert(succ_iter->B_to_C->pred->succ==succ_iter);
     683         213 :             B_to_C_iter_t const old_pos = succ_iter->B_to_C;
     684         213 :             B_to_C_desc_iter_t const old_B_to_C_slice = old_pos->B_to_C_slice;
     685         213 :             B_to_C_iter_t const after_new_pos = old_B_to_C_slice->end;          assert(B_to_C.end() > old_pos);
     686         213 :                                                                                 assert(old_pos->pred->succ->B_to_C == old_pos);
     687         213 :                                                                                 assert(B_to_C.end() == after_new_pos ||
     688             :                                                                                                            after_new_pos->pred->succ->B_to_C == after_new_pos);
     689         213 :             B_to_C_desc_iter_t new_B_to_C_slice;
     690         636 :             if (B_to_C.end() == after_new_pos ||
     691         356 :                     after_new_pos->pred->source->block != NewB ||
     692         143 :                         after_new_pos->pred->succ->target->constln() !=
     693         143 :                                                   succ_iter->target->constln())
     694             :             {
     695             :                 // create a new B_to_C-slice
     696             :                 // this can only happen when the first transition from
     697             :                 // *s_iter to a new constellation is handled.
     698          75 :                 if (!old_B_to_C_slice->needs_postprocessing())
     699             :                 {
     700             :                     // (During primary refinement [Line 2.23]: There is no need
     701             :                     // to put the FromRed-slice of the new blue block into
     702             :                     // position like in new_red_block_created(), as only the
     703             :                     // red subblock will be refined further in Line 2.24.)
     704             :                     // During postprocessing:
     705             :                     // the old_B_to_C_slice does not need postprocessing, so
     706             :                     // its corresponding new slice should be in a similar
     707             :                     // position near the beginning of the list of slices.
     708         150 :                     NewB->to_constln.emplace_front(after_new_pos,
     709          75 :                                                                 after_new_pos); // new_B_to_C_slice is not yet fully initialised, therefore
     710          75 :                     new_B_to_C_slice = NewB->to_constln.begin();                // the assertion fails:
     711             :                                                                                 // assert(new_B_to_C_slice->from_block() == NewB);
     712             :                 }
     713             :                 else
     714             :                 {
     715             :                     // During postprocessing:
     716             :                     // the old_B_to_C_slice needs postprocessing, so also the
     717             :                     // new_B_to_C_slice will need postprocessing.
     718           0 :                     NewB->to_constln.emplace_back(after_new_pos,after_new_pos);
     719           0 :                     new_B_to_C_slice = std::prev(NewB->to_constln.end());
     720             :                 }
     721             :                                                                                 #ifndef NDEBUG
     722          75 :                                                                                     new_B_to_C_slice->work_counter = old_B_to_C_slice->work_counter;
     723             :                                                                                 #endif
     724          75 :                 if (RfnB->inert_end() == after_new_pos)
     725             :                 {
     726          32 :                     /* this is the first transition from NewB to its own     */ assert(NewB->inert_begin() == B_to_C.begin());
     727          32 :                     /* constellation.  Adapt the pointers accordingly.       */ assert(NewB->inert_end() == B_to_C.begin());
     728          32 :                     NewB->set_inert_end(after_new_pos);
     729          32 :                     NewB->set_inert_begin(after_new_pos);
     730             :                 }
     731             :             }
     732             :             else
     733             :             {
     734             :                 // the slice at after_new_pos is already the correct one
     735         138 :                 new_B_to_C_slice = after_new_pos->B_to_C_slice;
     736             :             }
     737         213 :             --new_B_to_C_slice->begin;
     738         213 :             --old_B_to_C_slice->end;                                            assert(new_B_to_C_slice->begin == old_B_to_C_slice->end);
     739         213 :             B_to_C_iter_t new_pos = after_new_pos - 1;                          assert(B_to_C.end() > new_pos);
     740         213 :                                                                                 assert(new_pos->pred->succ->B_to_C == new_pos);
     741         213 :             if (RfnB->inert_end() == after_new_pos)
     742             :             {
     743             :                 // The transition goes from NewB to the constellation of
     744             :                 // RfnB and NewB.
     745         148 :                 if (RfnB->inert_begin() <= old_pos)
     746             :                 {
     747             :                     // The transition is inert and has to be moved over the
     748             :                     // non-inert transitions of NewB.
     749          60 :                     NewB->set_inert_begin(NewB->inert_begin() - 1);
     750          60 :                     new_pos = NewB->inert_begin();
     751             :                     // old_pos --> new_pos --> new_B_to_C_slice->begin -->
     752             :                     // old_pos
     753          60 :                     swap3_B_to_C(succ_iter, new_pos->pred->succ,
     754          60 :                                     new_B_to_C_slice->begin->pred->succ);
     755             :                 }
     756             :                 else
     757             :                 {
     758             :                     // The transition is non-inert, but it has to be moved
     759             :                     // over the inert transitions of RfnB.
     760          88 :                     RfnB->set_inert_begin(RfnB->inert_begin() - 1);
     761             :                     // old_pos --> new_pos --> RfnB->inert_begin() -> old_pos
     762          88 :                     swap3_B_to_C(succ_iter, new_pos->pred->succ,
     763         176 :                                     RfnB->inert_begin()->pred->succ);
     764             :                 }
     765         148 :                 RfnB->set_inert_end(RfnB->inert_end() - 1);
     766         148 :                 if (old_B_to_C_slice->begin == old_B_to_C_slice->end)
     767             :                 {
     768             :                     // This was the last transition from RfnB to its own
     769             :                     // constellation.
     770           5 :                     RfnB->set_inert_begin(B_to_C.begin());
     771           5 :                     RfnB->set_inert_end(B_to_C.begin());
     772             : 
     773           5 :                     RfnB->to_constln.erase(old_B_to_C_slice);
     774             :                 }
     775             :             }
     776             :             else
     777             :             {
     778             :                 // The transition goes from NewB to a constellation that
     779             :                 // does not contain RfnB or NewB.  No special treatment is
     780             :                 // required.
     781          65 :                 swap_B_to_C(succ_iter, new_pos->pred->succ);
     782          65 :                 if (old_B_to_C_slice->begin == old_B_to_C_slice->end)
     783             :                 {
     784          23 :                     RfnB->to_constln.erase(old_B_to_C_slice);
     785             :                 }
     786             :             }
     787         213 :             new_pos->B_to_C_slice = new_B_to_C_slice;
     788             :         }
     789             :     }
     790             :                                                                                 #ifndef NDEBUG
     791         132 :                                                                                     if (RfnB->inert_begin() == RfnB->inert_end() &&
     792         115 :                                                                                             RfnB->inert_end() != B_to_C.begin() &&
     793          59 :                                                                                                 (RfnB->inert_end()[-1].pred->source->block != RfnB ||
     794          58 :                                                                                                  RfnB->inert_end()[-1].pred->succ->target->constln()
     795           1 :                                                                                                                                            != RfnB->constln()))
     796             :                                                                                     {
     797           0 :                                                                                         assert(0 && "The old block has no transitions to its own "
     798             :                                                                                                            "constellation, but its inert_begin and "
     799             :                                                                                                            "inert_end pointers are not set to B_to_C.begin()");
     800             :                                                                                     }
     801          57 :                                                                                     if (RfnB->inert_end() != B_to_C.begin())
     802             :                                                                                     {
     803          40 :                                                                                         assert(RfnB->inert_end()[-1].pred->source->block == RfnB);
     804          40 :                                                                                         assert(RfnB->inert_end()[-1].pred->succ->target->constln() ==
     805             :                                                                                                                                               RfnB->constln());
     806             :                                                                                     }
     807         154 :                                                                                     if (NewB->inert_begin() == NewB->inert_end() &&
     808         129 :                                                                                             NewB->inert_end() != B_to_C.begin() &&
     809          87 :                                                                                                 (NewB->inert_end()[-1].pred->source->block != NewB ||
     810          72 :                                                                                                  NewB->inert_end()[-1].pred->succ->target->constln()
     811          15 :                                                                                                                                            != NewB->constln()))
     812             :                                                                                     {
     813           0 :                                                                                         assert(0 && "The new block has no transitions to its own "
     814             :                                                                                                            "constellation, but its inert_begin and "
     815             :                                                                                                            "inert_end pointers are not set to B_to_C.begin()");
     816             :                                                                                     }
     817          57 :                                                                                     if (NewB->inert_end() != B_to_C.begin())
     818             :                                                                                     {
     819          32 :                                                                                         assert(NewB->inert_end()[-1].pred->source->block == NewB);
     820          32 :                                                                                         assert(NewB->inert_end()[-1].pred->succ->target->constln() ==
     821             :                                                                                                                                               NewB->constln());
     822             :                                                                                     }
     823             :                                                                                 #endif
     824          57 : }
     825             : 
     826             : 
     827             : /// \brief handle B_to_C slices after a new red block has been created
     828             : /// \details part_trans_t::new_red_block_created splits the B_to_C-slices to
     829             : /// reflect that some transitions now start in the new block NewB.  They can no
     830             : /// longer be in the same slice as the transitions that start in the old block.
     831             : /// Its time complexity is O(1 + |out(NewB)|).
     832             : /// \param RfnB  the old block that has been refined (now the blue subblock)
     833             : /// \param NewB  the new block (the red subblock)
     834             : /// \param postprocessing  true iff the refinement happened during
     835             : ///                        postprocessing.  (Otherwise, the refinement should
     836             : ///                        preserve the information about `FromRed()`).
     837         308 : void part_trans_t::new_red_block_created(block_t* const RfnB,
     838             :                                 block_t* const NewB, bool const postprocessing)
     839         308 : {                                                                               assert(RfnB->constln()==NewB->constln());  assert(NewB->begin()==RfnB->end());
     840         308 :     NewB->set_inert_begin_and_end(B_to_C.begin(), B_to_C.begin());
     841         308 :     bool old_fromred_invalid = false;
     842             :                                                                                 #ifndef NDEBUG
     843         616 :                                                                                     unsigned const max_counter = check_complexity::log_n -
     844         616 :                                                                                                                          check_complexity::ilog2(NewB->size());
     845         308 :                                                                                     mCRL2complexity(NewB, add_work(check_complexity::
     846             :     /* for all outgoing transitions of NewB                                  */                   Move_Blue_or_Red_to_a_new_block_states_3_29, max_counter), );
     847             :                                                                                 #endif
     848         842 :     for(permutation_iter_t s_iter=NewB->begin(); NewB->end()!=s_iter; ++s_iter)
     849             :     {                                                                           // mCRL2complexity(*s_iter, ...) -- optimized to the above call
     850        1359 :         for (succ_iter_t succ_iter = (*s_iter)->succ_begin();
     851        1359 :                                (*s_iter)->succ_end() != succ_iter; ++succ_iter)
     852         825 :         {                                                                       mCRL2complexity(succ_iter->B_to_C->pred,add_work(check_complexity::
     853             :                                                                                                     Move_Blue_or_Red_to_a_new_block_succ_3_29, max_counter), );
     854         825 :             /* Move the transition to a new slice:                           */ assert(succ.end()>succ_iter); assert(succ_iter->B_to_C->pred->succ==succ_iter);
     855         825 :             B_to_C_iter_t const old_pos = succ_iter->B_to_C;
     856         825 :             B_to_C_desc_iter_t const old_B_to_C_slice = old_pos->B_to_C_slice;
     857         825 :             B_to_C_iter_t new_pos = old_B_to_C_slice->begin;                    assert(B_to_C.end() > old_pos); assert(old_pos->pred->succ->B_to_C == old_pos);
     858         825 :                                                                                 assert(B_to_C.end() > new_pos); assert(new_pos->pred->succ->B_to_C == new_pos);
     859         825 :             B_to_C_desc_iter_t new_B_to_C_slice;
     860        2429 :             if (B_to_C.begin() == new_pos ||
     861        1285 :                     new_pos[-1].pred->source->block != NewB ||
     862         460 :                         new_pos[-1].pred->succ->target->constln() !=
     863         460 :                                             succ_iter->target->constln())
     864             :             {
     865             :                 // create a new B_to_C-slice
     866             :                 // this can only happen when the first transition from
     867             :                 // *s_iter to a new constellation is handled.
     868        1294 :                 if (!postprocessing ? !old_fromred_invalid &&
     869         853 :                                   RfnB->to_constln.begin() == old_B_to_C_slice
     870           9 :                                    : !old_B_to_C_slice->needs_postprocessing())
     871             :                 {
     872             :                     // During primary refinement (Line 2.23):
     873             :                     // The old B_to_C_slice is in the FromRed-position, i. e.
     874             :                     // it contains the transitions to SpC.  So the new slice
     875             :                     // also contains the transitions to SpC.
     876             :                     // During postprocessing:
     877             :                     // The old_B_to_C_slice does not need postprocessing, so
     878             :                     // its corresponding new slice should be in a similar
     879             :                     // position near the beginning of the list of slices.
     880          94 :                     NewB->to_constln.emplace_front(new_pos, new_pos);           // new_B_to_C_slice is not yet fully initialised, therefore
     881          94 :                     new_B_to_C_slice = NewB->to_constln.begin();                // the assertion fails:
     882             :                                                                                 // assert(new_B_to_C_slice->from_block() == NewB);
     883             :                 }
     884             :                 else
     885             :                 {
     886             :                     // During primary refinement (Line 2.23):
     887             :                     // The old_B_to_C_slice is not in the FromRed-position. The
     888             :                     // corresponding slice of NewB should be moved into a
     889             :                     // position that does not change a potential FromRed-slice
     890             :                     // there.
     891             :                     // During postprocessing:
     892             :                     // The old_B_to_C_slice needs postprocessing, so also the
     893             :                     // new_B_to_C_slice will need postprocessing.
     894         338 :                     NewB->to_constln.emplace_back(new_pos, new_pos);
     895         338 :                     new_B_to_C_slice = std::prev(NewB->to_constln.end());
     896             :                 }
     897             :                                                                                 #ifndef NDEBUG
     898         432 :                                                                                     new_B_to_C_slice->work_counter = old_B_to_C_slice->work_counter;
     899             :                                                                                 #endif
     900         432 :                 if (RfnB->inert_end() == old_B_to_C_slice->end)
     901             :                 {
     902          80 :                     /* this is the first transition from NewB to its own     */ assert(NewB->inert_begin() == B_to_C.begin());
     903          80 :                     /* constellation.  Adapt the pointers accordingly.       */ assert(NewB->inert_end() == B_to_C.begin());
     904          80 :                     NewB->set_inert_end(new_pos);
     905          80 :                     NewB->set_inert_begin(new_pos);
     906             :                 }
     907             :             }
     908             :             else
     909             :             {
     910             :                 // the slice before new_pos is already the correct one
     911         393 :                 new_B_to_C_slice = new_pos[-1].B_to_C_slice;
     912             :             }
     913         825 :             ++new_B_to_C_slice->end;
     914         825 :             ++old_B_to_C_slice->begin;                                          assert(new_B_to_C_slice->end == old_B_to_C_slice->begin);
     915         825 :             if (RfnB->inert_end() == old_B_to_C_slice->end)
     916             :             {
     917             :                 // The transition goes from NewB to the constellation of
     918             :                 // RfnB and NewB.
     919         271 :                 NewB->set_inert_end(NewB->inert_end() + 1);
     920         271 :                 if (RfnB->inert_begin() <= old_pos)
     921             :                 {
     922             :                     // The transition is inert and has to be moved over the
     923             :                     // non-inert transitions of RfnB.
     924             :                     // old_pos --> new_pos --> RfnB->inert_begin() --> old_pos
     925         198 :                     swap3_B_to_C(succ_iter, new_pos->pred->succ,
     926         396 :                                               RfnB->inert_begin()->pred->succ);
     927         198 :                     RfnB->set_inert_begin(RfnB->inert_begin() + 1);
     928             :                 }
     929             :                 else
     930             :                 {
     931             :                     // The transition is non-inert, but it has to be moved
     932             :                     // over the inert transitions of NewB.
     933          73 :                     new_pos = NewB->inert_begin();
     934          73 :                     NewB->set_inert_begin(NewB->inert_begin() + 1);
     935             :                     // old_pos --> new_pos --> NewB->inert_end() - 1 -> old_pos
     936          73 :                     swap3_B_to_C(succ_iter, new_pos->pred->succ,
     937         146 :                                              NewB->inert_end()[-1].pred->succ);
     938             :                 }
     939         271 :                 if (old_B_to_C_slice->begin == old_B_to_C_slice->end)
     940             :                 {
     941             :                     // This was the last transition from RfnB to its own
     942             :                     // constellation.
     943          12 :                     RfnB->set_inert_begin(B_to_C.begin());
     944          12 :                     RfnB->set_inert_end(B_to_C.begin());
     945             : 
     946          36 :                     if (!old_fromred_invalid &&
     947          24 :                                   RfnB->to_constln.begin() == old_B_to_C_slice)
     948             :                     {
     949           5 :                         old_fromred_invalid = true;
     950             :                     }
     951          12 :                     RfnB->to_constln.erase(old_B_to_C_slice);
     952             :                 }
     953             :             }
     954             :             else
     955             :             {
     956             :                 // The transition goes from NewB to a constellation that
     957             :                 // does not contain RfnB or NewB.  No special treatment is
     958             :                 // required.
     959         554 :                 swap_B_to_C(succ_iter, new_pos->pred->succ);
     960         554 :                 if (old_B_to_C_slice->begin == old_B_to_C_slice->end)
     961             :                 {
     962         916 :                     if (!old_fromred_invalid &&
     963         610 :                                   RfnB->to_constln.begin() == old_B_to_C_slice)
     964             :                     {
     965          25 :                         old_fromred_invalid = true;
     966             :                     }
     967         306 :                     RfnB->to_constln.erase(old_B_to_C_slice);
     968             :                 }
     969             :             }
     970         825 :             new_pos->B_to_C_slice = new_B_to_C_slice;
     971             :         }
     972             :     }
     973             :                                                                                 #ifndef NDEBUG
     974         875 :                                                                                     if (RfnB->inert_begin() == RfnB->inert_end() &&
     975         693 :                                                                                             RfnB->inert_end() != B_to_C.begin() &&
     976         462 :                                                                                                 (RfnB->inert_end()[-1].pred->source->block != RfnB ||
     977         385 :                                                                                                  RfnB->inert_end()[-1].pred->succ->target->constln()
     978          77 :                                                                                                                                            != RfnB->constln()))
     979             :                                                                                     {
     980           0 :                                                                                         assert(0 && "The old block has no transitions to its own "
     981             :                                                                                                            "constellation, but its inert_begin and "
     982             :                                                                                                            "inert_end pointers are not set to B_to_C.begin()");
     983             :                                                                                     }
     984         308 :                                                                                     if (RfnB->inert_end() != B_to_C.begin())
     985             :                                                                                     {
     986         126 :                                                                                         assert(RfnB->inert_end()[-1].pred->source->block == RfnB);
     987         126 :                                                                                         assert(RfnB->inert_end()[-1].pred->succ->target->constln() ==
     988             :                                                                                                                                               RfnB->constln());
     989             :                                                                                     }
     990         869 :                                                                                     if (NewB->inert_begin() == NewB->inert_end() &&
     991         641 :                                                                                             NewB->inert_end() != B_to_C.begin() &&
     992         358 :                                                                                                 (NewB->inert_end()[-1].pred->source->block != NewB ||
     993         333 :                                                                                                  NewB->inert_end()[-1].pred->succ->target->constln()
     994          25 :                                                                                                                                            != NewB->constln()))
     995             :                                                                                     {
     996           0 :                                                                                         assert(0 && "The new block has no transitions to its own "
     997             :                                                                                                            "constellation, but its inert_begin and "
     998             :                                                                                                            "inert_end pointers are not set to B_to_C.begin()");
     999             :                                                                                     }
    1000         308 :                                                                                     if (NewB->inert_end() != B_to_C.begin())
    1001             :                                                                                     {
    1002          80 :                                                                                         assert(NewB->inert_end()[-1].pred->source->block == NewB);
    1003          80 :                                                                                         assert(NewB->inert_end()[-1].pred->succ->target->constln() ==
    1004             :                                                                                                                                               NewB->constln());
    1005             :                                                                                     }
    1006             :                                                                                 #endif
    1007         308 : }
    1008             :                                                                                 #ifndef NDEBUG
    1009             :                                                                                     /// \brief assert that the data structure is consistent and stable
    1010             :                                                                                     /// \details The data structure is tested against a large number of
    1011             :                                                                                     /// assertions to ensure that everything is consistent, e. g. pointers that
    1012             :                                                                                     /// should point to successors of state s actually point to a transition
    1013             :                                                                                     /// that starts in s.
    1014             :                                                                                     ///
    1015             :                                                                                     /// Additionally, it is asserted that the partition is stable. i. e. every
    1016             :                                                                                     /// bottom state in every block can reach exactly the constellations in the
    1017             :                                                                                     /// list of constellations that should be reachable from it, and every
    1018             :                                                                                     /// nonbottom state can reach a subset of them.
    1019         556 :                                                                                     void part_trans_t::assert_stability(const part_state_t& part_st) const
    1020             :                                                                                     {
    1021             :                                                                                         #ifdef PARANOID_CHECK
    1022        1112 :                                                                                             std::vector<state_info_const_ptr> part_st_predecessors;
    1023             :                                                                                         #endif
    1024             :                                                                                         // count the nontrivial constellations (to check later whether every
    1025             :                                                                                         // nontrivial constellation is reachable from the first nontrivial
    1026             :                                                                                         // constellation)
    1027         556 :                                                                                         state_type nr_of_nontrivial_constellations = 0;
    1028         556 :                                                                                         const constln_t* C = constln_t::get_some_nontrivial();
    1029         556 :                                                                                         if (nullptr != C)
    1030             :                                                                                         {
    1031             :                                                                                             for (;;)
    1032             :                                                                                             {
    1033         775 :                                                                                                 ++nr_of_nontrivial_constellations;
    1034         638 :                                                                                                 if (C->get_nontrivial_next() == C)  break;
    1035         137 :                                                                                                 C = C->get_nontrivial_next();
    1036         137 :                                                                                                 assert(nullptr != C);
    1037             :                                                                                             }
    1038             :                                                                                         }
    1039             : 
    1040             :                                                                                         // for all constellations C do
    1041         556 :                                                                                         C = part_st.permutation.front()->constln();
    1042         556 :                                                                                         assert(C->begin() == part_st.permutation.begin());
    1043             :                                                                                         for (;;)
    1044             :                                                                                         {
    1045             :                                                                                             // assert some properties of constellation C
    1046        8219 :                                                                                             assert(C->begin() < C->end());
    1047        8219 :                                                                                             assert(C->postprocess_begin == C->postprocess_end);
    1048       16438 :                                                                                             unsigned const max_C = check_complexity::log_n -
    1049       16438 :                                                                                                                             check_complexity::ilog2(C->size());
    1050        8219 :                                                                                             const block_t* B = (*C->begin())->block;
    1051        8219 :                                                                                             assert(C->begin() == B->begin());
    1052        8219 :                                                                                             if (C->is_trivial())
    1053             :                                                                                             {
    1054             :                                                                                                 // a trivial constellation contains exactly one block
    1055        7581 :                                                                                                 assert(B->end() == C->end());
    1056             :                                                                                             }
    1057             :                                                                                             else
    1058             :                                                                                             {
    1059             :                                                                                                 // a nontrivial constellation contains at least two blocks
    1060         638 :                                                                                                 assert(B->end() < C->end());
    1061         638 :                                                                                                 --nr_of_nontrivial_constellations;
    1062             :                                                                                             }
    1063             :                                                                                             // for all blocks B in C do
    1064             :                                                                                             for (;;)
    1065             :                                                                                             {
    1066             :                                                                                                 // assert some properties of block B
    1067       10406 :                                                                                                 assert(B->constln() == C);
    1068       10406 :                                                                                                 assert(B->nonbottom_begin() <= B->nonbottom_end());
    1069       10406 :                                                                                                 assert(B->marked_nonbottom_begin()==B->marked_nonbottom_end());
    1070       10406 :                                                                                                 assert(B->bottom_begin() < B->bottom_end());
    1071       10406 :                                                                                                 assert(B->marked_bottom_begin() == B->marked_bottom_end());
    1072       10406 :                                                                                                 assert(!B->is_refinable());
    1073       10406 :                                                                                                 assert(B->inert_begin() <= B->inert_end());
    1074       20812 :                                                                                                 unsigned const max_B = check_complexity::log_n -
    1075       20812 :                                                                                                                             check_complexity::ilog2(B->size());
    1076       10406 :                                                                                                 mCRL2complexity(B, no_temporary_work(max_C, max_B), );
    1077             :                                                                                                 // count inert transitions in block
    1078             :                                                                                                 state_type nr_of_inert_successors =
    1079       10406 :                                                                                                                                B->inert_end()-B->inert_begin();
    1080       10406 :                                                                                                 permutation_const_iter_t s_iter;
    1081             :                                                                                                 #ifdef PARANOID_CHECK
    1082       10406 :                                                                                                     state_type nr_of_inert_predecessors=nr_of_inert_successors;
    1083             :                                                                                                     // make sure that every non-bottom state can reach some
    1084             :                                                                                                     // bottom  state  in  the  block.   This  is  done  using
    1085             :                                                                                                     // a  simple  graph  algorithm  for  reachability.   The
    1086             :                                                                                                     // algorithm  should  mark  every  source  of  an  inert
    1087             :                                                                                                     // transition exactly once.  For this, we misuse the field
    1088             :                                                                                                     // state_info_entry::notblue:  It is == STATE_TYPE_MAX if
    1089             :                                                                                                     // and only if the state has been marked.
    1090             : 
    1091             :                                                                                                     // Because we run through the bottom states and their
    1092             :                                                                                                     // predecessor transitions anyway, we also verify a few
    1093             :                                                                                                     // other properties, in particular everything we want to
    1094             :                                                                                                     // verify about inert predecessor transitions.
    1095             : 
    1096             :                                                                                                     // for all bottom states s in B do
    1097       10406 :                                                                                                     assert(part_st_predecessors.empty());
    1098       10406 :                                                                                                     part_st_predecessors.reserve(B->nonbottom_end() -
    1099       20812 :                                                                                                                                          B->nonbottom_begin());
    1100       10406 :                                                                                                     s_iter = B->bottom_begin();
    1101       12767 :                                                                                                     do
    1102             :                                                                                                     {
    1103       23173 :                                                                                                         state_info_const_ptr const s = *s_iter;
    1104       23173 :                                                                                                         nr_of_inert_predecessors -=
    1105       46346 :                                                                                                                    s->inert_pred_end() - s->inert_pred_begin();
    1106             :                                                                                                         // for all inert predecessors pred of s do
    1107       25132 :                                                                                                         for (pred_const_iter_t pred_iter=s->inert_pred_begin();
    1108       25132 :                                                                                                                   pred_iter < s->inert_pred_end(); ++pred_iter)
    1109             :                                                                                                         {
    1110             :                                                                                                             // assert some properties of the predecessor
    1111             :                                                                                                             // transition
    1112        1959 :                                                                                                             assert(pred_iter->succ->B_to_C->B_to_C_slice->
    1113             :                                                                                                                                             from_block() == B);
    1114        1959 :                                                                                                             assert(pred_iter->succ->B_to_C->B_to_C_slice->
    1115             :                                                                                                                                             to_constln() == C);
    1116        1959 :                                                                                                             assert(pred_iter->succ->target == s);
    1117             : 
    1118        1959 :                                                                                                             state_info_const_ptr const pred=pred_iter->source;
    1119             :                                                                                                             // if pred is not yet marked as predecessor then
    1120        1959 :                                                                                                             if (STATE_TYPE_MAX != pred->notblue)
    1121             :                                                                                                             {
    1122             :                                                                                                                 // assert some properties of the predecessor
    1123             :                                                                                                                 // state
    1124        1836 :                                                                                                                 assert(pred->block == B);
    1125        1836 :                                                                                                                 assert(pred->pos < B->nonbottom_end());
    1126             :                                                                                                                 // mark pred as predecessor
    1127        1836 :                                                                                                                 const_cast<state_type&>(pred->notblue) =
    1128             :                                                                                                                                                 STATE_TYPE_MAX;
    1129             :                                                                                                                 // add pred to the list of predecessors
    1130        1836 :                                                                                                                 part_st_predecessors.push_back(pred);
    1131             :                                                                                                             // end if
    1132             :                                                                                                             }
    1133             :                                                                                                         // end for
    1134             :                                                                                                         }
    1135             :                                                                                                     // end for
    1136             :                                                                                                     }
    1137       23173 :                                                                                                     while(++s_iter < B->bottom_end());
    1138             : 
    1139             :                                                                                                     // Now that we have collected the predecessors of the
    1140             :                                                                                                     // bottom states, we have to extend this set to their
    1141             :                                                                                                     // indirect predecessors.
    1142             : 
    1143             :                                                                                                     // for all states s in the list of predecessors do
    1144        3060 :                                                                                                     for (std::vector<state_info_const_ptr>::iterator s_iter =
    1145       10406 :                                                                                                                   part_st_predecessors.begin();
    1146       13466 :                                                                                                                  s_iter < part_st_predecessors.end(); ++s_iter)
    1147             :                                                                                                     {
    1148        3060 :                                                                                                         state_info_const_ptr const s = *s_iter;
    1149        3060 :                                                                                                         nr_of_inert_predecessors -=
    1150        6120 :                                                                                                                    s->inert_pred_end() - s->inert_pred_begin();
    1151             :                                                                                                         // for all inert predecessors pred of s do
    1152        4585 :                                                                                                         for (pred_const_iter_t pred_iter=s->inert_pred_begin();
    1153        4585 :                                                                                                                   pred_iter < s->inert_pred_end(); ++pred_iter)
    1154             :                                                                                                         {
    1155             :                                                                                                             // assert some properties of the predecessor
    1156             :                                                                                                             // transition
    1157        1525 :                                                                                                             assert(pred_iter->succ->B_to_C->B_to_C_slice->
    1158             :                                                                                                                                             from_block() == B);
    1159        1525 :                                                                                                             assert(pred_iter->succ->B_to_C->B_to_C_slice->
    1160             :                                                                                                                                             to_constln() == C);
    1161        1525 :                                                                                                             assert(pred_iter->succ->target == s);
    1162             : 
    1163        1525 :                                                                                                             state_info_const_ptr const pred=pred_iter->source;
    1164             :                                                                                                             // if pred is not yet marked as predecessor then
    1165        1525 :                                                                                                             if (STATE_TYPE_MAX != pred->notblue)
    1166             :                                                                                                             {
    1167             :                                                                                                                 // assert some properties of the predecessor
    1168             :                                                                                                                 // state
    1169        1224 :                                                                                                                 assert(pred->block == B);
    1170        1224 :                                                                                                                 assert(pred->pos < B->nonbottom_end());
    1171             :                                                                                                                 // mark pred as predecessor
    1172        1224 :                                                                                                                 const_cast<state_type&>(pred->notblue) =
    1173             :                                                                                                                                                 STATE_TYPE_MAX;
    1174             :                                                                                                                 // add pred to the list of predecessors
    1175        1224 :                                                                                                                 part_st_predecessors.push_back(pred);
    1176             :                                                                                                             // end if
    1177             :                                                                                                             }
    1178             :                                                                                                         // end for
    1179             :                                                                                                         }
    1180             :                                                                                                     // end for
    1181             :                                                                                                     }
    1182       10406 :                                                                                                     assert(part_st_predecessors.size() == (std::size_t)
    1183             :                                                                                                                   (B->nonbottom_end() - B->nonbottom_begin()));
    1184       10406 :                                                                                                     part_st_predecessors.clear();
    1185       10406 :                                                                                                     assert(0 == nr_of_inert_predecessors);
    1186             :                                                                                                     // now all nonbottom states should have
    1187             :                                                                                                     // s->notblue == STATE_TYPE_MAX.
    1188             :                                                                                                 #endif
    1189             :                                                                                                 // verify to_constln list:
    1190       10406 :                                                                                                 bool to_own_constln = false;
    1191       24522 :                                                                                                 for (B_to_C_desc_const_iter_t iter = B->to_constln.begin();
    1192       24522 :                                                                                                                            B->to_constln.end() != iter; ++iter)
    1193             :                                                                                                 {
    1194       14116 :                                                                                                     assert(iter->from_block() == B);
    1195       14116 :                                                                                                     mCRL2complexity(iter, no_temporary_work(
    1196             :                                                                                                        check_complexity::log_n -
    1197             :                                                                                                        check_complexity::ilog2(iter->to_constln()->size())), );
    1198       14116 :                                                                                                     if (iter->to_constln() == C)
    1199             :                                                                                                     {
    1200        1647 :                                                                                                         assert(!to_own_constln);
    1201        1647 :                                                                                                         to_own_constln = true;
    1202        1647 :                                                                                                         assert(iter->begin <= B->inert_begin());
    1203        1647 :                                                                                                         assert(iter->end == B->inert_end());
    1204             :                                                                                                     }
    1205             :                                                                                                 }
    1206       10406 :                                                                                                 if (!to_own_constln)
    1207             :                                                                                                 {
    1208        8759 :                                                                                                     assert(B->nonbottom_begin() == B->nonbottom_end());
    1209        8759 :                                                                                                     assert(B->inert_begin() == B_to_C_begin());
    1210        8759 :                                                                                                     assert(B->inert_end() == B_to_C_begin());
    1211             :                                                                                                 }
    1212             : 
    1213             :                                                                                                 // for all states s in B do
    1214       10406 :                                                                                                 s_iter = B->begin();
    1215       15827 :                                                                                                 do
    1216             :                                                                                                 {
    1217       26233 :                                                                                                     state_info_const_ptr const s = *s_iter;
    1218             :                                                                                                     // assert some properties of state s
    1219       26233 :                                                                                                     assert(s->pos == s_iter);
    1220       26233 :                                                                                                     assert(s->block == B);
    1221       26233 :                                                                                                     assert(s->pred_begin() <= s->inert_pred_begin());
    1222       26233 :                                                                                                     assert(s->inert_pred_begin() <= s->inert_pred_end());
    1223       26233 :                                                                                                     assert(s->inert_pred_end() == s->pred_end());
    1224       26233 :                                                                                                     assert(s->succ_begin() <= s->inert_succ_begin());
    1225       26233 :                                                                                                     assert(s->inert_succ_begin() <= s->inert_succ_end());
    1226       26233 :                                                                                                     assert(s->inert_succ_end() <= s->succ_end());
    1227       26233 :                                                                                                     assert(s->succ_begin() == s->current_constln() ||
    1228             :                                                                                                              s->succ_end() == s->current_constln() ||
    1229             :                                                                                                                   *s->current_constln()[-1].target->constln() <
    1230             :                                                                                                                      *s->current_constln()->target->constln());
    1231       26233 :                                                                                                     mCRL2complexity(s, no_temporary_work(max_B,
    1232             :                                                                                                                                s_iter >= B->bottom_begin()), );
    1233             :                                                                                                     // count reachable constellations
    1234       26233 :                                                                                                     state_type nr_of_reachable_constlns = B->to_constln.size();
    1235             : 
    1236             :                                                                                                     // for all constln-slices of successors of s do
    1237       52466 :                                                                                                     if (succ_const_iter_t succ_iter = s->succ_begin();
    1238       26233 :                                                                                                                                      succ_iter < s->succ_end())
    1239             :                                                                                                     {
    1240             :                                                                                                         for (;;)
    1241             :                                                                                                         {
    1242             :                                                                                                             succ_const_iter_t before_end =
    1243       30049 :                                                                                                                         succ_iter->slice_begin_or_before_end();
    1244       30049 :                                                                                                             succ_const_iter_t slice_end = before_end + 1;
    1245       30049 :                                                                                                             assert(succ_iter < slice_end);
    1246       30049 :                                                                                                             assert(before_end->slice_begin_or_before_end() ==
    1247             :                                                                                                                                                     succ_iter);
    1248             :                                                                                                             const constln_t* const targetC =
    1249       30049 :                                                                                                                                   succ_iter->target->constln();
    1250             :                                                                                                             // for all noninert transitions in the
    1251             :                                                                                                             // constln-slice do
    1252       30049 :                                                                                                             if (targetC == C)
    1253             :                                                                                                             {
    1254        6043 :                                                                                                                 assert(s->inert_succ_end() == slice_end);
    1255        6043 :                                                                                                                 slice_end = s->inert_succ_begin();
    1256             :                                                                                                             }
    1257       89531 :                                                                                                             for (; succ_iter < slice_end; ++succ_iter)
    1258             :                                                                                                             {
    1259             :                                                                                                                 // assert some properties of the successor
    1260             :                                                                                                                 // transition
    1261       29741 :                                                                                                                 assert(succ_iter->target->block != B);
    1262       29741 :                                                                                                                 assert(succ_iter->target->constln()==targetC);
    1263       29741 :                                                                                                                 if (succ_iter != before_end)
    1264             :                                                                                                                 {
    1265        2752 :                                                                                                                     assert(succ_iter->
    1266             :                                                                                                                       slice_begin_or_before_end()==before_end);
    1267             :                                                                                                                 }
    1268       29741 :                                                                                                                 assert(succ_iter->B_to_C < B->inert_begin() ||
    1269             :                                                                                                                           B->inert_end() <= succ_iter->B_to_C);
    1270       29741 :                                                                                                                 assert(succ_iter->B_to_C->B_to_C_slice->
    1271             :                                                                                                                                             from_block() == B);
    1272       29741 :                                                                                                                 assert(succ_iter->B_to_C->B_to_C_slice->
    1273             :                                                                                                                                       to_constln() == targetC);
    1274       29741 :                                                                                                                 assert(succ_iter->B_to_C->pred->succ ==
    1275             :                                                                                                                                                     succ_iter);
    1276       29741 :                                                                                                                 assert(succ_iter->B_to_C->pred->source == s);
    1277       29741 :                                                                                                                 mCRL2complexity(succ_iter->B_to_C->pred,
    1278             :                                                                                                                     no_temporary_work(max_B, check_complexity::
    1279             :                                                                                                                        log_n - check_complexity::ilog2(
    1280             :                                                                                                                          succ_iter->target->constln()->size()),
    1281             :                                                                                                                    check_complexity::log_n - check_complexity::
    1282             :                                                                                                                        ilog2(succ_iter->target->block->size()),
    1283             :                                                                                                                                s_iter >= B->bottom_begin()), );
    1284             :                                                                                                             // end for
    1285             :                                                                                                             }
    1286             :                                                                                                             // if we have reached the inert transitions then
    1287       30049 :                                                                                                             if (targetC == C)
    1288             :                                                                                                             {
    1289             :                                                                                                                 // for all inert transitions in the
    1290             :                                                                                                                 // constln-slice do
    1291        9527 :                                                                                                                 for (slice_end = s->inert_succ_end();
    1292        9527 :                                                                                                                             succ_iter < slice_end; ++succ_iter)
    1293             :                                                                                                                 {
    1294             :                                                                                                                     // assert some properties of inert
    1295             :                                                                                                                     // transitions
    1296        3484 :                                                                                                                     assert(succ_iter->target->block == B);
    1297        3484 :                                                                                                                     if (succ_iter != before_end)
    1298             :                                                                                                                     {
    1299         424 :                                                                                                                         assert(before_end == succ_iter->
    1300             :                                                                                                                                   slice_begin_or_before_end());
    1301             :                                                                                                                     }
    1302        3484 :                                                                                                                     assert(B->inert_begin() <=
    1303             :                                                                                                                                             succ_iter->B_to_C);
    1304        3484 :                                                                                                                     assert(succ_iter->B_to_C < B->inert_end());
    1305        3484 :                                                                                                                     assert(succ_iter->B_to_C->B_to_C_slice->
    1306             :                                                                                                                                             from_block() == B);
    1307        3484 :                                                                                                                     assert(succ_iter->B_to_C->B_to_C_slice->
    1308             :                                                                                                                                       to_constln() == targetC);
    1309        3484 :                                                                                                                     assert(succ_iter->B_to_C->pred->succ ==
    1310             :                                                                                                                                                     succ_iter);
    1311        3484 :                                                                                                                     assert(succ_iter->B_to_C->pred->source==s);
    1312        3484 :                                                                                                                     mCRL2complexity(succ_iter->B_to_C->pred,
    1313             :                                                                                                                                 no_temporary_work(max_B,
    1314             :                                                                                                                                        max_C, max_B, false), );
    1315             :                                                                                                                 // end for
    1316             :                                                                                                                 }
    1317             :                                                                                                             // end if
    1318             :                                                                                                             }
    1319             :                                                                                                             else
    1320             :                                                                                                             {
    1321       24006 :                                                                                                                 --nr_of_reachable_constlns;
    1322             :                                                                                                             }
    1323             :                                                                                                     // end for
    1324       30049 :                                                                                                             if (s->succ_end() <= succ_iter)  break;
    1325        4819 :                                                                                                             assert(0 != nr_of_reachable_constlns);
    1326        4819 :                                                                                                             assert(*targetC < *succ_iter->target->constln());
    1327        4819 :                                                                                                         }
    1328             :                                                                                                     }
    1329             :                                                                                                     // if s is a nonbottom state then
    1330       26233 :                                                                                                     if (s_iter < B->bottom_begin())
    1331             :                                                                                                     {
    1332        3060 :                                                                                                         assert(s->inert_succ_begin() < s->inert_succ_end());
    1333        3060 :                                                                                                         nr_of_inert_successors -=
    1334        6120 :                                                                                                                    s->inert_succ_end() - s->inert_succ_begin();
    1335             :                                                                                                         // the following assertion is necessary because s must
    1336             :                                                                                                         // have a transition to its own constellation (namely
    1337             :                                                                                                         // an inert one), but this constln_slice is not
    1338             :                                                                                                         // counted.
    1339        3060 :                                                                                                         assert(0 != nr_of_reachable_constlns);
    1340             : 
    1341             :                                                                                                         #ifdef PARANOID_CHECK
    1342             :                                                                                                             // assert that s can reach a bottom state
    1343        3060 :                                                                                                             assert(STATE_TYPE_MAX == s->notblue);
    1344        3060 :                                                                                                             const_cast<state_type&>(s->notblue) = 1;
    1345             :                                                                                                         #endif
    1346             :                                                                                                     }
    1347             :                                                                                                     else
    1348             :                                                                                                     {
    1349             :                                                                                                         // (s is a bottom state.)
    1350             :                                                                                                         // assert that not too few constellations are
    1351             :                                                                                                         // reachable.
    1352       23173 :                                                                                                         assert((state_type) to_own_constln ==
    1353             :                                                                                                                                      nr_of_reachable_constlns);
    1354       23173 :                                                                                                         assert(s->inert_succ_begin() == s->inert_succ_end());
    1355             :                                                                                                         // the following assertions are necessary because it
    1356             :                                                                                                         // could be that the state has no transition to its own
    1357             :                                                                                                         // constellation.
    1358       23173 :                                                                                                         assert(s->succ_begin() == s->inert_succ_begin() ||
    1359             :                                                                                                            *s->inert_succ_begin()[-1].target->constln() <= *C);
    1360       23173 :                                                                                                         assert(s->inert_succ_end() == s->succ_end() ||
    1361             :                                                                                                                  *s->inert_succ_end()->target->constln() > *C);
    1362             :                                                                                                     }
    1363             : 
    1364             :                                                                                                     // for all noninert predecessors of s do
    1365       55974 :                                                                                                     for (pred_const_iter_t pred_iter=s->noninert_pred_begin();
    1366       55974 :                                                                                                                pred_iter < s->noninert_pred_end(); ++pred_iter)
    1367             :                                                                                                     {
    1368             :                                                                                                         // assert some properties of the predecessor
    1369       29741 :                                                                                                         assert(pred_iter->succ->B_to_C->B_to_C_slice->
    1370             :                                                                                                                                             from_block() != B);
    1371       29741 :                                                                                                         assert(pred_iter->succ->B_to_C->B_to_C_slice->
    1372             :                                                                                                                                             to_constln() == C);
    1373       29741 :                                                                                                         assert(pred_iter->succ->target == s);
    1374       29741 :                                                                                                         assert(pred_iter->source->block != B);
    1375             :                                                                                                     // end for
    1376             :                                                                                                     }
    1377             :                                                                                                     #ifndef PARANOID_CHECK
    1378             :                                                                                                         // for all inert predecessors of s do
    1379             :                                                                                                         for (pred_const_iter_t pred_iter=s->inert_pred_begin();
    1380             :                                                                                                                   pred_iter < s->inert_pred_end(); ++pred_iter)
    1381             :                                                                                                         {
    1382             :                                                                                                             // assert some properties of the predecessor
    1383             :                                                                                                             assert(pred_iter->succ->B_to_C->B_to_C_slice->
    1384             :                                                                                                                                             from_block() == B);
    1385             :                                                                                                             assert(pred_iter->succ->B_to_C->B_to_C_slice->
    1386             :                                                                                                                                             to_constln() == C);
    1387             :                                                                                                             assert(pred_iter->succ->target == s);
    1388             :                                                                                                             assert(pred_iter->source->block == B);
    1389             :                                                                                                             assert(pred_iter->source->pos<B->nonbottom_end());
    1390             :                                                                                                         // end for
    1391             :                                                                                                         }
    1392             :                                                                                                     #endif
    1393             :                                                                                                 // end for (all states s in B)
    1394             :                                                                                                 }
    1395       26233 :                                                                                                 while (++s_iter < B->end());
    1396       10406 :                                                                                                 assert(0 == nr_of_inert_successors);
    1397             :                                                                                             // end for (all blocks B in C)
    1398       10406 : /* ************************************************************************* */                 if (B->end() == C->end())  break;
    1399        2187 : /*                                                                           */                 assert(B->end() < C->end());
    1400        2187 : /*                            A L G O R I T H M S                            */                 assert(B->end() == (*B->end())->block->begin());
    1401        2187 : /*                                                                           */                 B = (*B->end())->block;
    1402        2187 : /* ************************************************************************* */             }
    1403             :                                                                                         // end for (all constellations C)
    1404        8775 :                                                                                             if (C->end() == part_st.permutation.end())  break;
    1405        7663 :                                                                                             assert(C->end() < part_st.permutation.end());
    1406        7663 :                                                                                             assert(C->end() == (*C->end())->constln()->begin());
    1407        7663 :                                                                                             C = (*C->end())->constln();
    1408        7663 : /*===========================================================================*/         }
    1409         556 : /*                           initialisation helper                           */         assert(0 == nr_of_nontrivial_constellations);
    1410        1112 : /*===========================================================================*/         return;
    1411             :                                                                                     }
    1412             :                                                                                 #endif
    1413             : /// \brief constructor of the helper class
    1414             : template<class LTS_TYPE>
    1415          55 : bisim_partitioner_gjkw_initialise_helper<LTS_TYPE>::
    1416             : bisim_partitioner_gjkw_initialise_helper(LTS_TYPE& l, bool const branching,
    1417             :                                                 bool const preserve_divergence)
    1418             :   : aut(l),
    1419             :     nr_of_states(l.num_states()),
    1420             :     orig_nr_of_states(l.num_states()),
    1421             :     nr_of_transitions(l.num_transitions()),
    1422             :     noninert_out_per_state(l.num_states(), 0),
    1423             :     inert_out_per_state(l.num_states(), 0),
    1424             :     noninert_in_per_state(l.num_states(), 0),
    1425             :     inert_in_per_state(l.num_states(), 0),
    1426             :     noninert_out_per_block(1, 0),
    1427             :     inert_out_per_block(1, 0),
    1428             :     states_per_block(1, l.num_states()),
    1429          55 :     nr_of_nonbottom_states(0)
    1430             : {
    1431             :     // log::mcrl2_logger::set_reporting_level(log::debug);
    1432             : 
    1433          55 :     mCRL2log(log::verbose) << "O(m log n) "
    1434             :                     << (preserve_divergence ? "Divergence preserving b" : "B")
    1435             :                     << (branching ? "ranching b" : "")
    1436           0 :                     << "isimulation partitioner created for " << l.num_states()
    1437           0 :                     << " states and " << l.num_transitions()
    1438             :                     << " transitions [GJKW 2017]\n";
    1439             :     // Iterate over the transitions and collect new states
    1440         781 :     for (const transition& t: aut.get_transitions())
    1441             :     {
    1442        1186 :         if (!branching || !aut.is_tau(aut.apply_hidden_label_map(t.label())) ||
    1443         195 :                                    (preserve_divergence && t.from() == t.to()))
    1444             :         {
    1445             :             // (possibly) create new state
    1446         460 :             Key const k(aut.apply_hidden_label_map(t.label()), t.to());
    1447             :             std::pair<typename std::unordered_map<Key, state_type,
    1448         920 :                 KeyHasher>::iterator,bool> extra_state = extra_kripke_states.
    1449         920 :                                     insert(std::make_pair(k, nr_of_states));
    1450         460 :             if (extra_state.second)
    1451             :             {
    1452         390 :                 noninert_in_per_state.push_back(0);
    1453         390 :                 inert_in_per_state.push_back(0);
    1454         390 :                 noninert_out_per_state.push_back(0);
    1455         390 :                 inert_out_per_state.push_back(0);
    1456             : 
    1457             :                 // (possibly) create new block
    1458             :                 std::pair<std::unordered_map<label_type, state_type>::iterator,
    1459         780 :                     bool> const action_block = action_block_map.insert(
    1460         780 :                           std::make_pair(aut.apply_hidden_label_map(t.label()),
    1461         780 :                                                      states_per_block.size()));
    1462         390 :                 if (action_block.second)
    1463             :                 {
    1464         136 :                     noninert_out_per_block.push_back(0);
    1465         136 :                     inert_out_per_block.push_back(0);
    1466         136 :                     states_per_block.push_back(0);
    1467             :                 }
    1468             : 
    1469         390 :                 ++noninert_in_per_state[t.to()];
    1470         390 :                 ++noninert_out_per_state[nr_of_states];
    1471         390 :                 ++noninert_out_per_block[action_block.first->second];
    1472         390 :                 ++states_per_block[action_block.first->second];
    1473         390 :                 ++nr_of_states;
    1474         390 :                 ++nr_of_transitions;
    1475             :             }
    1476         460 :             ++noninert_in_per_state[extra_state.first->second];
    1477         460 :             ++noninert_out_per_state[t.from()];
    1478         460 :             ++noninert_out_per_block[0];
    1479             :         }
    1480             :         else
    1481             :         {
    1482         266 :             ++inert_in_per_state[t.to()];
    1483         266 :             if (1 == ++inert_out_per_state[t.from()])
    1484             :             {
    1485             :                 // this is the first inert outgoing transition of t.from()
    1486         187 :                 ++nr_of_nonbottom_states;
    1487             :             }
    1488         266 :             ++inert_out_per_block[0];
    1489             :         }
    1490             :     }
    1491          55 :     mCRL2log(log::verbose) << "Number of extra states: "
    1492           0 :                                          << extra_kripke_states.size() << "\n";
    1493             :                                                                                 #ifndef NDEBUG
    1494          55 :                                                                                     check_complexity::init(nr_of_states);
    1495             :                                                                                 #endif
    1496          55 : }
    1497             : 
    1498             : 
    1499             : /// \brief initialise the state in part_st and the transitions in part_tr
    1500             : template<class LTS_TYPE>
    1501          55 : inline void bisim_partitioner_gjkw_initialise_helper<LTS_TYPE>::
    1502             : init_transitions(part_state_t& part_st, part_trans_t& part_tr,
    1503             :                           bool const branching, bool const preserve_divergence)
    1504          55 : {                                                                               assert(part_st.state_size() == get_nr_of_states());
    1505          55 :                                                                                 assert(part_tr.trans_size() == get_nr_of_transitions());
    1506             :     // initialise blocks and B_to_C slices
    1507          55 :     permutation_iter_t begin = part_st.permutation.begin();
    1508         165 :     constln_t* const constln = new constln_t(get_nr_of_states(), begin,
    1509         110 :                               part_st.permutation.end(), part_tr.B_to_C_end());
    1510          55 :     if (1 < states_per_block.size())
    1511             :     {
    1512          54 :         constln->make_nontrivial();
    1513             :     }
    1514         110 :     std::vector<block_t*> blocks(states_per_block.size());
    1515          55 :     B_to_C_iter_t B_to_C_begin = part_tr.B_to_C.begin();
    1516         246 :     for (state_type B = 0; B < states_per_block.size(); ++B)
    1517             :     {
    1518         191 :         permutation_iter_t const end = begin + states_per_block[B];
    1519         191 :         blocks[B] = new block_t(constln, begin, end);
    1520         191 :         if (0 == noninert_out_per_block[B] && 0 == inert_out_per_block[B])
    1521             :         {
    1522           0 :             blocks[B]->set_inert_begin_and_end(part_tr.B_to_C.begin(),
    1523           0 :                                                        part_tr.B_to_C.begin()); assert(blocks[B]->to_constln.empty());
    1524             :         }
    1525             :         else
    1526             :         {
    1527         573 :             blocks[B]->set_inert_begin_and_end(B_to_C_begin +
    1528             :                                                      noninert_out_per_block[B],
    1529         573 :                 B_to_C_begin + noninert_out_per_block[B] +
    1530             :                                                        inert_out_per_block[B]);
    1531         382 :             blocks[B]->to_constln.emplace_back(B_to_C_begin,
    1532         382 :                                                        blocks[B]->inert_end());
    1533         191 :             B_to_C_desc_iter_t const slice =
    1534         382 :                                         std::prev(blocks[B]->to_constln.end()); assert(B_to_C_begin < slice->end);
    1535        2423 :             for (; slice->end != B_to_C_begin; ++B_to_C_begin)
    1536             :             {
    1537        1116 :                 B_to_C_begin->B_to_C_slice = slice;
    1538             :             }
    1539             :         }
    1540         191 :         begin = end;
    1541          55 :     }                                                                           assert(part_st.permutation.end() == begin);
    1542          55 :     /* only block 0 has a sequence number and non-bottom states:             */ assert(part_tr.B_to_C.end() == B_to_C_begin);
    1543          55 :     blocks[0]->assign_seqnr();
    1544          55 :     blocks[0]->set_bottom_begin(blocks[0]->begin() + nr_of_nonbottom_states);
    1545          55 :     blocks[0]->set_marked_nonbottom_begin(blocks[0]->bottom_begin());
    1546             : 
    1547             :     // initialise states and succ slices
    1548          55 :     part_st.state_info.front().set_pred_begin(part_tr.pred.begin());
    1549          55 :     part_st.state_info.front().set_succ_begin(part_tr.succ.begin());
    1550         982 :     for (state_type s = 0; get_nr_of_states() != s; ++s)
    1551             :     {
    1552        1854 :         part_st.state_info[s].set_pred_end(part_st.state_info[s].pred_begin() +
    1553         927 :                              noninert_in_per_state[s] + inert_in_per_state[s]);
    1554        2781 :         part_st.state_info[s].set_inert_pred_begin(part_st.state_info[s].
    1555        2781 :                                       pred_begin() + noninert_in_per_state[s]);
    1556             :         // part_st.state_info[s+1].set_pred_begin(part_st.state_info[s].
    1557             :         //                                                         pred_end());
    1558             : 
    1559         927 :         succ_iter_t succ_iter = part_st.state_info[s].succ_begin();
    1560         927 :         succ_iter_t succ_end = succ_iter +
    1561         927 :                             noninert_out_per_state[s] + inert_out_per_state[s];
    1562         927 :         part_st.state_info[s].set_succ_end(succ_end);
    1563         927 :         part_st.state_info[s].set_current_constln(succ_end);
    1564        2781 :         part_st.state_info[s].set_inert_succ_begin_and_end(part_st.
    1565        2781 :             state_info[s].succ_begin() + noninert_out_per_state[s], succ_end);
    1566         927 :         if (succ_iter < succ_end)
    1567             :         {
    1568         844 :             --succ_end;
    1569        1388 :             for (; succ_iter < succ_end; ++succ_iter)
    1570             :             {
    1571         272 :                 succ_iter->set_slice_begin_or_before_end(succ_end);
    1572         844 :             }                                                                   assert(succ_iter == succ_end);
    1573        1688 :             succ_end->set_slice_begin_or_before_end(
    1574         844 :                                            part_st.state_info[s].succ_begin());
    1575          83 :         }                                                                       else  assert(succ_end == succ_iter);
    1576         927 :         if (s < aut.num_states())
    1577             :         {
    1578             :             // s is not an extra Kripke state.  It is in block 0.
    1579         537 :             part_st.state_info[s].block = blocks[0];
    1580         537 :             if (0 != inert_out_per_state[s])
    1581             :             {
    1582         187 :                 /* non-bottom state:                                         */ assert(0 != nr_of_nonbottom_states);
    1583         187 :                 --nr_of_nonbottom_states;
    1584         187 :                 part_st.state_info[s].pos = blocks[0]->begin() +
    1585         187 :                                                         nr_of_nonbottom_states;
    1586             :             }
    1587             :             else
    1588             :             {                                                                   // The following assertion is incomplete; only the second
    1589             :                 // bottom state:                                                // assertion (after the assignment) makes sure that not too
    1590             :                                                                                 // many states become part of this slice.
    1591         350 :                                                                                 assert(0 != states_per_block[0]);
    1592         350 :                 --states_per_block[0];
    1593         350 :                 part_st.state_info[s].pos = blocks[0]->begin() +
    1594         350 :                                                            states_per_block[0]; assert(part_st.state_info[s].pos >= blocks[0]->bottom_begin());
    1595             :             }
    1596         537 :             *part_st.state_info[s].pos = &part_st.state_info[s];
    1597             :             // part_st.state_info[s].notblue = 0;
    1598             :         }
    1599             :     }
    1600             : 
    1601             :     // initialise transitions (and finalise extra Kripke states)
    1602         781 :     for (const transition& t: aut.get_transitions())
    1603             :     {
    1604        1186 :         if (!branching || !aut.is_tau(aut.apply_hidden_label_map(t.label())) ||
    1605         195 :                                    (preserve_divergence && t.from() == t.to()))
    1606             :         {
    1607             :             // take transition through an extra intermediary state
    1608         460 :             Key const k(aut.apply_hidden_label_map(t.label()), t.to());
    1609         460 :             state_type const extra_state = extra_kripke_states[k];
    1610         460 :             if (0 != noninert_out_per_state[extra_state])
    1611             :             {
    1612         390 :                 state_type const extra_block =
    1613         780 :                        action_block_map[aut.apply_hidden_label_map(t.label())];
    1614             :                 // now initialise extra_state correctly
    1615         390 :                 part_st.state_info[extra_state].block = blocks[extra_block];    assert(0 != states_per_block[extra_block]);
    1616         390 :                 --states_per_block[extra_block];
    1617         390 :                 part_st.state_info[extra_state].pos = blocks[extra_block]->
    1618         780 :                                        begin() + states_per_block[extra_block];
    1619         390 :                 *part_st.state_info[extra_state].pos =
    1620         390 :                                               &part_st.state_info[extra_state];
    1621             :                 // part_st.state_info[extra_state].notblue = 0;
    1622             : 
    1623             :                 // state extra_state has exactly one outgoing transition,
    1624             :                 // namely a noninert transition to to t.to().  It has to be
    1625         390 :                 /* initialised now.                                          */ assert(0 != noninert_in_per_state[t.to()]);
    1626         390 :                 --noninert_in_per_state[t.to()];
    1627         390 :                 pred_iter_t const t_pred =
    1628         780 :                              part_st.state_info[t.to()].noninert_pred_begin() +
    1629             :                                                  noninert_in_per_state[t.to()];
    1630         390 :                 --noninert_out_per_state[extra_state];                          assert(0 == noninert_out_per_state[extra_state]);
    1631         390 :                 succ_iter_t const t_succ =
    1632         780 :                                   part_st.state_info[extra_state].succ_begin(); assert(0 != noninert_out_per_block[extra_block]);
    1633         390 :                 B_to_C_iter_t const t_B_to_C =
    1634         780 :                                          blocks[extra_block]->inert_begin() -
    1635         390 :                                          noninert_out_per_block[extra_block]--;
    1636         390 :                 t_pred->source = &part_st.state_info[extra_state];
    1637         390 :                 t_pred->succ = t_succ;
    1638         390 :                 t_succ->target = &part_st.state_info[t.to()];
    1639         390 :                 t_succ->B_to_C = t_B_to_C;
    1640             :                 // t_B_to_C->B_to_C_slice = (already initialised);
    1641         390 :                 t_B_to_C->pred = t_pred;
    1642             :             }
    1643         460 :             /* noninert transition from t.from() to extra_state              */ assert(0 != noninert_in_per_state[extra_state]);
    1644         460 :             --noninert_in_per_state[extra_state];
    1645         460 :             pred_iter_t const t_pred =
    1646         920 :                         part_st.state_info[extra_state].noninert_pred_begin() +
    1647         460 :                                             noninert_in_per_state[extra_state]; assert(0 != noninert_out_per_state[t.from()]);
    1648         460 :             --noninert_out_per_state[t.from()];
    1649         460 :             succ_iter_t const t_succ=part_st.state_info[t.from()].succ_begin()+
    1650         460 :                                               noninert_out_per_state[t.from()]; assert(0 != noninert_out_per_block[0]);
    1651         460 :             B_to_C_iter_t const t_B_to_C = blocks[0]->inert_begin() -
    1652         460 :                                                    noninert_out_per_block[0]--;
    1653             : 
    1654         460 :             t_pred->source = &part_st.state_info[t.from()];
    1655         460 :             t_pred->succ = t_succ;
    1656         460 :             t_succ->target = &part_st.state_info[extra_state];
    1657         460 :             t_succ->B_to_C = t_B_to_C;
    1658             :             // t_B_to_C->B_to_C_slice = (already initialised);
    1659         460 :             t_B_to_C->pred = t_pred;
    1660             :         }
    1661             :         else
    1662             :         {
    1663         266 :             /* inert transition from t.from() to t.to()                      */ assert(0 != inert_in_per_state[t.to()]);
    1664         266 :             --inert_in_per_state[t.to()];
    1665         266 :             pred_iter_t const t_pred =
    1666         532 :                                 part_st.state_info[t.to()].inert_pred_begin() +
    1667         266 :                                                     inert_in_per_state[t.to()]; assert(0 != inert_out_per_state[t.from()]);
    1668         266 :             --inert_out_per_state[t.from()];
    1669         266 :             succ_iter_t const t_succ =
    1670         532 :                               part_st.state_info[t.from()].inert_succ_begin() +
    1671         266 :                                                  inert_out_per_state[t.from()]; assert(0 != inert_out_per_block[0]);
    1672         266 :             --inert_out_per_block[0];
    1673         266 :             B_to_C_iter_t const t_B_to_C = blocks[0]->inert_begin() +
    1674             :                                                         inert_out_per_block[0];
    1675             : 
    1676         266 :             t_pred->source = &part_st.state_info[t.from()];
    1677         266 :             t_pred->succ = t_succ;
    1678         266 :             t_succ->target = &part_st.state_info[t.to()];
    1679         266 :             t_succ->B_to_C = t_B_to_C;
    1680             :             // t_B_to_C->B_to_C_slice = (already initialised);
    1681         266 :             t_B_to_C->pred = t_pred;
    1682             :         }
    1683             :     }
    1684          55 :     noninert_out_per_state.clear(); inert_out_per_state.clear();
    1685          55 :     noninert_in_per_state.clear();  inert_in_per_state.clear();
    1686          55 :     noninert_out_per_block.clear(); inert_out_per_block.clear();
    1687          55 :     states_per_block.clear();
    1688             : 
    1689          55 :     aut.clear_transitions();
    1690             : 
    1691          55 :     mCRL2log(log::verbose) << "Size of the resulting Kripke structure: "
    1692           0 :                                << get_nr_of_states() << " states and "
    1693           0 :                                << get_nr_of_transitions() << " transitions.\n";
    1694          55 : }
    1695             : 
    1696             : /// \brief Replaces the transition relation of the current LTS by the
    1697             : /// transitions of the bisimulation-reduced transition system.
    1698             : /// \details Each transition (s, l, s') is replaced by a transition (t, l, t'),
    1699             : /// where t and t' are the equivalence classes of s and s', respectively.  If
    1700             : /// the label l is internal, then the transition is only added if t != t' or
    1701             : /// preserve_divergence == true.  This effectively removes all inert
    1702             : /// transitions.  Duplicates are removed from the transitions in the new LTS.
    1703             : ///
    1704             : /// Note that the number of states nor the initial state are not adapted by
    1705             : /// this method.  These must be set separately.
    1706             : ///
    1707             : /// The code is very much inspired by liblts_bisim_gw.h, which was written by
    1708             : /// Anton Wijs.
    1709             : ///
    1710             : /// \pre The bisimulation equivalence classes have been computed.
    1711             : /// \param branching Causes non-internal transitions to be removed.
    1712             : template <class LTS_TYPE>
    1713          53 : void bisim_partitioner_gjkw_initialise_helper<LTS_TYPE>::
    1714             :          replace_transition_system(const part_state_t& part_st,                 ONLY_IF_DEBUG( const bool branching, )
    1715             :                                    const bool preserve_divergence)
    1716             : {
    1717         106 :     std::unordered_map <state_type, Key> to_lts_map;
    1718             :     // obtain a map from state to <action, state> pair from extra_kripke_states
    1719         425 :     for (typename std::unordered_map<Key, state_type, KeyHasher>::iterator it =
    1720         425 :             extra_kripke_states.begin(); it != extra_kripke_states.end(); ++it)
    1721             :     {
    1722         372 :         to_lts_map.insert(std::make_pair(it->second, it->first));
    1723             :     }
    1724          53 :     extra_kripke_states.clear();
    1725             : 
    1726          53 :     label_type const tau_label = aut.tau_label_index();
    1727             :     // In the following loop, we visit a bottom state of each block and take
    1728             :     // its transitions.  As the partition is (assumed to be) stable, in this
    1729             :     // way we visit each transition of a lumped state exactly once.
    1730         320 :     for (permutation_const_iter_t s_iter = part_st.permutation.begin();
    1731         320 :                                  part_st.permutation.end() != s_iter; ++s_iter)
    1732             :     {
    1733         319 :         block_t *B = (*s_iter)->block;
    1734             :         // forward to last state of block, i. e. to a bottom state:
    1735         319 :         s_iter = B->end() - 1;                                                  assert(B->bottom_end() > s_iter);  assert(B->bottom_begin() <= s_iter);
    1736         319 :                                                                                 assert(B->end() == B->constln()->end());
    1737         319 :         state_type const s_eq = B->seqnr();
    1738         319 :         if (BLOCK_NO_SEQNR == s_eq)
    1739             :         {
    1740          52 :             break;
    1741             :         }
    1742             : 
    1743         677 :         for (succ_const_iter_t succ_iter = (*s_iter)->succ_begin();
    1744         677 :                                           (*s_iter)->succ_end() != succ_iter; )
    1745             :         {
    1746         410 :             if (state_type t_eq = succ_iter->target->block->seqnr();
    1747             :                                                         BLOCK_NO_SEQNR != t_eq)
    1748          85 :             {                                                                   assert(branching);
    1749             :                 // We have a transition that originally was inert.
    1750          85 :                 if (s_eq == t_eq)
    1751             :                 {
    1752             :                     // The transition is still inert.
    1753           0 :                     if (!preserve_divergence)
    1754             :                     {
    1755             :                         // As we do not preserve divergence, we do not add it.
    1756             :                         // Nor will we add other transitions to the same
    1757             :                         // constellation.
    1758           0 :                         succ_iter = succ_entry::slice_end(succ_iter);
    1759           0 :                         continue;
    1760             :                     }
    1761           0 :                     if (*s_iter != succ_iter->target)
    1762             :                     {
    1763             :                         // The transition was not a self-loop to start with.
    1764             :                         // So we do not add it either.
    1765           0 :                         ++succ_iter;
    1766           0 :                         continue;
    1767             :                     }
    1768          85 :                 }                                                               assert((label_type) -1 != tau_label);
    1769          85 :                 aut.add_transition(transition(s_eq, tau_label, t_eq));
    1770             :             }
    1771             :             else
    1772             :             {
    1773         650 :                 state_type const tgt_id = succ_iter->target -
    1774         325 :                                                    &part_st.state_info.front();
    1775             :                 // We have a non-inert transition to an intermediary state.
    1776             :                 // Look up the label and where the transition from the
    1777             :                 // intermediary state goes.
    1778         325 :                 Key const k = to_lts_map.find(tgt_id)->second;
    1779         325 :                 t_eq = part_st.state_info[k.second].block->seqnr();             assert(BLOCK_NO_SEQNR != t_eq);
    1780         325 :                 aut.add_transition(transition(s_eq, k.first, t_eq));            // The target state could also be found through the pointer
    1781             :                                                                                 // structure (but we also need the labels, which are not stored
    1782             :                                                                                 // in the refinable partition):
    1783         325 :                                                                                 assert(&part_st.state_info[k.second]==succ_iter->target->succ_begin()->target);
    1784         325 :                                                                                 assert(1 == succ_iter->target->succ_end() - succ_iter->target->succ_begin());
    1785             :             }
    1786             :             // Skip over other transitions from the same state to the same
    1787             :             // constellation -- they would be mapped to the same resulting
    1788             :             // transition.
    1789         410 :             succ_iter = succ_entry::slice_end(succ_iter);
    1790             :         }
    1791             :     }
    1792             : 
    1793             :     // Merge the states, by setting the state labels of each state to the concatenation of the state labels of its
    1794             :     // equivalence class.
    1795             : 
    1796          53 :     if (aut.has_state_info())   /* If there are no state labels this step can be ignored */
    1797             :     {
    1798             :       /* Create a vector for the new labels */
    1799           0 :       std::vector<typename LTS_TYPE::state_label_t> new_labels(block_t::nr_of_blocks);
    1800             : 
    1801           0 :       for(std::size_t i=aut.num_states(); i>0; )
    1802             :       {
    1803           0 :         --i;
    1804           0 :         const std::size_t new_index=part_st.block(i)->seqnr();  /* get_eq_class(i) */
    1805           0 :         new_labels[new_index] = new_labels[new_index] + aut.state_label(i);
    1806             :       }
    1807             : 
    1808           0 :       aut.set_num_states(block_t::nr_of_blocks);
    1809           0 :       for(std::size_t i=0; i<block_t::nr_of_blocks; ++i)
    1810             :       {
    1811           0 :         aut.set_state_label(i,new_labels[i]);
    1812             :       }
    1813             :     }
    1814             :     else
    1815             :     {
    1816          53 :       aut.set_num_states(block_t::nr_of_blocks);
    1817             :     }
    1818             : 
    1819          53 :     aut.set_initial_state(part_st.block(aut.initial_state())->seqnr());
    1820          53 : }
    1821             : 
    1822             : } // end namespace bisim_gjkw
    1823             : 
    1824             : 
    1825             : 
    1826             : /*=============================================================================
    1827             : =            dbStutteringEquivalence -- Algorithm 2 in [GJKW 2017]            =
    1828             : =============================================================================*/
    1829             : 
    1830             : 
    1831             : 
    1832             : template <class LTS_TYPE>
    1833          55 : void bisim_partitioner_gjkw<LTS_TYPE>::create_initial_partition_gjkw(
    1834             :                           bool const branching, bool const preserve_divergence)
    1835             : {
    1836             :     // 2.2: P := P_0, i. e. the initial, cycle-free partition; C = {S}
    1837             :     // and
    1838             :     // 2.3: Initialise all temporary data
    1839          55 :     init_helper.init_transitions(part_st, part_tr, branching,
    1840             :                                                           preserve_divergence);
    1841          55 : }
    1842             : 
    1843             : 
    1844             : template <class LTS_TYPE>
    1845          55 : void bisim_partitioner_gjkw<LTS_TYPE>::
    1846             :                                 refine_partition_until_it_becomes_stable_gjkw()
    1847             : {
    1848             :                                                                                 #ifndef NDEBUG
    1849          55 :                                                                                     if (mCRL2logEnabled(log::debug, "bisim_gjkw"))
    1850             :                                                                                     {
    1851           0 :                                                                                         part_st.print_part(part_tr);
    1852           0 :                                                                                         part_st.print_trans();
    1853             :                                                                                     }
    1854             : 
    1855          55 :                                                                                     part_tr.assert_stability(part_st);
    1856             :                                                                                 #endif
    1857             :     // 2.4: while C contains a nontrivial constellation SpC do
    1858        1057 :     while (nullptr != bisim_gjkw::constln_t::get_some_nontrivial())
    1859             :     {                                                                           // check_complexity::add_work is called below, after SpB has been found
    1860         501 :         bisim_gjkw::constln_t* const SpC =
    1861             :                                   bisim_gjkw::constln_t::get_some_nontrivial();
    1862             :         // 2.5: Choose a small splitter block SpB subset of SpC from P,
    1863             :         //      i.e. |SpB| <= 1/2*|SpC|
    1864             :         // and
    1865             :         // 2.6: Create a new constellation NewC and move SpB from SpC to NewC
    1866             :         // and
    1867             :         // 2.7: C := partition C where SpB is removed from SpC and NewC is
    1868             :         //      added
    1869         501 :         bisim_gjkw::block_t* const SpB = SpC->split_off_small_block();
    1870         501 :         bisim_gjkw::constln_t* const NewC = SpB->constln();
    1871             :                                                                                 #ifndef NDEBUG
    1872        1002 :                                                                                     unsigned const max_counter = bisim_gjkw::check_complexity::log_n -
    1873         501 :         /*-------------------- find predecessors of SpB ---------------------*/                               bisim_gjkw::check_complexity::ilog2(SpB->size());
    1874             :                                                                                 #endif
    1875         501 :         /* 2.8: Mark block SpB as refinable                                  */ mCRL2complexity(SpB, add_work(bisim_gjkw::check_complexity::
    1876             :         /* 2.9: Mark all states of SpB as predecessors                       */               while_C_contains_a_nontrivial_constellation_2_4, max_counter), );
    1877         501 :             /* we deviate from the published algorithm: only states with a   */ assert(nullptr == bisim_gjkw::block_t::get_some_refinable());
    1878             :             // transition to SpC will be marked.  SpB will be split separately.
    1879             :         // 2.17: Register that the transitions from s to inert_out(s) go to
    1880             :         //       NewC (instead of SpC)
    1881             :             // (Before we enter the loop, we already adapt the ``B_to_C''
    1882             :             // transition array.)
    1883         501 :         part_tr.split_inert_to_C(SpB);
    1884             :         // 2.10: for all s in SpB do
    1885         501 :             /* We have to walk through the states from end to beginning so   */ mCRL2complexity(SpB, add_work(bisim_gjkw::check_complexity::
    1886             :             /* we can mark state s if necessary.  Marking will move s to a   */                                         for_all_s_in_SpB_2_10, max_counter), );
    1887             :             // position that has already been visited.
    1888        1450 :         for (bisim_gjkw::permutation_iter_t s_iter = SpB->end();
    1889        1450 :                                                       SpB->begin() != s_iter; )
    1890             :         {
    1891         949 :             --s_iter;
    1892         949 :             bisim_gjkw::state_info_ptr const s = *s_iter;                       // mCRL2complexity(s, ...) -- optimized to the above call.
    1893             :             // 2.11: for all s_prime in noninert_in(s) do
    1894        1995 :             for (bisim_gjkw::pred_iter_t pred_iter = s->noninert_pred_begin();
    1895        1995 :                               s->noninert_pred_end() != pred_iter; ++pred_iter)
    1896        1046 :             {                                                                   mCRL2complexity(pred_iter, add_work(bisim_gjkw::
    1897             :                                                                                              check_complexity::for_all_s_prime_in_pred_s_2_11, max_counter), );
    1898        1046 :                                                                                 assert(part_tr.pred_end() > pred_iter);
    1899        1046 :                                                                                 assert(pred_iter->succ->B_to_C->pred == pred_iter);
    1900        1046 :                 bisim_gjkw::state_info_ptr const s_prime = pred_iter->source;
    1901             :                 // 2.12: Mark the block of s_prime as refinable
    1902        1046 :                 bool const first_transition_of_block =
    1903        1046 :                                               s_prime->block->make_refinable();
    1904             :                 // 2.13: Mark s_prime as predecessor of SpB
    1905        1046 :                 bool const first_transition_of_state =
    1906        1046 :                                                  s_prime->block->mark(s_prime);
    1907             :                 // 2.14: Register that s_prime->s goes to NewC (instead of SpC)
    1908             :                 // and
    1909             :                 // 2.15: Store whether s' still has some transition to SpC\SpB
    1910        1046 :                 s_prime->set_current_constln(part_tr.change_to_C(pred_iter,     ONLY_IF_DEBUG( SpC, NewC, )
    1911             :                         first_transition_of_state, first_transition_of_block));
    1912             :             // 2.16: end for
    1913             :             }
    1914             :             // 2.17: Register that the transitions from s to inert_out(s) go to
    1915             :             //       NewC (instead of SpC)
    1916             :                 // (Here, we only adapt the ``succ'' transition array.)
    1917         949 :             if (part_tr.split_s_inert_out(s                                     ONLY_IF_DEBUG( , SpC )
    1918             :                                            ))
    1919             :             {
    1920             :                 // 2.18: Store whether s still has some transition to SpC\SpB
    1921             :                     // we deviate from the explanation of the published
    1922             :                     // algorithm: we store this information by marking states
    1923             :                     // with transitions to SpC.
    1924         425 :                 SpB->mark(s);
    1925             :             }
    1926             :         // 2.19: end for
    1927             :         }
    1928             : 
    1929             :         // second pass through the predecessors to correct the pointers to the
    1930             :         // constln_slices
    1931        1450 :         for (bisim_gjkw::permutation_iter_t s_iter = SpB->begin();
    1932        1450 :                                                 SpB->end() != s_iter; ++s_iter)
    1933             :         {
    1934         949 :             bisim_gjkw::state_info_ptr const s = *s_iter;
    1935        1995 :             for (bisim_gjkw::pred_iter_t pred_iter = s->noninert_pred_begin();
    1936        1995 :                               s->noninert_pred_end() != pred_iter; ++pred_iter)
    1937             :             {
    1938        1046 :                 bisim_gjkw::succ_iter_t succ = pred_iter->succ;
    1939        1046 :                 bisim_gjkw::succ_iter_t before_end =
    1940        2092 :                                       pred_iter->source->current_constln() - 1;
    1941        1046 :                 if (succ != before_end)
    1942          33 :                 {                                                               assert(succ<before_end); assert(succ>=before_end->slice_begin_or_before_end());
    1943          33 :                                                                                 assert(succ->slice_begin_or_before_end() ==
    1944             :                                                                                                                       before_end->slice_begin_or_before_end());
    1945          33 :                     succ->set_slice_begin_or_before_end(before_end);
    1946             :                 }
    1947             :             }
    1948             :         }
    1949             :                                                                                 #ifndef NDEBUG
    1950             :                                                                                     // The following tests cannot be executed during the above loops
    1951             :                                                                                     // because a state s_prime may have multiple transitions to SpB.
    1952        1450 :                                                                                     for (bisim_gjkw::permutation_const_iter_t s_iter = SpB->begin();
    1953        1450 :                                                                                                                                 SpB->end() != s_iter; ++s_iter)
    1954             :                                                                                     {
    1955         949 :                                                                                         bisim_gjkw::state_info_ptr const s = *s_iter;
    1956        1995 :                                                                                         for (bisim_gjkw::pred_const_iter_t pred_iter=s->noninert_pred_begin();
    1957        1995 :                                                                                                               s->noninert_pred_end() != pred_iter; ++pred_iter)
    1958             :                                                                                         {
    1959        1046 :                                                                                             bisim_gjkw::state_info_const_ptr const s_prime = pred_iter->source;
    1960             :                                                                                             // check consistency of s_prime->current_constln()
    1961        1046 :                                                                                             assert(s_prime->succ_begin() == s_prime->current_constln() ||
    1962             :                                                                                                     *s_prime->current_constln()[-1].target->constln() <= *SpC);
    1963        1046 :                                                                                             assert(s_prime->succ_end() == s_prime->current_constln() ||
    1964             :                                                                                                        *SpC <= *s_prime->current_constln()->target->constln());
    1965             :                                                                                                 // s_prime must have a transition to the new constellation
    1966        1046 :                                                                                             assert(s_prime->succ_begin() < s_prime->current_constln());
    1967        1046 :                                                                                             assert(s_prime->current_constln()[-1].target->constln() == NewC);
    1968             :                                                                                             // check consistency of s_prime->inert_succ_begin() and
    1969             :                                                                                             // s_prime->inert_succ_end()
    1970        1046 :                                                                                             assert(s_prime->succ_begin() == s_prime->inert_succ_begin() ||
    1971             :                                                                                                       *s_prime->inert_succ_begin()[-1].target->constln() <=
    1972             :                                                                                                                                           *s_prime->constln());
    1973        1046 :                                                                                             assert(s_prime->succ_begin() == s_prime->inert_succ_begin() ||
    1974             :                                                                                                            s_prime->inert_succ_begin()[-1].target->block !=
    1975             :                                                                                                                                                s_prime->block);
    1976        1046 :                                                                                             assert(s_prime->inert_succ_begin()==s_prime->inert_succ_end()||
    1977             :                                                                                                       (s_prime->inert_succ_begin()->target->block ==
    1978             :                                                                                                                                             s_prime->block &&
    1979             :                                                                                                        s_prime->inert_succ_end()[-1].target->block ==
    1980             :                                                                                                                                               s_prime->block));
    1981        1046 :                                                                                             assert(s_prime->succ_end() == s_prime->inert_succ_end() ||
    1982             :                                                                                                       *s_prime->constln() <
    1983             :                                                                                                                 *s_prime->inert_succ_end()->target->constln());
    1984             :                                                                                         }
    1985             :                                                                                         // check consistency of s->inert_succ_begin() and
    1986             :                                                                                         // s->inert_succ_end()
    1987         949 :                                                                                         assert(s->succ_begin() == s->inert_succ_begin() ||
    1988             :                                                                                                  *s->inert_succ_begin()[-1].target->constln() < *s->constln());
    1989         949 :                                                                                         assert(s->inert_succ_begin() == s->inert_succ_end() ||
    1990             :         /*------------------ stabilise the partition again ------------------*/                       (s->inert_succ_begin()->target->block == s->block &&
    1991             :                                                                                                            s->inert_succ_end()[-1].target->block == s->block));
    1992         949 :         /* deviation from the published algorithm: we first refine the       */         assert(s->succ_end() == s->inert_succ_end() ||
    1993             :         /* splitter according to the marking of states (marked states have a */                       *s->constln() < *s->inert_succ_end()->target->constln());
    1994             :         /* transition to SpC).                                               */     }
    1995             :                                                                                 #endif // ifndef NDEBUG
    1996         501 :         if (0 != SpB->marked_size())
    1997             :         {
    1998         168 :             if (1 == SpB->size())
    1999             :             {
    2000             :                 // if the block only contains a single state, the refinement
    2001             :                 // would be trivial anyway (and it cannot find new bottom
    2002             :                 // states).
    2003          84 :                 SpB->set_marked_bottom_begin(SpB->bottom_end());
    2004             :             }
    2005             :             else
    2006             :             {
    2007          84 :                 bisim_gjkw::block_t* RedB = refine(SpB, SpC, nullptr, false);
    2008          84 :                 if (0 != RedB->unmarked_bottom_size())
    2009             :                 {
    2010           3 :                     postprocess_new_bottom(RedB);
    2011             :                 }
    2012             :                 else
    2013             :                 {
    2014          81 :                     RedB->set_marked_bottom_begin(RedB->bottom_end());
    2015             :                 }
    2016             :             }
    2017             :         }
    2018             : 
    2019             :         // 2.20: for all refinable blocks RfnB do
    2020        1749 :         while (nullptr != bisim_gjkw::block_t::get_some_refinable())
    2021             :         {
    2022         624 :             bisim_gjkw::block_t* const RfnB =
    2023             :                                      bisim_gjkw::block_t::get_some_refinable();
    2024             :             // 2.21: Mark block RfnB as non-refinable
    2025         624 :             RfnB->make_nonrefinable();
    2026             :                                                                                 #ifndef NDEBUG
    2027             :                                                                                     // The work in this loop has to be assigned to the B_to_C-
    2028             :                                                                                     // slice that contains the transitions from RfnB to NewC.
    2029             :                                                                                     // Note that this is not FromRed, so we have to find it in a
    2030             :                                                                                     // different way.  First find a marked state:
    2031         624 :                                                                                     bisim_gjkw::permutation_iter_t s_mark_iter = RfnB->marked_bottom_begin();
    2032         624 :                                                                                     if (s_mark_iter == RfnB->marked_bottom_end())
    2033             :                                                                                     {
    2034          38 :                                                                                         s_mark_iter = RfnB->marked_nonbottom_begin();
    2035          38 :                                                                                         assert(s_mark_iter < RfnB->marked_nonbottom_end());
    2036             :                                                                                     }
    2037             :                                                                                     // Now, using the current_constln pointer of s, find a
    2038             :                                                                                     // transition to NewC.
    2039         624 :                                                                                     bisim_gjkw::succ_iter_t to_NewC =
    2040         624 :                                                                                                                   std::prev((*s_mark_iter)->current_constln());
    2041         624 :                                                                                     assert((*s_mark_iter)->succ_begin() <= to_NewC);
    2042         624 :                                                                                     assert(to_NewC->target->constln() == NewC);
    2043         624 :                                                                                     mCRL2complexity(to_NewC->B_to_C->B_to_C_slice, add_work(
    2044             :                                                                                                            bisim_gjkw::check_complexity::
    2045             :                                                                                                            for_all_refinable_blocks_RfnB_2_20, max_counter), );
    2046             :                                                                                 #endif
    2047         822 :             if (1 == RfnB->size())
    2048             :             {
    2049             :                 // if the block only contains a single state, the refinement
    2050             :                 // would be trivial anyway (and it cannot find new bottom
    2051             :                 // states).
    2052         198 :                 RfnB->set_marked_bottom_begin(RfnB->bottom_end());
    2053         739 :                 continue;
    2054             :             }
    2055             :             // 2.22: <RedB, BlueB> := Refine(RfnB, NewC, {marked states in
    2056             :             //                                                       RfnB}, {})
    2057         426 :             bisim_gjkw::block_t* RedB = refine(RfnB, NewC, nullptr, false);
    2058             :             // 2.23: if RedB contains new bottom states then
    2059         426 :             if (0 != RedB->unmarked_bottom_size())
    2060             :             {
    2061             :                 // 2.24: RedB := PostprocessNewBottom(RedB, BlueB)
    2062          46 :                 RedB = postprocess_new_bottom(RedB);
    2063          46 :                 if (nullptr == RedB)  continue;
    2064             :             // 2.25: end if
    2065             :             }
    2066             :             // 2.30: Unmark all states of the original RfnB as predecessors
    2067             :                 // (first part) This needs to be done to make sure the call to
    2068             :                 // Refine in line 2.26 does not regard some states as marked.
    2069             :             else
    2070             :             {
    2071         380 :                 RedB->set_marked_bottom_begin(RedB->bottom_end());
    2072             :             }
    2073         388 :                                                                                 assert(0 == RedB->marked_size());
    2074         388 :             if (1 == RedB->size() || nullptr == RedB->FromRed(SpC))
    2075             :             {
    2076             :                 // If the block only contains a single state or has no
    2077             :                 // transitions to SpC, the refinement would be trivial anyway
    2078             :                 // (and it cannot find new bottom states).
    2079         305 :                 continue;
    2080             :             }
    2081             : 
    2082             :             // 2.26: <RedB, BlueB> := Refine(RedB, SpC\SpB, {}, {transitions
    2083             :             //                                           from RedB to SpC\SpB})
    2084          83 :             RedB = refine(RedB, SpC, RedB->FromRed(SpC), false                  ONLY_IF_DEBUG( , NewC )
    2085             :                                                               );
    2086             :             // 2.27: if RedB contains new bottom states then
    2087          83 :             if (0 != RedB->unmarked_bottom_size())
    2088             :             {
    2089             :                 // 2.28: PostprocessNewBottom(RedB, BlueB)
    2090           8 :                 postprocess_new_bottom(RedB);
    2091             :             // 2.29: endif
    2092             :             }
    2093             :             // 2.30: Unmark all states of the original RfnB as predecessors
    2094             :                 // if postprocess_new_bottom is called, that procedure already
    2095             :                 // unmarks the new bottom states.
    2096             :             else
    2097             :             {
    2098          75 :                 RedB->set_marked_bottom_begin(RedB->bottom_end());
    2099          83 :             }                                                                   assert(0 == RedB->marked_size());
    2100             :         // 2.31: end for
    2101             :         }
    2102             :                                                                                 #ifndef NDEBUG
    2103         501 :                                                                                     if (mCRL2logEnabled(log::debug, "bisim_gjkw"))
    2104             :                                                                                     {
    2105           0 :                                                                                         part_st.print_part(part_tr);
    2106           0 :                                                                                         part_st.print_trans();
    2107             :                                                                                     }
    2108             : 
    2109         501 :     /* 2.32: end while                                                       */     part_tr.assert_stability(part_st);
    2110             :                                                                                 #endif
    2111             :     }
    2112             :     // 2.33: return P
    2113             :         // (this happens implicitly, through the bisim_partitioner_gjkw object
    2114             :         // data)
    2115          55 :     mCRL2log(log::verbose) << "number of blocks in the quotient: "
    2116           0 :                                   << bisim_gjkw::block_t::nr_of_blocks << '\n';
    2117          55 : }
    2118             :                                                                                 #ifndef NDEBUG
    2119             :                                                                                     namespace bisim_gjkw
    2120             :                                                                                     {
    2121             : /*=============================================================================
    2122             : =                     Refine -- Algorithm 3 in [GJKW 2017]                    =
    2123             : =============================================================================*/
    2124             :                                                                                     /// \brief moves temporary counters to normal ones if the blue block is
    2125             :                                                                                     /// smaller
    2126             :                                                                                     /// \details When a refinement has finished and the blue block turns out to
    2127             :                                                                                     /// be smaller, this function moves the corresponding temporary work to the
    2128             :                                                                                     /// normal counters and cancels the work on the red state counters.
    2129             :                                                                                     /// \param BlueB  pointer to the blue block
    2130             :                                                                                     /// \param RedB   pointer to the red block
    2131             :                                                                                     /// \param NewC   (only needed if called after the refinement in line 2.26)
    2132             :                                                                                     ///               pointer to the constellation NewC, i. e. the
    2133             :                                                                                     ///               constellation that was used as the basis of marking
    2134             :                                                                                     ///               states.  If blue_is_smaller() is called from another
    2135             :                                                                                     ///               place, this parameter should be nullptr.
    2136         269 :                                                                                     static void blue_is_smaller(block_t* BlueB, block_t* RedB,
    2137             :                                                                                                                                          const constln_t* NewC)
    2138             :                                                                                     {
    2139         269 :                                                                                         assert(nullptr != RedB);
    2140         269 :                                                                                         if (nullptr != BlueB)
    2141             :                                                                                         {
    2142          57 :                                                                                             assert(BlueB->size() <= RedB->size());
    2143         114 :                                                                                             unsigned const max_NewB = nullptr == BlueB ? 0
    2144         114 :                                                                                               : check_complexity::log_n-check_complexity::ilog2(BlueB->size());
    2145         211 :                                                                                             for (permutation_iter_t i = BlueB->begin(); BlueB->end() != i; ++i)
    2146             :                                                                                             {
    2147         154 :                                                                                                 state_info_ptr s = *i;
    2148         154 :                                                                                                 mCRL2complexity(s, finalise_work(check_complexity::
    2149             :                                                                                                                   while_Test_is_not_empty_3_6l_s_is_blue_3_11l,
    2150             :                                                                                                                   check_complexity::refine_bottom_state_3_6l,
    2151             :                                                                                                                   max_NewB), );
    2152         154 :                                                                                                 mCRL2complexity(s, finalise_work(check_complexity::
    2153             :                                                                                                                    while_Blue_contains_unvisited_states_3_15l,
    2154             :                                                                                                                    check_complexity::refine_visited_state_3_15,
    2155             :                                                                                                                    max_NewB), );
    2156         367 :                                                                                                 for (succ_iter_t succ = s->succ_begin(); s->succ_end() != succ;
    2157             :                                                                                                                                                         ++succ)
    2158             :                                                                                                 {
    2159         213 :                                                                                                     mCRL2complexity(succ->B_to_C->pred,finalise_work(
    2160             :                                                                                                            check_complexity::
    2161             :                                                                                                            if___s_prime_has_transition_to_SpC_3_23l,
    2162             :                                                                                                            check_complexity::
    2163             :                                                                                                            refine_outgoing_transition_3_6_or_23l, max_NewB), );
    2164             :                                                                                                 }
    2165         351 :                                                                                                 for (pred_iter_t pred = s->pred_begin(); s->pred_end() != pred;
    2166             :                                                                                                                                                         ++pred)
    2167             :                                                                                                 {
    2168         197 :                                                                                                     mCRL2complexity(pred, finalise_work(check_complexity::
    2169             :                                                                                                              for_all_s_prime_in_pred_s_setminus_Red_3_18l,
    2170             :                                                                                                              check_complexity::refine_incoming_transition_3_18,
    2171             :                                                                                                              max_NewB), );
    2172             :                                                                                                 }
    2173             :                                                                                             }
    2174             :                                                                                         }
    2175             :                                                                                         // cancel work counters for the red states, and also measure the work
    2176             :                                                                                         // done in the blue coroutine on states that turned out to be red.
    2177         288 :                                                                                         unsigned const max_NewC = nullptr == NewC ? 0
    2178         288 :                                                                                              : check_complexity::log_n - check_complexity::ilog2(NewC->size());
    2179        1489 :                                                                                         for (permutation_iter_t i = RedB->begin(); RedB->end() != i; ++i)
    2180             :                                                                                         {
    2181        1220 :                                                                                             state_info_ptr s = *i;
    2182        1220 :                                                                                             mCRL2complexity(s, cancel_work(check_complexity::
    2183             :                                                                                                                  while_Red_contains_unvisited_states_3_15r), );
    2184        3544 :                                                                                             for (succ_iter_t succ=s->succ_begin(); s->succ_end()!=succ; ++succ)
    2185             :                                                                                             {
    2186        2324 :                                                                                                 mCRL2complexity(succ->B_to_C->pred, cancel_work(
    2187             :                                                                                                          check_complexity::while_FromRed_is_not_empty_3_6r), );
    2188             :                                                                                                 // the following counter should only be set for transitions to
    2189             :                                                                                                 // the splitter constellation.  For others transitions, no
    2190             :                                                                                                 // (temporary) work should have been done.
    2191        2324 :                                                                                                 mCRL2complexity(succ->B_to_C->pred, finalise_work(
    2192             :                                                                                                             check_complexity::
    2193             :                                                                                                             while_Test_is_not_empty_3_6l_s_is_red_3_9l,
    2194             :                                                                                                             check_complexity::
    2195             :                                                                                                             refine_outgoing_transition_to_marked_state_3_6l,
    2196             :                                                                                                             succ->target->constln() == NewC ? max_NewC : 0), );
    2197             :                                                                                                 // the following counter only gets 1 during postprocessing, at
    2198             :                                                                                                 // a time when state s is already stored as bottom state.
    2199        2324 :                                                                                                 mCRL2complexity(succ->B_to_C->pred, finalise_work(
    2200             :                                                                                                      check_complexity::
    2201             :                                                                                                      while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing,
    2202             :                                                                                                      check_complexity::
    2203             :                                                                                                      refine_outgoing_transition_postprocess_new_bottom_3_6l,
    2204             :                                                                                                      1), );
    2205             :                                                                                                 // the following counter only gets 1 before postprocessing, at
    2206             :                                                                                                 // the same time as when it is discovered to be a new bottom
    2207             :                                                                                                 // state
    2208        2324 :                                                                                                 mCRL2complexity(succ->B_to_C->pred, finalise_work(
    2209             :                                                                                                     check_complexity::if___s_prime_has_transition_to_SpC_3_23l,
    2210             :                                                                                                     check_complexity::
    2211             :                                                                                                     refine_outgoing_transition_from_new_bottom_3_23l, 1), );
    2212             :                                                                                             }
    2213        2836 :                                                                                             for (pred_iter_t pred=s->pred_begin(); s->pred_end()!=pred; ++pred)
    2214             :                                                                                             {
    2215        1616 :                                                                                                 mCRL2complexity(pred, cancel_work(check_complexity::
    2216             :                                                                                                                            for_all_s_prime_in_pred_s_3_18r), );
    2217             :                                                                                             }
    2218             :                                                                                         }
    2219             :                                                                                         // check the balance between useful and cancelled work:
    2220         269 :                                                                                         check_complexity::check_temporary_work();
    2221         269 :                                                                                     }
    2222             : 
    2223             :                                                                                     /// \brief moves temporary counters to normal ones if the red block is
    2224             :                                                                                     /// smaller
    2225             :                                                                                     /// \details When a refinement has finished and the red block turns out to
    2226             :                                                                                     /// be smaller, this function moves the corresponding temporary work to the
    2227             :                                                                                     /// normal counters and cancels the work on the blue state counters.
    2228             :                                                                                     /// \param BlueB  pointer to the blue block
    2229             :                                                                                     /// \param RedB   pointer to the red block
    2230         308 :                                                                                     static void red_is_smaller(block_t* BlueB, block_t* RedB)
    2231             :                                                                                     {
    2232         308 :                                                                                         assert(nullptr != BlueB);
    2233         308 :                                                                                         assert(nullptr != RedB);
    2234         308 :                                                                                         assert(BlueB->size() >= RedB->size());
    2235        3163 :                                                                                         for (permutation_iter_t i = BlueB->begin(); BlueB->end() != i; ++i)
    2236             :                                                                                         {
    2237        2855 :                                                                                             state_info_ptr s = *i;
    2238        2855 :                                                                                             mCRL2complexity(s, cancel_work(check_complexity::
    2239             :                                                                                                               while_Test_is_not_empty_3_6l_s_is_blue_3_11l), );
    2240        2855 :                                                                                             mCRL2complexity(s, cancel_work(check_complexity::
    2241             :                                                                                                                 while_Blue_contains_unvisited_states_3_15l), );
    2242        6167 :                                                                                             for (succ_iter_t succ=s->succ_begin(); s->succ_end()!=succ; ++succ)
    2243             :                                                                                             {
    2244        3312 :                                                                                                 mCRL2complexity(succ->B_to_C->pred, cancel_work(
    2245             :                                                                                                                   check_complexity::
    2246             :                                                                                                                   if___s_prime_has_transition_to_SpC_3_23l), );
    2247             :                                                                                             }
    2248        6289 :                                                                                             for (pred_iter_t pred=s->pred_begin(); s->pred_end()!=pred; ++pred)
    2249             :                                                                                             {
    2250        3434 :                                                                                                 mCRL2complexity(pred, cancel_work(check_complexity::
    2251             :                                                                                                               for_all_s_prime_in_pred_s_setminus_Red_3_18l), );
    2252             :                                                                                             }
    2253             :                                                                                         }
    2254         616 :                                                                                         unsigned const max_NewB = check_complexity::log_n -
    2255         616 :                                                                                                                          check_complexity::ilog2(RedB->size());
    2256         842 :                                                                                         for (permutation_iter_t i = RedB->begin(); RedB->end() != i; ++i)
    2257             :                                                                                         {
    2258         534 :                                                                                             state_info_ptr s = *i;
    2259         534 :                                                                                             mCRL2complexity(s, finalise_work(check_complexity::
    2260             :                                                                                                      while_Red_contains_unvisited_states_3_15r,
    2261             :                                                                                                      check_complexity::refine_visited_state_3_15, max_NewB), );
    2262        1359 :                                                                                             for (succ_iter_t succ=s->succ_begin(); s->succ_end()!=succ; ++succ)
    2263             :                                                                                             {
    2264         825 :                                                                                                 mCRL2complexity(succ->B_to_C->pred, finalise_work(
    2265             :                                                                                                            check_complexity::while_FromRed_is_not_empty_3_6r,
    2266             :                                                                                                            check_complexity::
    2267             :                                                                                                            refine_outgoing_transition_3_6_or_23l, max_NewB), );
    2268         825 :                                                                                                 mCRL2complexity(succ->B_to_C->pred, cancel_work(
    2269             :                                                                                                                 check_complexity::
    2270             :                                                                                                                 while_Test_is_not_empty_3_6l_s_is_red_3_9l), );
    2271         825 :                                                                                                 mCRL2complexity(succ->B_to_C->pred, cancel_work(
    2272             :                                                                                                  check_complexity::
    2273             :                                                                                                  while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing), );
    2274         825 :                                                                                                 mCRL2complexity(succ->B_to_C->pred, cancel_work(
    2275             :                                                                                                                   check_complexity::
    2276             :                                                                                                                   if___s_prime_has_transition_to_SpC_3_23l), );
    2277             :                                                                                             }
    2278        1177 :                                                                                             for (pred_iter_t pred=s->pred_begin(); s->pred_end()!=pred; ++pred)
    2279             :                                                                                             {
    2280         643 :                                                                                                 mCRL2complexity(pred, finalise_work(check_complexity::
    2281             :                                                                                                              for_all_s_prime_in_pred_s_3_18r,
    2282             :                                                                                                              check_complexity::refine_incoming_transition_3_18,
    2283             :                                                                                                              max_NewB), );
    2284             :                                                                                             }
    2285             :                                                                                         }
    2286         308 :                                                                                         check_complexity::check_temporary_work();
    2287         308 :                                                                                     }
    2288             : 
    2289             :                                                                                     } // end namespace bisim_gjkw
    2290             :                                                                                 #endif
    2291             : /// \brief refine a block into the part that can reach `SpC` and the part that
    2292             : /// cannot
    2293             : ///
    2294             : /// \details At the beginning of a call to `refine()`, the block RfnB is sliced
    2295             : /// into these parts:
    2296             : ///
    2297             : ///     |          unmarked         |marked |         unmarked         |marked|
    2298             : ///     |         non-bottom        |non-bot|          bottom          |bottom|
    2299             : ///
    2300             : /// The procedure will partition the block into two parts, called ``blue'' and
    2301             : /// ``red''.  The red part can reach the splitter constellation `SpC`, the blue
    2302             : /// part cannot.  Upon calling `refine()`, it is known that all marked states
    2303             : /// are red.
    2304             : ///
    2305             : /// If states with a strong transition to `SpC` have not yet been found, the
    2306             : /// parameter `FromRed` indicates all such transitions, so `refine()` can
    2307             : /// easily find their sources.  It is required that either some states are
    2308             : /// marked or a non-nullptr `FromRed` is supplied.  In the latter case, also
    2309             : /// the _current constellation_ pointer of all unmarked bottom states is set in
    2310             : /// a way that it makes easy to check whether the state has a transition to
    2311             : /// `SpC`.  (Some non-bottom states may have their _current constellation_
    2312             : /// pointer set similarly; while this is not required, it still speeds up
    2313             : /// `refine()`.)
    2314             : ///
    2315             : /// `refine()` works by starting two coroutines to find states in the parts;
    2316             : /// as soon as the first coroutine finishes, the refinement can be completed.
    2317             : ///
    2318             : /// Refine slices these states further as follows:
    2319             : ///
    2320             : ///                                          refine_blue()    refine_red()
    2321             : ///              shared variable            local variable   local variable
    2322             : ///          notblue_initialised_end          visited_end     visited_begin
    2323             : ///                     v                          v                v
    2324             : ///     | blue  |notblue|notblue|    red    | blue |unknown|not blue|   red   |
    2325             : ///     |non-bot|  > 0  |undef'd| non-bottom|bottom|bottom | bottom | bottom  |
    2326             : ///             ^               ^                          ^
    2327             : ///       refine_blue()    block.unmarked_          block.unmarked_
    2328             : ///      local variable    nonbottom_end()           bottom_end()
    2329             : ///     blue_nonbottom_end
    2330             : ///
    2331             : /// - *blue non-bottom:* states of which it is known that they are blue
    2332             : /// - *notblue > 0:* states that have an inert transition to some blue state,
    2333             : ///   but for some transition it is not yet known whether they go to a red or a
    2334             : ///   blue state
    2335             : /// - *notblue undefined:* for no inert transition it is known whether it goes
    2336             : ///   to a red or a blue state
    2337             : /// - *red non-bottom:* states of which it is known that they are red
    2338             : /// - *blue bottom:* states of which it is known that they are blue
    2339             : /// - *unknown bottom:* states that have not yet been checked
    2340             : /// - *not blue bottom:* states of which the blue coroutine has found that they
    2341             : ///   are red, but the red coroutine has not yet handled them
    2342             : /// - *red bottom:* states of which everybody knows that they are red
    2343             : ///
    2344             : /// Note that the slices of red non-bottom and the red bottom states may become
    2345             : /// larger than the marked (non-)bottom states have been at the start of
    2346             : /// `refine()`.  Upon termination of one of the two coroutines, states whose
    2347             : /// colour has not yet been determined become known to be of the colour of the
    2348             : /// unfinished coroutine.
    2349             : ///
    2350             : /// \param RfnB             the block that has to be refined
    2351             : /// \param SpC              the splitter constellation
    2352             : /// \param FromRed          the set of transitions from `RfnB` to `SpC`
    2353             : /// \param size_SpB         (only used for measuring the time complexity, and
    2354             : ///                         only if called from line 2.26) the size of the
    2355             : ///                         original splitter block SpB, to which the work on
    2356             : ///                         red bottom states is ascribed.
    2357             : /// \param postprocessing   true iff `refine()` is called during postprocessing
    2358             : ///                         new bottom states
    2359             : /// \result a pointer to the block that contains the red part of `RfnB`.
    2360             : 
    2361             : template <class LTS_TYPE>
    2362         660 : bisim_gjkw::block_t* bisim_partitioner_gjkw<LTS_TYPE>::refine(
    2363             :        bisim_gjkw::block_t* const RfnB, const bisim_gjkw::constln_t* const SpC,
    2364             :        const bisim_gjkw::B_to_C_descriptor* const FromRed,
    2365             :        bool const postprocessing                                                ONLY_IF_DEBUG( , const bisim_gjkw::constln_t* NewC )
    2366             :        )
    2367             : {
    2368             :                                                                                 #ifndef NDEBUG
    2369         660 :                                                                                     if (nullptr != FromRed)
    2370             :                                                                                     {
    2371         141 :                                                                                         assert(FromRed->from_block() == RfnB);
    2372         141 :                                                                                         assert(FromRed->to_constln() == SpC);
    2373         141 :                                                                                         assert(nullptr != SpC);
    2374         141 :                                                                                         assert(0 == RfnB->marked_size());
    2375             :                                                                                     }
    2376             :                                                                                     else
    2377             :                                                                                     {
    2378         519 :                                                                                         assert(0 != RfnB->marked_size());
    2379             :                                                                                     }
    2380         660 :                                                                                     assert(1 < RfnB->size());
    2381             :                                                                                 #endif
    2382             :     // 3.2: if RfnB subseteq SpC then return RfnB
    2383         660 :     if (RfnB->constln() == SpC)
    2384             :     {
    2385             :         // Mark all bottom states to indicate there are no new bottom states.
    2386          83 :         RfnB->set_marked_nonbottom_begin(RfnB->nonbottom_end());
    2387          83 :         RfnB->set_marked_bottom_begin(RfnB->bottom_begin());
    2388          83 :         return RfnB;
    2389             :     }
    2390             :     // 3.3: Test := {bottom states}\Red, ...
    2391             :     // 3.4: Spend the same amount of work on either coroutine:
    2392             :     // and
    2393             :     // 3.39: RedB := RfnB  or  RedB := NewB , respectively
    2394             :                                                                                 #ifndef NDEBUG
    2395         577 :                                                                                     bisim_gjkw::permutation_iter_t const red_end = RfnB->end();
    2396             :                                                                                 #endif
    2397             :     bisim_gjkw::block_t* RedB;
    2398             : 
    2399             :     COROUTINES_SECTION
    2400             :         // common variables
    2401         577 :             bisim_gjkw::permutation_iter_t notblue_initialised_end =
    2402             :                                                        RfnB->nonbottom_begin();
    2403         577 :             bool FromRed_is_empty = nullptr == FromRed;
    2404             : 
    2405             :         // variables for the blue coroutine
    2406         577 :             bisim_gjkw::permutation_iter_t blue_visited_end;
    2407             :             bisim_gjkw::state_info_ptr blue_s;
    2408         577 :             bisim_gjkw::pred_iter_t blue_pred_iter;
    2409             :             bisim_gjkw::state_info_ptr blue_s_prime;
    2410         577 :             bisim_gjkw::permutation_iter_t blue_blue_nonbottom_end;
    2411         577 :             bisim_gjkw::succ_const_iter_t blue_begin;
    2412         577 :             bisim_gjkw::succ_const_iter_t blue_end;
    2413             : 
    2414             :         // variables for the red coroutine
    2415         577 :             bisim_gjkw::B_to_C_iter_t red_fromred_visited_begin;
    2416         577 :             bisim_gjkw::permutation_iter_t red_visited_begin;
    2417             :             bisim_gjkw::state_info_ptr red_s;
    2418         577 :             bisim_gjkw::pred_iter_t red_pred_iter;
    2419             : 
    2420         577 :         COROUTINE_LABELS(   (REFINE_BLUE_PREDECESSOR_HANDLED)
    2421             :                             (REFINE_BLUE_TESTING)
    2422             :                             (REFINE_BLUE_STATE_HANDLED)
    2423             :                             (REFINE_BLUE_COLLECT_BOTTOM)
    2424             :                             (REFINE_RED_COLLECT_FROMRED)
    2425             :                             (REFINE_RED_PREDECESSOR_HANDLED)
    2426             :                             (REFINE_RED_STATE_HANDLED))
    2427             : 
    2428             : /*--------------------------- handle blue states ----------------------------*/
    2429             : 
    2430             : /// The blue coroutine finds blue states in a block, i. e. states that cannot
    2431             : /// reach the splitter.  It is one of the two coroutines that together
    2432             : /// implement the fast refinement of block `RfnB` into states that can reach
    2433             : /// the splitter `SpC` (red states) and those that cannot (blue states).
    2434             : ///
    2435             : /// This coroutine assumes that `RfnB` is nontrivial, i. e. contains at least
    2436             : /// two states.  `refine()` may be called in two ways:  either the initially
    2437             : /// red states are marked, or a set of transitions from `RfnB` to `SpC` is
    2438             : /// given.  In the first case, all unmarked bottom states are blue.  In the
    2439             : /// second case, however, the first thing this coroutine has to do is to decide
    2440             : /// which bottom states are blue and which ones are not.  In that case, it
    2441             : /// assumes that the `current_constln` pointer of bottom states is pointing to
    2442             : /// a place where a transition to `SpC` could be inserted.  If there is already
    2443             : /// such a transition just before or after that memory location, the bottom
    2444             : /// state is actually red; otherwise, it is blue.
    2445             : ///
    2446             : /// After having found the blue bottom states, the coroutine proceeds to find
    2447             : /// blue non-bottom states by walking through the predecessors of the blue
    2448             : /// states.  As soon as can be determined that all inert outgoing transitions
    2449             : /// of a state lead to (other) blue states, this state is also blue -- with one
    2450             : /// exception:  if this state has a (non-inert) transition to the splitter.  If
    2451             : /// `refine()` was called in the second way, one has to check the outgoing
    2452             : /// non-inert transitions to find out whether such a transition exists.
    2453             : ///
    2454             : /// As soon as it becomes clear that the blue subblock will be larger, this
    2455             : /// coroutine is aborted.  Otherwise, at the end `RfnB` is actually split into
    2456             : /// its two parts, and the coroutine closes with updating the inert-ness of
    2457             : /// transitions and finding new bottom states.  New bottom states will be
    2458             : /// unmarked bottom states.  (It may also happen that the blue subblock is
    2459             : /// empty;  in that case, `RfnB` is not split.)
    2460             : ///
    2461             : /// The coroutine implements the left-hand side of Algorithm 3 in [GJKW 2017].
    2462             : 
    2463         577 :         COROUTINE                                                               assert(RfnB->nonbottom_begin() == notblue_initialised_end);
    2464             :             // we have to decide which unmarked bottom states are blue.  So we
    2465             :             // walk over all of them and check whether they have a transition
    2466             :             // to SpC or not.
    2467             :             // 3.3: ..., Blue := {}
    2468         577 :             blue_visited_end = RfnB->unmarked_bottom_begin();
    2469             :             // 3.5l: whenever |Blue| > |RfnB|/2 do  Abort this coroutine
    2470             :                 // nothing needs to be done now, as |Blue| = 0 here.
    2471             : 
    2472             :     /*  -  -  -  -  -  -  - collect blue bottom states -  -  -  -  -  -  -  */
    2473             : 
    2474             :             // 3.6l: while Test is not empty and FromRed is not empty do
    2475             :                 // We use the variable blue_visited_end in this loop to
    2476             :                 // indicate the boundary between blue states (namely those
    2477             :                 // in the interval [RfnB->unmarked_bottom_begin(),
    2478             :                 // blue_visited_end) ) and Test states (namely those in
    2479             :                 // [blue_visited_end, RfnB->unmarked_bottom_end()) ).
    2480        1209 :             COROUTINE_WHILE (REFINE_BLUE_COLLECT_BOTTOM,
    2481             :                                 RfnB->unmarked_bottom_end() > blue_visited_end)
    2482             :             {
    2483         417 :                 if (FromRed_is_empty)
    2484             :                 {
    2485             :                     // 3.14l: Blue := Blue union Test
    2486             :                         // done implicitly: we now regard all unmarked
    2487             :                         // bottom states as blue, i. e. the whole
    2488             :                         // interval [RfnB->unmarked_bottom_begin(),
    2489             :                         // RfnB->unmarked_bottom_end()).
    2490             :                     // 3.5l: whenever |Blue|>|RfnB|/2 do  Abort this coroutine
    2491             :                         // In this case, Test may not yet be empty, so here we
    2492             :                         // have to check the condition of Line 3.5l.
    2493         353 :                     if (RfnB->unmarked_bottom_size() > RfnB->size() / 2)
    2494             :                     {
    2495         181 :                         ABORT_THIS_COROUTINE();
    2496             :                     }
    2497         172 :                     break;
    2498             :                 }
    2499             :                 // 3.7l: Choose s in Test
    2500          64 :                 blue_s = *blue_visited_end;
    2501             :                 // 3.8l: if s --> SpC then
    2502          64 :                 if (blue_s->surely_has_transition_to(SpC))
    2503             :                 {
    2504             :                     // 3.9l: Move s from Test to Red
    2505             :                     // The state s is not blue.  Move it to the slice of
    2506             :                     // non-blue bottom states.
    2507          51 :                     RfnB->set_marked_bottom_begin(
    2508         102 :                                               RfnB->marked_bottom_begin() - 1);
    2509          51 :                     bisim_gjkw::swap_permutation(blue_visited_end,
    2510             :                                                   RfnB->marked_bottom_begin());
    2511             :                     // 3.5r: whenever |Red|>|RfnB|/2 do Abort the red coroutine
    2512          51 :                     if (RfnB->marked_size() > RfnB->size() / 2)
    2513             :                     {
    2514           3 :                         ABORT_OTHER_COROUTINE();
    2515             :                     }
    2516             :                                                                                 #ifndef NDEBUG
    2517             :                                                                                     // The state is red.  Depending on the context of refinement, the work done
    2518             :                                                                                     // on this state is attributed to one or another element of the Kripke
    2519             :                                                                                     // structure.
    2520          51 :                                                                                     if (postprocessing)
    2521             :                                                                                     {
    2522             :                                                                                         // refine() has been called from line 4.14.  During postprocessing, the
    2523             :                                                                                         // work is ascribed to the transitions from s to SpC.
    2524             :                                                                                         // Using the current_constln pointer of s, find a transition to SpC.
    2525             :                                                                                         // The work has to be ascribed to the transitions from s to SpC.
    2526          31 :                                                                                         bisim_gjkw::succ_iter_t to_SpC = blue_s->current_constln();
    2527          31 :                                                                                         if (to_SpC == blue_s->succ_end() || to_SpC->target->constln() != SpC)
    2528             :                                                                                         {
    2529           0 :                                                                                             assert(blue_s->succ_begin() < to_SpC);
    2530           0 :                                                                                             --to_SpC;
    2531           0 :                                                                                             assert(to_SpC->target->constln() == SpC);
    2532             :                                                                                         }
    2533          31 :                                                                                         bisim_gjkw::succ_entry::slice_add_work_to_transns(to_SpC,
    2534             :                                                                                                  bisim_gjkw::check_complexity::
    2535             :                                                                                                  while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing, 1);
    2536             :                                                                                     }
    2537             :                                                                                     else
    2538             :                                                                                     {
    2539             :                                                                                         // refine() has been called from line 2.26, and RfnB is a block with a
    2540             :                                                                                         // transition to SpB.  The state has been marked because of these
    2541             :                                                                                         // transitions (which are not transitions to SpC!).
    2542             :                                                                                         // code similar to the case if (postprocessing).
    2543          20 :                                                                                         bisim_gjkw::succ_iter_t to_NewC = blue_s->current_constln();
    2544          20 :                                                                                         if (to_NewC == blue_s->succ_end() || to_NewC->target->constln() == SpC)
    2545             :                                                                                         {
    2546          20 :                                                                                             assert(blue_s->succ_begin() < to_NewC);
    2547          20 :                                                                                             --to_NewC;
    2548          20 :                                                                                             assert(to_NewC->target->constln() != SpC);
    2549             :                                                                                         }
    2550          20 :                                                                                         bisim_gjkw::succ_entry::slice_add_work_to_transns(to_NewC, bisim_gjkw::
    2551             :                                                                                               check_complexity::while_Test_is_not_empty_3_6l_s_is_red_3_9l, 1);
    2552             :                                                                                     }
    2553             :                                                                                 #endif
    2554             :                 // 3.10l: else
    2555             :                 }
    2556             :                 else
    2557          13 :                 {                                                               assert(blue_s->surely_has_no_transition_to(SpC));
    2558             :                     // 3.11l: Move s from Test to Blue
    2559          13 :                     ++blue_visited_end;
    2560             :                     // 3.5l: whenever |Blue|>|RfnB|/2 do  Abort this coroutine
    2561          26 :                     if ((state_type) (blue_visited_end -
    2562          26 :                              RfnB->unmarked_bottom_begin()) > RfnB->size() / 2)
    2563             :                     {
    2564           1 :                         ABORT_THIS_COROUTINE();
    2565          12 :                     }                                                           mCRL2complexity(blue_s, add_work(bisim_gjkw::check_complexity::
    2566             :                                                                                                            while_Test_is_not_empty_3_6l_s_is_blue_3_11l, 1), );
    2567             :                 // 3.12l: end if
    2568             :                 }
    2569             :             // 3.13l: end while
    2570             :             }
    2571         395 :             END_COROUTINE_WHILE;                                                assert(RfnB->constln() != SpC);
    2572             : 
    2573         395 :             if (0 == RfnB->unmarked_bottom_size())
    2574             :             {
    2575             :                 // all bottom states are red, so there cannot be any blue
    2576             :                 // states.
    2577         212 :                 RfnB->set_marked_nonbottom_begin(RfnB->marked_nonbottom_end());
    2578             :                 // RfnB->set_marked_bottom_begin(RfnB->bottom_begin());
    2579         212 :                 RedB = RfnB;                                                    ONLY_IF_DEBUG( blue_is_smaller(nullptr, RedB, NewC); )
    2580         481 :                 TERMINATE_COROUTINE_SUCCESSFULLY();
    2581             :             }
    2582             : 
    2583             :     /*  -  -  -  -  -  -  -  - visit blue states -  -  -  -  -  -  -  -  */
    2584             : 
    2585             :             // 3.15l: while Blue contains unvisited states do
    2586         183 :             blue_visited_end = RfnB->unmarked_bottom_begin();
    2587         183 :             blue_blue_nonbottom_end = RfnB->unmarked_nonbottom_begin();
    2588         183 :             COROUTINE_DO_WHILE (REFINE_BLUE_STATE_HANDLED,
    2589             :                                    blue_visited_end != blue_blue_nonbottom_end)
    2590             :             {
    2591             :                 // 3.16l: Choose an unvisited s in Blue
    2592         351 :                 blue_s = *blue_visited_end;                                     assert(blue_visited_end < blue_blue_nonbottom_end ||
    2593             :                                                                                                        (RfnB->unmarked_bottom_begin() <= blue_visited_end &&
    2594             :                                                                                                               RfnB->unmarked_bottom_end() > blue_visited_end));
    2595         351 :                                                                                 assert(RfnB->unmarked_nonbottom_begin() <= blue_blue_nonbottom_end);
    2596         351 :                                                                                 assert(blue_blue_nonbottom_end <= notblue_initialised_end);
    2597         351 :                 /* 3.17l: Mark s as visited                                  */ assert(RfnB->unmarked_nonbottom_end() >= notblue_initialised_end);
    2598         351 :                 ++blue_visited_end;
    2599             :                 // 3.18l: for all s_prime in inert_in(s) \ Red do
    2600         552 :                 COROUTINE_FOR (REFINE_BLUE_PREDECESSOR_HANDLED,
    2601             :                     blue_pred_iter = blue_s->inert_pred_begin(),
    2602             :                     blue_s->inert_pred_end()!=blue_pred_iter, ++blue_pred_iter)
    2603             :                 {
    2604         226 :                     blue_s_prime = blue_pred_iter->source;
    2605         287 :                     if (blue_s_prime->pos >= RfnB->marked_nonbottom_begin())
    2606          61 :                     {                                                           mCRL2complexity(blue_pred_iter, add_work(bisim_gjkw::check_complexity::
    2607             :                                                                                                            for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
    2608          61 :                         continue;
    2609             :                     }
    2610             :                     // 3.19l: if notblue(s_prime) undefined then
    2611         165 :                     if (blue_s_prime->pos >= notblue_initialised_end)
    2612             :                     {
    2613             :                         // 3.20l: notblue(s_prime) := |inert_out(s_prime)|
    2614         158 :                         blue_s_prime->notblue = blue_s_prime->inert_succ_end()-
    2615         316 :                                               blue_s_prime->inert_succ_begin();
    2616         158 :                         bisim_gjkw::swap_permutation(blue_s_prime->pos,
    2617             :                                                       notblue_initialised_end);
    2618         158 :                         ++notblue_initialised_end;
    2619             :                     // 3.21l: end if
    2620             :                     }
    2621             :                     // 3.22l: notblue(s_prime) := notblue(s_prime) - 1
    2622         165 :                     --blue_s_prime->notblue;
    2623             :                     // 3.23l: if notblue(s_prime) == 0 && ...
    2624         188 :                     if (0 != blue_s_prime->notblue)
    2625          23 :                     {                                                           mCRL2complexity(blue_pred_iter, add_work(bisim_gjkw::check_complexity::
    2626             :                                                                                                            for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
    2627          23 :                         continue;
    2628             :                     }
    2629             :                     // 3.23l: ... && (FromRed == {} ||
    2630             :                     //          out_noninert(s_prime) intersect SpC == {}) then
    2631         142 :                     if (!FromRed_is_empty)
    2632             :                     {
    2633           3 :                         if (blue_s_prime->surely_has_transition_to(SpC))
    2634           0 :                         {                                                       mCRL2complexity(blue_pred_iter, add_work(bisim_gjkw::check_complexity::
    2635             :                                                                                                            for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
    2636           0 :                             continue;
    2637             :                         }
    2638           3 :                         if (!blue_s_prime->surely_has_no_transition_to(SpC))
    2639             :                         {
    2640             :                             // It is not yet known whether s_prime has a
    2641             :                             // transition to SpC or not.  Execute the slow test
    2642             :                             // now.
    2643           2 :                             COROUTINE_FOR (REFINE_BLUE_TESTING,
    2644             :                                 (blue_begin = blue_s_prime->succ_begin(),
    2645             :                                  blue_end   = blue_s_prime->succ_end()   ),
    2646             :                                                blue_begin < blue_end, (void) 0)
    2647             :                             {
    2648             :                                 // binary search for transitions from s_prime
    2649             :                                 // to constellation SpC.
    2650           1 :                                 bisim_gjkw::succ_const_iter_t const mid =
    2651           1 :                                       blue_begin + (blue_end - blue_begin) / 2;
    2652           1 :                                 if (*SpC <= *mid->target->constln())
    2653             :                                 {
    2654           1 :                                     blue_end = mid->slice_begin();
    2655             :                                 }
    2656           1 :                                 if (*mid->target->constln() <= *SpC)
    2657             :                                 {
    2658           1 :                                     blue_begin =
    2659             :                                         bisim_gjkw::succ_entry::slice_end(mid);
    2660             :                                 }
    2661             :                                                                                 #ifndef NDEBUG
    2662           1 :                                                                                     bisim_gjkw::succ_entry::slice_add_work_to_transns(mid, bisim_gjkw::
    2663             :                                                                                                 check_complexity::if___s_prime_has_transition_to_SpC_3_23l, 1);
    2664             :                                                                                 #endif
    2665             :                             }
    2666             :                             END_COROUTINE_FOR;
    2667           2 :                             if (blue_begin != blue_end)
    2668           1 :                             {                                                   mCRL2complexity(blue_pred_iter, add_work(bisim_gjkw::check_complexity::
    2669             :                                                                                                            for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
    2670           1 :                                 continue;
    2671             :                             }
    2672             :                         }
    2673             :                     }
    2674             :                     // 3.24l: Blue := Blue union {s_prime}
    2675         141 :                     bisim_gjkw::swap_permutation(blue_s_prime->pos,
    2676             :                                                       blue_blue_nonbottom_end);
    2677         141 :                     ++blue_blue_nonbottom_end;
    2678             :                     // 3.5l: whenever |Blue|>|RfnB| / 2 do Abort this coroutine
    2679         282 :                     if (blue_blue_nonbottom_end -
    2680         423 :                                RfnB->unmarked_nonbottom_begin() +
    2681         282 :                                RfnB->unmarked_bottom_size() > RfnB->size() / 2)
    2682             :                     {
    2683          25 :                         ABORT_THIS_COROUTINE();
    2684             :                     }
    2685             :                     // 3.25l: end if
    2686             :                         // this is implicit in the `continue` statements above.
    2687         116 :                 /* 3.26l: end for                                            */ mCRL2complexity(blue_pred_iter, add_work(bisim_gjkw::check_complexity::
    2688             :                                                                                                            for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
    2689             :                 }
    2690             :                 END_COROUTINE_FOR;
    2691         307 :             /* 3.27l: end while                                              */ mCRL2complexity(blue_s, add_work(bisim_gjkw::check_complexity::
    2692             :                                                                                                              while_Blue_contains_unvisited_states_3_15l, 1), );
    2693         307 :                 if (RfnB->unmarked_bottom_end() == blue_visited_end)
    2694             :                 {
    2695         133 :                     blue_visited_end = RfnB->unmarked_nonbottom_begin();
    2696             :                 }
    2697         307 :             }
    2698             :             END_COROUTINE_DO_WHILE;
    2699             : 
    2700             :     /*  -  -  -  -  -  -  -  - split off blue block -  -  -  -  -  -  -  -  */
    2701             : 
    2702             :             // 3.28l: Abort the other coroutine
    2703          57 :             ABORT_OTHER_COROUTINE();
    2704             :             // All non-blue states are red.
    2705             :             // 3.29l: Move Blue to a new block NewB
    2706             :             // and
    2707             :             // 3.30l: Destroy all temporary data
    2708          57 :             bisim_gjkw::block_t* const NewB =
    2709          57 :                                  RfnB->split_off_blue(blue_blue_nonbottom_end);
    2710          57 :             part_tr.new_blue_block_created(RfnB, NewB);
    2711             :                                                                                 #ifndef NDEBUG
    2712         114 :                                                                                     unsigned const max_counter = bisim_gjkw::check_complexity::log_n -
    2713          57 :                                                                                                              bisim_gjkw::check_complexity::ilog2(NewB->size());
    2714          57 :                                                                                     mCRL2complexity(NewB, add_work(bisim_gjkw::check_complexity::
    2715             :                                                                                                                        for_all_s_in_NewB_3_31, max_counter), );
    2716             :                                                                                 #endif
    2717             :             // 3.31l: for all s in NewB do
    2718         211 :             for (bisim_gjkw::permutation_iter_t s_iter = NewB->begin();
    2719         211 :                                                NewB->end() != s_iter; ++s_iter)
    2720             :             {
    2721         154 :                 blue_s = *s_iter;                                               // mCRL2complexity(s, ...) -- optimized to the above call.
    2722             :                 // 3.32l: for all s_prime in inert_in(s) \ NewB do
    2723         241 :                 for (blue_pred_iter = blue_s->inert_pred_begin();
    2724         241 :                     blue_s->inert_pred_end()!=blue_pred_iter; ++blue_pred_iter)
    2725          87 :                 {                                                               mCRL2complexity(blue_pred_iter, add_work(bisim_gjkw::check_complexity::
    2726             :                                                                                                               for_all_s_prime_in_pred_s_3_32l, max_counter), );
    2727          87 :                                                                                 assert(part_tr.pred_end() > blue_pred_iter);
    2728          87 :                                                                                 assert(blue_pred_iter->succ->B_to_C->pred == blue_pred_iter);
    2729          87 :                     blue_s_prime = blue_pred_iter->source;
    2730          87 :                     if (blue_s_prime->block == NewB)  continue;                 assert(blue_s_prime->block == RfnB);
    2731             :                     // 3.33l: s_prime --> s is no longer inert
    2732          27 :                     part_tr.make_noninert(blue_pred_iter->succ);
    2733             :                     // 3.34l: if |inert_out(s_prime)| == 0 then
    2734          54 :                     if (blue_s_prime->inert_succ_begin() ==
    2735          54 :                                                 blue_s_prime->inert_succ_end())
    2736             :                     {
    2737             :                         // 3.35l: s_prime is a new bottom state
    2738          21 :                         RfnB->set_marked_nonbottom_begin(
    2739          42 :                                                      RfnB->bottom_begin() - 1);
    2740          21 :                         RfnB->set_bottom_begin(RfnB->marked_nonbottom_begin());
    2741          21 :                         swap_permutation(blue_s_prime->pos,
    2742             :                                                          RfnB->bottom_begin()); // assert("blue_s_prime has a transition to SpC");
    2743             :                     // 3.36l: end if
    2744             :                     }
    2745             :                 // 3.37l: end for
    2746             :                 }
    2747             :             // 3.38l: end for
    2748             :             }
    2749             : 
    2750          57 :             RedB = RfnB;                                                        ONLY_IF_DEBUG( blue_is_smaller(NewB, RedB, NewC); )
    2751          57 :         END_COROUTINE
    2752             : 
    2753             : /*---------------------------- handle red states ----------------------------*/
    2754             : 
    2755             : /// The red coroutine find red states in a block, i. e. states that can reach
    2756             : /// the splitter.  It is one of the two coroutines that together implement
    2757             : /// the fast refinement of block `RfnB` into states that can reach the splitter
    2758             : /// (red states) and those that cannot (blue states).
    2759             : ///
    2760             : /// This coroutine assumes that `RfnB` is nontrivial, i. e. contains at least
    2761             : /// two states, and that there is at least one red state in `RfnB`.  The red
    2762             : /// states can be indicated in one of two ways: either some states of `RfnB`
    2763             : /// are marked, or the parameter `FromRed` indicates the set of transitions
    2764             : /// from `RfnB` to the splitter.  Exactly one of the two must be chosen:  If
    2765             : /// and only if some states are marked, `FromRed` should be `nullptr`.
    2766             : ///
    2767             : /// If `FromRed` is not `nullptr`, the coroutine first finds initially red
    2768             : /// states, i. e. states with a transition to the splitter, and marks them.
    2769             : /// Note that it may happen that some non-bottom states (or even only
    2770             : /// non-bottom states) may be initially red as well.  When all initially red
    2771             : /// states are marked, it proceeds to find other red states by walking through
    2772             : /// the inert predecessors of red states.  Every such predecessor is also a red
    2773             : /// state.
    2774             : ///
    2775             : /// As soon as it becomes clear that the red subblock will be larger, this
    2776             : /// coroutine is aborted.  Otherwise, at the end `RfnB` is actually split into
    2777             : /// its two parts, and the coroutine closes with updating the inert-ness of
    2778             : /// transitions and finding new bottom states.  New bottom states will be
    2779             : /// unmarked bottom states.
    2780             : ///
    2781             : /// The coroutine implements the right-hand side of Algorithm 3 in [GJKW 2017].
    2782             : 
    2783         411 :         COROUTINE
    2784             :             // 3.5r: whenever |Red| > |RfnB|/2 then  Abort this coroutine
    2785         411 :             if (RfnB->marked_size() > RfnB->size()/2)  ABORT_THIS_COROUTINE();
    2786             :             // The red block contains at most RfnB->size() -
    2787             :             // RfnB->unmarked_bottom_size() + FromRed->size() states.  If that
    2788             :             // is <= RfnB->size() / 2, we could abort the other coroutine
    2789             :             // immediately.  We don't do it here because we want to investigate
    2790             :             // the effect of this and similar heuristics more systematically.
    2791             : 
    2792             :     /*  -  -  -  -  -  -  - collect states from FromRed -  -  -  -  -  -  -  */
    2793             : 
    2794             :             // 3.6r: while FromRed != {} do
    2795         394 :             if (nullptr != FromRed)
    2796          58 :             {                                                                   assert(FromRed->from_block() == RfnB);
    2797          58 :                 red_fromred_visited_begin = FromRed->end;                       assert(RfnB->inert_end() <= FromRed->begin ||
    2798             :                                                                                                         (RfnB->inert_begin() >= red_fromred_visited_begin &&
    2799             :                                                                                                                RfnB->inert_end() > red_fromred_visited_begin));
    2800         123 :                 COROUTINE_WHILE (REFINE_RED_COLLECT_FROMRED,
    2801             :                                    FromRed->begin != red_fromred_visited_begin)
    2802             :                 {
    2803             :                     // 3.10r (order of lines changed): FromRed := FromRed \ {s --> t}
    2804             :                         // We can change the order of lines because the
    2805             :                         // coroutine is not interrupted in between.
    2806          87 :                     --red_fromred_visited_begin;
    2807             :                     // 3.7r: Choose s --> t in FromRed
    2808          87 :                     bisim_gjkw::state_info_ptr const red_s =
    2809         174 :                                        red_fromred_visited_begin->pred->source; assert(RfnB->begin() <= red_s->pos);
    2810          87 :                     /* 3.8r: Test := Test \ {s}                              */ assert(red_s->pos < RfnB->end());
    2811             :                     // and
    2812             :                     // 3.9r: Red := Red union {s}
    2813          87 :                     if (red_s->pos < notblue_initialised_end)
    2814             :                     {
    2815             :                         // The non-bottom state has a transition to a blue
    2816             :                         // state, so notblue is initialised; however, now it is
    2817             :                         // revealed to be red anyway.
    2818           1 :                         bisim_gjkw::swap_permutation(red_s->pos,
    2819           1 :                                                     --notblue_initialised_end);
    2820             :                     }
    2821         132 :                     if (RfnB->mark(red_s) &&
    2822             :                     // 3.5r: whenever |Red| > |RfnB|/2 do  Abort this coroutine
    2823          45 :                                         RfnB->marked_size() > RfnB->size() / 2)
    2824             :                     {
    2825          22 :                         ABORT_THIS_COROUTINE();
    2826             :                     }
    2827          65 :                 /* 3.13r: end while                                          */ mCRL2complexity(red_fromred_visited_begin->pred, add_work(bisim_gjkw::
    2828             :                                                                                                       check_complexity::while_FromRed_is_not_empty_3_6r, 1), );
    2829             :                 }
    2830             :                 END_COROUTINE_WHILE;
    2831             : 
    2832             :                 // The shared variable FromRed_is_empty is set to true as soon
    2833             :                 // as FromRed should be considered empty.  (From that moment
    2834             :                 // on, no slow tests are needed any more.)
    2835          24 :                 FromRed_is_empty = true;
    2836         360 :             }                                                                   assert(FromRed_is_empty);  assert(0 != RfnB->marked_size());
    2837             : 
    2838             :     /*  -  -  -  -  -  -  -  - visit red states -  -  -  -  -  -  -  -  */
    2839             : 
    2840         360 :             red_visited_begin = RfnB->marked_bottom_end();
    2841         360 :             if (RfnB->marked_bottom_begin() == red_visited_begin)
    2842             :             {
    2843             :                 // It may happen that all found states are non-bottom states.
    2844             :                 // (In that case, some of these states will become new bottom
    2845             :                 // states.)
    2846          50 :                 red_visited_begin = RfnB->marked_nonbottom_end();
    2847             :             }
    2848             :             // 3.15r: while Red contains unvisited states do
    2849         360 :             COROUTINE_DO_WHILE(REFINE_RED_STATE_HANDLED,
    2850             :                            RfnB->marked_nonbottom_begin() != red_visited_begin)
    2851             :             {
    2852             :                 // 3.17r (order of lines changed): Mark s as visited
    2853         655 :                 --red_visited_begin;                                            assert(RfnB->marked_bottom_begin() <= red_visited_begin ||
    2854             :                                                                                                      (RfnB->marked_nonbottom_begin() <= red_visited_begin &&
    2855             :                                                                                                             RfnB->marked_nonbottom_end() > red_visited_begin));
    2856             :                 // 3.16r: Choose an unvisited s in Red
    2857         655 :                 red_s = *red_visited_begin;
    2858             :                 // 3.18r: for all s_prime in inert_in(s) do
    2859         832 :                 COROUTINE_FOR (REFINE_RED_PREDECESSOR_HANDLED,
    2860             :                      red_pred_iter = red_s->inert_pred_begin(),
    2861             :                      red_s->inert_pred_end() != red_pred_iter, ++red_pred_iter)
    2862             :                 {
    2863         204 :                     bisim_gjkw::state_info_ptr const s_prime =
    2864         204 :                                                          red_pred_iter->source;
    2865             :                     // 3.24r: Red := Red union {s_prime}
    2866         204 :                     if (s_prime->pos < notblue_initialised_end)
    2867             :                     {
    2868             :                         // The state has a transition to a blue state, so
    2869             :                         // notblue is initialised; however, now it is revealed
    2870             :                         // to be red anyway.
    2871           2 :                         bisim_gjkw::swap_permutation(s_prime->pos,
    2872           2 :                                                     --notblue_initialised_end);
    2873             :                     }
    2874         375 :                     if (RfnB->mark_nonbottom(s_prime) &&
    2875             :                     // 3.5r: whenever |Red| > |RfnB|/2 do  Abort this coroutine
    2876         171 :                                         RfnB->marked_size() > RfnB->size() / 2)
    2877             :                     {
    2878          27 :                         ABORT_THIS_COROUTINE();
    2879             :                     }
    2880         177 :                 /* 3.26r: end for                                            */ mCRL2complexity(red_pred_iter, add_work(bisim_gjkw::check_complexity::
    2881             :                                                                                                                         for_all_s_prime_in_pred_s_3_18r, 1), );
    2882             :                 }
    2883             :                 END_COROUTINE_FOR;
    2884         617 :             /* 3.27r: end while                                              */ mCRL2complexity(red_s, add_work(bisim_gjkw::check_complexity::
    2885             :                                                                                                               while_Red_contains_unvisited_states_3_15r, 1), );
    2886         617 :                 if (RfnB->marked_bottom_begin() == red_visited_begin)
    2887             :                 {
    2888         286 :                     red_visited_begin = RfnB->marked_nonbottom_end();
    2889             :                 }
    2890         617 :             }
    2891             :             END_COROUTINE_DO_WHILE;
    2892             : 
    2893             :     /*  -  -  -  -  -  -  -  - split off red block -  -  -  -  -  -  -  -  */
    2894             : 
    2895             :             // 3.28r: Abort the other coroutine
    2896         308 :             ABORT_OTHER_COROUTINE();
    2897             :             // All non-red states are blue.
    2898             :             // 3.29r: Move Red to a new block RedB
    2899             :             // and
    2900             :             // 3.30r: Destroy all temporary data
    2901         308 :             RedB = RfnB->split_off_red(RfnB->marked_nonbottom_begin());
    2902         308 :             part_tr.new_red_block_created(RfnB, RedB, postprocessing);
    2903             :                                                                                 #ifndef NDEBUG
    2904         616 :                                                                                     unsigned const max_counter = bisim_gjkw::check_complexity::log_n -
    2905         308 :                                                                                                              bisim_gjkw::check_complexity::ilog2(RedB->size());
    2906         308 :                                                                                     mCRL2complexity(RedB, add_work(bisim_gjkw::check_complexity::
    2907             :                                                                                                                        for_all_s_in_NewB_3_31, max_counter), );
    2908             :                                                                                 #endif
    2909             :             // 3.31r: for all non-bottom s in RedB do
    2910             :                 // we have to run through the states backwards because
    2911             :                 // otherwise, we might miss out some states.
    2912         435 :             for (bisim_gjkw::permutation_iter_t s_iter = RedB->nonbottom_end();
    2913         435 :                                            RedB->nonbottom_begin() != s_iter; )
    2914             :             {
    2915         127 :                 --s_iter;
    2916         127 :                 red_s = *s_iter;                                                // mCRL2complexity(s, ...) -- optimized to the above call.
    2917             :                 // 3.32r: for all s_prime in inert_out(s) \ RedB do
    2918         198 :                 for (bisim_gjkw::succ_iter_t
    2919         127 :                                succ_iter = red_s->inert_succ_begin();
    2920         325 :                                red_s->inert_succ_end()!=succ_iter; ++succ_iter)
    2921         198 :                 {                                                               mCRL2complexity(succ_iter->B_to_C->pred, add_work(bisim_gjkw::
    2922             :                                                                                             check_complexity::for_all_s_prime_in_succ_s_3_32r, max_counter), );
    2923         198 :                                                                                 assert(part_tr.succ_end() > succ_iter);
    2924         198 :                                                                                 assert(succ_iter->B_to_C->pred->succ == succ_iter);
    2925         396 :                     if (bisim_gjkw::state_info_ptr const s_prime =
    2926         198 :                                                              succ_iter->target;
    2927         198 :                                                         s_prime->block == RedB)
    2928             :                     {
    2929          83 :                         continue;
    2930         115 :                     }                                                           else  assert(s_prime->block == RfnB);
    2931             :                     // 3.33r: s --> s_prime is no longer inert
    2932         115 :                     part_tr.make_noninert(succ_iter);
    2933             :                 // 3.34r: end for
    2934             :                 }
    2935             :                 // 3.35r: if |inert_out(s)| == 0 then
    2936         127 :                 if (red_s->inert_succ_begin() == red_s->inert_succ_end())
    2937             :                 {
    2938             :                     // 3.36r: s is a new bottom state
    2939          54 :                     RedB->set_marked_nonbottom_begin(RedB->bottom_begin() - 1);
    2940          54 :                     RedB->set_bottom_begin(RedB->marked_nonbottom_begin());
    2941          54 :                     swap_permutation(red_s->pos, RedB->bottom_begin());         // assert("red_s has a transition to SpC");
    2942             :                 // 3.37r: end if
    2943             :                 }
    2944             :             // 3.38r: end for
    2945         308 :             }                                                                   assert(RfnB->end() < red_end);
    2946         308 :                                                                                 ONLY_IF_DEBUG( red_is_smaller(RfnB, RedB); )
    2947         308 :         END_COROUTINE
    2948           0 :     END_COROUTINES_SECTION
    2949             : 
    2950             : 
    2951         577 :     /* 3.41 P := partition P where NewB is added and the states in NewB are  */ assert(RedB->end() == red_end);
    2952             :     //                             removed from RfnB
    2953             :         // done through adapting the data structures in the coroutines.
    2954             :     // 3.42: return <RedB, BlueB> (with old and new bottom states separated)
    2955             :         // The separation is indicated by marking the old bottom states.
    2956             :         // Only RedB is returned explicitly, as most calls to Refine only use
    2957             :         // RedB.
    2958         577 :     return RedB;
    2959             : }
    2960             : 
    2961             : 
    2962             : 
    2963             : /*=============================================================================
    2964             : =              PostprocessNewBottom -- Algorithm 4 in [GJKW 2017]             =
    2965             : =============================================================================*/
    2966             : 
    2967             : 
    2968             : 
    2969             : /// \brief function object to compare two constln_t pointers based on their
    2970             : /// contents
    2971             : /// \details This function object is used to create a sorted set of
    2972             : /// constellations, namely those that are reachable from the block of new
    2973             : /// bottom states in Algorithm 4.
    2974             : class constln_ptr_less
    2975             : {
    2976             :   public:
    2977          74 :     bool operator() (const bisim_gjkw::constln_t* a,
    2978             :                                           const bisim_gjkw::constln_t* b) const
    2979             :     {
    2980          74 :         return *a < *b;
    2981             :     }
    2982             : };
    2983             : 
    2984             : 
    2985             : typedef std::set<bisim_gjkw::constln_t*, constln_ptr_less> R_map_t;
    2986             : 
    2987             : 
    2988             : /// \brief Split a block with new bottom states as needed
    2989             : /// \details The function splits RedB by checking whether all new bottom
    2990             : /// states can reach the constellations that RedB can reach.
    2991             : ///
    2992             : /// When this function starts, it assumes that the old bottom states of RedB
    2993             : /// are marked and the new ones are not.  It is an error if RedB does not
    2994             : /// contain any new bottom states.
    2995             : /// The function implements Algorithm 4 of [GJKW 2017].  It first separates the
    2996             : /// old from the new bottom states; then it walks through all constellations
    2997             : /// that can be reached from the new bottom states to separate them into
    2998             : /// smaller, stable subblocks.  The return value is the block containing the
    2999             : /// old bottom states, resulting from the first separation.
    3000             : /// \param RedB  block containing new bottom states that need to be stabilised
    3001             : /// \returns the block containing the old bottom states (and every state in
    3002             : ///          RedB that can reach some old bottom state through inert
    3003             : ///          transitions)
    3004             : template <class LTS_TYPE>
    3005          57 : bisim_gjkw::block_t* bisim_partitioner_gjkw<LTS_TYPE>::postprocess_new_bottom(
    3006             :                                             bisim_gjkw::block_t* RedB
    3007             :                                             /* , bisim_gjkw::block_t* BlueB */)
    3008          57 : {                                                                               assert(0 != RedB->unmarked_bottom_size());
    3009          57 :                                                                                 assert(RedB->marked_nonbottom_begin() == RedB->marked_nonbottom_end());
    3010             :     /*------- collect constellations reachable from new bottom states -------*/
    3011             : 
    3012             :     // 4.3: <ResultB, RfnB> := Refine(RedB, cosplit(RedB, BlueB), {old bottom
    3013             :     //                                                     states in RedB}, {})
    3014             :     bisim_gjkw::block_t* ResultB;
    3015             :     bisim_gjkw::block_t* RfnB;
    3016             :                                                                                 #ifndef NDEBUG
    3017          57 :                                                                                     bisim_gjkw::permutation_const_iter_t blue_begin = RedB->begin();
    3018             :                                                                                 #endif
    3019          57 :     if (0 != RedB->marked_bottom_size())
    3020             :     {
    3021             :         // postprocessing == false is required here because we need to keep
    3022             :         // ResultB->FromRed().
    3023           9 :         ResultB = refine(RedB, nullptr, nullptr, false);                        assert(nullptr != ResultB);  assert(0 == ResultB->unmarked_bottom_size());
    3024             :         // 4.26: Destroy all temporary data
    3025             :             // As part of this line, we unmark all states.
    3026           9 :         ResultB->set_marked_bottom_begin(ResultB->bottom_end());                assert(ResultB->begin() > blue_begin);
    3027           9 :         RfnB = ResultB->begin()[-1]->block;
    3028             :     }
    3029             :     else
    3030             :     {
    3031          48 :         RfnB = RedB;
    3032          48 :         ResultB = nullptr;
    3033          57 :     }                                                                           assert(ResultB != RfnB);  assert(RfnB->begin() == blue_begin);
    3034             :     // do not refine a trivial block
    3035          57 :     if (1 == RfnB->size())
    3036          29 :     {                                                                           assert(0 == RfnB->marked_size());
    3037          29 :         return ResultB;
    3038             :     }
    3039             :     // 4.2: Create an empty search tree R of constellations
    3040          56 :     R_map_t R;
    3041          28 : Line_4_4:
    3042          28 :     /* 4.4: for all constellations C not in R reachable from RfnB do         */ assert(0 == RfnB->marked_bottom_size());
    3043         148 :     while (!RfnB->to_constln.front().needs_postprocessing())
    3044             :     {
    3045          60 :         bisim_gjkw::B_to_C_desc_iter_t const new_slice =
    3046          60 :                                                       RfnB->to_constln.begin(); // try to assign the work to the transitions from bottom states in RfnB to C.
    3047             :                                                                                 #ifndef NDEBUG
    3048          60 :                                                                                     if (!new_slice->add_work_to_bottom_transns(bisim_gjkw::check_complexity::
    3049             :                                                                                                        for_all_transitions_from_bottom_states_a_priori_4_4, 1))
    3050             :                                                                                     {
    3051             :                                                                                         // It didn't work out -- now assign it temporarily to the
    3052             :                                                                                         // B_to_C slice itself.
    3053           3 :                                                                                         mCRL2complexity(new_slice, add_work(bisim_gjkw::check_complexity::
    3054             :                                                                                                         for_all_constellations_C_not_in_R_from_RfnB_4_4, 1), );
    3055             :                                                                                     }
    3056             :                                                                                 #endif
    3057          60 :         bisim_gjkw::constln_t* const C = new_slice->to_constln();
    3058             :         // 4.5: Add C to R
    3059          60 :         if (!R.insert(C).second) //< complexity log(n)
    3060           0 :         {                                                                       assert(0 && "The constellation already was in R");
    3061             :         }
    3062             :         // 4.6: Register that the transitions from RfnB to C need
    3063          60 :         /*      postprocessing                                               */ assert(C->postprocess_begin == C->postprocess_end);
    3064          60 :         C->postprocess_begin = new_slice->begin;
    3065          60 :         C->postprocess_end = new_slice->end;                                    assert(C->postprocess_begin < C->postprocess_end);
    3066             :         // move the set of transitions to the end of the list
    3067          60 :         RfnB->to_constln.splice(RfnB->to_constln.end(), RfnB->to_constln,
    3068             :                                                                     new_slice);
    3069             :     // 4.7: end for
    3070             :     }
    3071             :     // 4.8: for all bottom states s in RfnB do
    3072          28 :     bisim_gjkw::permutation_iter_t s_iter = RfnB->unmarked_bottom_begin();
    3073          15 :     do
    3074             :     {
    3075          43 :         bisim_gjkw::state_info_ptr const s = *s_iter;                           mCRL2complexity(s, add_work(bisim_gjkw::check_complexity::
    3076             :                                                                                                                     for_all_bottom_states_s_in_RfnB_4_8, 1), );
    3077             :         // 4.9: Set the current constellation pointer of s to the first
    3078             :         //      constellation it can reach
    3079          43 :         s->set_current_constln(s->succ_begin());
    3080             :     // 4.10: end for
    3081             :     }
    3082          43 :     while (RfnB->unmarked_bottom_end() != ++s_iter);
    3083             : 
    3084             :     /*--------------- stabilise w. r. t. found constellations ---------------*/
    3085             : 
    3086             :     // 4.11: for all constellations SpC in R (in order) do
    3087         148 :     while (!R.empty())
    3088             :     {                                                                           // the work has to be assigned to the transitions from (new) bottom
    3089          60 :         bisim_gjkw::constln_t* const SpC = *R.begin();                          // states to constellation SpC.  We do that assignment in the inner
    3090             :         // 4.12: for all blocks B with transitions to SpC that need             // loop.  Ensure that the inner loop is executed:
    3091          60 :         /*               postprocessing do                                   */ assert(SpC->postprocess_begin != SpC->postprocess_end);
    3092           6 :         do
    3093             :         {
    3094             :             // add_work is called indirectly: after refining, work is assigned
    3095             :             // to every (new) bottom state in the refined block.
    3096          66 :             bisim_gjkw::B_to_C_iter_t const B_iter = SpC->postprocess_begin;    assert(part_tr.B_to_C_end() > B_iter);
    3097          66 :             bisim_gjkw::block_t* const B = B_iter->pred->source->block;         assert(B_iter->pred->succ->B_to_C == B_iter);
    3098          66 :             bisim_gjkw::B_to_C_desc_iter_t FromRed = B_iter->B_to_C_slice;      assert(FromRed->begin == B_iter);
    3099             :                                                                                 #ifndef NDEBUG
    3100          66 :                                                                                     bool postproc_a_posteriori = !FromRed->
    3101          66 :                                                                                         add_work_to_bottom_transns(bisim_gjkw::check_complexity::
    3102             :                                                                                                       for_all_transitions_that_need_postproc_a_priori_4_12, 1);
    3103             :                                                                                 #endif
    3104             :             // 4.13: Delete the transitions from B to SpC from those that need
    3105             :             //       postprocessing
    3106          66 :             SpC->postprocess_begin = FromRed->end;                              assert(SpC->postprocess_begin <= SpC->postprocess_end);
    3107          66 :                                                                                 assert(!B->to_constln.empty());
    3108          66 :             if (B->to_constln.begin() != FromRed)
    3109          63 :             {                                                                   assert(FromRed->from_block() == B);
    3110          63 :                 B->to_constln.splice(B->to_constln.begin(), B->to_constln,
    3111             :                                                                       FromRed);
    3112             :             }
    3113          66 :             /* do not refine a trivial block                                 */ assert(0 == B->marked_size());
    3114          74 :             if (1 == B->size())
    3115           8 :             {                                                                   assert(!postproc_a_posteriori);
    3116             :                                                                                 #ifndef NDEBUG
    3117           8 :                                                                                     if (0 != FromRed->work_counter.get_work_counter_4_4())
    3118             :                                                                                     {
    3119           0 :                                                                                         assert(FromRed->add_work_to_bottom_transns(
    3120             :                                                                                                   bisim_gjkw::check_complexity::
    3121             :                                                                                                   for_all_transitions_from_bottom_states_a_posteriori_4_4, 1));
    3122           0 :                                                                                         FromRed->work_counter.reset_work_counter_4_4();
    3123             :                                                                                     }
    3124             :                                                                                 #endif
    3125          19 :                 continue;
    3126             :             }
    3127             :             // refine() may destroy FromRed:  if the red subblock is smaller,
    3128             :             // the transitions in FromRed are moved to a new B_to_C slice.
    3129             :             // Therefore we select some transition from it, to restore the
    3130             :             // slice afterwards.  Any transition should do.
    3131             :                                                                                 #ifndef NDEBUG
    3132          58 :                                                                                     bisim_gjkw::pred_iter_t FromRed_save = FromRed->begin->pred;
    3133             :                                                                                 #endif
    3134             :             // 4.14: <RedB, BlueB> := Refine(B, SpC, {}, {transitions to SpC})
    3135          58 :             RedB = refine(B, SpC, &*FromRed, true);
    3136             :                                                                                 #ifndef NDEBUG
    3137          58 :                                                                                     FromRed = FromRed_save->succ->B_to_C->B_to_C_slice;
    3138          58 :                                                                                     if (postproc_a_posteriori && !FromRed->add_work_to_bottom_transns(
    3139             :                                                                                                   bisim_gjkw::check_complexity::
    3140             :                                                                                                   for_all_transitions_that_need_postproc_a_posteriori_4_12, 1))
    3141             :                                                                                     {
    3142           0 :                                                                                         assert(0 && "no new bottom states to assign work to");
    3143             :                                                                                     }
    3144             :                                                                                     // try to move the work that was not yet moved to the
    3145             :                                                                                     // transitions from (new) bottom states now.
    3146          58 :                                                                                     if (0 != FromRed->work_counter.get_work_counter_4_4())
    3147             :                                                                                     {
    3148           3 :                                                                                         if (!FromRed->add_work_to_bottom_transns(bisim_gjkw::check_complexity::
    3149             :                                                                                                    for_all_transitions_from_bottom_states_a_posteriori_4_4, 1))
    3150             :                                                                                         {
    3151           0 :                                                                                             assert(0 && "no new bottom states to assign work to");
    3152             :                                                                                         }
    3153           3 :                                                                                         FromRed->work_counter.reset_work_counter_4_4();
    3154             :                                                                                     }
    3155             :                                                                                 #endif
    3156             :             // 4.15: for all old bottom states s in RedB do
    3157          85 :             for (bisim_gjkw::permutation_iter_t
    3158          58 :                                  s_iter = RedB->marked_bottom_begin();
    3159         143 :                                  RedB->marked_bottom_end() != s_iter; ++s_iter)
    3160             :             {
    3161          85 :                 bisim_gjkw::state_info_ptr const s = *s_iter;
    3162             :                 // 4.16: Advance the current constellation pointer of s to the
    3163             :                 //       next constellation it can reach
    3164         255 :                 if (s->current_constln() < s->succ_end() &&
    3165         170 :                                 s->current_constln()->target->constln() == SpC)
    3166             :                 {
    3167             :                                                                                 #ifndef NDEBUG
    3168          85 :                                                                                     bisim_gjkw::succ_entry::slice_add_work_to_transns(s->current_constln(),
    3169             :                                                                                      bisim_gjkw::check_complexity::for_all_old_bottom_states_s_in_RedB_4_15,1);
    3170             :                                                                                 #endif
    3171          85 :                     s->set_current_constln(bisim_gjkw::succ_entry::slice_end(
    3172             :                                                         s->current_constln()));
    3173             :                 }                                                               else
    3174           0 :                                                                                 {   mCRL2complexity(s, add_work(bisim_gjkw::check_complexity::
    3175             :                                                                                                       for_all_old_bottom_states_s_in_RedB_selfloop_4_15, 1), );
    3176           0 :                                                                                     assert(B == RedB /* we should test: BlueB is empty */);
    3177           0 :                                                                                     assert(B->constln() == SpC);
    3178             :                                                                                 }
    3179          85 :                                                                                 assert(s->succ_end() == s->current_constln() ||
    3180             :             /* 4.17: end for                                                 */                               *SpC < *s->current_constln()->target->constln());
    3181             :             }
    3182          58 :             /* 4.18: if RedB contains new bottom states then                 */ assert(RedB->marked_nonbottom_begin() == RedB->marked_nonbottom_end());
    3183          58 :             if (0 != RedB->unmarked_bottom_size())
    3184             :             {
    3185             :                 // 4.19: <_, RfnB> := Refine(RedB, cosplit(RedB, BlueB), {old
    3186             :                 //                           bottom states in RedB}, {})
    3187             :                                                                                 #ifndef NDEBUG
    3188           3 :                                                                                     blue_begin = RedB->begin();
    3189             :                                                                                 #endif
    3190           3 :                 if (0 != RedB->marked_bottom_size())
    3191             :                 {
    3192           0 :                     RedB = refine(RedB, nullptr, nullptr, true);                assert(nullptr != RedB);  assert(0 == RedB->unmarked_bottom_size());
    3193             :                     // 4.26: Destroy all temporary data
    3194             :                         // As part of this line, we unmark all states.
    3195           0 :                     RedB->set_marked_bottom_begin(RedB->bottom_end());          assert(RedB->begin() > blue_begin);
    3196           0 :                     RfnB = RedB->begin()[-1]->block;
    3197             :                 }
    3198             :                 else
    3199             :                 {
    3200           3 :                     RfnB = RedB;
    3201             :                                                                                 #ifndef NDEBUG
    3202           3 :                                                                                     RedB = nullptr;
    3203             :                                                                                 #endif
    3204           3 :                 }                                                               assert(RedB != RfnB);
    3205           3 :                                                                                 assert(RfnB->begin() == blue_begin);
    3206             :                 // do not refine a trivial block
    3207           6 :                 if (1 == RfnB->size())
    3208           3 :                 {                                                               assert(0 == RfnB->marked_size());
    3209           3 :                     continue;
    3210             :                 }
    3211             :                 // 4.20: Register that the transitions from RfnB to SpC need
    3212             :                 //       postprocessing
    3213           0 :                 bisim_gjkw::B_to_C_desc_iter_t new_slice =
    3214           0 :                                        SpC->postprocess_begin[-1].B_to_C_slice; assert(new_slice->from_block() == RfnB);
    3215           0 :                                                                                 assert(new_slice->to_constln() == SpC);
    3216           0 :                 SpC->postprocess_begin = new_slice->begin;                      assert(new_slice->end <= SpC->postprocess_end);
    3217             :                 // move the set of transitions to the end of the list
    3218           0 :                 RfnB->to_constln.splice(RfnB->to_constln.end(),
    3219             :                                                   RfnB->to_constln, new_slice);
    3220             :                 // 4.21: Restart the procedure (but keep R),
    3221             :                 //       i. e. go to Line 4.4
    3222           0 :                 goto Line_4_4;
    3223             :             // 4.22: end if
    3224             :             }
    3225             :             // 4.26: Destroy all temporary data
    3226             :                 // As part of this line, we unmark all states.
    3227          55 :             RedB->set_marked_bottom_begin(RedB->bottom_end());
    3228             :         // 4.23: end for
    3229             :         }
    3230          66 :         while (SpC->postprocess_begin != SpC->postprocess_end);
    3231             :         // 4.24: Delete SpC from R
    3232          60 :         R.erase(R.begin());
    3233             :     // 4.25: end for
    3234             :     }
    3235          28 :     /* 4.26: Destroy all temporary data                                      */ assert(R.empty());
    3236             : 
    3237          28 :     return ResultB;
    3238             : }
    3239             : 
    3240             : 
    3241             : 
    3242             : /*=============================================================================
    3243             : =                       explicit instantiation requests                       =
    3244             : =============================================================================*/
    3245             : 
    3246             : 
    3247             : 
    3248             : namespace bisim_gjkw
    3249             : {
    3250             : 
    3251             : template class bisim_partitioner_gjkw_initialise_helper<lts_lts_t>;
    3252             : template class bisim_partitioner_gjkw_initialise_helper<lts_aut_t>;
    3253             : template class bisim_partitioner_gjkw_initialise_helper<lts_fsm_t>;
    3254             : 
    3255             : } // end namespace bisim_gjkw
    3256             : 
    3257             : template class bisim_partitioner_gjkw<lts_lts_t>;
    3258             : template class bisim_partitioner_gjkw<lts_aut_t>;
    3259             : template class bisim_partitioner_gjkw<lts_fsm_t>;
    3260             : 
    3261             : } // end namespace detail
    3262             : } // end namespace lts
    3263          21 : } // end namespace mcrl2

Generated by: LCOV version 1.13