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

Generated by: LCOV version 1.12