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

Generated by: LCOV version 1.12