liblts_bisim_gj.h

Go to the documentation of this file.

// Author(s): Jan Friso Groote (with edits by David N. Jansen)
//
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
 
 
#ifndef LIBLTS_BISIM_GJ_H
#define LIBLTS_BISIM_GJ_H
 
#include <iomanip> // for std::fixed, std::setprecision(), std::setw()
#include <ctime> // for std::clock_t, std::clock()
//#include "mcrl2/utilities/hash_utility.h"
#include "mcrl2/lts/detail/liblts_scc.h"
#include "mcrl2/lts/detail/liblts_merge.h"
#include "mcrl2/lts/detail/check_complexity.h"
#include "mcrl2/lts/detail/fixed_vector.h"
#include "mcrl2/lts/detail/simple_list.h"
#define linked_list simple_list
 
// If `USE_FOUR_WAY_SPLIT` is defined, then splitting a block will use a
// four-way split function that can split under a main and a co-splitter at the
// same time, together with creating the new bottom state block.
#define USE_FOUR_WAY_SPLIT
 
namespace mcrl2
{
namespace lts
{
namespace detail
{
 
template <class LTS_TYPE> class bisim_partitioner_gj;
 
namespace bisimulation_gj
{
 
// Forward declaration.
struct state_type_gj;
struct block_type;
struct constellation_type;
struct transition_type;
struct outgoing_transition_type;
 
typedef std::size_t state_index;
typedef std::size_t transition_index;
 
 
typedef std::size_t label_index;
typedef fixed_vector<outgoing_transition_type>::iterator
                                                       outgoing_transitions_it;
typedef fixed_vector<outgoing_transition_type>::const_iterator
                                                 outgoing_transitions_const_it;
 
constexpr constellation_type* null_constellation=nullptr;
constexpr transition_index null_transition=-1;
constexpr label_index null_action=-1;
constexpr state_index null_state=-1;
constexpr block_type* null_block=nullptr;
constexpr transition_index undefined=0;
constexpr transition_index Rmarked=-1;
constexpr transition_index Umarked=1;
 
#ifdef USE_FOUR_WAY_SPLIT
  constexpr transition_index marked_range=
    (std::numeric_limits<transition_index>::max()-2)/3;
 
  enum subblocks { ReachAlw=0,// states that can reach always all splitters
                   MissMain,  // states that cannot inertly reach the main
                              // splitter (while it is not empty)
                   XcludeCo,  // states that cannot inertly reach the
                              // co-splitter (while it is not empty)
                   MultiSub}; // states that can inertly reach multiple of
                              // the above subblocks
                // The following values are used only for temporary marking
                // and are not really associated with a subblock:
                // Hit_Main -- states that can (non-inertly) reach the main
                //             splitter; they can be in any subblock except
                //             MissMain.  Necessary for correctness.
 
  static inline constexpr transition_index marked(enum subblocks subblock)
  {
    return
                                                                                assert(ReachAlw==subblock || MissMain==subblock ||
                                                                                       XcludeCo==subblock || MultiSub==subblock),
           marked_range*subblock+1;
  }
 
  constexpr transition_index marked_MultiSub=marked(MultiSub);                  static_assert(marked_MultiSub<std::numeric_limits<transition_index>::max());
  constexpr transition_index marked_Hit_Main=marked_MultiSub+1;
 
  static inline constexpr bool is_in_marked_range_of
                            (transition_index counter, enum subblocks subblock)
  {
    return                                                                      assert(ReachAlw==subblock || MissMain==subblock || XcludeCo==subblock),
           counter-marked(subblock)<marked_range;
  }
#endif
 
template <class CONTAINER>
static inline void clear(CONTAINER& c)
{
  if (c.size()>1000) { c=CONTAINER(); } else { c.clear(); }
}
 
// The struct below facilitates to walk through a LBC_list starting from an
// arbitrary transition.
typedef transition_index* BLC_list_iterator; // should not be nullptr
typedef transition_index* BLC_list_iterator_or_null; // can be nullptr
typedef const transition_index* BLC_list_const_iterator; // should not be nullptr
 
struct outgoing_transition_type
{
  union iterator_or_counter
  {
    transition_index transitions;
    BLC_list_iterator BLC_transitions;
    iterator_or_counter()
      : transitions()
    {}
    void convert_to_iterator(const BLC_list_iterator other)
    {
      new (&BLC_transitions) BLC_list_iterator(other);
    }
    ~iterator_or_counter()  {  BLC_transitions.~BLC_list_iterator();  }
  } ref;
 
  outgoing_transitions_it start_same_saC;
 
  // The default initialiser does not initialize the fields of this struct.
  outgoing_transition_type()
  {}
 
  outgoing_transition_type(const outgoing_transitions_it sssaC)
   : ref(),
     start_same_saC(sssaC)
  {}
};
 
struct state_in_block_pointer
{
  state_in_block_pointer(fixed_vector<state_type_gj>::iterator new_ref_state)
   : ref_state(new_ref_state)
  {}
 
  state_in_block_pointer()
  {}
 
  fixed_vector<state_type_gj>::iterator ref_state;
 
  bool operator==(const state_in_block_pointer& other) const
  {
    return ref_state==other.ref_state;
  }
 
  bool operator!=(const state_in_block_pointer& other) const
  {
    return ref_state!=other.ref_state;
  }
};
 
class todo_state_vector
{
  std::size_t m_todo_indicator=0;
  std::vector<state_in_block_pointer> m_vec;
 
  public:
    typedef std::vector<state_in_block_pointer>::const_iterator const_iterator;
                                                                                #ifndef NDEBUG
                                                                                  bool find(const state_in_block_pointer s) const
                                                                                  {
                                                                                    return std::find(m_vec.begin(), m_vec.end(), s)!=m_vec.end();
                                                                                  }
                                                                                #endif
    void add_todo(const state_in_block_pointer s)
    {                                                                           assert(!find(s));
      m_vec.push_back(s);
    }
 
    std::size_t todo_is_empty() const
    {
      return m_vec.size()==m_todo_indicator;
    }
 
    // Move a state from the todo part to the definitive vector.
    state_in_block_pointer move_from_todo()
    {                                                                           assert(!todo_is_empty());
      state_in_block_pointer result=m_vec[m_todo_indicator];
      m_todo_indicator++;
      return result;
    }
 
    void swap_vec(std::vector<state_in_block_pointer>& other_vec)
    {
      m_vec.swap(other_vec);
      m_todo_indicator=0;
    }
 
    std::size_t size() const
    {
      return m_vec.size();
    }
 
    std::size_t empty() const
    {
      return m_vec.empty();
    }
 
    const_iterator begin() const
    {
      return m_vec.begin();
    }
 
    const_iterator end() const
    {
      return m_vec.end();
    }
 
    const state_in_block_pointer* data() const
    {
      return m_vec.data();
    }
 
    const state_in_block_pointer* data_end() const
    {
      return m_vec.data() + m_vec.size();
    }
 
    const state_in_block_pointer& front() const
    {
      return m_vec.front();
    }
 
    //const state_in_block_pointer& back() const
    //{
    //  return m_vec.back();
    //}
 
#ifdef USE_FOUR_WAY_SPLIT
    void reserve(std::vector<state_in_block_pointer>::size_type new_cap)
    {
      m_vec.reserve(new_cap);
    }
 
    typedef std::vector<state_in_block_pointer>::iterator iterator;
 
    iterator begin()
    {
      return m_vec.begin();
    }
 
    iterator end()
    {
      return m_vec.end();
    }
 
    // add all elements in [begin, end) to the vector
    void add_todo(iterator begin, iterator end)
    {
      m_vec.insert(m_vec.end(), begin, end);
    }
#endif
 
    void clear()
    {
      m_todo_indicator=0;
      bisimulation_gj::clear(m_vec);
    }
};
 
 
 
// Below the four main data structures are listed.
struct state_type_gj
{
  block_type* block=null_block;
  std::vector<transition>::iterator start_incoming_transitions;
  outgoing_transitions_it start_outgoing_transitions;
  state_in_block_pointer* ref_states_in_blocks;
  transition_index no_of_outgoing_block_inert_transitions=0;
  transition_index counter=undefined;
                                                                                #ifndef NDEBUG
                                                                                  template<class LTS_TYPE>
                                                                                  std::string debug_id_short(const bisim_partitioner_gj<LTS_TYPE>& partitioner) const
                                                                                  {
                                                                                    assert(partitioner.m_states.data()<=this);
                                                                                    assert(this<partitioner.m_states.data_end());
                                                                                    return std::to_string(this-partitioner.m_states.data());
                                                                                  }
 
                                                                                  template<class LTS_TYPE>
                                                                                  std::string debug_id(const bisim_partitioner_gj<LTS_TYPE>& partitioner) const
                                                                                  {
                                                                                    return "state " + debug_id_short(partitioner);
                                                                                  }
                                                                                #endif
                                                                                #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
                                                                                  mutable check_complexity::state_gj_counter_t work_counter;
                                                                                #endif
};
 
struct BLC_indicators
{
  BLC_list_iterator start_same_BLC;
 
  // If the source block of the BLC_indicator has new bottom states,
  // it is undefined whether the BLC_indicator should be regarded as stable or
  // unstable. Otherwise, the BLC_indicator is regarded as stable if and only
  // if start_marked_BLC is ==nullptr.
  BLC_list_iterator_or_null start_marked_BLC;
  BLC_list_iterator end_same_BLC;
 
  BLC_indicators(BLC_list_iterator start, BLC_list_iterator end,bool is_stable)
   : start_same_BLC(start),
     start_marked_BLC(is_stable ? nullptr : end),
     end_same_BLC(end)
  {                                                                             assert(nullptr!=start_same_BLC);  assert(nullptr!=end_same_BLC);
                                                                                assert(start_same_BLC<=end_same_BLC);
  }
 
  bool is_stable() const
  {                                                                             assert(nullptr!=start_same_BLC);  assert(nullptr!=end_same_BLC);
                                                                                assert(nullptr==start_marked_BLC || start_same_BLC<=start_marked_BLC);
                                                                                assert(nullptr==start_marked_BLC || start_marked_BLC<=end_same_BLC);
                                                                                assert(start_same_BLC<=end_same_BLC);
    return nullptr==start_marked_BLC;
  }
 
  bool has_marked_transitions() const
  {
    if (is_stable())
    {
      return false;
    }                                                                           assert(start_same_BLC<=start_marked_BLC);
                                                                                assert(start_marked_BLC<=end_same_BLC);
    return start_marked_BLC<end_same_BLC;
  }
 
  void make_stable()
  {                                                                             assert(!is_stable());
    start_marked_BLC=nullptr;
  }
 
  void make_unstable()
  {                                                                             assert(is_stable());
    start_marked_BLC=end_same_BLC;
  }
 
  bool operator==(const BLC_indicators& other) const
  {
    return start_same_BLC==other.start_same_BLC &&
           start_marked_BLC==other.start_marked_BLC &&
           end_same_BLC==other.end_same_BLC;
  }
 
  bool operator!=(const BLC_indicators& other) const
  {
    return !operator==(other);
  }
                                                                                #ifndef NDEBUG
                                                                                  template<class LTS_TYPE>
                                                                                  std::string debug_id(const bisim_partitioner_gj<LTS_TYPE>& partitioner,
                                                                                                                 const block_type* from_block=nullptr) const
                                                                                  {
                                                                                    assert(partitioner.m_BLC_transitions.data()<=start_same_BLC);
                                                                                    assert(nullptr==start_marked_BLC || start_same_BLC<=start_marked_BLC);
                                                                                    assert(nullptr==start_marked_BLC || start_marked_BLC<=end_same_BLC);
                                                                                    assert(start_same_BLC<=end_same_BLC);
                                                                                    assert(end_same_BLC<=partitioner.m_BLC_transitions.data_end());
                                                                                    std::string result("BLC set ["+std::to_string(std::distance<BLC_list_const_iterator>(&*partitioner.m_BLC_transitions.begin(), start_same_BLC))+","+std::to_string(std::distance<BLC_list_const_iterator>(&*partitioner.m_BLC_transitions.begin(), end_same_BLC))+")");
                                                                                    if (start_same_BLC==end_same_BLC)
                                                                                    {
                                                                                      return "Empty "+result;
                                                                                    }
                                                                                    result += " from "+(nullptr==from_block ? partitioner.m_states[partitioner.m_aut.get_transitions()[*start_same_BLC].from()].block : from_block)->debug_id(partitioner);
                                                                                    result += " to ";
                                                                                    result += partitioner.m_states[partitioner.m_aut.get_transitions()[*start_same_BLC].to()].block->c.onstellation->debug_id(partitioner);
                                                                                    result += " containing the ";
                                                                                    if (std::distance(start_same_BLC, end_same_BLC)>1)
                                                                                    {
                                                                                        result+=std::to_string(std::distance(start_same_BLC, end_same_BLC));
                                                                                        result += " transitions ";
                                                                                    }
                                                                                    else
                                                                                    {
                                                                                        result += "transition ";
                                                                                    }
                                                                                    BLC_list_const_iterator iter = start_same_BLC;
                                                                                    if (start_marked_BLC == iter)
                                                                                    {
                                                                                        result += "| ";
                                                                                    }
                                                                                    result += partitioner.m_transitions[*iter].debug_id_short(partitioner);
                                                                                    if (std::distance(start_same_BLC, end_same_BLC)>4)
                                                                                    {
                                                                                        ++iter;
                                                                                        result += start_marked_BLC == iter ? " | " : ", ";
                                                                                        result += partitioner.m_transitions[*iter].debug_id_short(partitioner);
                                                                                        result += std::next(iter) == start_marked_BLC ? " | ..."
                                                                                                  : (!is_stable() && start_marked_BLC>std::next(iter) && start_marked_BLC<=end_same_BLC-3 ? ", ..|.." : ", ...");
                                                                                        iter = end_same_BLC-3;
                                                                                    }
                                                                                    while (++iter!=end_same_BLC)
                                                                                    {
                                                                                        result += start_marked_BLC == iter ? " | " : ", ";
                                                                                        result += partitioner.m_transitions[*iter].debug_id_short(partitioner);
                                                                                    }
                                                                                    if (start_marked_BLC == iter)
                                                                                    {
                                                                                        result += " |";
                                                                                    }
                                                                                    return result;
                                                                                  }
                                                                                #endif
                                                                                #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
                                                                                  mutable check_complexity::BLC_gj_counter_t work_counter;
                                                                                #endif
};
 
struct transition_type
{
  // The position of the transition type corresponds to m_aut.get_transitions().
  // std::size_t from, label, to are found in m_aut.get_transitions().
  linked_list<BLC_indicators>::iterator transitions_per_block_to_constellation;
  outgoing_transitions_it ref_outgoing_transitions;  // This refers to the position of this transition in m_outgoing_transitions.
                                                     // During initialisation m_outgoing_transitions contains the indices of this
                                                     // transition. After initialisation m_outgoing_transitions refers to the corresponding
                                                     // entry in m_BLC_transitions, of which the field transition contains the index
                                                     // of this transition.
                                                                                #ifndef NDEBUG
                                                                                  template<class LTS_TYPE>
                                                                                  std::string debug_id_short(const bisim_partitioner_gj<LTS_TYPE>& partitioner) const
                                                                                  {
                                                                                    assert(partitioner.m_transitions.data()<=this);
                                                                                    assert(this<partitioner.m_transitions.data_end());
                                                                                    const transition& t=partitioner.m_aut.get_transitions()
                                                                                                                       [this-partitioner.m_transitions.data()];
                                                                                    return partitioner.m_states[t.from()].debug_id_short(partitioner) + " -" +
                                                                                           pp(partitioner.m_aut.action_label(t.label())) + "-> " +
                                                                                           partitioner.m_states[t.to()].debug_id_short(partitioner);
                                                                                  }
 
                                                                                  template<class LTS_TYPE>
                                                                                  std::string debug_id(const bisim_partitioner_gj<LTS_TYPE>& partitioner) const
                                                                                  {
                                                                                    return "transition " + debug_id_short(partitioner);
                                                                                  }
                                                                                #endif
                                                                                #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
                                                                                  mutable check_complexity::trans_gj_counter_t work_counter;
                                                                                #endif
};
 
struct block_type
{
  union constellation_or_first_unmarked_bottom_state
  {
    constellation_type* onstellation;
 
    state_in_block_pointer* first_unmarked_bottom_state;
 
    constellation_or_first_unmarked_bottom_state(constellation_type* new_c)
      :onstellation(new_c)
    {}
  } c;
 
  state_in_block_pointer* start_bottom_states;
 
  union start_non_bottom_states_or_state_in_reduced_LTS
  {
    state_in_block_pointer* rt_non_bottom_states;
 
    state_index te_in_reduced_LTS;
 
    start_non_bottom_states_or_state_in_reduced_LTS(state_in_block_pointer* s)
      : rt_non_bottom_states(s)
    {}
  } sta;
 
  state_in_block_pointer* end_states;
 
  union btc_R
  {
    linked_list<BLC_indicators> to_constellation;                               static_assert(std::is_trivially_destructible
                                                                                                                        <linked_list<BLC_indicators> >::value);
    std::vector<state_in_block_pointer>* R;
 
    btc_R()
      : R(nullptr)
    {}
 
    static bool if_R_is_nullptr_then_to_constellation_is_empty_list()
    {
      btc_R test_should_be_empty_BLC_list=btc_R();                              assert(nullptr==test_should_be_empty_BLC_list.R);
      if constexpr (sizeof(test_should_be_empty_BLC_list.R)!=
                        sizeof(test_should_be_empty_BLC_list.to_constellation))
      {
        return false;
      }
      if (test_should_be_empty_BLC_list.to_constellation.empty() &&
          test_should_be_empty_BLC_list.to_constellation==
                                                 linked_list<BLC_indicators>())
      {
        // no need to change `test_should_be_empty_BLC_list` from a pointer
        // to a linked_list explicitly, as the two seem to have the same bit
        // pattern; the destructor will work fine.
        return true;
      }
      // The destructor expects a linked list:
      new (&test_should_be_empty_BLC_list) linked_list<BLC_indicators>();
      return false;
    }
  } block;
 
  block_type(const block_type& other)
    : c(other.c.onstellation),
      start_bottom_states(other.start_bottom_states),
      sta(other.sta.rt_non_bottom_states),
      end_states(other.end_states),
      block(other.block),
      contains_new_bottom_states(other.contains_new_bottom_states)
  {}
 
  bool contains_new_bottom_states;
 
#ifndef USE_FOUR_WAY_SPLIT
  block_type(state_in_block_pointer* beginning_of_states,
             constellation_type* new_c)
    : c(new_c),
      start_bottom_states(beginning_of_states),
      sta(beginning_of_states),
      end_states(beginning_of_states),
      block(),
      contains_new_bottom_states(false)
  {}
#endif
 
  block_type(state_in_block_pointer* start_bottom,
             state_in_block_pointer* start_non_bottom,
             state_in_block_pointer* end,
             constellation_type* new_c)
    : c(new_c),
      start_bottom_states(start_bottom),
      sta(start_non_bottom),
      end_states(end),
      block(),
      contains_new_bottom_states(false)
  {                                                                             assert(start_bottom<=start_non_bottom);  assert(start_non_bottom<=end);
  }
                                                                                #ifndef NDEBUG
                                                                                  template<class LTS_TYPE>
                                                                                  std::string debug_id(const bisim_partitioner_gj<LTS_TYPE>& partitioner) const
                                                                                  { assert(partitioner.m_states_in_blocks.data()<=start_bottom_states);
                                                                                    assert(start_bottom_states<=sta.rt_non_bottom_states);
                                                                                    assert(sta.rt_non_bottom_states<=end_states);
                                                                                    assert(end_states<=partitioner.m_states_in_blocks.data_end());
                                                                                    return"block ["+std::to_string
                                                                                          (std::distance<const state_in_block_pointer*>
                                                                                            (partitioner.m_states_in_blocks.data(), start_bottom_states))+","+
                                                                                        std::to_string
                                                                                          (std::distance<const state_in_block_pointer*>
                                                                                            (partitioner.m_states_in_blocks.data(), end_states))+")";
                                                                                  }
                                                                                #endif
                                                                                #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
                                                                                  mutable check_complexity::block_gj_counter_t work_counter;
                                                                                #endif
};
 
struct constellation_type
{
  state_in_block_pointer* start_const_states;
 
  state_in_block_pointer* end_const_states;
 
  constellation_type(state_in_block_pointer* const new_start,
                     state_in_block_pointer* const new_end)
    : start_const_states(new_start),
      end_const_states(new_end)
  {}
                                                                                #ifndef NDEBUG
                                                                                  template<class LTS_TYPE>
                                                                                  std::string debug_id(const bisim_partitioner_gj<LTS_TYPE>& partitioner) const
                                                                                  { assert(partitioner.m_states_in_blocks.data()<=start_const_states);
                                                                                    assert(start_const_states<end_const_states);
                                                                                    assert(end_const_states<=partitioner.m_states_in_blocks.data_end());
                                                                                    return "constellation ["+std::to_string
                                                                                          (std::distance<const state_in_block_pointer*>
                                                                                            (partitioner.m_states_in_blocks.data(), start_const_states))+","+
                                                                                        std::to_string
                                                                                          (std::distance<const state_in_block_pointer*>
                                                                                            (partitioner.m_states_in_blocks.data(), end_const_states))+")";
                                                                                  }
                                                                                #endif
};
 
} // end namespace bisimulation_gj
 
 
/*=============================================================================
=                                 main class                                  =
=============================================================================*/
 
 
using namespace mcrl2::lts::detail::bisimulation_gj;
 
template <class LTS_TYPE>
class bisim_partitioner_gj
{
  private:
 
    typedef std::unordered_set<state_index> set_of_states_type;
    typedef std::unordered_set<transition_index> set_of_transitions_type;
                                                                                #ifndef NDEBUG
                                                                                  public: // needed for the debugging functions, e.g. debug_id().
                                                                                #endif
    LTS_TYPE& m_aut;
 
    // Generic data structures.
    fixed_vector<state_type_gj> m_states;
 
    fixed_vector<outgoing_transition_type> m_outgoing_transitions;
                                                                  // During refining this contains the index in m_BLC_transition, of which
                                                                  // the transition field contains the index of the transition.
    fixed_vector<transition_type> m_transitions;
    fixed_vector<state_in_block_pointer> m_states_in_blocks;
    state_index no_of_blocks;
    state_index no_of_constellations;
    fixed_vector<transition_index> m_BLC_transitions;
  private:
    std::vector<block_type*> m_blocks_with_new_bottom_states;
 
#ifndef USE_FOUR_WAY_SPLIT
    todo_state_vector m_R, m_U;
    std::vector<state_in_block_pointer> m_U_counter_reset_vector;
#endif
 
    std::vector<constellation_type*> m_non_trivial_constellations;
 
    std::vector<linked_list<BLC_indicators>::iterator>
                                                m_BLC_indicators_to_be_deleted;
 
#ifndef USE_FOUR_WAY_SPLIT
    std::vector<std::pair<BLC_list_iterator, block_type*> >
                                                  m_co_splitters_to_be_checked;
#endif
 
    const bool m_branching;
 
    const bool m_preserve_divergence;
 
    static typename LTS_TYPE::labels_size_type m_aut_apply_hidden_label_map
                                        (typename LTS_TYPE::labels_size_type l)
    {
      return l;
    }
 
    bool is_inert_during_init_if_branching(const transition& t) const
    {                                                                           assert(m_branching);
      return m_aut.is_tau(m_aut_apply_hidden_label_map(t.label())) &&
             (!m_preserve_divergence || t.from() != t.to());
    }
 
    bool is_inert_during_init(const transition& t) const
    {
      return m_branching && is_inert_during_init_if_branching(t);
    }
 
    label_index label_or_divergence(const transition& t,
                                    const label_index divergent_label=-2
                                        /* different from null_action */) const
    {
      label_index result = m_aut_apply_hidden_label_map(t.label());             assert(divergent_label!=result);  assert(null_action!=divergent_label);
      if (m_preserve_divergence && (                                            assert(m_branching),
           t.from() == t.to()) &&
          m_aut.is_tau(result))
      {
        return divergent_label;
      }
      return result;
    }
                                                                                #ifndef NDEBUG
                                                                                  void check_transitions(const bool initialisation,
                                                                                                         const bool check_temporary_complexity_counters,
                                                                                                         const bool check_block_to_constellation = true) const
                                                                                  {
                                                                                    for(transition_index ti=0; ti<m_aut.num_transitions(); ++ti)
                                                                                    {
                                                                                      const BLC_list_const_iterator btc_ti=
                                                                                               m_transitions[ti].ref_outgoing_transitions->ref.BLC_transitions;
                                                                                      assert(*btc_ti==ti);
 
                                                                                      const transition& t=m_aut.get_transitions()[ti];
                                                                                      assert(&*m_states[t.to()].start_incoming_transitions<=&t);
                                                                                      if (t.to()+1!=m_aut.num_states())
                                                                                      {
                                                                                        assert(&t<=&*std::prev(m_states[t.to()+1].start_incoming_transitions));
                                                                                      }
                                                                                      else
                                                                                      {
                                                                                        assert(&t<=&m_aut.get_transitions().back());
                                                                                      }
 
                                                                                      assert(m_states[t.from()].start_outgoing_transitions<=
                                                                                                                   m_transitions[ti].ref_outgoing_transitions);
                                                                                      if (t.from()+1==m_aut.num_states())
                                                                                      {
                                                                                        assert(m_transitions[ti].ref_outgoing_transitions<
                                                                                                                                 m_outgoing_transitions.end());
                                                                                      }
                                                                                      else
                                                                                      {
                                                                                        assert(m_transitions[ti].ref_outgoing_transitions<
                                                                                                            m_states[t.from() + 1].start_outgoing_transitions);
                                                                                      }
 
                                                                                      assert(m_transitions[ti].
                                                                                               transitions_per_block_to_constellation->start_same_BLC<=btc_ti);
                                                                                      assert(btc_ti<m_transitions[ti].
                                                                                                         transitions_per_block_to_constellation->end_same_BLC);
 
                                                                                      if (!check_block_to_constellation)
                                                                                        continue;
 
                                                                                      block_type* const b=m_states[t.from()].block;
 
                                                                                      const label_index t_label = label_or_divergence(t);
                                                                                      bool found=false;
                                                                                      for(const BLC_indicators& blc: b->block.to_constellation)
                                                                                      {
                                                                                        if (!blc.is_stable())
                                                                                        {
                                                                                          assert(blc.start_same_BLC<=blc.start_marked_BLC);
                                                                                          assert(blc.start_marked_BLC<=blc.end_same_BLC);
                                                                                        }
                                                                                        assert(blc.start_same_BLC<blc.end_same_BLC);
                                                                                        transition& first_t = m_aut.get_transitions()[*blc.start_same_BLC];
                                                                                        assert(b == m_states[first_t.from()].block);
                                                                                        if (t_label == label_or_divergence(first_t) &&
                                                                                            m_states[first_t.to()].block->c.onstellation ==
                                                                                                                        m_states[t.to()].block->c.onstellation)
                                                                                        {
// if (found) { std::cerr << "Found multiple BLC sets with transitions (" << b->debug_id(*this) << " -" << m_aut.action_label(t.label()) << "-> " << m_states[t.to()].block->c.onstellation->debug_id(*this) << ")\n"; }
                                                                                          assert(!found);
                                                                                          assert(blc.start_same_BLC <= btc_ti);
                                                                                          assert(btc_ti<blc.end_same_BLC);
                                                                                          assert(&blc == &*m_transitions[ti].transitions_per_block_to_constellation);
                                                                                          found = true;
                                                                                        }
                                                                                      }
                                                                                      assert(found);
                                                                                      if (check_temporary_complexity_counters)
                                                                                      {
                                                                                        block_type* const targetb = m_states[t.to()].block;
                                                                                        const unsigned max_sourceB = check_complexity::log_n-
                                                                                                        check_complexity::ilog2(number_of_states_in_block(*b));
                                                                                        const unsigned max_targetC = check_complexity::log_n-
                                                                                              check_complexity::ilog2(number_of_states_in_constellation
                                                                                                                                   (*targetb->c.onstellation));
                                                                                        const unsigned max_targetB = check_complexity::log_n-
                                                                                                  check_complexity::ilog2(number_of_states_in_block(*targetb));
                                                                                        mCRL2complexity(&m_transitions[ti],
                                                                                                no_temporary_work(max_sourceB, max_targetC, max_targetB,
                                                                                                !initialisation &&
                                                                                                0==m_states[t.from()].no_of_outgoing_block_inert_transitions),
                                                                                                                                                        *this);
                                                                                      }
                                                                                    }
                                                                                  }
 
                                                                                  [[nodiscard]]
                                                                                  bool check_data_structures(const std::string& tag, const bool initialisation=false, const bool check_temporary_complexity_counters=true) const
                                                                                  {
                                                                                    mCRL2log(log::debug) << "Check data structures: " << tag << ".\n";
                                                                                    assert(m_states.size()==m_aut.num_states());
                                                                                    assert(m_states_in_blocks.size()==m_aut.num_states());
                                                                                    assert(m_transitions.size()==m_aut.num_transitions());
                                                                                    assert(m_outgoing_transitions.size()==m_aut.num_transitions());
                                                                                    assert(m_BLC_transitions.size()==m_aut.num_transitions());
 
                                                                                    // Check that the elements in m_states are well formed.
                                                                                    for (fixed_vector<state_type_gj>::iterator si=
                                                                                            const_cast<fixed_vector<state_type_gj>&>(m_states).begin();
                                                                                                                                      si<m_states.cend(); si++)
                                                                                    {
                                                                                      const state_type_gj& s=*si;
 
                                                                                      assert(s.counter==undefined);
                                                                                      assert(s.block->start_bottom_states< s.block->sta.rt_non_bottom_states);
                                                                                      assert(s.block->sta.rt_non_bottom_states<=s.block->end_states);
 
                                                                                      // In the following line we need that si is an iterator (not a const_iterator)
                                                                                      assert(std::find(s.block->start_bottom_states,
                                                                                                    s.block->end_states,
                                                                                                    state_in_block_pointer(si))!=s.block->end_states);
 
                                                                                      assert(s.ref_states_in_blocks->ref_state==si);
 
                                                                                      // ensure that in the incoming transitions we first have the transitions
                                                                                      // with label tau, and then the other transitions:
                                                                                      bool maybe_tau=true;
                                                                                      const std::vector<transition>::const_iterator end_it1=
                                                                                            std::next(si)>=m_states.end() ? m_aut.get_transitions().end()
                                                                                                                   : std::next(si)->start_incoming_transitions;
                                                                                      for (std::vector<transition>::const_iterator
                                                                                                            it=s.start_incoming_transitions; it!=end_it1; ++it)
                                                                                      {
                                                                                        const transition& t=*it;
                                                                                        if (m_aut.is_tau(m_aut_apply_hidden_label_map(t.label())))
                                                                                        {
                                                                                          assert(maybe_tau);
                                                                                        }
                                                                                        else
                                                                                        {
                                                                                          maybe_tau=false;
                                                                                        }
                                                                                        // potentially we might test that the transitions are grouped per label
                                                                                      }
 
                                                                                      // Check that for each state the outgoing transitions satisfy the
                                                                                      // following invariant:  First there are (originally) inert transitions
                                                                                      // (inert transitions may be separated over multiple constellations, so
                                                                                      // we cannot require that the inert transitions come before other
                                                                                      // tau-transitions).  Then there are other transitions sorted per label
                                                                                      // and constellation.
                                                                                      std::unordered_set<std::pair<label_index, const constellation_type*> >
                                                                                                                                           constellations_seen;
 
                                                                                      maybe_tau=true;
                                                                                      // The construction below is to enable translation on Windows.
                                                                                      const outgoing_transitions_const_it end_it2=
                                                                                            std::next(si)>=m_states.end() ? m_outgoing_transitions.cend()
                                                                                                                   : std::next(si)->start_outgoing_transitions;
                                                                                      for(outgoing_transitions_const_it it=s.start_outgoing_transitions;
                                                                                                                                             it!=end_it2; ++it)
                                                                                      {
                                                                                        const transition& t=m_aut.get_transitions()[!initialisation
                                                                                                             ? *it->ref.BLC_transitions : it->ref.transitions];
// if (t.from() != si) { std::cerr << m_transitions[*it->ref.BLC_transitions].debug_id(*this) << " is an outgoing transition of state " << si << "!\n"; }
                                                                                        assert(m_states.cbegin()+t.from()==si);
                                                                                        assert(m_transitions[!initialisation ? *it->ref.BLC_transitions
                                                                                                          : it->ref.transitions].ref_outgoing_transitions==it);
                                                                                        assert((it->start_same_saC>it &&
                                                                                                it->start_same_saC<m_outgoing_transitions.end() &&
                                                                                                ((it+1)->start_same_saC==it->start_same_saC ||
                                                                                                 (it+1)->start_same_saC<=it)) ||
                                                                                               (it->start_same_saC<=it &&
                                                                                                (it+1==m_outgoing_transitions.end() ||
                                                                                                 (it+1)->start_same_saC>it)));
// if (it->start_same_saC < it->start_same_saC->start_same_saC) { std::cerr << "Now checking transitions " << m_transitions[*it->start_same_saC->ref.BLC_transitions].debug_id_short(*this) << " ... " << m_transitions[*it->start_same_saC->start_same_saC->ref.BLC_transitions].debug_id_short(*this) << '\n'; }
                                                                                        const label_index t_label = label_or_divergence(t);
                                                                                        // The following for loop is only executed if it is the last transition in the saC-slice.
                                                                                        for(outgoing_transitions_const_it itt=it->start_same_saC;
                                                                                                                 itt<it->start_same_saC->start_same_saC; ++itt)
                                                                                        {
                                                                                          const transition& t1=m_aut.get_transitions()[!initialisation
                                                                                                           ? *itt->ref.BLC_transitions : itt->ref.transitions];
// if (t1.from()!=si) { assert(!initialisation); std::cerr << m_transitions[*itt->ref.BLC_transitions].debug_id(*this) << " does not start in state " << si << '\n'; }
                                                                                          assert(m_states.cbegin()+t1.from()==si);
                                                                                          assert(label_or_divergence(t1) == t_label);
                                                                                          assert(m_states[t.to()].block->c.onstellation==
                                                                                                                      m_states[t1.to()].block->c.onstellation);
                                                                                        }
 
                                                                                        const label_index label = label_or_divergence(t);
                                                                                        // Check that if the target constellation, if not new, is equal to the
                                                                                        // target constellation of the previous outgoing transition.
                                                                                        const constellation_type* t_to_constellation=
                                                                                                                        m_states[t.to()].block->c.onstellation;
                                                                                        if (constellations_seen.count(std::pair(label,t_to_constellation))>0)
                                                                                        {
                                                                                          assert(it!=s.start_outgoing_transitions);
                                                                                          const transition& old_t=m_aut.get_transitions()[!initialisation
                                                                                                                          ? *std::prev(it)->ref.BLC_transitions
                                                                                                                          : std::prev(it)->ref.transitions];
                                                                                          assert(label_or_divergence(old_t)==label);
                                                                                          assert(t_to_constellation==
                                                                                                                   m_states[old_t.to()].block->c.onstellation);
                                                                                        }
                                                                                        else
                                                                                        {
                                                                                          if (m_branching && m_aut.is_tau(label))
                                                                                          {
//if (!maybe_tau) { std::cerr << "maybe_tau==false for " << m_transitions[!initialisation ? *it->ref.BLC_transitions : it->ref.transitions].debug_id(*this) << '\n'; }
                                                                                            assert(maybe_tau);
                                                                                          }
                                                                                          else
                                                                                          {
                                                                                            maybe_tau=false;
                                                                                          }
                                                                                          constellations_seen.emplace(label,t_to_constellation);
                                                                                        }
                                                                                      }
                                                                                    }
                                                                                    // Check that the elements in m_transitions are well formed.
                                                                                    if (!initialisation)
                                                                                    {
                                                                                      check_transitions(initialisation, check_temporary_complexity_counters);
                                                                                    }
                                                                                    // Check that the elements in m_blocks are well formed.
                                                                                    {
                                                                                      set_of_transitions_type all_transitions;
                                                                                      transition_index actual_no_of_non_constellation_inert_BLC_sets=0;
                                                                                      for (const state_in_block_pointer* si=m_states_in_blocks.data();
                                                                                        m_states_in_blocks.data_end()!=si; si=si->ref_state->block->end_states)
                                                                                      {
                                                                                        const block_type& b=*si->ref_state->block;
                                                                                        const constellation_type& c=*b.c.onstellation;
                                                                                        assert(m_states_in_blocks.data()<=c.start_const_states);
                                                                                        assert(c.start_const_states<=b.start_bottom_states);
                                                                                        assert(b.start_bottom_states<b.sta.rt_non_bottom_states);
                                                                                        assert(b.sta.rt_non_bottom_states<=b.end_states);
                                                                                        assert(b.end_states<=c.end_const_states);
                                                                                        assert(c.end_const_states<=m_states_in_blocks.data_end());
 
                                                                                        unsigned char const max_B=check_complexity::log_n-
                                                                                                         check_complexity::ilog2(number_of_states_in_block(b));
                                                                                        unsigned char const max_C=check_complexity::log_n-check_complexity::
                                                                                                   ilog2(number_of_states_in_constellation(*b.c.onstellation));
                                                                                        for (const state_in_block_pointer*
                                                                                                is=b.start_bottom_states; is!=b.sta.rt_non_bottom_states; ++is)
                                                                                        {
                                                                                          assert(is->ref_state->block==&b);
                                                                                          assert(is->ref_state->no_of_outgoing_block_inert_transitions==0);
                                                                                          if (check_temporary_complexity_counters)
                                                                                          {
                                                                                            // During initialisation, new bottom state counters must remain 0
                                                                                            mCRL2complexity(is->ref_state, no_temporary_work(max_B,
                                                                                                                                      !initialisation), *this);
                                                                                          }
                                                                                        }
                                                                                        for (const state_in_block_pointer*
                                                                                                         is=b.sta.rt_non_bottom_states; is!=b.end_states; ++is)
                                                                                        {
                                                                                          assert(is->ref_state->block==&b);
                                                                                          assert(is->ref_state->no_of_outgoing_block_inert_transitions>0);
                                                                                          // Because there cannot be new bottom states among non-bottom states,
                                                                                          // we can always check the temporary work of non-bottom states:
                                                                                          mCRL2complexity(is->ref_state,no_temporary_work(max_B,false),*this);
                                                                                        }
                                                                                        // Because a block has no temporary or new-bottom-state-related
                                                                                        // counters, we can always check its temporary work:
                                                                                        mCRL2complexity(&b, no_temporary_work(max_C, max_B), *this);
 
                                                                                        if (!initialisation)
                                                                                        {
                                                                                          assert(b.block.to_constellation.check_linked_list());
                                                                                          for (linked_list<BLC_indicators>::const_iterator
                                                                                                                    ind=b.block.to_constellation.begin();
                                                                                                                    ind!=b.block.to_constellation.end(); ++ind)
                                                                                          {
                                                                                            assert(ind->start_same_BLC<ind->end_same_BLC);
                                                                                            const transition& first_transition=
                                                                                                               m_aut.get_transitions()[*(ind->start_same_BLC)];
                                                                                            const label_index first_transition_label=
                                                                                                                         label_or_divergence(first_transition);
                                                                                            if(!is_inert_during_init(first_transition) ||
                                                                                               m_states[first_transition.from()].block->c.onstellation!=
                                                                                                         m_states[first_transition.to()].block->c.onstellation)
                                                                                            {
                                                                                              ++actual_no_of_non_constellation_inert_BLC_sets;
                                                                                            }
                                                                                            for(BLC_list_const_iterator i=ind->start_same_BLC;
                                                                                                                                      i<ind->end_same_BLC; ++i)
                                                                                            {
                                                                                              const transition& t=m_aut.get_transitions()[*i];
                                                                                              assert(m_transitions[*i].transitions_per_block_to_constellation==
                                                                                                                                                          ind);
                                                                                              all_transitions.emplace(*i);
                                                                                              assert(m_states[t.from()].block==&b);
                                                                                              assert(m_states[t.to()].block->c.onstellation==
                                                                                                        m_states[first_transition.to()].block->c.onstellation);
                                                                                              assert(label_or_divergence(t)==first_transition_label);
                                                                                              if (is_inert_during_init(t) && b.c.onstellation==
                                                                                                                        m_states[t.to()].block->c.onstellation)
                                                                                              {
                                                                                                // The inert transitions should be in the first element of
                                                                                                // `block.to_constellation`:
                                                                                                assert(b.block.to_constellation.begin()==ind);
                                                                                              }
                                                                                            }
                                                                                            if (check_temporary_complexity_counters)
                                                                                            {
                                                                                              mCRL2complexity(ind, no_temporary_work(max_C,
                                                                                                 check_complexity::log_n-check_complexity::ilog2
                                                                                                   (number_of_states_in_constellation(*m_states
                                                                                                      [first_transition.to()].block->c.onstellation))), *this);
                                                                                            }
                                                                                          }
                                                                                        }
                                                                                      }
                                                                                      if (!initialisation) {
                                                                                        assert(all_transitions.size()==m_aut.num_transitions());
                                                                                        assert(actual_no_of_non_constellation_inert_BLC_sets==
                                                                                                                       no_of_non_constellation_inert_BLC_sets);
                                                                                      }
                                                                                      // destruct `all_transitions` here
                                                                                    }
 
                                                                                    // TODO: Check that the elements in m_constellations are well formed.
 
                                                                                    // Check that the states in m_states_in_blocks refer to with ref_states_in_block to the right position.
                                                                                    // and that a state is correctly designated as a (non-)bottom state.
                                                                                    for (const state_in_block_pointer*
                                                                                          si=m_states_in_blocks.data(); si<m_states_in_blocks.data_end(); ++si)
                                                                                    {
                                                                                      assert(si==si->ref_state->ref_states_in_blocks);
                                                                                    }
 
                                                                                    // Check that the blocks in m_blocks_with_new_bottom_states are bottom states.
                                                                                    for(const block_type* bi: m_blocks_with_new_bottom_states)
                                                                                    {
                                                                                      assert(bi->contains_new_bottom_states);
                                                                                    }
 
                                                                                    // Check that the non-trivial constellations are non trivial.
                                                                                    for(const constellation_type* ci: m_non_trivial_constellations)
                                                                                    {
                                                                                      // There are at least two blocks in a non-trivial constellation.
                                                                                      const block_type* const first_bi=ci->start_const_states->ref_state->block;
                                                                                      const block_type* const last_bi=std::prev(ci->end_const_states)->ref_state->block;
                                                                                      assert(first_bi != last_bi);
                                                                                    }
                                                                                    return true;
                                                                                  }
 
                                                                                  [[nodiscard]]
                                                                                  bool check_stability(const std::string& tag,
                                                                                        const std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> >*
                                                                                                                                                calM=nullptr,
                                                                                        const std::pair<BLC_list_iterator,BLC_list_iterator>* calM_elt=nullptr,
                                                                                        const constellation_type* const old_constellation=null_constellation,
                                                                                        const constellation_type* const new_constellation=null_constellation)
                                                                                                                                                          const
                                                                                  {
                                                                                    assert((old_constellation==null_constellation &&
                                                                                            new_constellation==null_constellation   ) ||
                                                                                           (old_constellation!=null_constellation &&
                                                                                            new_constellation!=null_constellation &&
                                                                                            old_constellation!=new_constellation    ));
                                                                                    mCRL2log(log::debug) << "Check stability: " << tag << ".\n";
                                                                                    for (const state_in_block_pointer* si=m_states_in_blocks.data();
                                                                                        m_states_in_blocks.data_end()!=si; si=si->ref_state->block->end_states)
                                                                                    {
                                                                                      const block_type& b=*si->ref_state->block;
                                                                                      bool previous_stable=true;
                                                                                      for (linked_list<BLC_indicators>::const_iterator
                                                                                                   ind=b.block.to_constellation.begin();
                                                                                                   ind!=b.block.to_constellation.end(); ++ind)
                                                                                      {
                                                                                        set_of_states_type all_source_bottom_states;
 
                                                                                        assert(ind->start_same_BLC<ind->end_same_BLC);
                                                                                        const transition&first_t=m_aut.get_transitions()[*ind->start_same_BLC];
                                                                                        const label_index first_t_label=label_or_divergence(first_t);
                                                                                        const bool all_transitions_in_BLC_are_inert =
                                                                                                   is_inert_during_init(first_t) && b.c.onstellation==
                                                                                                                  m_states[first_t.to()].block->c.onstellation;
                                                                                        assert(!all_transitions_in_BLC_are_inert ||
                                                                                               b.block.to_constellation.begin()==ind);
                                                                                        for (BLC_list_const_iterator i=ind->start_same_BLC;
                                                                                                                                      i<ind->end_same_BLC; ++i)
                                                                                        {
                                                                                          assert(m_BLC_transitions.data()<=i);
                                                                                          assert(i<m_BLC_transitions.data_end());
                                                                                          const transition& t=m_aut.get_transitions()[*i];
// if (m_states[t.from()].block != bi) { std::cerr << m_transitions[*ind->start_same_BLC].debug_id(*this) << " should start in block " << bi << '\n'; }
                                                                                          assert(m_states[t.from()].block == &b);
                                                                                          assert(label_or_divergence(t) == first_t_label);
                                                                                          assert(m_states[t.to()].block->c.onstellation==
                                                                                                                 m_states[first_t.to()].block->c.onstellation);
                                                                                          if (is_inert_during_init(t) && b.c.onstellation==
                                                                                                                        m_states[t.to()].block->c.onstellation)
                                                                                          {
                                                                                            assert(all_transitions_in_BLC_are_inert);
                                                                                          }
                                                                                          else
                                                                                          {
                                                                                            // This is a constellation-non-inert transition.
                                                                                            assert(!all_transitions_in_BLC_are_inert);
                                                                                            if (0 == m_states[t.from()].no_of_outgoing_block_inert_transitions)
                                                                                            {
                                                                                              assert(b.start_bottom_states<=
                                                                                                                      m_states[t.from()].ref_states_in_blocks);
                                                                                              assert(m_states[t.from()].ref_states_in_blocks<
                                                                                                                                   b.sta.rt_non_bottom_states);
                                                                                              all_source_bottom_states.emplace(t.from());
                                                                                            }
                                                                                            else
                                                                                            {
                                                                                              assert(b.sta.rt_non_bottom_states<=
                                                                                                                      m_states[t.from()].ref_states_in_blocks);
                                                                                              assert(m_states[t.from()].ref_states_in_blocks < b.end_states);
                                                                                            }
                                                                                          }
                                                                                        }
                                                                                        assert(all_source_bottom_states.size()<=static_cast<std::size_t>
                                                                                           (std::distance(b.start_bottom_states, b.sta.rt_non_bottom_states)));
                                                                                        // check that every bottom state has a transition in this BLC entry:
                                                                                        bool eventual_instability_is_ok = true;
                                                                                        bool eventual_marking_is_ok = true;
                                                                                        if (!all_transitions_in_BLC_are_inert &&
                                                                                            all_source_bottom_states.size()!=static_cast<std::size_t>
                                                                                            (std::distance(b.start_bottom_states, b.sta.rt_non_bottom_states)))
                                                                                        {
                                                                                          // only splitters should be instable.
                                                                                          mCRL2log(log::debug) << "Not all "
                                                                                            << std::distance(b.start_bottom_states, b.sta.rt_non_bottom_states)
                                                                                              << (m_branching ? " bottom states have a transition in the "
                                                                                                              : " states have a transition in the ")
                                                                                              << ind->debug_id(*this) << ": transitions found from states";
                                                                                          for (set_of_states_type::iterator
                                                                                                           asbc_it=all_source_bottom_states.begin();
                                                                                                           asbc_it!=all_source_bottom_states.end() ; ++asbc_it)
                                                                                          { mCRL2log(log::debug) << ' ' << *asbc_it; }
                                                                                          mCRL2log(log::debug) << '\n';
                                                                                          eventual_instability_is_ok = false;
                                                                                        }
                                                                                        if (!ind->is_stable())
                                                                                        {
                                                                                          // only splitters should contain marked transitions.
                                                                                          mCRL2log(log::debug) << ind->debug_id(*this) << " contains " << std::distance(ind->start_marked_BLC, ind->end_same_BLC) << " marked transitions.\n";
                                                                                          eventual_marking_is_ok = false;
                                                                                        }
                                                                                        if (b.contains_new_bottom_states)
                                                                                        {
                                                                                          /* I would like the following to check more closely because in a
                                                                                             block with new bottom states, one should have...
                                                                                          if (!eventual_marking_is_ok)
                                                                                          {
                                                                                            eventual_marking_is_ok = true;
                                                                                            for (BLC_list_const_iterator i=ind->start_marked_BLC; i<ind->end_same_BLC; ++i)
                                                                                            {
                                                                                              const state_index from = m_aut.get_transitions()[*i].from();
                                                                                              // assert(m_states[from].block == bi); -- already checked earlier
                                                                                              if (0 != m_states[from].no_of_outgoing_block_inert_transitions)
                                                                                              {
                                                                                                // the state is a non-bottom state
                                                                                                eventual_marking_is_ok = false;
                                                                                                break;
                                                                                              }
                                                                                            }
                                                                                            if (eventual_marking_is_ok)
                                                                                            {
                                                                                              mCRL2log(log::debug) << "  This is ok because all marked transitions begin in new bottom states of " << bi->debug_id(*this) << ".\n";
                                                                                              eventual_instability_is_ok = true;
                                                                                            }
                                                                                          } */
                                                                                          if (!(eventual_instability_is_ok && eventual_marking_is_ok))
                                                                                          {
                                                                                            mCRL2log(log::debug) << "  This is ok because " << b.debug_id(*this) << " contains new bottom states.\n";
                                                                                            eventual_instability_is_ok = true;
                                                                                            eventual_marking_is_ok = true;
                                                                                          }
                                                                                        }
                                                                                        if (!(eventual_instability_is_ok && eventual_marking_is_ok) && nullptr != calM && calM->begin() != calM->end())
                                                                                        {
                                                                                          std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> >::const_iterator calM_iter = calM->begin();
                                                                                          if (nullptr != calM_elt)
                                                                                          {
                                                                                            for(;;)
                                                                                            {
                                                                                              assert(calM->end() != calM_iter);
                                                                                              if (calM_iter->first <= calM_elt->first && calM_elt->second <= calM_iter->second)
                                                                                              {
                                                                                                break;
                                                                                              }
                                                                                              ++calM_iter;
                                                                                            }
                                                                                            if (calM_elt->first<=ind->start_same_BLC && ind->end_same_BLC<=calM_elt->second)
                                                                                            {
                                                                                              mCRL2log(log::debug) <<"  This is ok because the BLC set ("
                                                                                                  << b.debug_id(*this) << " -" << m_aut.action_label(first_t.label())
                                                                                                  << "-> " << m_states[first_t.to()].
                                                                                                                         block->c.onstellation->debug_id(*this)
                                                                                                  << ") is soon going to be a main splitter.\n";
                                                                                              eventual_instability_is_ok = true;
                                                                                              eventual_marking_is_ok = true;
                                                                                            }
                                                                                            else
                                                                                            {
                                                                                              if (old_constellation==
                                                                                                                  m_states[first_t.to()].block->c.onstellation)
                                                                                              {
                                                                                                const linked_list<BLC_indicators>::const_iterator main_splitter=b.block.to_constellation.next(ind);
                                                                                                if (main_splitter!=b.block.to_constellation.end())
                                                                                                {
                                                                                                  assert(main_splitter->start_same_BLC < main_splitter->end_same_BLC);
                                                                                                  const transition& main_t = m_aut.get_transitions()[*main_splitter->start_same_BLC];
                                                                                                  assert(m_states[main_t.from()].block == &b);
                                                                                                  if(label_or_divergence(first_t)==label_or_divergence(main_t)
                                                                                                     && m_states[main_t.to()].block->c.onstellation==
                                                                                                                                             new_constellation)
                                                                                                  {
//std::cerr << "Corresponding main splitter: " << main_splitter->debug_id(*this) << '\n';
                                                                                                    if (calM_elt->first<=main_splitter->start_same_BLC && main_splitter->end_same_BLC<=calM_elt->second)
                                                                                                    {
                                                                                                      assert(new_constellation==
                                                                                                                  m_states[main_t.to()].block->c.onstellation);
                                                                                                      mCRL2log(log::debug) << "  This is ok because the BLC set (" << b.debug_id(*this) << " -" << m_aut.action_label(first_t.label()) << "-> " << old_constellation->debug_id(*this) << ") is soon going to be a co-splitter.\n";
                                                                                                      eventual_instability_is_ok = true;
                                                                                                      eventual_marking_is_ok = true;
                                                                                                    }
//else { std::cerr << "Main splitter is not in calM_elt = [" << std::distance(m_BLC_transitions.begin(), calM_elt->first) << ',' << std::distance(m_BLC_transitions.begin(), calM_elt->second) << ")\n" };
                                                                                                  }
                                                                                                }
                                                                                              }
                                                                                            }
                                                                                            ++calM_iter;
                                                                                          }
                                                                                          for(; !(eventual_instability_is_ok && eventual_marking_is_ok) && calM->end() != calM_iter; ++calM_iter)
                                                                                          {
                                                                                            if (calM_iter->first<=ind->start_same_BLC && ind->end_same_BLC<=calM_iter->second)
                                                                                            {
                                                                                              mCRL2log(log::debug) <<"  This is ok because the BLC set ("
                                                                                                  << b.debug_id(*this) << " -" << m_aut.action_label(first_t.label())
                                                                                                  << "-> "
                                                                                                  << m_states[first_t.to()].block->c.onstellation->debug_id(*this)
                                                                                                  << ") is going to be a main splitter later.\n";
                                                                                              eventual_instability_is_ok = true;
                                                                                              eventual_marking_is_ok = true;
                                                                                            }
                                                                                            else
                                                                                            {
                                                                                              if (old_constellation==
                                                                                                                  m_states[first_t.to()].block->c.onstellation)
                                                                                              {
                                                                                                const linked_list<BLC_indicators>::const_iterator main_splitter=b.block.to_constellation.next(ind);
                                                                                                if (main_splitter != b.block.to_constellation.end())
                                                                                                {
                                                                                                  assert(main_splitter->start_same_BLC < main_splitter->end_same_BLC);
                                                                                                  const transition& main_t = m_aut.get_transitions()[*main_splitter->start_same_BLC];
                                                                                                  assert(m_states[main_t.from()].block == &b);
                                                                                                  if(label_or_divergence(first_t)==label_or_divergence(main_t)
                                                                                                     && m_states[main_t.to()].block->c.onstellation==
                                                                                                                                             new_constellation)
                                                                                                  {
                                                                                                    if (calM_iter->first<=main_splitter->start_same_BLC && main_splitter->end_same_BLC<=calM_iter->second)
                                                                                                    {
                                                                                                      assert(new_constellation==
                                                                                                                  m_states[main_t.to()].block->c.onstellation);
                                                                                                      mCRL2log(log::debug) << "  This is ok because the BLC "
                                                                                                          "set (" << b.debug_id(*this) << " -"
                                                                                                          << m_aut.action_label(first_t.label())
                                                                                                          << "-> " << old_constellation->debug_id(*this)
                                                                                                          << ") is going to be a co-splitter later.\n";
                                                                                                      eventual_instability_is_ok = true;
                                                                                                      eventual_marking_is_ok = true;
                                                                                                    }
//else { std::cerr << "Main splitter is not in calM_iter = [" << std::distance(m_BLC_transitions.begin(), calM_iter->first) << ',' << std::distance(m_BLC_transitions.begin(), calM_iter->second) << ")\n" };
                                                                                                  }
                                                                                                }
                                                                                              }
                                                                                            }
                                                                                          }
                                                                                        }
                                                                                        if (1>=number_of_states_in_block(b))
                                                                                        {
                                                                                          if (!eventual_marking_is_ok)
                                                                                          {
                                                                                            mCRL2log(log::debug) << "  (This is ok because the source block contains only 1 state.)\n";
                                                                                            eventual_marking_is_ok = true;
                                                                                          }
                                                                                        }
                                                                                        else if (1<no_of_constellations /* i.e. !initialisation */ &&
                                                                                                   !b.contains_new_bottom_states)
                                                                                        {
                                                                                          assert(eventual_marking_is_ok);
                                                                                          assert(eventual_instability_is_ok);
                                                                                          if (null_constellation==old_constellation && ind->is_stable()) {
                                                                                            assert(previous_stable);
                                                                                          }
                                                                                          else
                                                                                          {
                                                                                            previous_stable=false;
                                                                                          }
                                                                                        }
                                                                                      }
                                                                                    }
                                                                                    mCRL2log(log::debug) << "Check stability finished: " << tag << ".\n";
                                                                                    return true;
                                                                                  }
 
                                                                                  void display_BLC_list(const block_type* const bi) const
                                                                                  {
                                                                                    mCRL2log(log::debug) << "\n  BLC_List\n";
                                                                                    for(const BLC_indicators& blc_it: bi->block.to_constellation)
                                                                                    {
                                                                                      const transition& first_t=m_aut.get_transitions()[*blc_it.start_same_BLC];
                                                                                      const label_index l=label_or_divergence(first_t, null_action);
                                                                                      mCRL2log(log::debug) << "\n    BLC set "
                                                                                          << std::distance<BLC_list_const_iterator>(m_BLC_transitions.data(),
                                                                                                                               blc_it.start_same_BLC) << " -- "
                                                                                          << std::distance<BLC_list_const_iterator>(m_BLC_transitions.data(),
                                                                                                                                  blc_it.end_same_BLC)
                                                                                          << " of " << (null_action==l ? "divergent self-loop " : pp(m_aut.action_label(l))+"-")
                                                                                          << "transitions to " << m_states[first_t.to()].block->c.onstellation->debug_id(*this) << ":\n";
                                                                                      for (BLC_list_const_iterator i=blc_it.start_same_BLC; ; ++i)
                                                                                      {
                                                                                        if (i == blc_it.start_marked_BLC)
                                                                                        {
                                                                                          mCRL2log(log::debug) << "        (The BLC set is unstable, and the "
                                                                                                                       " following transitions are marked.)\n";
                                                                                        }
                                                                                        if (i>=blc_it.end_same_BLC)
                                                                                        {
                                                                                          break;
                                                                                        }
                                                                                        const transition& t=m_aut.get_transitions()[*i];
                                                                                        mCRL2log(log::debug) << "        " << t.from() << " -"
                                                                                                           << m_aut.action_label(t.label()) << "-> " << t.to();
                                                                                        if (is_inert_during_init(t) &&
                                                                                            m_states[t.from()].block==m_states[t.to()].block)
                                                                                        {
                                                                                          mCRL2log(log::debug) << " (block-inert)";
                                                                                        }
                                                                                        else if (is_inert_during_init(t) &&
                                                                                                 m_states[t.from()].block->c.onstellation==
                                                                                                                        m_states[t.to()].block->c.onstellation)
                                                                                        {
                                                                                          mCRL2log(log::debug) << " (constellation-inert)";
                                                                                        }
                                                                                        mCRL2log(log::debug) << '\n';
                                                                                      }
                                                                                    }
                                                                                    mCRL2log(log::debug) << "  BLC_List end\n";
                                                                                  }
 
                                                                                  void print_data_structures(const std::string& header,
                                                                                                             const bool initialisation=false) const
                                                                                  {
                                                                                    if (!mCRL2logEnabled(log::debug))  {  return;  }
                                                                                    mCRL2log(log::debug) << "========= PRINT DATASTRUCTURE: " << header << " =======================================\n"
                                                                                                            "++++++++++++++++++++    States    ++++++++++++++++++++++++++++\n";
                                                                                    for(state_index si=0; si<m_aut.num_states(); ++si)
                                                                                    {
                                                                                      mCRL2log(log::debug) << "State " << si <<" (" << m_states[si].block->debug_id(*this) << "):\n"
                                                                                                              "  #Inert outgoing transitions: " << m_states[si].no_of_outgoing_block_inert_transitions << "\n"
 
                                                                                                              "  Incoming transitions:\n";
                                                                                      std::vector<transition>::const_iterator end=(si+1==m_aut.num_states()?m_aut.get_transitions().end():m_states[si+1].start_incoming_transitions);
                                                                                      for(std::vector<transition>::const_iterator it=m_states[si].start_incoming_transitions; it!=end; ++it)
                                                                                      {
                                                                                         mCRL2log(log::debug) << "    " << ptr(*it) << "\n";
                                                                                      }
 
                                                                                      mCRL2log(log::debug) << "  Outgoing transitions:\n";
                                                                                      label_index t_label=m_aut.tau_label_index();
                                                                                      const constellation_type* to_constln=null_constellation;
                                                                                      for(outgoing_transitions_const_it it=m_states[si].start_outgoing_transitions;
                                                                                                      it!=m_outgoing_transitions.end() &&
                                                                                                      (si+1>=m_aut.num_states() || it!=m_states[si+1].start_outgoing_transitions);
                                                                                                   ++it)
                                                                                      {
                                                                                        const transition& t=m_aut.get_transitions()[!initialisation
                                                                                                             ? *it->ref.BLC_transitions : it->ref.transitions];
                                                                                        bool start_same_saC_valid=
                                                                                            m_outgoing_transitions.cbegin()<=it->start_same_saC &&
                                                                                            it->start_same_saC<m_outgoing_transitions.end();
                                                                                        if (start_same_saC_valid &&
                                                                                            it->start_same_saC->start_same_saC==it &&
                                                                                            it->start_same_saC >= it)
                                                                                        {
                                                                                          // it is at the beginning of a saC slice
                                                                                          const label_index old_t_label=t_label;
                                                                                          t_label=label_or_divergence(t, null_action);
                                                                                          to_constln=m_states[t.to()].block->c.onstellation;
                                                                                          mCRL2log(log::debug) << "    -  -  -  - saC slice of "
                                                                                                << (null_action==t_label ? "divergent self-loop " : pp(m_aut.action_label(t_label))+"-")
                                                                                                << "transitions to " << to_constln->debug_id(*this)
                                                                                                << (m_aut.is_tau(t_label) && !m_aut.is_tau(old_t_label)
                                                                                                        ? " -- error: tau-transitions should come first\n"
                                                                                                        : ":\n");
                                                                                        }
                                                                                        mCRL2log(log::debug) << "    " << ptr(t);
                                                                                        if (start_same_saC_valid)
                                                                                        {
                                                                                          if (label_or_divergence(t, null_action)!=t_label)
                                                                                          {
                                                                                            mCRL2log(log::debug) << " -- error: different label";
                                                                                          }
                                                                                          if (!initialisation && m_states[t.to()].block->c.onstellation!=to_constln)
                                                                                          {
                                                                                            mCRL2log(log::debug) << " -- error: different target " << m_states[t.to()].block->c.onstellation->debug_id(*this);
                                                                                          }
                                                                                          if (it->start_same_saC->start_same_saC == it)
                                                                                          {
                                                                                            // Transition t must be the beginning and/or the end of a saC-slice
                                                                                            if (it->start_same_saC >= it && it > m_outgoing_transitions.cbegin())
                                                                                            {
                                                                                              // Transition t must be the beginning of a saC-slice
                                                                                              const transition& prev_t=m_aut.get_transitions()[
                                                                                                        !initialisation ? *std::prev(it)->ref.BLC_transitions
                                                                                                                            : std::prev(it)->ref.transitions];
                                                                                              if (prev_t.from()==t.from() &&
                                                                                                  label_or_divergence(prev_t)==t_label &&
                                                                                                  (initialisation ||
                                                                                                   m_states[prev_t.to()].block->c.onstellation==
                                                                                                                       m_states[t.to()].block->c.onstellation))
                                                                                              {
                                                                                                mCRL2log(log::debug) << " -- error: not the beginning of a saC-slice";
                                                                                              }
                                                                                            }
                                                                                            if (it->start_same_saC <= it && std::next(it) < m_outgoing_transitions.end())
                                                                                            {
                                                                                              // Transition t must be the end of a saC-slice
                                                                                              const transition& next_t=m_aut.get_transitions()[
                                                                                                        !initialisation ? *std::next(it)->ref.BLC_transitions
                                                                                                                            : std::next(it)->ref.transitions];
                                                                                              if (next_t.from()==t.from() &&
                                                                                                  label_or_divergence(next_t)==t_label &&
                                                                                                  (initialisation ||
                                                                                                   m_states[next_t.to()].block->c.onstellation==
                                                                                                                       m_states[t.to()].block->c.onstellation))
                                                                                              {
                                                                                                mCRL2log(log::debug) << " -- error: not the end of a saC-slice";
                                                                                              }
                                                                                            }
                                                                                          }
                                                                                          else if (it->start_same_saC > it ? it->start_same_saC->start_same_saC > it : it->start_same_saC->start_same_saC < it)
                                                                                          {
                                                                                            mCRL2log(log::debug) << " -- error: not pointing to its own saC-slice";
                                                                                          }
                                                                                        }
                                                                                        mCRL2log(log::debug) << '\n';
                                                                                      }
                                                                                      mCRL2log(log::debug) << "  Ref states in blocks: " << std::distance<fixed_vector<state_type_gj>::const_iterator>(m_states.cbegin(), m_states[si].ref_states_in_blocks->ref_state) << ". Must be " << si <<".\n";
                                                                                      mCRL2log(log::debug) << "---------------------------------------------------\n";
                                                                                    }
                                                                                    mCRL2log(log::debug) << "++++++++++++++++++++ Transitions ++++++++++++++++++++++++++++\n";
                                                                                    for(transition_index ti=0; ti<m_aut.num_transitions(); ++ti)
                                                                                    {
                                                                                      const transition& t=m_aut.get_transitions()[ti];
                                                                                      mCRL2log(log::debug) << "Transition " << ti <<": " << t.from()
                                                                                                                            << " -" << m_aut.action_label(t.label()) << "-> "
                                                                                                                            << t.to() << "\n";
                                                                                    }
 
                                                                                    mCRL2log(log::debug) << "++++++++++++++++++++ Blocks ++++++++++++++++++++++++++++\n";
                                                                                    for (const state_in_block_pointer* si=m_states_in_blocks.data();
                                                                                        m_states_in_blocks.data_end()!=si; si=si->ref_state->block->end_states)
                                                                                    {
                                                                                      block_type* const bi=si->ref_state->block;
                                                                                      mCRL2log(log::debug) << "  Block " << bi;
                                                                                      if (!initialisation) {
                                                                                        mCRL2log(log::debug) << " (" << bi->c.onstellation->debug_id(*this) << ')';
                                                                                      }
                                                                                      mCRL2log(log::debug) << ":\n  " << std::distance(bi->start_bottom_states,
                                                                                                                       bi->sta.rt_non_bottom_states)
                                                                                          << (m_branching ? " Bottom state" : " State")
                                                                                          << (1==std::distance(bi->start_bottom_states,
                                                                                                               bi->sta.rt_non_bottom_states) ? ": " : "s: ");
                                                                                      for (const state_in_block_pointer*
                                                                                         sit=bi->start_bottom_states; sit!=bi->sta.rt_non_bottom_states; ++sit)
                                                                                      {
                                                                                        mCRL2log(log::debug) << sit->ref_state->debug_id_short(*this) << "  ";
                                                                                      }
                                                                                      if (m_branching)
                                                                                      {
                                                                                        mCRL2log(log::debug) << "\n  " << std::distance
                                                                                                                 (bi->sta.rt_non_bottom_states, bi->end_states)
                                                                                            << " Non-bottom state" << (1==std::distance
                                                                                                                 (bi->sta.rt_non_bottom_states, bi->end_states)
                                                                                                                  ? ": " : "s: ");
                                                                                        for (const state_in_block_pointer*
                                                                                                  sit=bi->sta.rt_non_bottom_states; sit!=bi->end_states; ++sit)
                                                                                        {
                                                                                          mCRL2log(log::debug) << sit->ref_state->debug_id_short(*this) << "  ";
                                                                                        }
                                                                                      }
                                                                                      else
                                                                                      {
                                                                                        assert(bi->sta.rt_non_bottom_states==bi->end_states);
                                                                                      }
                                                                                      if (!initialisation)
                                                                                      {
                                                                                        display_BLC_list(bi);
                                                                                      }
                                                                                      mCRL2log(log::debug) << "\n";
                                                                                    }
 
                                                                                    mCRL2log(log::debug) << "++++++++++++++++++++ Constellations ++++++++++++++++++++++++++++\n";
                                                                                    for (const state_in_block_pointer* si=m_states_in_blocks.data();
                                                                                                     m_states_in_blocks.data_end()!=si;
                                                                                                     si=si->ref_state->block->c.onstellation->end_const_states)
                                                                                    {
                                                                                      const constellation_type* const ci=si->ref_state->block->c.onstellation;
                                                                                      mCRL2log(log::debug) << "  " << ci->debug_id(*this) << ":\n";
                                                                                      mCRL2log(log::debug) << "    Blocks in constellation:";
                                                                                      for (const state_in_block_pointer*
                                                                                                            constln_it=ci->start_const_states;
                                                                                                            constln_it<ci->end_const_states; )
                                                                                      {
                                                                                        const block_type* const bi=constln_it->ref_state->block;
                                                                                        mCRL2log(log::debug) << " " << bi->debug_id(*this);
                                                                                        constln_it = bi->end_states;
                                                                                      }
                                                                                      mCRL2log(log::debug) << "\n";
                                                                                    }
                                                                                    mCRL2log(log::debug) << "Non-trivial constellations:";
                                                                                    for (const constellation_type* ci: m_non_trivial_constellations)
                                                                                    {
                                                                                      mCRL2log(log::debug) << " " << ci->debug_id(*this);
                                                                                    }
 
                                                                                    mCRL2log(log::debug) <<
                                                                                         "\n++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++\n"
                                                                                         "Outgoing transitions:\n";
 
                                                                                    for (outgoing_transitions_const_it pi = m_outgoing_transitions.cbegin();
                                                                                                                       pi < m_outgoing_transitions.cend(); ++pi)
                                                                                    {
                                                                                      const transition& t=m_aut.get_transitions()[!initialisation
                                                                                                             ? *pi->ref.BLC_transitions : pi->ref.transitions];
                                                                                      mCRL2log(log::debug) << "  " << t.from() << " -"
                                                                                                           << m_aut.action_label(t.label()) << "-> " << t.to();
                                                                                      if (m_outgoing_transitions.cbegin()<=pi->start_same_saC &&
                                                                                          pi->start_same_saC<m_outgoing_transitions.end())
                                                                                      {
                                                                                        const transition& t1=m_aut.get_transitions()[!initialisation
                                                                                                                     ? *pi->start_same_saC->ref.BLC_transitions
                                                                                                                     : pi->start_same_saC->ref.transitions];
                                                                                        mCRL2log(log::debug) << "  \t(same saC: " << t1.from() << " -" << m_aut.action_label(t1.label()) << "-> " << t1.to();
                                                                                        const label_index t_label = label_or_divergence(t);
                                                                                        if (pi->start_same_saC->start_same_saC == pi)
                                                                                        {
                                                                                          // Transition t must be the beginning and/or the end of a saC-slice
                                                                                          if (pi->start_same_saC >= pi && pi > m_outgoing_transitions.cbegin())
                                                                                          {
                                                                                            // Transition t must be the beginning of a saC-slice
                                                                                            const transition& prev_t=m_aut.get_transitions()[
                                                                                                      !initialisation ? *std::prev(pi)->ref.BLC_transitions
                                                                                                                          : std::prev(pi)->ref.transitions];
                                                                                            if (prev_t.from()==t.from() &&
                                                                                                label_or_divergence(prev_t)==t_label &&
                                                                                                (initialisation ||
                                                                                                 m_states[prev_t.to()].block->c.onstellation==
                                                                                                                       m_states[t.to()].block->c.onstellation))
                                                                                            {
                                                                                              mCRL2log(log::debug) << " -- error: not the beginning of a saC-slice";
                                                                                            }
                                                                                          }
                                                                                          if (pi->start_same_saC <= pi && std::next(pi) < m_outgoing_transitions.end())
                                                                                          {
                                                                                            // Transition t must be the end of a saC-slice
                                                                                            const transition& next_t=m_aut.get_transitions()[
                                                                                                      !initialisation ? *std::next(pi)->ref.BLC_transitions
                                                                                                                          : std::next(pi)->ref.transitions];
                                                                                            if (next_t.from()==t.from() &&
                                                                                                label_or_divergence(next_t)==t_label &&
                                                                                                (initialisation ||
                                                                                                 m_states[next_t.to()].block->c.onstellation==
                                                                                                                       m_states[t.to()].block->c.onstellation))
                                                                                            {
                                                                                              mCRL2log(log::debug) << " -- error: not the end of a saC-slice";
                                                                                            }
                                                                                          }
                                                                                        }
                                                                                        else if (pi->start_same_saC > pi ? pi->start_same_saC->start_same_saC > pi : pi->start_same_saC->start_same_saC < pi)
                                                                                        {
                                                                                          mCRL2log(log::debug) << " -- error: not in its own saC-slice";
                                                                                        }
                                                                                        mCRL2log(log::debug) << ')';
                                                                                      }
                                                                                      mCRL2log(log::debug) << '\n';
                                                                                    }
                                                                                    mCRL2log(log::debug) << "++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++\n"
                                                                                                            "New bottom blocks to be investigated:";
 
                                                                                    for(const block_type* bi: m_blocks_with_new_bottom_states)
                                                                                    {
                                                                                      mCRL2log(log::debug) << "  " << bi->debug_id(*this) << '\n';
                                                                                    }
 
                                                                                    mCRL2log(log::debug) << "\n========= END PRINT DATASTRUCTURE: " << header << " =======================================\n";
                                                                                  }
                                                                                #endif // ifndef NDEBUG
  public:
    std::size_t num_eq_classes() const
    {
      return no_of_blocks;
    }
 
 
    state_index get_eq_class(const state_index si) const
    {                                                                           assert(si<m_states.size());
      return m_states[si].block->sta.te_in_reduced_LTS;
    }
 
 
    void finalize_minimized_LTS()
    {
      // Assign numbers to the blocks (i.e. to the states of the reduced LTS)
      // One could devise a fancy scheme where the block containing state i
      // tries to get block number i; but let's just do something simple now.
      // We no longer need sta.rt_non_bottom_states at this moment, so we can
      // reuse that field to store the block number:
      state_index block_number=0;
      for (state_in_block_pointer*
            si=m_states_in_blocks.data(); m_states_in_blocks.data_end()!=si;
                                           si=si->ref_state->block->end_states)
      {
        block_type* const bi=si->ref_state->block;
        // destruct bi->sta.rt_non_bottom_states; -- trivial
        new (&bi->sta.te_in_reduced_LTS) state_index(block_number);
        ++block_number;
      }
 
      // The transitions are most efficiently directly extracted from the
      // block.to_constellation lists in blocks.
      typename std::remove_reference<decltype(m_aut.get_transitions())>::type
                                                                             T;
      for (state_in_block_pointer*
            si=m_states_in_blocks.data(); m_states_in_blocks.data_end()!=si;
                                           si=si->ref_state->block->end_states)
      {
        const block_type& B=*si->ref_state->block;                              //mCRL2complexity(&B, add_work(..., 1), *this);
                                                                                    // Because every block is touched exactly once, we do not store a
                                                                                    // physical counter for this.
        for(const BLC_indicators blc_ind: B.block.to_constellation)
        {                                                                       // mCRL2complexity(&blc_ind, add_work(..., 1), *this);
                                                                                    // Because every BLC set is touched exactly once, we do not store
                                                                                    // a physical counter for this.
                                                                                assert(blc_ind.start_same_BLC<blc_ind.end_same_BLC);
          const transition& t=m_aut.get_transitions()[*blc_ind.start_same_BLC];
          const state_index new_to=get_eq_class(t.to());
          if (!is_inert_during_init(t) || B.sta.te_in_reduced_LTS!=new_to)
          {
            T.emplace_back(B.sta.te_in_reduced_LTS, t.label(), new_to);
          }
        }
      }
      m_aut.clear_transitions();
      T.swap(m_aut.get_transitions());
      //
      // Merge the states, by setting the state labels of each state to the
      // concatenation of the state labels of its equivalence class.
 
      if (m_aut.has_state_info())   // If there are no state labels
      {                             // this step is not needed
        /* Create a vector for the new labels */
        typename std::remove_reference<decltype(m_aut.state_labels())>::type
                                                  new_labels(num_eq_classes());
 
        for(std::size_t i=0; i<m_aut.num_states(); ++i)
        {                                                                       //mCRL2complexity(&m_states[i], add_work(..., 1), *this);
                                                                                    // Because every state is touched exactly once, we do not store a
                                                                                    // physical counter for this.
          const state_index new_index(get_eq_class(i));
          new_labels[new_index]=new_labels[new_index]+m_aut.state_label(i);
        }
 
        m_aut.set_num_states(num_eq_classes(), false);                          assert(0==m_aut.num_state_labels());
        //m_aut.clear_state_labels();
        new_labels.swap(m_aut.state_labels());
      }
      else
      {
        m_aut.set_num_states(num_eq_classes(), false);
      }
 
      m_aut.set_initial_state(get_eq_class(m_aut.initial_state()));
    }
 
 
    bool in_same_class(state_index const s, state_index const t) const
    {
      return get_eq_class(s) == get_eq_class(t);
    }
  private:
                                                                                #ifndef NDEBUG
                                                                                  std::string ptr(const transition& t) const
                                                                                  {
                                                                                    return std::to_string(t.from())+" -"+pp(m_aut.action_label(t.label()))+
                                                                                                                                "-> "+std::to_string(t.to());
                                                                                  }
                                                                                #endif
    /*--------------------------- main algorithm ----------------------------*/
 
    /*----------------- splitB -- Algorithm 3 of [GJ 2024] -----------------*/
 
    state_index number_of_states_in_block(const block_type& B) const
    {                                                                           assert(B.start_bottom_states<B.end_states);
      return std::distance(B.start_bottom_states, B.end_states);
    }
 
    state_index number_of_states_in_constellation(const constellation_type& C)
                                                                          const
    {                                                                           assert(C.start_const_states<C.end_const_states);
      return std::distance(C.start_const_states, C.end_const_states);
    }
 
    void swap_states_in_states_in_block_never_equal(
                    state_in_block_pointer* pos1, state_in_block_pointer* pos2)
    {                                                                           assert(m_states_in_blocks.data()<=pos1);
      std::swap(*pos1,*pos2);                                                   assert(pos1<m_states_in_blocks.data_end());
      pos1->ref_state->ref_states_in_blocks=pos1;                               assert(m_states_in_blocks.data()<=pos2);
      pos2->ref_state->ref_states_in_blocks=pos2;                               assert(pos2<m_states_in_blocks.data_end());  assert(pos1!=pos2);
    }
 
    void swap_states_in_states_in_block(
                    state_in_block_pointer* pos1, state_in_block_pointer* pos2)
    {
      if (pos1!=pos2)
      {
        swap_states_in_states_in_block_never_equal(pos1, pos2);
      }
    }
 
    void swap_states_in_states_in_block_23_never_equal(
              state_in_block_pointer* pos1,
              state_in_block_pointer* pos2,
              state_in_block_pointer* pos3)
    {                                                                           assert(m_states_in_blocks.data()<=pos2);   assert(pos2<pos3);
                                                                                assert(pos1<m_states_in_blocks.data_end());
      if (pos1==pos3)
      {
        std::swap(*pos1,*pos2);
      }
      else
      {                                                                         assert(pos3<pos1);
        const state_in_block_pointer temp=*pos1;
        *pos1=*pos3;
        *pos3=*pos2;
        *pos2=temp;
 
        pos3->ref_state->ref_states_in_blocks=pos3;
      }
      pos1->ref_state->ref_states_in_blocks=pos1;
      pos2->ref_state->ref_states_in_blocks=pos2;
    }
 
    void swap_states_in_states_in_block(
              state_in_block_pointer* pos1,
              state_in_block_pointer* pos2,
              state_in_block_pointer* pos3)
    {
      if (pos2==pos3)
      {
        swap_states_in_states_in_block(pos1,pos2);
      }
      else
      {
        swap_states_in_states_in_block_23_never_equal(pos1,pos2,pos3);
      }
    }
 
    void multiple_swap_states_in_states_in_block(
              state_in_block_pointer* pos1,
              state_in_block_pointer* pos2,
              state_index count
                                                                                #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
                                                                                  , const state_in_block_pointer* assign_work_to,
                                                                                    unsigned char const max_B,
                                                                                    enum check_complexity::counter_type const ctr=check_complexity::
                                                                                                       multiple_swap_states_in_block__swap_state_in_small_block
                                                                                #endif
              )
    {                                                                           assert(count<m_aut.num_states());  assert(m_states_in_blocks.data()<=pos1);
      /* if (pos1 > pos2)  std::swap(pos1, pos2);                            */ assert(pos1<pos2);  assert(pos2<=m_states_in_blocks.data_end()-count);
      {
        std::make_signed<state_index>::type
                                       overlap=std::distance(pos2, pos1)+count;
        if (overlap > 0)
        {
          count -= overlap;
                                                                                #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
                                                                                  // If we do not change `assign_work_to`, then there should be no overlap
                                                                                  // between the area starting at `pos2` and the one at `assign_work_to`;
                                                                                  // otherwise it may happen that work is assigned to unexpected counters.
                                                                                  if (pos2==assign_work_to) {
                                                                                    assign_work_to+=overlap;
                                                                                  } else  {  assert(assign_work_to+count<=pos2+overlap ||
                                                                                                    pos2+overlap+count<=assign_work_to);  }
                                                                                #endif
          pos2 += overlap;
        }
      }                                                                         assert(0 < count);
      state_in_block_pointer temp=*pos1;
      while (--count > 0)
      {                                                                         mCRL2complexity(assign_work_to->ref_state, add_work(ctr, max_B), *this);
                                                                                #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
                                                                                  ++assign_work_to;
                                                                                #endif
        *pos1 = *pos2;
        pos1->ref_state->ref_states_in_blocks=pos1;
        ++pos1;
        *pos2 = *pos1;
        pos2->ref_state->ref_states_in_blocks=pos2;
        ++pos2;
      }
      *pos1 = *pos2;
      pos1->ref_state->ref_states_in_blocks=pos1;
      *pos2 = temp;
      pos2->ref_state->ref_states_in_blocks=pos2;
                                                                                #ifndef NDEBUG
                                                                                  for (fixed_vector<state_type_gj>::const_iterator
                                                                                                                si=m_states.cbegin(); si<m_states.cend(); ++si)
                                                                                  {
                                                                                    assert(si==si->ref_states_in_blocks->ref_state);
                                                                                  }
                                                                                #endif
    }
 
    void mark_BLC_transition(const outgoing_transitions_it out_pos)
    {
      BLC_list_iterator old_pos = out_pos->ref.BLC_transitions;
      linked_list<BLC_indicators>::iterator ind =
                m_transitions[*old_pos].transitions_per_block_to_constellation; assert(ind->start_same_BLC<=old_pos);
                                                                                assert(old_pos<m_BLC_transitions.data_end());
                                                                                assert(old_pos<ind->end_same_BLC);  assert(!ind->is_stable());
      if (old_pos < ind->start_marked_BLC)
      {
        /* The transition is not marked */                                      assert(ind->start_same_BLC<ind->start_marked_BLC);
        BLC_list_iterator new_pos = std::prev(ind->start_marked_BLC);           assert(ind->start_same_BLC<=new_pos);  assert(new_pos<ind->end_same_BLC);
                                                                                assert(new_pos<m_BLC_transitions.data_end());
        if (old_pos < new_pos)
        {
          std::swap(*old_pos, *new_pos);
          m_transitions[*old_pos].ref_outgoing_transitions->
                                                 ref.BLC_transitions = old_pos; assert(out_pos==m_transitions[*new_pos].ref_outgoing_transitions);
          out_pos->ref.BLC_transitions = new_pos;
        }
        ind->start_marked_BLC--;
      }
 
                                                                                #ifndef NDEBUG
                                                                                  for (BLC_list_const_iterator it=m_BLC_transitions.data();
                                                                                                                         it<m_BLC_transitions.data_end(); ++it)
                                                                                  {
                                                                                    assert(m_transitions[*it].ref_outgoing_transitions->ref.BLC_transitions==
                                                                                                                                                           it);
                                                                                    assert(m_transitions[*it].transitions_per_block_to_constellation->
                                                                                                                                           start_same_BLC<=it);
                                                                                    assert(it<
                                                                                      m_transitions[*it].transitions_per_block_to_constellation->end_same_BLC);
                                                                                  }
                                                                                #endif
    }
 
#ifndef USE_FOUR_WAY_SPLIT
    template <bool initialisation=false>
    block_type* split_block_B_into_R_and_BminR(
        block_type* const B,
        state_in_block_pointer* first_bottom_state_in_R,
        state_in_block_pointer* last_bottom_state_in_R,
        const todo_state_vector& R)
    {                                                                           assert(B->start_bottom_states<=first_bottom_state_in_R);
//std::cerr << "split_block_B_into_R_and_BminR" << (initialisation ? "<true>(" : "(") << B->debug_id(*this)
//<< ",&m_states_in_blocks[" << std::distance(m_states_in_blocks.begin(), first_bottom_state_in_R)
//<< "..." << std::distance(m_states_in_blocks.begin(), last_bottom_state_in_R)
//<< "),R = {";
//for(auto s:R){ std::cerr << ' ' << std::distance(m_states.begin(), s.ref_state); }
//std::cerr << " }"
//")\n";
//std::cerr << "SPLIT BLOCK " << B << " by removing "; for(auto s = first_bottom_state_in_R; s < last_bottom_state_in_R; ++s){ std::cerr << std::distance(m_states.begin(), s->ref_state) << ' ';} for(auto s:R){ std::cerr << ' ' << std::distance(m_states.begin(), s.ref_state); } std::cerr << '\n';
      /* Basic administration. Make a new block and add it to the current    */ assert(first_bottom_state_in_R<=last_bottom_state_in_R);
      /* constellation.                                                      */ assert(last_bottom_state_in_R<=B->sta.rt_non_bottom_states);
      constellation_type* const ci=B->c.onstellation;
      block_type* const B_new=
                #ifdef USE_POOL_ALLOCATOR
                    simple_list<BLC_indicators>::get_pool().
                    template construct<block_type>
                #else
                    new block_type
                #endif
                                  (B->start_bottom_states, ci);
      ++no_of_blocks;
                                                                                #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
                                                                                  B_new->work_counter=B->work_counter;
                                                                                #endif
                                                                                assert(m_states_in_blocks.data()<=ci->start_const_states);
                                                                                assert(ci->start_const_states<ci->end_const_states);
                                                                                assert(ci->end_const_states<=m_states_in_blocks.data_end());
      if (ci->start_const_states->ref_state->block==
            std::prev(ci->end_const_states)->ref_state->block)
      {                                                                         assert(std::find(m_non_trivial_constellations.begin(),
        /* This constellation was trivial, as it will be split add it to the */                  m_non_trivial_constellations.end(),
        /* non-trivial constellations.                                       */                  ci)==m_non_trivial_constellations.end());
        m_non_trivial_constellations.emplace_back(ci);
      }                                                                         // The size of the new block is not yet number_of_states_in_block(...)
                                                                                #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
                                                                                  unsigned char const max_B = check_complexity::log_n -
                                                                                      check_complexity::ilog2(std::distance(first_bottom_state_in_R,
      /* Carry out the split.                                                */                                             last_bottom_state_in_R) + R.size());
                                                                                #endif
      if (B->start_bottom_states!=first_bottom_state_in_R)
      {                                                                         assert(first_bottom_state_in_R!=last_bottom_state_in_R);
        multiple_swap_states_in_states_in_block(
                B->start_bottom_states, first_bottom_state_in_R,
                std::distance(first_bottom_state_in_R, last_bottom_state_in_R)
                                                                                #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
                                                                                  , first_bottom_state_in_R, max_B
                                                                                #endif
                );
        last_bottom_state_in_R = B->start_bottom_states +
                std::distance(first_bottom_state_in_R, last_bottom_state_in_R);
        first_bottom_state_in_R = B->start_bottom_states;
      }
                                                                                assert(B_new->start_bottom_states==first_bottom_state_in_R);
      B_new->sta.rt_non_bottom_states=last_bottom_state_in_R;
      // Update the block pointers for R-bottom states:
      for (state_in_block_pointer*
             s_it=first_bottom_state_in_R; s_it<last_bottom_state_in_R; ++s_it)
      {                                                                         mCRL2complexity(s_it->ref_state, add_work(check_complexity::
                                                                                                split_block_B_into_R_and_BminR__carry_out_split, max_B), *this);
//std::cerr << "MOVE STATE TO NEW BLOCK: " << std::distance(m_states.begin(), s_it->ref_state) << "\n";
                                                                                assert(B==s_it->ref_state->block);
        s_it->ref_state->block=B_new;                                           assert(s_it->ref_state->ref_states_in_blocks==s_it);
      }
      // Now the R bottom states are in the correct position, and we don't have
      // to look into them any more.
      B_new->end_states=last_bottom_state_in_R;
      B->start_bottom_states=last_bottom_state_in_R;
 
        // Move the non-bottom states to their correct positions:
        for(state_in_block_pointer s: R)
        {                                                                       mCRL2complexity(s.ref_state, add_work(check_complexity::
                                                                                               split_block_B_into_R_and_BminR__carry_out_split, max_B), *this);
//std::cerr << "MOVE STATE TO NEW BLOCK: " << s << "\n";
                                                                                assert(B==s.ref_state->block);
          s.ref_state->block=B_new;
          state_in_block_pointer* pos=s.ref_state->ref_states_in_blocks;        assert(pos>=B->sta.rt_non_bottom_states); // it's a non-bottom state
          // pos -> B.start_bottom_states -> B.sta.rt_non_bottom_states -> pos
          swap_states_in_states_in_block(pos, B->start_bottom_states,
                                                  B->sta.rt_non_bottom_states);
          B->sta.rt_non_bottom_states++;
          B->start_bottom_states++;
          B_new->end_states++;                                                  assert(B->start_bottom_states<=B->sta.rt_non_bottom_states);
                                                                                assert(B_new->start_bottom_states<B_new->end_states);
        }
      return B_new;
    }
#endif
 
    void swap_three_iterators_and_update_m_transitions(
                                                    const BLC_list_iterator i1,
                                                    const BLC_list_iterator i2,
                                                    const BLC_list_iterator i3)
    {                                                                           assert(i3<=i2);  assert(i2<=i1);
      if (i1==i3)
      {
        return;
      }
      if ((i1==i2)||(i2==i3))
      {
        std::swap(*i1,*i3);
        m_transitions[*i1].ref_outgoing_transitions->ref.BLC_transitions = i1;
        m_transitions[*i3].ref_outgoing_transitions->ref.BLC_transitions = i3;
      }
      else  // swap all three elements.
      {
        transition_index temp = *i1;
        *i1=*i2;
        *i2=*i3;
        *i3=temp;
        m_transitions[*i1].ref_outgoing_transitions->ref.BLC_transitions = i1;
        m_transitions[*i2].ref_outgoing_transitions->ref.BLC_transitions = i2;
        m_transitions[*i3].ref_outgoing_transitions->ref.BLC_transitions = i3;
      }
    }
 
    [[nodiscard]]
    bool swap_in_the_doubly_linked_list_LBC_in_blocks_new_constellation(
               const transition_index ti,
               linked_list<BLC_indicators>::iterator new_BLC_block,
               linked_list<BLC_indicators>::iterator old_BLC_block)
    {                                                                           assert(new_BLC_block->is_stable());
      BLC_list_iterator old_position=
               m_transitions[ti].ref_outgoing_transitions->ref.BLC_transitions; assert(old_BLC_block->start_same_BLC <= old_position);
                                                                                assert(old_position<old_BLC_block->end_same_BLC);
                                                                                assert(new_BLC_block->end_same_BLC==old_BLC_block->start_same_BLC);
                                                                                assert(m_transitions[ti].transitions_per_block_to_constellation == old_BLC_block);
                                                                                assert(ti == *old_position);
      if (!old_BLC_block->is_stable())
      {                                                                         assert(old_BLC_block->start_same_BLC<=old_BLC_block->start_marked_BLC);
                                                                                assert(old_BLC_block->start_marked_BLC<=old_BLC_block->end_same_BLC);
        if (old_BLC_block->start_marked_BLC<=old_position)
        {                                                                       assert(m_states[m_aut.get_transitions()[ti].from()].block->
                                                                                                                                  contains_new_bottom_states ||
                                                                                       number_of_states_in_block
                                                                                                     (*m_states[m_aut.get_transitions()[ti].from()].block)<=1);
          // It's ok to unmark transitions because they start in blocks with
          // new bottom states, or in blocks with only 1 state.
          // (However, it may happen that unmarked transitions from other blocks
          // are moved, even if there are marked transitions in the same BLC set---
          // namely for the co-splitters. So we can only unmark transitions if
          // transition ti itself is marked.)
          old_BLC_block->start_marked_BLC=old_BLC_block->end_same_BLC;
        }
      }
      if (old_position!=old_BLC_block->start_same_BLC)
      {
        std::swap(*old_position,*old_BLC_block->start_same_BLC);
        m_transitions[*old_position].ref_outgoing_transitions->
                                            ref.BLC_transitions = old_position;
        m_transitions[*old_BLC_block->start_same_BLC].
                    ref_outgoing_transitions->ref.BLC_transitions =
                                                 old_BLC_block->start_same_BLC;
      }
      new_BLC_block->end_same_BLC=++old_BLC_block->start_same_BLC;
      m_transitions[ti].transitions_per_block_to_constellation=new_BLC_block;
//std::cerr << " to new " << new_BLC_block->debug_id(*this) << '\n';
      return old_BLC_block->start_same_BLC==old_BLC_block->end_same_BLC;
    }
 
    [[nodiscard]]
    bool update_the_doubly_linked_list_LBC_new_constellation(
               block_type* const index_block_B,
               const transition& t,
               const transition_index ti)
    {                                                                           assert(m_states[t.to()].block==index_block_B);
//std::cerr << "update_the_doubly_linked_list_LBC_new_constellation(" << index_block_B->debug_id(*this) << ',' << m_transitions[ti].debug_id(*this) << ")\n";
      block_type* const from_block=m_states[t.from()].block;                    assert(&m_aut.get_transitions()[ti] == &t);
      bool new_block_created = false;                                           assert(from_block->block.to_constellation.check_linked_list());
      linked_list<BLC_indicators>::iterator this_block_to_constellation=
                      m_transitions[ti].transitions_per_block_to_constellation;
                                                                                #ifndef NDEBUG
                                                                                  // Check whether this_block_to_constellation is in the corresponding list
                                                                                  for (linked_list<BLC_indicators>::const_iterator i=from_block->block.to_constellation.begin();
                                                                                       i!=this_block_to_constellation; ++i)
                                                                                  {
                                                                                    assert(i!=from_block->block.to_constellation.end());
                                                                                  }
                                                                                #endif
                                                                                assert(this_block_to_constellation!=from_block->block.to_constellation.end());
                                                                                assert(this_block_to_constellation->start_same_BLC <= m_transitions[ti].ref_outgoing_transitions->ref.BLC_transitions);
                                                                                // the transition is never marked:
                                                                                assert(from_block->contains_new_bottom_states ||
                                                                                       number_of_states_in_block(*from_block)<=1 ||
                                                                                       this_block_to_constellation->is_stable() ||
                                                                                       m_transitions[ti].ref_outgoing_transitions->ref.BLC_transitions<this_block_to_constellation->start_marked_BLC);
      linked_list<BLC_indicators>::iterator next_block_to_constellation;
      // if this transition is inert, it is inserted in a block in front.
      // Otherwise, it is inserted after the current element in the list.
      if (is_inert_during_init(t) && from_block==index_block_B)
      {
        next_block_to_constellation=from_block->block.to_constellation.begin(); assert(next_block_to_constellation->start_same_BLC <
                                                                                                                      next_block_to_constellation->end_same_BLC);
                                                                                assert(m_states[m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)].from()].block==index_block_B);
                                                                                assert(m_aut.is_tau(m_aut_apply_hidden_label_map(m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)].label())));
        if (next_block_to_constellation==this_block_to_constellation)
        {
          // Make a new entry in the list block.to_constellation, at the
          // beginning;
//std::cerr << "Creating new BLC set for inert " << m_transitions[ti].debug_id(*this) << ": ";
 
          next_block_to_constellation=from_block->block.to_constellation.
                       emplace_front(//first_block_to_constellation,
                             this_block_to_constellation->start_same_BLC,
                             this_block_to_constellation->start_same_BLC,true);
                                                                                #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
                                                                                  next_block_to_constellation->work_counter = this_block_to_constellation->work_counter;
                                                                                #endif
        }                                                                       else
                                                                                {
//std::cerr << "Extending existing BLC set for inert " << m_transitions[ti].debug_id(*this) << ": ";
                                                                                  assert(m_states[m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)].to()].block==index_block_B);
                                                                                }
      }
      else
      {
        // The transition is not constellation-inert.
        // The transition will be placed in a BLC set immediately after the BLC
        // set it came from, so that main splitters (with transitions to the
        // new constellation) come after co-splitters (with transitions to the
        // old constellation).
 
        // This method also ensures that transitions from the old constellation
        // to the old constellation will remain at the beginning of their
        // respective BLC set.
        next_block_to_constellation=from_block->
                      block.to_constellation.next(this_block_to_constellation);
        const transition* first_t;
        if (next_block_to_constellation==
                                    from_block->block.to_constellation.end() ||
            (first_t=&m_aut.get_transitions()
                      [*(next_block_to_constellation->start_same_BLC)],
             assert(m_states[first_t->from()].block==from_block),
             m_states[first_t->to()].block!=index_block_B) ||
            label_or_divergence(*first_t)!=label_or_divergence(t))
        {
//std::cerr << "Creating new BLC set for " << m_transitions[ti].debug_id(*this) << ": ";
          // Make a new entry in the list next_block_to_constellation, after the current list element.
          new_block_created = true;
          next_block_to_constellation=from_block->block.to_constellation.
                       emplace_after(this_block_to_constellation,
                             this_block_to_constellation->start_same_BLC,
                             this_block_to_constellation->start_same_BLC,true);
                                                                                #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
          /* The entry will be marked as unstable later                      */   next_block_to_constellation->work_counter=
                                                                                                                     this_block_to_constellation->work_counter;
                                                                                #endif
          ++no_of_non_constellation_inert_BLC_sets;
        }
//else { std::cerr << "Extending existing BLC set for " << m_transitions[ti].debug_id(*this) << ": "; }
      }
 
      if (swap_in_the_doubly_linked_list_LBC_in_blocks_new_constellation(ti,
                     next_block_to_constellation, this_block_to_constellation))
      {
        from_block->block.to_constellation.erase(this_block_to_constellation);
//std::cerr << "Erasing the old BLC set";
        if (!is_inert_during_init(t) ||
            from_block->c.onstellation!=index_block_B->c.onstellation)
            // i.e. if transition t is not a (formerly) inert transition (in
            // that case, the old BLC set would havold BLC set did *not*
            // contain the (formerly) inert tau-transitions from the old to the
            // new constellation, or the still-inert tau-transitions of the
            // old constellation
        {
          --no_of_non_constellation_inert_BLC_sets;
        }
      }
//std::cerr << '\n';
                                                                                #ifndef NDEBUG
                                                                                  check_transitions(false, false, false);
                                                                                #endif
      return new_block_created;
    }
 
    [[nodiscard]]
    bool swap_in_the_doubly_linked_list_LBC_in_blocks_new_block(
               const transition_index ti,
               linked_list<BLC_indicators>::iterator new_BLC_block,
               linked_list<BLC_indicators>::iterator old_BLC_block)
    {                                                                           assert(new_BLC_block->end_same_BLC==old_BLC_block->start_same_BLC);
      BLC_list_iterator old_position =
               m_transitions[ti].ref_outgoing_transitions->ref.BLC_transitions; assert(old_BLC_block->start_same_BLC<=old_position);
                                                                                assert(old_position<old_BLC_block->end_same_BLC);
                                                                                #ifndef NDEBUG
                                                                                  if (!old_BLC_block->is_stable())
                                                                                  {
                                                                                    assert(old_BLC_block->start_same_BLC<=old_BLC_block->start_marked_BLC);
                                                                                    assert(old_BLC_block->start_marked_BLC<=old_BLC_block->end_same_BLC);
                                                                                  }
                                                                                  if (!new_BLC_block->is_stable())
                                                                                  {
                                                                                    assert(new_BLC_block->start_same_BLC<=new_BLC_block->start_marked_BLC);
                                                                                    assert(new_BLC_block->start_marked_BLC<=new_BLC_block->end_same_BLC);
                                                                                  }
                                                                                #endif
                                                                                assert(m_transitions[ti].transitions_per_block_to_constellation==
                                                                                                                                                old_BLC_block);
                                                                                //assert(new block==m_states[m_aut.get_transitions()[ti].from()].block);
                                                                                assert(ti==*old_position);
      if (old_BLC_block->is_stable() ||
          old_position<old_BLC_block->start_marked_BLC)
      {                                                                         assert(old_BLC_block->start_same_BLC <= old_position);
//std::cerr << "Moving unmarked " << m_transitions[*old_position].debug_id(*this);
        if (new_BLC_block->is_stable())
        {
                                                                                #ifndef NDEBUG
                                                                                  if (!old_BLC_block->is_stable())
                                                                                  {
                                                                                    // different stability status: check that ti is inert
                                                                                    const transition& t=m_aut.get_transitions()[ti];
                                                                                    assert(is_inert_during_init(t) &&
                                                                                           (no_of_constellations<=1 /* i.e. initialisation */ ||
                                                                                            m_states[t.from()].block->c.onstellation==
                                                                                                                      m_states[t.to()].block->c.onstellation));
                                                                                  }
                                                                                #endif
          if (old_position!=old_BLC_block->start_same_BLC)
          {
            std::swap(*old_position, *old_BLC_block->start_same_BLC);
            m_transitions[*old_position].ref_outgoing_transitions->
                                              ref.BLC_transitions=old_position;
            m_transitions[*old_BLC_block->start_same_BLC].
                      ref_outgoing_transitions->ref.BLC_transitions=
                                                 old_BLC_block->start_same_BLC;
          }
        }
        else
        {                                                                       assert(new_BLC_block->start_marked_BLC<=old_BLC_block->start_same_BLC);
                                                                                #ifndef NDEBUG
                                                                                  if (old_BLC_block->is_stable())
                                                                                  {
                                                                                    // different stability status: check that ti is inert
                                                                                    const transition& t=m_aut.get_transitions()[ti];
                                                                                    assert(is_inert_during_init(t) &&
                                                                                           (/*initialisation ||*/
                                                                                            m_states[t.from()].block->c.onstellation==
                                                                                                                      m_states[t.to()].block->c.onstellation));
                                                                                  }
                                                                                #endif
          swap_three_iterators_and_update_m_transitions(old_position,
             old_BLC_block->start_same_BLC, new_BLC_block->start_marked_BLC++);
        }
      }
      else
      {                                                                         assert(old_BLC_block->start_marked_BLC <= old_position);
//std::cerr << "Moving marked " << m_transitions[*old_position].debug_id(*this);
                                                                                assert(old_BLC_block->start_same_BLC <= old_BLC_block->start_marked_BLC);
                                                                                assert(!new_BLC_block->is_stable());
        swap_three_iterators_and_update_m_transitions(old_position,
             old_BLC_block->start_marked_BLC++, old_BLC_block->start_same_BLC);
      }
      m_transitions[ti].transitions_per_block_to_constellation=new_BLC_block;
      new_BLC_block->end_same_BLC=++old_BLC_block->start_same_BLC;
//std::cerr << " to new " << new_BLC_block->debug_id(*this) << '\n';
      return old_BLC_block->start_same_BLC==old_BLC_block->end_same_BLC;
    }
 
    void update_the_doubly_linked_list_LBC_new_block(
               block_type* const old_bi,
               block_type* const new_bi,
               const transition_index ti,
               constellation_type* old_constellation,
               constellation_type*const new_constellation
                 // used to maintain the order of BLC sets:
                 // main splitter BLC sets (target constellation == new constellation) follow immediately
                 // after co-splitter BLC sets (target constellation == old_constellation) in the BLC sets
               )
    {                                                                           assert(old_bi->block.to_constellation.check_linked_list());
//std::cerr << "update_the_doubly_linked_list_LBC_new_block(old_bi==" << old_bi << ", new_bi==" << new_bi << ", transition_index==" << ti << "==" << m_transitions[ti].debug_id_short(*this) << ", old_constellation==" << old_constellation->debug_id(*this) << ")\n";
      const transition& t=m_aut.get_transitions()[ti];                          assert(new_bi->block.to_constellation.check_linked_list());
                                                                                assert(m_states[t.from()].block==new_bi);
      linked_list<BLC_indicators>::iterator this_block_to_constellation=
                      m_transitions[ti].transitions_per_block_to_constellation;
//std::cerr << "This transition is originally in " << this_block_to_constellation->debug_id(*this, old_bi) << '\n';
                                                                                #ifndef NDEBUG
                                                                                  // Check whether this_block_to_constellation is in the corresponding list
                                                                                  for (linked_list<BLC_indicators>::const_iterator i=old_bi->block.to_constellation.begin();
                                                                                       i!=this_block_to_constellation; ++i)
                                                                                  {
                                                                                    assert(i!=old_bi->block.to_constellation.end());
                                                                                  }
                                                                                #endif
      const label_index a=label_or_divergence(t);
      constellation_type* const to_constln=
                                        m_states[t.to()].block->c.onstellation;
      linked_list<BLC_indicators>::iterator new_BLC_block;
      const bool t_is_inert=is_inert_during_init(t);
      if (t_is_inert && to_constln==new_bi->c.onstellation)
      {
          /* Before correcting the BLC lists, we already inserted an empty   */ assert(this_block_to_constellation==old_bi->block.to_constellation.begin());
          /* BLC_indicator into the list to take the constellation-inert     */
          /* transitions. */                                                    assert(!new_bi->block.to_constellation.empty());
          new_BLC_block=new_bi->block.to_constellation.begin();                 assert(this_block_to_constellation->start_same_BLC==new_BLC_block->end_same_BLC);
                                                                                #ifndef NDEBUG
//std::cerr << "This transition remains constellation-inert and is moved to " << new_BLC_block->debug_id(*this) << '\n';
                                                                                  if (new_BLC_block->start_same_BLC<new_BLC_block->end_same_BLC)
                                                                                  {
                                                                                    const transition& inert_t=m_aut.get_transitions()[*new_BLC_block->start_same_BLC];
                                                                                    assert(new_bi==m_states[inert_t.from()].block);
                                                                                    assert(a==label_or_divergence(inert_t));
                                                                                    assert(to_constln==m_states[inert_t.to()].block->c.onstellation);
                                                                                  }
                                                                                #endif
      }
      else
      {
        transition_index perhaps_new_BLC_block_transition;
        const transition* perhaps_new_BLC_t;
        if (this_block_to_constellation->start_same_BLC!=
                                                    m_BLC_transitions.data() &&
            (perhaps_new_BLC_block_transition=
                    *std::prev(this_block_to_constellation->start_same_BLC),
             perhaps_new_BLC_t=
                 &m_aut.get_transitions()[perhaps_new_BLC_block_transition],
             m_states[perhaps_new_BLC_t->from()].block==new_bi) &&
            a==label_or_divergence(*perhaps_new_BLC_t) &&
            to_constln==m_states
                               [perhaps_new_BLC_t->to()].block->c.onstellation)
        {
          // Found the entry where the transition should go to
          // Move the current transition to the new list.
          new_BLC_block=m_transitions[perhaps_new_BLC_block_transition].
                                        transitions_per_block_to_constellation;
                                                                                #ifndef NDEBUG
//std::cerr << "It will be moved to the existing " << new_BLC_block->debug_id(*this) << '\n';
                                                                                  if (this_block_to_constellation->is_stable()) { assert(new_BLC_block->is_stable()); }
                                                                                  else { assert(!new_BLC_block->is_stable()); }
                                                                                #endif
        }
        else
        {
          // Make a new entry in the list next_block_to_constellation;
 
          // We first calculate the position where the new BLC set should go to
          // in new_position.
          // Default position: at the beginning.
          linked_list<BLC_indicators>::iterator new_position=
                                          new_bi->block.to_constellation.end(); assert(!is_inert_during_init(t)||to_constln!=new_bi->c.onstellation);
#ifndef USE_FOUR_WAY_SPLIT
          BLC_list_iterator_or_null old_co_splitter_end=nullptr;
          if (this_block_to_constellation->is_stable())
          {
//std::cerr << "Transition is in a stable BLC set.\n";
            if (m_branching)
            {
              // We always inserted a new BLC set for the inert transitions,
              // so we can place the BLC set after that one.
              new_position=new_bi->block.to_constellation.begin();
//std::cerr << "    and is placed after " << new_position->debug_id(*this) << '\n';
            }
            // Because the BLC set is stable, one does not need to keep main
            // splitter and co-splitter together.
            // If the BLC set becomes empty, one can immediately delete it.
            old_constellation=null_constellation;
          }
          else
#endif
          {
            if (new_bi->block.to_constellation.empty())
            {                                                                   assert(!m_branching);
              /* This is the first transition that is moved. */                 assert(new_bi->block.to_constellation.end()==new_position);
//std::cerr << "This is the first transition that is moved.\n";
            }
            else
            {
              // default position: place it at the end of the list
              new_position=new_bi->block.to_constellation.before_end();         assert(new_bi->block.to_constellation.end()!=new_position);
            }
            if (null_constellation!=old_constellation)
            {
              if (t_is_inert &&
                  ((to_constln==new_constellation &&
                    new_bi->c.onstellation==old_constellation) ||
                      // < The transition goes from the old constellation to
                      // the splitter block and was constellation-inert before.
                      // It is in a main splitter without (unstable)
                      // co-splitter. We do not need to find the co-splitter.
                   (to_constln==old_constellation &&
                    new_bi->c.onstellation==new_constellation)))
                      // < The formerly constellation-inert transition goes
                      // from the new constellation to the old constellation,
                      // it is in a co-splitter without (unstable) main
                      // splitter, and this co-splitter was handled as the
                      // first splitting action.
              {
                old_constellation=null_constellation;
//std::cerr << (old_constellation==to_constln ? "This transition was constellation-inert earlier, so we do not need to find a main splitter.\n" : "This transition was constellation-inert earlier, so we do not need to find a co-splitter.\n");
              }
              else
              {                                                                 assert(old_constellation!=new_constellation);
                // The following comments are all formulated for the case that
                // this_block_to_constellation is a main splitter (except when
                // indicated explicitly).
                linked_list<BLC_indicators>::const_iterator old_co_splitter;
                constellation_type* co_to_constln;
                if ((old_constellation==to_constln &&
                     // i.e. `this_block_to_constellation` is a co-splitter
                     (old_co_splitter=old_bi->block.to_constellation.
                                             next(this_block_to_constellation),
                      co_to_constln=new_constellation,
//(std::cerr << "Transition is originally in a co-splitter; "),
                                                                      true)) ||
                    (new_constellation==to_constln &&
                     // i.e. `this_block_to_constellation` is a main splitter
                     (old_co_splitter=old_bi->block.to_constellation.
                                             prev(this_block_to_constellation),
                      co_to_constln=old_constellation,
//(std::cerr << "Transition is originally in a main splitter; "),
                                                                        true)))
                {
                  if (old_bi->block.to_constellation.end()!=old_co_splitter)
                  {
//std::cerr << (old_constellation == to_constln ? "Current old main splitter candidate: " : "Current old co-splitter candidate: ") << old_co_splitter->debug_id(*this, old_bi);
                    // If the co-splitter belonging to
                    // `this_block_to_constellation` exists, then it is
                    // `old_co_splitter` (but if there is no such co-splitter,
                    // `old_co_splitter` could be a different main splitter, a
                    // different co-splitter without main splitter, or a
                    // completely unrelated splitter).
 
                    // Try to find out whether there is already a corresponding
                    // co-splitter in `new_bi->block.to_constellation`
                    // This co-splitter would be just before `old_co_splitter`
                    // in `m_BLC_transitions`.
                    if (new_bi->block.to_constellation.end()!=new_position &&
                        m_BLC_transitions.data()<
                                               old_co_splitter->start_same_BLC)
                        // i.e. this is not the first transition -- neither the
                        // first to be moved to the new block nor the first in
                        // m_BLC_transitions
                    {
                      // Check the transition in the potential corresponding
                      // new co-splitter:
                      const transition_index perhaps_new_co_spl_transition=
                                   *std::prev(old_co_splitter->start_same_BLC);
                      const transition& perhaps_new_co_spl_t=
                        m_aut.get_transitions()[perhaps_new_co_spl_transition];
                      if(new_bi==m_states[perhaps_new_co_spl_t.from()].block &&
                         a==label_or_divergence(perhaps_new_co_spl_t) &&
                         co_to_constln==m_states
                             [perhaps_new_co_spl_t.to()].block->c.onstellation)
                      {
                        // `perhaps_new_co_spl_transition` is in the
                        // corresponding new co-splitter; place the new BLC set
                        // immediately after this co-splitter in the list
                        // `new_bi->block.to_constellation`.
                        new_position=m_transitions
                                      [perhaps_new_co_spl_transition].
                                        transitions_per_block_to_constellation;
                        if (old_constellation==to_constln)
                        {
                          // (`this_block_to_constellation` was a co-splitter:)
                          // `perhaps_new_co_spl_transition` is in the new main
                          // splitter; place the new BLC set immediately before
                          // this main splitter in the list
                          // `new_bi->block.to_constellation`.
                          new_position=new_bi->block.to_constellation.
                                                            prev(new_position);
//std::cerr << ". This is a real old main splitter.\n";
                        }
//else { std::cerr << ". This is a real old co-splitter.\n"; }
                                                                                #ifndef NDEBUG
                        /* The new co-splitter was found, and                */   if (old_co_splitter->start_same_BLC<old_co_splitter->end_same_BLC)
                        /* `old_co_splitter` must have been the old          */   {
                        /* co-splitter.                                      */     const transition& co_t=m_aut.get_transitions()
                                                                                                                            [*old_co_splitter->start_same_BLC];
                        /* Now the new main splitter is about to be created. */     assert(old_bi==m_states[co_t.from()].block ||
                        /* In this case it is ok to delete                   */            new_bi==m_states[co_t.from()].block);
                        /* `this_block_to_constellation` when it becomes     */     assert(a==label_or_divergence(co_t));
                        /* empty; therefore we set `old_constellation` in a  */     assert(co_to_constln==m_states[co_t.to()].block->c.onstellation);
                        /* way that it's going to delete it immediately:     */   }
                                                                                #endif
                        old_constellation=null_constellation;
                        // We should not use `old_constellation` for anything
                        // else after this point.
                      }
#ifdef USE_FOUR_WAY_SPLIT
//else  {  std::cerr << ". The transition just before it in m_BLC_transitions (" << m_transitions[perhaps_new_co_spl_transition].debug_id_short(*this) << ") does not belong to the new co-splitter.\n";  }
#else
                      else if (new_constellation==to_constln)
                      {
                        const transition* co_t;
                        if (old_co_splitter->start_same_BLC<
                                               old_co_splitter->end_same_BLC &&
                            (co_t=&m_aut.get_transitions()
                                          [*old_co_splitter->start_same_BLC],   assert(old_bi==m_states[co_t->from()].block ||
                                                                                       new_bi==m_states[co_t->from()].block),
                             a==label_or_divergence(*co_t)) &&
                            old_constellation==m_states
                                            [co_t->to()].block->c.onstellation)
                        {
//std::cerr << ". The transition just before it in m_BLC_transitions (" << m_transitions[perhaps_new_co_spl_transition].debug_id_short(*this) << ") does not belong to the new co-splitter.\n";
                          old_co_splitter_end=old_co_splitter->end_same_BLC;
                        }
                        else
                        {
//std::cerr << ". In fact, it is not a true candidate.\n";
                          // As there is no old co-splitter, we do not need to keep an empty old main splitter.
                          old_constellation=null_constellation;
                        }
                      }                                                         else
                                                                                {
                                                                                  assert(old_constellation==to_constln);
//std::cerr << ". The transition just before it in m_BLC_transitions (" << m_transitions[perhaps_new_co_spl_transition].debug_id_short(*this) << ") does not belong to the new main splitter.\n";
                                                                                }
#endif
                    }
#ifdef USE_FOUR_WAY_SPLIT
//else  {  std::cerr << ". This candidate is at the beginning of m_BLC_transitions, or it is the first transition. There is no new co-splitter yet.\n";  }
#else
                    else if (new_constellation==to_constln)
                    {
                      const transition* co_t;
                      if (old_co_splitter->start_same_BLC<
                                               old_co_splitter->end_same_BLC &&
                          (co_t=&m_aut.get_transitions()
                                          [*old_co_splitter->start_same_BLC],   assert(old_bi==m_states[co_t->from()].block ||
                                                                                       new_bi==m_states[co_t->from()].block),
                           a==label_or_divergence(*co_t)) &&
                          old_constellation==m_states
                                            [co_t->to()].block->c.onstellation)
                      {
//std::cerr << ". This candidate is at the beginning of m_BLC_transitions, or it is the first transition. There is no new co-splitter yet.\n";
                        old_co_splitter_end=old_co_splitter->end_same_BLC;
                      }
                      else
                      {
//std::cerr << ". In fact, it is a false candidate.\n";
                        // As there is no old co-splitter, we do not need to
                        // keep an empty old main splitter.
                        old_constellation=null_constellation;
                      }
                    }                                                           else
                                                                                {
                                                                                  assert(old_constellation==to_constln);
//std::cerr << ". This candidate is at the beginning of m_BLC_transitions, or it is the first transition. There is no new main splitter yet.\n";
                                                                                }
#endif
                  }
                  else
                  {
                    // this_block_to_constellation is a main splitter
                    // but it has no corresponding co-splitter.
                    // If it becomes empty, one can immediately delete it.
                    old_constellation=null_constellation;
//std::cerr << (old_constellation == to_constln ? "There is no candidate old main splitter.\n" : "There is no candidate old co-splitter.\n");
                  }
                }
                else
                {
                  // this_block_to_constellation is neither a main splitter nor
                  // a co-splitter.  If it becomes empty, one can immediately
                  // delete it.
                  old_constellation=null_constellation;
                }
              }
            }
#ifdef USE_FOUR_WAY_SPLIT
            else if (this_block_to_constellation->is_stable())
            {
              // default position during new bottom splits: at the beginning of
              // the list (but after the BLC set of inert transitions)
              new_position=m_branching ? new_bi->block.to_constellation.begin()
                                       : new_bi->block.to_constellation.end();
            }
#endif
          }                                                                     assert(!m_branching || new_bi->block.to_constellation.end()!=new_position);
          const BLC_list_iterator old_BLC_start=this_block_to_constellation->start_same_BLC;
          new_BLC_block=new_bi->block.to_constellation.emplace_after
                          (new_position, old_BLC_start, old_BLC_start,
                                     this_block_to_constellation->is_stable());
                                                                                #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
                                                                                  new_BLC_block->work_counter=this_block_to_constellation->work_counter;
                                                                                #endif
          ++no_of_non_constellation_inert_BLC_sets;
#ifndef USE_FOUR_WAY_SPLIT
          if (null_constellation!=old_constellation)
          {
            // This is a new main splitter without new co-splitter, or a new
            // co-splitter without new main splitter
            if (old_constellation==to_constln)
            {
              // this is a new co-splitter but we haven't yet found the new
              // main splitter.  Perhaps we will have to stabilize it later.
              m_co_splitters_to_be_checked.emplace_back
                                       (new_BLC_block->start_same_BLC, new_bi);
//std::cerr << "We will check the stability of the new and old co-splitters later.\n";
              /* We may also have to stabilize the old co-splitter later.    */ assert(m_BLC_transitions.data()<this_block_to_constellation->end_same_BLC);
              m_co_splitters_to_be_checked.emplace_back
                (std::prev(this_block_to_constellation->end_same_BLC), old_bi);
            }
            else
            {                                                                   assert(new_constellation==to_constln);
              /* this is a new main splitter but we haven't yet found the new*/ assert(nullptr!=old_co_splitter_end);
              /* co-splitter.  Perhaps we will have to stabilize the old     */ assert(m_BLC_transitions.data()<old_co_splitter_end);
              /* co-splitter later.                                          */ assert(old_co_splitter_end<=m_BLC_transitions.data_end());
              m_co_splitters_to_be_checked.emplace_back
                                      (std::prev(old_co_splitter_end), old_bi);
//std::cerr << "We will check the stability of the old co-splitter later.\n";
            }
          }
#endif
        }
      }
      const bool last_element_removed=
              swap_in_the_doubly_linked_list_LBC_in_blocks_new_block(ti,
                                   new_BLC_block, this_block_to_constellation);
 
      if (last_element_removed)
      {
//std::cerr << "This was the last element in the old BLC set, which ";
        if (null_constellation != old_constellation)
        {
          // Sometimes we could still remove this_block_to_constellation
          // immediately (namely if the new main splitter and the new
          // co-splitter already exist, or if the old co-splitter does not
          // exist at all).  A few such cases are handled above, but other
          // cases would require additional, possibly extensive, checks:
          // if (co_block_found) {
          //   copy more or less the code from above that decides
          //   whether this_block_to_constellation is a main splitter
          //   that has an old co-splitter but not a new co-splitter
          //   or vice versa.
          // }
//std::cerr << "will be deleted later.";
          m_BLC_indicators_to_be_deleted.push_back
                                                 (this_block_to_constellation);
        }
        else
        {
//std::cerr << "is deleted immediately.";
          // Remove this element.
          old_bi->block.to_constellation.erase(this_block_to_constellation);
        }
        if (!t_is_inert || to_constln!=new_bi->c.onstellation)
        {
          --no_of_non_constellation_inert_BLC_sets;
        }
//std::cerr << '\n';
      }                                                                         assert(old_bi->block.to_constellation.check_linked_list());
                                                                                #ifndef NDEBUG
                                                                                  assert(new_bi->block.to_constellation.check_linked_list());
                                                                                  check_transitions(no_of_constellations<=1, false, false);
                                                                                #endif
      return;
    }
 
#ifdef USE_FOUR_WAY_SPLIT
    void clear_state_counters(
            std::vector<state_in_block_pointer>::const_iterator begin,
            std::vector<state_in_block_pointer>::const_iterator const end,
            block_type* const block)
    {
      (void) block; // avoid unused parameter warning
      while (begin!=end)
      {                                                                         assert(block==begin->ref_state->block);
        begin->ref_state->counter=undefined;
        ++begin;
      }
    }
 
#else
 
    void clear_state_counters(bool restrict_to_R=false)
    {
      for(const state_in_block_pointer& si: m_R)
      {                                                                         assert(Rmarked == si.ref_state->counter);
        // The work in this loop is accounted for by the same action that set
        // the counter to `Rmarked`
        si.ref_state->counter=undefined;
      }
      if (restrict_to_R)
      {                                                                         assert(m_U_counter_reset_vector.empty());
        return;
      }
      for(const state_in_block_pointer& si: m_U_counter_reset_vector)
      {                                                                         assert(undefined!=si.ref_state->counter || m_R.find(si));
        /* The work in this loop is accounted for by the action that set the */ assert(Rmarked!=si.ref_state->counter);
        // counter to some defined value (possibly to `Rmarked`, but then it
        // has already been changed back to `undefined` by the loop above).
        si.ref_state->counter=undefined;
      }
      clear(m_U_counter_reset_vector);
    }
 
    template <bool initialisation=false,
                          class Iterator=linked_list<BLC_indicators>::iterator>
    block_type* simple_splitB(block_type* const B,
                  Iterator splitter,
                  state_in_block_pointer* const first_unmarked_bottom_state,
                  const BLC_list_iterator_or_null splitter_end_unmarked_BLC,
                  block_type*& ptr_to_new_block)
    {
//std::cerr << "simple_splitB" << (initialisation ? "<true>(" : "(") << B->debug_id(*this) << ",...)\n";
      typedef enum { initializing, state_checking, aborted,
                     aborted_after_initialisation,
                     incoming_inert_transition_checking,
                     outgoing_action_constellation_check } status_type;         assert(1 < number_of_states_in_block(*B));
      status_type U_status=state_checking;                                      assert(!B->contains_new_bottom_states);
      status_type R_status=initializing;                                        assert(m_U.empty());  assert(m_U_counter_reset_vector.empty());
      BLC_list_iterator M_it;
      if constexpr (initialisation)
      {
        M_it=splitter_end_unmarked_BLC;
      }
      else
      {                                                                         assert(splitter_end_unmarked_BLC<=splitter->end_same_BLC);
        M_it=splitter->start_same_BLC;                                          assert(splitter_end_unmarked_BLC==splitter->start_marked_BLC ||
                                                                                       splitter_end_unmarked_BLC==M_it);
                                                                                assert(m_BLC_transitions.data()<=M_it);  assert(!splitter->is_stable());
                                                                                assert(splitter->start_same_BLC<splitter->end_same_BLC);
                                                                                assert(splitter->end_same_BLC<=m_BLC_transitions.data_end());
                                                                                assert(m_states[m_aut.get_transitions()
                                                                                                                 [*splitter->start_same_BLC].from()].block==B);
      }
      std::vector<transition>::iterator current_U_incoming_transition_iterator;
      std::vector<transition>::iterator
                                    current_U_incoming_transition_iterator_end; assert(M_it <= splitter_end_unmarked_BLC);
      state_in_block_pointer current_U_outgoing_state;
      outgoing_transitions_it current_U_outgoing_transition_iterator;
      outgoing_transitions_it current_U_outgoing_transition_iterator_end;
      std::vector<transition>::iterator current_R_incoming_transition_iterator;
      state_in_block_pointer* current_R_incoming_bottom_state_iterator=
                                                        B->start_bottom_states; assert(current_R_incoming_bottom_state_iterator<=first_unmarked_bottom_state);
      std::vector<transition>::iterator
                                    current_R_incoming_transition_iterator_end; assert(current_R_incoming_bottom_state_iterator<first_unmarked_bottom_state ||
                                                                                       !m_R.empty() || M_it<splitter_end_unmarked_BLC);
      state_in_block_pointer* current_U_incoming_bottom_state_iterator=
                                                   first_unmarked_bottom_state; assert(current_U_incoming_bottom_state_iterator<B->sta.rt_non_bottom_states);
      const std::make_signed<state_index>::type max_R_nonbottom_size=
                    number_of_states_in_block(*B)/2-
                                    std::distance(B->start_bottom_states,
                                                  first_unmarked_bottom_state); // can underflow
      if (max_R_nonbottom_size <
                  static_cast<std::make_signed<state_index>::type>(m_R.size()))
      {                                                                         assert(number_of_states_in_block(*B)/2 < std::distance(
                                                                                      B->start_bottom_states, first_unmarked_bottom_state)+m_R.size());
        R_status = (M_it == splitter_end_unmarked_BLC)
                   ? aborted_after_initialisation : aborted;
      }
      else
      {                                                                         assert(number_of_states_in_block(*B)/2 >= std::distance(
                                                                                      B->start_bottom_states, first_unmarked_bottom_state)+m_R.size());
        if (B->sta.rt_non_bottom_states==B->end_states)
        {                                                                       assert(B->start_bottom_states<first_unmarked_bottom_state);
          /* There are no non-bottom states, hence we do not need to carry */   assert(std::distance(B->start_bottom_states,
          /* out the tau closure. */                                                                 first_unmarked_bottom_state) <=
          /* Also, there cannot be any new bottom states. */                          std::distance(first_unmarked_bottom_state, B->sta.rt_non_bottom_states));
                                                                                assert(m_R.empty()); // m_R.clear(); is superfluous
                                                                                assert(m_U.empty()); // m_U.clear(); is superfluous;
                                                                                assert(m_U_counter_reset_vector.empty()); // clear_state_counters(); is superfluous
          // split_block B into R and B\R.
          ptr_to_new_block=split_block_B_into_R_and_BminR<initialisation>
                 (B, B->start_bottom_states, first_unmarked_bottom_state, m_R);
          return ptr_to_new_block;
        }
        else if (M_it==splitter_end_unmarked_BLC)
        {
          // There are no more transitions in the splitter whose source states
          // need to be added to R.
                                                                                //assert(B->start_bottom_states < first_unmarked_bottom_state || !m_R.empty());
          R_status=state_checking;
        }
      }
      const std::make_signed<state_index>::type max_U_nonbottom_size=
                  number_of_states_in_block(*B)/2-
                  std::distance(first_unmarked_bottom_state,
                                B->sta.rt_non_bottom_states); // can underflow
      if (max_U_nonbottom_size<0)
      {                                                                         assert(static_cast<std::make_signed<state_index>::type>
                                                                                                (number_of_states_in_block(*B)/2) <
                                                                                std::distance(first_unmarked_bottom_state, B->sta.rt_non_bottom_states));
        U_status=aborted_after_initialisation;                                  assert(aborted != R_status); assert(aborted_after_initialisation != R_status);
      }
      else
      {                                                                         assert(static_cast<std::make_signed<state_index>::type>
                                                                                                (number_of_states_in_block(*B)/2) >=
                                                                                      std::distance(first_unmarked_bottom_state, B->sta.rt_non_bottom_states));
        if (B->sta.rt_non_bottom_states==B->end_states)
        {                                                                       assert(first_unmarked_bottom_state<B->sta.rt_non_bottom_states);
          /* There are no non-bottom states, hence we do not need to carry */   assert(std::distance(first_unmarked_bottom_state,
          /* out the tau closure.                                          */                        B->sta.rt_non_bottom_states) <=
          /* Also, there cannot be any new bottom states.                  */              std::distance(B->start_bottom_states, first_unmarked_bottom_state));
                                                                                assert(m_R.empty()); // m_R.clear(); is superfluous
                                                                                assert(m_U.empty()); // m_U.clear(); is superfluous;
                                                                                assert(m_U_counter_reset_vector.empty()); // clear_state_counters(); is superfluous
          // split_block B into U and B\U.
          ptr_to_new_block=split_block_B_into_R_and_BminR<initialisation>
                          (B, first_unmarked_bottom_state, B->end_states, m_U);
          return B;
        }
      }                                                                         assert(B->sta.rt_non_bottom_states<B->end_states);
      label_index a=null_action;
      constellation_type* C;
      if constexpr (!initialisation)
      {                                                                         assert(splitter->start_same_BLC<splitter->end_same_BLC);
        const transition& first_t=
                            m_aut.get_transitions()[*splitter->start_same_BLC];
        a=label_or_divergence(first_t);
        C=m_states[first_t.to()].block->c.onstellation;
      }                                                                         else{assert(state_checking==R_status||aborted_after_initialisation==R_status);}
                                                                                #ifndef NDEBUG
                                                                                  if constexpr (!initialisation)
                                                                                  {
                                                                                    if (initializing==R_status || aborted==R_status)
                                                                                    {
                                                                                      // For constellation-inert splitters (which only happens for the special
      /* Algorithm 3, line 3.2 left.                                         */       // split to separate new from old bottom states), one has to mark all
                                                                                      // transitions in the splitter.
      /* start coroutines. Each co-routine handles one state, and then gives */       assert(!m_aut.is_tau(a) || B->c.onstellation != C);
      /* control to the other co-routine. The coroutines can be found        */     }
      /* sequentially below surrounded by a while loop.                      */   }
                                                                                #endif
//std::cerr << "simple_splitB() before while\n";
      while (true)
      {                                                                         assert(U_status!=aborted_after_initialisation ||
                                                                                       (R_status!=aborted && R_status!=aborted_after_initialisation));
                                                                                #ifndef NDEBUG
                                                                                  for(state_in_block_pointer si=state_in_block_pointer(m_states.begin()); si.ref_state<m_states.end(); ++si.ref_state)
                                                                                  {
                                                                                    if (si.ref_state->block!=B || 0==si.ref_state->no_of_outgoing_block_inert_transitions)
                                                                                    {
                                                                                      assert((initialisation &&
                                                                                              0!=si.ref_state->no_of_outgoing_block_inert_transitions) ||
                                                                                             undefined==si.ref_state->counter);
                                                                                      assert(!m_R.find(si));
                                                                                      assert(!m_U.find(si));
                                                                                      assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), si) == m_U_counter_reset_vector.end());
                                                                                    }
                                                                                    else
                                                                                    {
                                                                                      switch(si.ref_state->counter)
                                                                                      {
                                                                                      case undefined:  assert(!m_U.find(si)); assert(!m_R.find(si));
                                                                                                       assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), si) == m_U_counter_reset_vector.end());
                                                                                                       break;
                                                                                      case Rmarked:    assert( m_R.find(si)); assert(!m_U.find(si));
                                                                                                       // It can happen that the state has a tau-transition
                                                                                                       // to a U-state, then it will be in the
                                                                                                       // m_U_counter_reset_vector.
                                                                                                       break;
                                                                                      case Umarked:    assert(!m_R.find(si)); // It can happen that the state
                                                                                                                              // is in U or is not in U
                                                                                                       assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), si) != m_U_counter_reset_vector.end());
                                                                                                       break;
                                                                                      default:         assert(!m_R.find(si)); assert(!m_U.find(si));
                                                                                                       assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), si) != m_U_counter_reset_vector.end());
                                                                                                       break;
                                                                                      }
                                                                                    }
        /* The code for the right co-routine.                                */   }
                                                                                #endif
        if (incoming_inert_transition_checking==R_status) // 18178 times (large 1394-fin.lts example: 372431 times)
        {                                                                       assert(current_R_incoming_transition_iterator <
                                                                                                                    current_R_incoming_transition_iterator_end);
                                                                                mCRL2complexity(&m_transitions[std::distance(m_aut.get_transitions().begin(), current_R_incoming_transition_iterator)],
                                                                                              add_work(check_complexity::simple_splitB_R__handle_transition_to_R_state, 1), *this);
                                                                                assert(m_aut.is_tau(m_aut_apply_hidden_label_map(current_R_incoming_transition_iterator->label())));
                                                                                assert(m_states[current_R_incoming_transition_iterator->to()].block==B);
          const transition& tr=*current_R_incoming_transition_iterator;
          if (m_states[tr.from()].block==B &&
              !(m_preserve_divergence && tr.from() == tr.to()))
          {
            if (m_states[tr.from()].counter!=Rmarked)
            {                                                                   assert(!m_R.find(m_states.begin() + tr.from()));
//std::cerr << "R_todo2 insert: " << tr.from() << "\n";
              m_R.add_todo(m_states.begin() + tr.from());
              m_states[tr.from()].counter=Rmarked;
 
              // Algorithm 3, line 3.10 and line 3.11, right.
              if (m_R.size()>static_cast<state_index>(max_R_nonbottom_size))
              {                                                                 assert(aborted_after_initialisation!=U_status);
                R_status=aborted_after_initialisation;
                goto R_handled_and_is_not_state_checking;
              }
            }                                                                   else  {  assert(m_R.find(m_states.begin() + tr.from()));  }
                                                                                assert(!m_U.find(m_states.begin() + tr.from()));
          }
          ++current_R_incoming_transition_iterator;
          if (current_R_incoming_transition_iterator!=
                                  current_R_incoming_transition_iterator_end &&
              m_aut.is_tau(m_aut_apply_hidden_label_map
                            (current_R_incoming_transition_iterator->label())))
          {
            goto R_handled_and_is_not_state_checking;
          }
          R_status=state_checking;
        }
        else if (state_checking==R_status) // 18014 times (large 1394-fin.lts example: 331708 times)
        {
          const state_in_block_pointer s=
                  (current_R_incoming_bottom_state_iterator<
                                                    first_unmarked_bottom_state
                                  ? *current_R_incoming_bottom_state_iterator++
                                  : m_R.move_from_todo());
                                                                                mCRL2complexity(s.ref_state, add_work(check_complexity::simple_splitB_R__find_predecessors, 1), *this);
//std::cerr << "R insert: " << s.ref_state->debug_id(*this) << "\n";
                                                                                assert(s.ref_state->block==B);
          if (std::next(s.ref_state)==m_states.end())
          {
            current_R_incoming_transition_iterator_end=
                                                 m_aut.get_transitions().end();
          }
          else
          {
            current_R_incoming_transition_iterator_end=
                            std::next(s.ref_state)->start_incoming_transitions;
          }
          current_R_incoming_transition_iterator=
                                       s.ref_state->start_incoming_transitions;
          if (current_R_incoming_transition_iterator!=
                                  current_R_incoming_transition_iterator_end &&
              m_aut.is_tau(m_aut_apply_hidden_label_map
                            (current_R_incoming_transition_iterator->label())))
          {
            R_status=incoming_inert_transition_checking;
            goto R_handled_and_is_not_state_checking;
          }
        }
        else if (initializing!=R_status)
        {
                                                                                assert(aborted_after_initialisation==R_status || // 10280 times (large 1394-fin.lts example: 550 times)
                                                                                       aborted==R_status); // 663 times (large 1394-fin.lts example: 584 times)
          goto R_handled_and_is_not_state_checking;
        }
        else // initializing==R_status: 2742 times (large 1394-fin.lts example: 1200 times)
        {                                                                       assert(M_it<splitter_end_unmarked_BLC);
            // Algorithm 3, line 3.3, right.
          const state_in_block_pointer
                    si(m_states.begin()+m_aut.get_transitions()[*M_it].from()); mCRL2complexity(&m_transitions[*M_it], add_work(check_complexity::
                                                                                                   simple_splitB_R__handle_transition_from_R_state, 1), *this);
                                                                                assert(si.ref_state->block==B);
                                                                                assert(!is_inert_during_init(m_aut.get_transitions()[*M_it]) ||
                                                                                       B->c.onstellation!=
                                                                                          m_states[m_aut.get_transitions()[*M_it].to()].block->c.onstellation);
          ++M_it;
          if (0==si.ref_state->no_of_outgoing_block_inert_transitions)
          {                                                                     assert(B->start_bottom_states<=si.ref_state->ref_states_in_blocks);
            /* The state is a bottom state, it should be in R already */        assert(si.ref_state->ref_states_in_blocks<first_unmarked_bottom_state);
                                                                                assert(!m_R.find(si));
          }
          else if (si.ref_state->counter!=Rmarked)
          {                                                                     assert(B->sta.rt_non_bottom_states<=si.ref_state->ref_states_in_blocks);
            /* The state is a nonbottom state that is not yet in R */           assert(si.ref_state->ref_states_in_blocks<B->end_states);
            m_R.add_todo(si);
            si.ref_state->counter=Rmarked;
//std::cerr << "R_todo1 insert: " << si.ref_state->debug_id(*this) << "\n";
            if (m_R.size()>static_cast<state_index>(max_R_nonbottom_size))
            {                                                                   assert(aborted_after_initialisation!=U_status);
              R_status=aborted;
              goto R_handled_and_is_not_state_checking;
            }
          }                                                                     else  {  assert(m_R.find(si));  }
                                                                                assert(!m_U.find(si));
          if (M_it!=splitter_end_unmarked_BLC)
          {
            goto R_handled_and_is_not_state_checking;
          }                                                                     assert(B->sta.rt_non_bottom_states<B->end_states);
          R_status=state_checking;
        }                                                                       assert(state_checking==R_status);
        if (current_R_incoming_bottom_state_iterator==
                            first_unmarked_bottom_state && m_R.todo_is_empty())
        {                                                                       assert(0 < std::distance(B->start_bottom_states,
                                                                                                                    first_unmarked_bottom_state) + m_R.size());
//std::cerr << "R empty: " << "\n";
          /* split_block B into R and B\R. */                                   assert(std::distance(B->start_bottom_states, first_unmarked_bottom_state) +
                                                                                                                m_R.size() <= number_of_states_in_block(*B)/2);
          ptr_to_new_block=split_block_B_into_R_and_BminR
             <initialisation>(B, B->start_bottom_states,
                                    first_unmarked_bottom_state, m_R);
          clear_state_counters();
          m_R.clear();
          m_U.clear();
          return ptr_to_new_block;
        }
    R_handled_and_is_not_state_checking:                                        assert(state_checking!=R_status ||
                                                                                       current_R_incoming_bottom_state_iterator!=first_unmarked_bottom_state ||
                                                                                       !m_R.todo_is_empty());
                                                                                #ifndef NDEBUG
                                                                                  for (state_in_block_pointer si=state_in_block_pointer(m_states.begin());
                                                                                                                   si.ref_state<m_states.end(); ++si.ref_state)
                                                                                  {
                                                                                    if (si.ref_state->block!=B ||
                                                                                        0==si.ref_state->no_of_outgoing_block_inert_transitions)
                                                                                    {
                                                                                      assert((initialisation &&
                                                                                              0!=si.ref_state->no_of_outgoing_block_inert_transitions) ||
                                                                                             undefined==si.ref_state->counter);
                                                                                      assert(!m_R.find(si));
                                                                                      assert(!m_U.find(si));
                                                                                      assert(std::find(m_U_counter_reset_vector.begin(),
                                                                                          m_U_counter_reset_vector.end(), si)==m_U_counter_reset_vector.end());
                                                                                    }
                                                                                    else
                                                                                    {
                                                                                      switch(si.ref_state->counter)
                                                                                      {
                                                                                      case undefined:  assert(!m_U.find(si)); assert(!m_R.find(si));
                                                                                                       assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), si) == m_U_counter_reset_vector.end());
                                                                                                       break;
                                                                                      case Rmarked:    assert( m_R.find(si)); assert(!m_U.find(si));
                                                                                                       // It can happen that the state has a tau-transition
                                                                                                       // to a U-state, then it will be in the
                                                                                                       // m_U_counter_reset_vector.
                                                                                                       break;
                                                                                      case Umarked:    assert(!m_R.find(si)); // It can happen that the state
                                                                                                                              // is in U or is not in U
                                                                                                       assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), si) != m_U_counter_reset_vector.end());
                                                                                                       break;
                                                                                      default:         assert(!m_R.find(si)); assert(!m_U.find(si));
                                                                                                       assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), si) != m_U_counter_reset_vector.end());
                                                                                                       break;
                                                                                      }
                                                                                    }
                                                                                  }
                                                                                #endif
        // The code for the left co-routine.
        if (incoming_inert_transition_checking==U_status) // 20299 times (large 1394-fin.lts example: 360327 times)
        {                                                                       assert(current_U_incoming_transition_iterator<
                                                                                                                   current_U_incoming_transition_iterator_end);
//std::cerr << "U_incoming_inert_transition_checking\n";
            /* Algorithm 3, line 3.8, left.                                  */ assert(m_aut.is_tau(m_aut_apply_hidden_label_map
                                                                                                           (current_U_incoming_transition_iterator->label())));
            /* Check one incoming transition.                                */ mCRL2complexity(&m_transitions[std::distance(m_aut.get_transitions().begin(),
            /* Algorithm 3, line 3.12, left.                                 */                                       current_U_incoming_transition_iterator)],
                                                                                                add_work(check_complexity::
                                                                                                     simple_splitB_U__handle_transition_to_U_state, 1), *this);
          current_U_outgoing_state=state_in_block_pointer(m_states.begin()+
                               current_U_incoming_transition_iterator->from()); assert(m_states[current_U_incoming_transition_iterator->to()].block==B);
          current_U_incoming_transition_iterator++;
//std::cerr << "FROM " << std::distance(m_states.begin(), current_U_outgoing_state.ref_state) << "\n";
          if (current_U_outgoing_state.ref_state->block==B &&
              !(m_preserve_divergence &&
                std::prev(current_U_incoming_transition_iterator)->from()==
                std::prev(current_U_incoming_transition_iterator)->to()))
          {                                                                     assert(!m_U.find(current_U_outgoing_state));
            if (current_U_outgoing_state.ref_state->counter!=Rmarked)
            {
              if (current_U_outgoing_state.ref_state->counter==undefined)
              {
                  // Algorithm 3, line 3.13, left.
                  // Algorithm 3, line 3.15 and 3.18, left.
                current_U_outgoing_state.ref_state->counter=Umarked-1+
                            current_U_outgoing_state.ref_state->
                                        no_of_outgoing_block_inert_transitions;
                m_U_counter_reset_vector.push_back(current_U_outgoing_state);
              }
              else
              {                                                                 assert(std::find(m_U_counter_reset_vector.begin(),
                                                                                                 m_U_counter_reset_vector.end(),
                                                                                                 current_U_outgoing_state) != m_U_counter_reset_vector.end());
                /* Algorithm 3, line 3.18, left. */                             assert(current_U_outgoing_state.ref_state->counter>Umarked);
                current_U_outgoing_state.ref_state->counter--;
              }
//std::cerr << "COUNTER " << current_U_outgoing_state.ref_state->counter << "\n";
                // Algorithm 3, line 3.19, left.
              if (current_U_outgoing_state.ref_state->counter==Umarked)
              {
                if (initializing==R_status || aborted==R_status)
                {
                  // Start searching for an outgoing transition with action a
                  // to constellation C.
                  current_U_outgoing_transition_iterator=
                              current_U_outgoing_state.ref_state->
                                                    start_outgoing_transitions; assert(m_outgoing_transitions.begin()<=current_U_outgoing_transition_iterator);
                                                                                assert(current_U_outgoing_transition_iterator<m_outgoing_transitions.end());
                  current_U_outgoing_transition_iterator_end=
                      (std::next(current_U_outgoing_state.ref_state)>=
                                                                m_states.end()
                          ? m_outgoing_transitions.end()
                          : std::next(current_U_outgoing_state.ref_state)->
                                                   start_outgoing_transitions); assert(current_U_outgoing_transition_iterator<
                                                                                                                    current_U_outgoing_transition_iterator_end);
                                                                                assert(m_states.begin()+m_aut.get_transitions()[*current_U_outgoing_transition_iterator->ref.BLC_transitions].from()==current_U_outgoing_state.ref_state);
                  U_status=outgoing_action_constellation_check;
                  goto U_handled_and_is_not_state_checking;
                }
                    // The state can be added to U_todo immediately.
                                                                                #ifndef NDEBUG
                                                                                  if constexpr (!initialisation)
                                                                                  {
                                                                                    // check that the state has no transition in the splitter
                                                                                    const outgoing_transitions_it out_it_end =
                                                                                          std::next(current_U_outgoing_state.ref_state)>=m_states.end()
                                                                                                ? m_outgoing_transitions.end()
                                                                                                : std::next(current_U_outgoing_state.ref_state)->
                                                                                                                                    start_outgoing_transitions;
                                                                                    for (outgoing_transitions_it out_it=current_U_outgoing_state.ref_state->
                                                                                                                                    start_outgoing_transitions;
                                                                                             out_it<out_it_end; ++out_it)
                                                                                    {
                                                                                      assert(m_outgoing_transitions.begin()<=out_it);
                                                                                      assert(out_it<m_outgoing_transitions.end());
                                                                                      assert(m_BLC_transitions.data()<=out_it->ref.BLC_transitions);
                                                                                      assert(out_it->ref.BLC_transitions<m_BLC_transitions.data_end());
                                                                                      /* assert(0<=*out_it->ref.BLC_transitions); Always true */
                                                                                      assert(*out_it->ref.BLC_transitions<m_aut.num_transitions());
                                                                                      assert(m_transitions[*out_it->ref.BLC_transitions].ref_outgoing_transitions==out_it);
                                                                                      const transition& t=m_aut.get_transitions()[*out_it->ref.BLC_transitions];
                                                                                      assert(m_states.begin()+t.from()==current_U_outgoing_state.ref_state);
                                                                                      if (a==label_or_divergence(t) &&
                                                                                          C==m_states[t.to()].block->c.onstellation)
                                                                                      {
                                                                                            // The transition is in the splitter, so it must be in the part of the splitter that is disregarded.
//std::cerr << "State " << std::distance(m_states.begin(), current_U_outgoing_state.ref_state) << " has a transition in the splitter, namely " << m_transitions[*out_it->ref.BLC_transitions].debug_id_short(*this) << '\n';
                                                                                        assert(out_it->ref.BLC_transitions>=splitter_end_unmarked_BLC);
                                                                                        assert(splitter->start_same_BLC<=out_it->ref.BLC_transitions);
                                                                                        assert(out_it->ref.BLC_transitions<splitter->end_same_BLC);
                                                                                      }
                                                                                    }
                                                                                  }
                                                                                #endif
                m_U.add_todo(current_U_outgoing_state);
                    // Algorithm 3, line 3.10 and line 3.11 left.
                if (m_U.size()>static_cast<state_index>(max_U_nonbottom_size))
                {                                                               assert(aborted!=R_status); assert(aborted_after_initialisation!=R_status);
                  U_status=aborted_after_initialisation;
                  goto U_handled_and_is_not_state_checking;
                }
              }
            }                                                                   else  {  assert(m_R.find(current_U_outgoing_state));  }
          }
          if (current_U_incoming_transition_iterator!=
                                  current_U_incoming_transition_iterator_end &&
                m_aut.is_tau(m_aut_apply_hidden_label_map(
                             current_U_incoming_transition_iterator->label())))
          {                                                                     assert(incoming_inert_transition_checking==U_status);
            goto U_handled_and_is_not_state_checking;
          }
          U_status=state_checking;
        }
        else if (state_checking==U_status) // 18920 times (large 1394-fin.lts example: 340893 times)
        {
//std::cerr << "U_state_checking\n";
 
            // Algorithm 3, line 3.23 and line 3.24, left.
          const state_in_block_pointer s=
                          (current_U_incoming_bottom_state_iterator<
                                                    B->sta.rt_non_bottom_states
                               ? *current_U_incoming_bottom_state_iterator++
                               : m_U.move_from_todo());                         assert(!m_R.find(s));
                                                                                mCRL2complexity(s.ref_state, add_work(check_complexity::simple_splitB_U__find_predecessors, 1), *this);
//std::cerr << "U insert/ U_todo_remove: " << s.ref_state->debug_id(*this) << "\n";
          current_U_incoming_transition_iterator=
                                       s.ref_state->start_incoming_transitions;
          current_U_incoming_transition_iterator_end=
                        (std::next(s.ref_state)>=m_states.end()
                         ? m_aut.get_transitions().end()
                         : std::next(s.ref_state)->start_incoming_transitions);
          if (current_U_incoming_transition_iterator!=
                                  current_U_incoming_transition_iterator_end &&
              m_aut.is_tau(m_aut_apply_hidden_label_map(
                             current_U_incoming_transition_iterator->label())))
          {
            U_status=incoming_inert_transition_checking;
            goto U_handled_and_is_not_state_checking;
          }
        }
        else if (initialisation ||
                 aborted_after_initialisation==U_status) // 6284 times (large 1394-fin.lts example: 2500 times)
        {                                                                       assert(aborted_after_initialisation==U_status);
          goto U_handled_and_is_not_state_checking;
        }
        else if constexpr (!initialisation) // the condition holds always
        {                                                                       assert(outgoing_action_constellation_check==U_status); // 911 times (large 1394-fin.lts example: 912 times)
//std::cerr << "U_outgoing_action_constellation_check\n";
                                                                                assert(current_U_outgoing_transition_iterator!=
                                                                                                                   current_U_outgoing_transition_iterator_end);
                                                                                  // will only be used if the transitions are not constellation-inert:
                                                                                assert(!m_aut.is_tau(a) || B->c.onstellation!=C);
                                                                                assert(splitter_end_unmarked_BLC==splitter->start_marked_BLC);
                                                                                mCRL2complexity((&m_transitions[*current_U_outgoing_transition_iterator->ref.BLC_transitions]), add_work(check_complexity::simple_splitB_U__handle_transition_from_potential_U_state, 1), *this);
                                                                                #ifndef NDEBUG
                                                                                  // This is one step in the coroutine, so we should assign the work to exactly one transition.
                                                                                  // But to make sure, we also mark the other transitions that we skipped in the optimisation.
                                                                                  for (outgoing_transitions_it out_it=current_U_outgoing_transition_iterator; out_it<current_U_outgoing_transition_iterator->start_same_saC; )
                                                                                  {
                                                                                    ++out_it;
                                                                                    mCRL2complexity(&m_transitions[*out_it->ref.BLC_transitions], add_work_notemporary(check_complexity::simple_splitB_U__handle_transition_from_potential_U_state, 1), *this);
                                                                                  }
                                                                                #endif
          const transition& t_local=m_aut.get_transitions()
                [*current_U_outgoing_transition_iterator->ref.BLC_transitions];
          current_U_outgoing_transition_iterator= // This is an optimisation.
                        current_U_outgoing_transition_iterator->start_same_saC;
          ++current_U_outgoing_transition_iterator;                             assert(m_states.begin()+t_local.from()==current_U_outgoing_state.ref_state);
                                                                                assert(m_branching);
          if (m_states[t_local.to()].block->c.onstellation==C &&
              label_or_divergence(t_local) == a)
          {
                // This state must be blocked.
          }
          else if (current_U_outgoing_transition_iterator==
                                    current_U_outgoing_transition_iterator_end)
          {                                                                     assert(!m_U.find(current_U_outgoing_state));
//std::cerr << "U_todo4 insert: " << std::distance(m_states.begin(), current_U_outgoing_state.ref_state) << "   " << m_U.size() << "    " << number_of_states_in_block(*B) << "\n";
            m_U.add_todo(current_U_outgoing_state);
              // Algorithm 3, line 3.10 and line 3.11 left.
            if (m_U.size()>static_cast<state_index>(max_U_nonbottom_size))
            {                                                                   assert(aborted!=R_status); assert(aborted_after_initialisation!=R_status);
              U_status=aborted_after_initialisation;
              goto U_handled_and_is_not_state_checking;
            }
          }
          else
          {
            goto U_handled_and_is_not_state_checking;
          }
 
          if (current_U_incoming_transition_iterator!=
                                  current_U_incoming_transition_iterator_end &&
              m_aut.is_tau(m_aut_apply_hidden_label_map(
                             current_U_incoming_transition_iterator->label())))
          {
            U_status = incoming_inert_transition_checking;
            goto U_handled_and_is_not_state_checking;
          }
          U_status=state_checking;
        }                                                                       else  {  assert(0);  }
                                                                                assert(state_checking==U_status);
        if (current_U_incoming_bottom_state_iterator==
                            B->sta.rt_non_bottom_states && m_U.todo_is_empty())
        {
          // split_block B into U and B\U.
//std::cerr << "U_todo empty:\n";
                                                                                assert(0 < std::distance(first_unmarked_bottom_state,
                                                                                                                    B->sta.rt_non_bottom_states) + m_U.size());
                                                                                assert(std::distance(first_unmarked_bottom_state, B->sta.rt_non_bottom_states)+
                                                                                                                 m_U.size() <= number_of_states_in_block(*B)/2);
          ptr_to_new_block=split_block_B_into_R_and_BminR<initialisation>
            (B, first_unmarked_bottom_state, B->sta.rt_non_bottom_states, m_U);
          clear_state_counters();
          m_R.clear();
          m_U.clear();
          return B;
        }
    U_handled_and_is_not_state_checking:                                        assert(state_checking!=U_status ||
                                                                                       current_U_incoming_bottom_state_iterator!=B->sta.rt_non_bottom_states ||
                                                                                       !m_U.todo_is_empty());
      }                                                                         assert(0);
    }
 
    // Mark all states that are sources of the marked transitions in splitter
    // and move them to the beginning.
    // (Marking of bottom states is done by moving them to the beginning of the
    // bottom states. Marking of non-bottom states is done by adding them to m_R
    // and setting m_states[*].counter = Rmarked.)
    // Also make the splitter stable and move it to the beginning of the respective
    // list of BLC sets.
    // If all bottom states are marked, reset markers and m_R.
    // Otherwise, if not all
    // bottom states are touched, leave the marked non-bottom states in m_R and leave
    // the markers in m_states[*].counter in place.
    // The marked bottom states are moved to the front in m_states_in_blocks and
    // the return value indicates the position (in m_states_in_blocks)
    // of the first non-marked bottom state.
    [[nodiscard]]
    state_in_block_pointer*
    not_all_bottom_states_are_touched(
            block_type* const bi,
            linked_list<BLC_indicators>::iterator splitter
                                                                                #ifndef NDEBUG
                                                                                  , const BLC_list_const_iterator splitter_end_unmarked_BLC
                                                                                    // = splitter->start_marked_BLC -- this default argument is not allowed
                                                                                #endif
            )
    {                                                                           assert(!splitter->is_stable());
//std::cerr << "not_all_bottom_states_are_touched(" << bi << ',' << splitter->debug_id(*this) << ")\n";
                                                                                assert(bi==
                                                                                    m_states[m_aut.get_transitions()[*splitter->start_same_BLC].from()].block);
                                                                                assert(splitter_end_unmarked_BLC<=splitter->start_marked_BLC);
      block_type& B=*bi;                                                        assert(m_R.empty());  assert(m_U.empty());
                                                                                assert(1 < number_of_states_in_block(B));
                                                                                // If the above assertion is false, one can just: return B.end_states;
      state_in_block_pointer*first_unmarked_bottom_state=B.start_bottom_states; assert(!B.contains_new_bottom_states);
      // Now go through the marked transitions in detail:
      BLC_list_iterator marked_t_it = splitter->start_marked_BLC;
      for(; marked_t_it<splitter->end_same_BLC; ++marked_t_it)
      {
        const transition& t = m_aut.get_transitions()[*marked_t_it];            // mCRL2complexity(&m_transitions[*marked_t_it], add_work(...), *this);
                                                                                    // not needed as this work can be attributed to marking of the transition
        const state_in_block_pointer s(m_states.begin()+t.from());
        state_in_block_pointer* const pos_s=s.ref_state->ref_states_in_blocks;  assert(B.start_bottom_states<=pos_s);  assert(pos_s<B.end_states);
        if (first_unmarked_bottom_state<=pos_s)
        {
          if (0==s.ref_state->no_of_outgoing_block_inert_transitions)
          {                                                                     assert(pos_s<B.sta.rt_non_bottom_states);
            swap_states_in_states_in_block(first_unmarked_bottom_state, pos_s); assert(undefined==s.ref_state->counter);
            first_unmarked_bottom_state++;
          }
          else if (Rmarked!=s.ref_state->counter)
          {                                                                     assert(B.sta.rt_non_bottom_states<=pos_s);
            m_R.add_todo(s);                                                    assert(undefined==s.ref_state->counter);
            s.ref_state->counter=Rmarked;
          }
        }
      }
                                                                                #ifndef NDEBUG
                                                                                  // ensure that the unmarked transitions do not add any bottom states.
                                                                                  assert(splitter->start_same_BLC <= splitter_end_unmarked_BLC);
                                                                                  for(BLC_list_const_iterator i = splitter->start_same_BLC; i < splitter_end_unmarked_BLC; ++i)
                                                                                  {
                                                                                    assert(splitter_end_unmarked_BLC == splitter->start_marked_BLC);
                                                                                    const transition& t = m_aut.get_transitions()[*i];
                                                                                    const state_in_block_pointer s(m_states.begin()+t.from());
                                                                                    assert(s.ref_state->block == bi);
                                                                                    const state_in_block_pointer*const pos_s=s.ref_state->ref_states_in_blocks;
                                                                                    assert(*pos_s==s);
                                                                                    assert(B.start_bottom_states <= pos_s);
                                                                                    assert(pos_s < B.end_states);
                                                                                    if (0==s.ref_state->no_of_outgoing_block_inert_transitions)
                                                                                    {
                                                                                      // State s is a bottom state. It should already have been marked.
                                                                                      assert(pos_s<first_unmarked_bottom_state);
                                                                                    }
                                                                                    else
                                                                                    {
                                                                                      assert(B.sta.rt_non_bottom_states <= pos_s);
                                                                                    }
                                                                                  }
                                                                                #endif
      if (first_unmarked_bottom_state==B.sta.rt_non_bottom_states)
      {
        // All bottom states are marked. No splitting is possible. Reset m_R,
        // m_states[s].counter for s in m_R.
        clear_state_counters(true);
        m_R.clear();
      }
      return first_unmarked_bottom_state;
    }
 
    void make_transition_non_block_inert(const transition& t)
    {                                                                           assert(is_inert_during_init(t));
                                                                                assert(m_states[t.to()].block!=m_states[t.from()].block);
      m_states[t.from()].no_of_outgoing_block_inert_transitions--;              assert(no_of_constellations<=1 /* initialisation */ ||
                                                                                       m_states[t.to()].block->c.onstellation ==
                                                                                                                     m_states[t.from()].block->c.onstellation);
//std::cerr << "    " << m_transitions[std::distance<const transition *>(m_aut.get_transitions().data(), &t)].debug_id(*this) << " has become non-block-inert\n";
    }
#endif
 
    void change_non_bottom_state_to_bottom_state(
                                const fixed_vector<state_type_gj>::iterator si)
    {                                                                           assert(m_states.begin()<=si);
//std::cerr << "change_non_bottom_state_to_bottom_state(" << si->debug_id(*this) << ")\n";
      block_type* bi = si->block;                                               assert(si<m_states.end());
      swap_states_in_states_in_block(si->ref_states_in_blocks,
                                                 bi->sta.rt_non_bottom_states); assert(0 == si->no_of_outgoing_block_inert_transitions);
      bi->sta.rt_non_bottom_states++;                                           assert(!bi->contains_new_bottom_states);
      ++no_of_new_bottom_states;
    }
 
    void make_stable_and_move_to_start_of_BLC(block_type* const from_block,
                          const linked_list<BLC_indicators>::iterator splitter)
    {                                                                           assert(from_block->block.to_constellation.end()!=splitter);
      splitter->make_stable();                                                  assert(splitter->start_same_BLC<splitter->end_same_BLC);
                                                                                #ifndef NDEBUG
                                                                                  const transition& t=m_aut.get_transitions()[*splitter->start_same_BLC];
                                                                                  assert(from_block==m_states[t.from()].block);
                                                                                #endif
      linked_list<BLC_indicators>& btc=from_block->block.to_constellation;      assert(!btc.empty());
      if (splitter!=btc.begin())
      {
        linked_list<BLC_indicators>::iterator move_splitter_after=btc.end();
        if (m_branching)
        {                                                                       // The following assertion may fail because we sometimes make a splitter
          const transition& perhaps_inert_t=                                    // stable before all BLC sets are split:
                         m_aut.get_transitions()[*btc.begin()->start_same_BLC]; // assert(m_states[perhaps_inert_t.from()].block==from_block);
          if (is_inert_during_init_if_branching(perhaps_inert_t) &&
              m_states[perhaps_inert_t.to()].block->c.onstellation==
                                                    from_block->c.onstellation)
          {
            move_splitter_after=btc.begin();
          }
        }
        btc.splice_to_after(move_splitter_after, btc, splitter);
      }
    }
 
#ifndef USE_FOUR_WAY_SPLIT
    template<bool initialisation, class Iterator>
    inline constellation_type* target_constellation(Iterator splitter) const
    {
      if constexpr (initialisation)
      {                                                                         assert(0);
        return nullptr;
      }
      else
      {
        return m_states[m_aut.get_transitions()
                       [*splitter->start_same_BLC].to()].block->c.onstellation;
      }
    }
 
    template <bool initialisation=false,
              class Iterator=linked_list<BLC_indicators>::iterator>
    block_type* splitB(block_type* const B,
                      Iterator splitter,
                      state_in_block_pointer* first_unmarked_bottom_state,
                      const BLC_list_iterator splitter_end_unmarked_BLC
                                    /* =splitter->start_marked_BLC -- but
                                       this default argument is not allowed */,
                      block_type*& bi,
                      constellation_type* const old_constellation,
                      constellation_type* const new_constellation,
                      const bool split_off_new_bottom_states=true)
    {
//std::cerr << (initialisation ? "splitB<true>(" : "splitB(") << B->debug_id(*this) << ", splitter==";
//if constexpr (!initialisation) { std::cerr << splitter->debug_id(*this); }
//else { std::cerr << splitter; }
//std::cerr << ", first_unmarked_bottom_state==" << first_unmarked_bottom_state->ref_state->debug_id(*this) << ", splitter_end_unmarked_BLC==";
//if constexpr (!initialisation) { std::cerr << (split_off_new_bottom_states && splitter_end_unmarked_BLC == splitter->start_marked_BLC ? "start_marked_BLC" : (splitter_end_unmarked_BLC == splitter->start_same_BLC ? "start_same_BLC" : "?")); }
//else { std::cerr << splitter_end_unmarked_BLC; }
//std::cerr << ", old_constellation==" << old_constellation->debug_id(*this) << ", split_off_new_bottom_states==" << split_off_new_bottom_states << ")\n";
//std::cerr << (m_branching ? "Marked bottom states:" : "Marked states:"); for (const state_in_block_pointer* it=B->start_bottom_states; it!=first_unmarked_bottom_state; ++it) { std::cerr << ' ' << std::distance(m_states.begin(), it->ref_state); }
//std::cerr << (m_branching ? "\nUnmarked bottom states:" : "\nUnmarked states:"); for (const state_in_block_pointer* it=first_unmarked_bottom_state; it!=B->sta.rt_non_bottom_states; ++it) { std::cerr << ' ' << std::distance(m_states.begin(), it->ref_state); } std::cerr << '\n';
//if (m_branching) { std::cerr << "Additionally, " << m_R.size() << " non-bottom states have been marked.\n"; }
                                                                                if constexpr (initialisation) {
                                                                                  assert(no_of_constellations==1);
                                                                                  assert(null_constellation==old_constellation);
                                                                                  assert(!split_off_new_bottom_states);
                                                                                } else {
                                                                                  assert(split_off_new_bottom_states ||
                                                                                         B->block.to_constellation.begin()==splitter);
                                                                                }
                                                                                if constexpr (!initialisation) {
                                                                                  assert(m_states[m_aut.get_transitions()[*splitter->start_same_BLC].from()].
                                                                                                                                            block==B);
                                                                                  assert(!splitter->is_stable());
                                                                                  assert(!split_off_new_bottom_states ||
                                                                                         splitter_end_unmarked_BLC==splitter->start_marked_BLC);
                                                                                }
      if (1 >= number_of_states_in_block(*B))
      {
        mCRL2log(log::debug) << "Trying to split up singleton block "<<B<<'\n';
        clear_state_counters();
        return null_block;
      }
      block_type* R_block=simple_splitB<initialisation, Iterator>(B, splitter,
                   first_unmarked_bottom_state, splitter_end_unmarked_BLC, bi); assert(bi == R_block || B == R_block);
//std::cerr << "Split block of size " << number_of_states_in_block(*B) + number_of_states_in_block(*bi) << " taking away " << number_of_states_in_block(*bi) << " states (namely"; for (auto it=bi->start_bottom_states; it<bi->end_states; ++it) { std::cerr << ' ' << std::distance(m_states.begin(), it->ref_state); } std::cerr << (bi == R_block ? ", the R-subblock)\n" : ", the U-subblock)\n");
                                                                                assert(number_of_states_in_block(*B) >= number_of_states_in_block(*bi));
                                                                                // Because we visit all states of block bi and almost all their incoming and
                                                                                // outgoing transitions, we subsume all this bookkeeping in a single block
                                                                                // counter:
                                                                                mCRL2complexity(bi, add_work(check_complexity::
      /* Update the BLC_list, and bottom states, and invariant on inert      */     splitB__update_BLC_of_smaller_subblock, check_complexity::log_n -
      /* transitions.                                                        */     check_complexity::ilog2(number_of_states_in_block(*bi))), *this);
      state_in_block_pointer* const
                     start_new_bottom_states=R_block->sta.rt_non_bottom_states;
      linked_list<BLC_indicators>::iterator R_to_U_tau_splitter =
                                         R_block->block.to_constellation.end(); assert(bi->block.to_constellation.empty());
      bool skip_transitions_in_splitter=false;                                  assert(m_BLC_indicators_to_be_deleted.empty());
      bool make_splitter_stable_early=false;
 
      if (initialisation || !split_off_new_bottom_states ||
          null_constellation==old_constellation ||
          target_constellation<initialisation, Iterator>(splitter)==
                                                             old_constellation)
      {
        // splitter is not a main splitter. So it can be stabilized already
        // (as we do not need to maintain the order of main/co-splitter).
        make_splitter_stable_early=true;
//std::cerr << "Making splitter ";
        if constexpr (!initialisation)
        {
//std::cerr << splitter->debug_id(*this) << " stable early.\n";
          // However, we may need to move the splitter to its new constellation
          // at the same time.
          if (bi==R_block &&
              (initialisation || split_off_new_bottom_states ||
               splitter_end_unmarked_BLC==splitter->start_marked_BLC))
          {
            splitter->make_stable();
            // move splitter as a whole from its current list to the new list
            // where it will be part of:
            // (This only works if the whole splitter BLC set has moved.)
            R_block->block.to_constellation.splice(
                                         R_block->block.to_constellation.end(),
                                         B->block.to_constellation, splitter);
            skip_transitions_in_splitter=true;
//std::cerr << "    and moving it to the BLC list of " << R_block << '\n';
          }
          else if (!initialisation && split_off_new_bottom_states &&
                   null_constellation==old_constellation)
          {
            // Only during new bottom state splits, we really need to move the
            // splitter to the beginning of the list of splitters.
            make_stable_and_move_to_start_of_BLC(R_block, splitter);
          }
          else
          {
            // During initialisation, we do not bother to move the splitter to
            // the beginning of the BLC list, as every splitter will become
            // stable.
            splitter->make_stable();
          }
        }                                                                       else
                                                                                {
                                                                                  assert(nullptr==splitter);
//std::cerr << "(nullptr) stable early.\n";
                                                                                }
      }
      else if constexpr (!initialisation) // actually the condition always
                                          // holds, but we need "constexpr"
      {                                                                         assert(!splitter->is_stable());
        // unmark all states in the splitter (needed to avoid that parts of the
        // splitter will retain marked states)
        splitter->start_marked_BLC=splitter->end_same_BLC;
        if (bi==R_block)
        {
          // insert a dummy old main splitter to help with placing the
          // corresponding co-splitter correctly:
//std::cerr << "Inserting a dummy old main splitter at m_BLC_transitions[" << std::distance(m_BLC_transitions.data(), splitter->end_same_BLC) << "]\n";
          m_BLC_indicators_to_be_deleted.push_back(
                B->block.to_constellation.emplace_after(splitter,
                         splitter->end_same_BLC, splitter->end_same_BLC, false)
          );                                                                    // ...->work_counter=... -- not needed, as the set will be deleted soon again.
          // ++no_of_non_constellation_inert_BLC_sets; -- not needed, as BLC sets in m_BLC_indicators_to_be_deleted are not counted
          // move splitter as a whole from its current list to the new list
          // where it will be part of:
          // (This only works if the whole splitter BLC set has moved, i.e.
          // only if split_off_new_bottom_states == true.)
          R_block->block.to_constellation.splice(
                                         R_block->block.to_constellation.end(),
                                         B->block.to_constellation, splitter);
          skip_transitions_in_splitter=true;
        }
      }                                                                         else  {  assert(0);  }
                                                                                assert(!initialisation || make_splitter_stable_early);
//std::cerr << "initialisation==" << initialisation
//<< ", m_branching==" << m_branching << ", split_off_new_bottom_states==" << split_off_new_bottom_states
//<< ", make_splitter_stable_early==" << make_splitter_stable_early << ", skip_transitions_in_splitter==" << skip_transitions_in_splitter << '\n';
      if (!initialisation && m_branching)
      {
        if (initialisation || split_off_new_bottom_states ||
            !make_splitter_stable_early || !skip_transitions_in_splitter)
        {
                                                                                #ifndef NDEBUG
          /* insert an empty BLC set into bi->block.to_constellation         */   if (!B->block.to_constellation.empty())  {  const transition* t;
          /* for the inert transitions out of *bi (unless the                */     assert(bi->block.to_constellation.empty() ||
          /* splitter inserted above was the set of inert transitions),      */            (t=&m_aut.get_transitions()[*bi->
          /* to avoid the need to check whether such a BLC set already exists*/                              block.to_constellation.begin()->start_same_BLC],
          /* in update_the_doubly_linked_list_LBC_new_block().               */             !is_inert_during_init(*t)) ||
          /* This set, if it remains empty, will need to be deleted          */            m_states[t->from()].block->c.onstellation!=
          /* after updating the BLC sets.                                    */                                    m_states[t->to()].block->c.onstellation);  }
                                                                                #endif
//std::cerr << "Inserting an empty BLC set for the constellation-inert transitions into the BLC list of " << bi->debug_id(*this) << '\n';
          BLC_list_iterator start_inert_BLC=
               B->block.to_constellation.empty()
                  ? m_BLC_transitions.data_end() // there are no inert transitions but we still insert a dummy set
                  : B->block.to_constellation.begin()->start_same_BLC; // if there are inert transitions, they are here
                                                                                linked_list<BLC_indicators>::iterator new_inert_BLC_set=
          bi->block.to_constellation.emplace_front(start_inert_BLC,
                                                        start_inert_BLC, true);
                                                                                #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
                                                                                  if (!B->block.to_constellation.empty() &&
                                                                                      start_inert_BLC<B->block.to_constellation.begin()->end_same_BLC)
                                                                                      // the first element that's currently in the old BLC list could be the
                                                                                      // dummy main splitter
                                                                                  {
                                                                                    const transition&perhaps_inert_t=m_aut.get_transitions()[*start_inert_BLC];
//std::cerr << "perhaps_inert_t==" << m_transitions[*start_inert_BLC].debug_id(*this) << '\n';
                                                                                    assert(m_states[perhaps_inert_t.from()].block==B ||
                                                                                           m_states[perhaps_inert_t.from()].block==bi);
                                                                                    if(is_inert_during_init(perhaps_inert_t) &&
                                                                                       m_states[perhaps_inert_t.to()].block->c.onstellation==B->c.onstellation)
                                                                                    {
                                                                                      // This are really the inert transitions, so we should copy the work
                                                                                      // counter
                                                                                      new_inert_BLC_set->work_counter=
                                                                                                               B->block.to_constellation.begin()->work_counter;
                                                                                    }
                                                                                  }
                                                                                #else
                                                                                  (void) new_inert_BLC_set; // avoid unused variable warning
                                                                                #endif
          // ++no_of_non_constellation_inert_BLC_sets; -- not needed, as this BLC set will contain constellation-inert transitions
        }                                                                       else
                                                                                {
                                                                                  #ifndef NDEBUG
                                                                                    assert(!bi->block.to_constellation.empty());
                                                                                    assert(bi->block.to_constellation.begin()->start_same_BLC<
                                                                                                             bi->block.to_constellation.begin()->end_same_BLC);
                                                                                    const transition& t=m_aut.get_transitions()
                                                                                                         [*bi->block.to_constellation.begin()->start_same_BLC];
                                                                                    assert(is_inert_during_init(t));
                                                                                    assert(m_states[t.from()].block->c.onstellation==
                                                                                                                       m_states[t.to()].block->c.onstellation);
                                                                                  #endif
                                                                                }
      }
                                                                                #ifndef USE_FOUR_WAY_SPLIT
      /* Recall new LBC positions.                                           */   assert(m_co_splitters_to_be_checked.empty());
                                                                                #endif
      for (state_in_block_pointer*
                       ssi=bi->start_bottom_states; ssi!=bi->end_states; ++ssi)
      {
        state_type_gj& s=*ssi->ref_state;                                       assert(s.ref_states_in_blocks==ssi);
                                                                                // mCRL2complexity(s, add_work(..., max_bi_counter), *this);
        const outgoing_transitions_it end_it=                                       // is subsumed in the above call
                       (std::next(ssi->ref_state)==m_states.end())
                       ? m_outgoing_transitions.end()
                       : std::next(ssi->ref_state)->start_outgoing_transitions; assert(s.block==bi);
        if constexpr (!initialisation)
        {
          // update the BLC_lists.
          for(outgoing_transitions_it ti=s.start_outgoing_transitions;
                                                              ti!=end_it; ti++)
          {                                                                     assert(m_states.begin()+m_aut.get_transitions()
                                                                                                            [*ti->ref.BLC_transitions].from()==ssi->ref_state);
                                                                                // mCRL2complexity(&m_transitions[*ti->ref.BLC_transitions],
                                                                                //                 add_work(..., max_bi_counter), *this);
            if (!skip_transitions_in_splitter ||                                    // is subsumed in the above call
                m_transitions[*ti->ref.BLC_transitions].
                              transitions_per_block_to_constellation!=splitter)
            {
              update_the_doubly_linked_list_LBC_new_block(B, bi,
               *ti->ref.BLC_transitions, old_constellation, new_constellation);
            }
          }
        }
 
        // Situation below is only relevant if the new block contains the
        // R-states:
        if (bi==R_block)
        {
          if (0 < s.no_of_outgoing_block_inert_transitions)
          {                                                                     assert(ssi>=R_block->sta.rt_non_bottom_states);
            // si is a non_bottom_state in the smallest block containing M.
//std::cerr << "Checking whether outgoing transitions of " << s.debug_id(*this) << " have become non-block-inert:\n";
            bool non_bottom_state_becomes_bottom_state=true;                    assert(m_branching);
 
            for(outgoing_transitions_it ti=s.start_outgoing_transitions;
                                                              ti!=end_it; ti++)
            {                                                                   // mCRL2complexity(&m_transitions[*ti->ref.BLC_transitions],
                                                                                //                 add_work(..., max_bi_counter), *this);
              const transition& t=m_aut.get_transitions()[!initialisation           // is subsumed in the above call
                             ? *ti->ref.BLC_transitions : ti->ref.transitions]; assert(m_states.begin()+t.from()==ssi->ref_state);
              if (!m_aut.is_tau(m_aut_apply_hidden_label_map(t.label())))
              {
                break;
              }
              if (m_states[t.to()].block==B)
              {
                // if (is_inert_during_init(t)) -- always true because it
                                                // cannot be a tau-self-loop
                {
                  // This is a transition that has become non-block-inert.
                  // (However, it is still constellation-inert.)
                  make_transition_non_block_inert(t);
                  if (!initialisation && split_off_new_bottom_states)
                  {
                    const linked_list<BLC_indicators>::iterator new_splitter=
                                  m_transitions[*ti->ref.BLC_transitions].
                                        transitions_per_block_to_constellation; assert(R_block->block.to_constellation.begin()==new_splitter);
                    if (R_to_U_tau_splitter==
                                         R_block->block.to_constellation.end())
                    {
                      R_to_U_tau_splitter=new_splitter;
                      R_to_U_tau_splitter->make_unstable();
                    }                                                           else
                                                                                {
                                                                                  assert(R_to_U_tau_splitter==new_splitter);
                    /* immediately mark this transition, in case we get */        assert(!R_to_U_tau_splitter->is_stable());
                    /* new bottom states: */                                    }
                    mark_BLC_transition(ti);
                  }
                }
              }
              else if (m_preserve_divergence && t.from()==t.to())
              {                                                                 assert(!is_inert_during_init(t));
                // transition is a divergent tau-self-loop. It never was inert.
              }
              else if (m_states[t.to()].block==R_block)
              {                                                                 assert(is_inert_during_init(t));
                // There is an outgoing inert tau. State remains non-bottom.
                non_bottom_state_becomes_bottom_state=false;
              }
            }
            if (non_bottom_state_becomes_bottom_state)
            {                                                                   assert(initialisation || !split_off_new_bottom_states ||
              /* The state at si has become a bottom_state. */                         R_block->block.to_constellation.end()!=R_to_U_tau_splitter);
              change_non_bottom_state_to_bottom_state(ssi->ref_state);
            }
          }
        }
        // Investigate the incoming formerly inert tau transitions.
        else if (R_block->sta.rt_non_bottom_states<R_block->end_states)
        {
//std::cerr << "Checking whether incoming transitions of " << s.debug_id(*this) << " have become non-block-inert:\n";
          const std::vector<transition>::iterator it_end =
                      std::next(ssi->ref_state)>=m_states.end()
                      ? m_aut.get_transitions().end()
                      : std::next(ssi->ref_state)->start_incoming_transitions;
          for(std::vector<transition>::iterator it =
                                s.start_incoming_transitions; it!=it_end; it++)
          {                                                                     // mCRL2complexity(&m_transitions[std::distance(m_aut.get_transitions().
                                                                                //                 begin(), it)], add_work(..., max_bi_counter), *this);
                                                                                    // subsumed in the above call
            const transition& t=*it;                                            assert(m_states.begin()+t.to()==ssi->ref_state);
            if (!m_aut.is_tau(m_aut_apply_hidden_label_map(t.label())))
            {
              break; // All tau transitions have been investigated.
            }
 
            const fixed_vector<state_type_gj>::iterator from
                                                   (m_states.begin()+t.from());
            if (from->block==R_block)
            {
              // This transition did become non-block-inert.
              // (However, it is still constellation-inert.)
              make_transition_non_block_inert(t);
              if (!initialisation && split_off_new_bottom_states)
              {
                const linked_list<BLC_indicators>::iterator new_splitter=
                   m_transitions[std::distance(m_aut.get_transitions().begin(),
                                  it)].transitions_per_block_to_constellation;  assert(R_block->block.to_constellation.begin()==new_splitter);
                if (R_to_U_tau_splitter==R_block->block.to_constellation.end())
                {
                  R_to_U_tau_splitter=new_splitter;
                  R_to_U_tau_splitter->make_unstable();
                }                                                               else
                                                                                {
                                                                                  assert(R_to_U_tau_splitter==new_splitter);
                /* immediately mark this transition, in case we get new */        assert(!R_to_U_tau_splitter->is_stable());
                /* bottom states: */                                            }
                mark_BLC_transition(m_transitions
                      [std::distance(m_aut.get_transitions().begin(), it)].
                                                     ref_outgoing_transitions);
              }
              // Check whether from is a new bottom state.
              if (from->no_of_outgoing_block_inert_transitions==0)
              {
                // This state has no more outgoing inert transitions. It
                // becomes a bottom state.
                change_non_bottom_state_to_bottom_state(from);
              }
            }
          }
        }
      }                                                                         assert(R_block->start_bottom_states<R_block->sta.rt_non_bottom_states);
      if constexpr (!initialisation)
      {
        if (m_branching)
        {                                                                         assert(!bi->block.to_constellation.empty());
          // Before the loop we inserted an empty BLC set for the inert
          // transitions into bi->block.to_constellation.
          // If it is still empty, we have to remove it again.
          linked_list<BLC_indicators>::iterator
                                  inert_ind=bi->block.to_constellation.begin();
          if (inert_ind->start_same_BLC==inert_ind->end_same_BLC)
          {                                                                     assert(inert_ind->is_stable());
            bi->block.to_constellation.erase(inert_ind);
          }                                                                     else
                                                                                { // assert(perhaps_inert_ind->is_stable()); -- it may be unstable
                                                                                  //                         if there are tau-transitions from R_block==bi to U
                                                                                  #ifndef NDEBUG
                                                                                    const transition& inert_t=
                                                                                                   m_aut.get_transitions()[*inert_ind->start_same_BLC];
                                                                                    assert(is_inert_during_init(inert_t));
                                                                                    assert(bi==m_states[inert_t.from()].block);
                                                                                    assert(bi->c.onstellation==m_states[inert_t.to()].block->c.onstellation);
                                                                                  #endif
                                                                                }
        }
        for (std::vector<linked_list<BLC_indicators>::iterator>::iterator
                                 it=m_BLC_indicators_to_be_deleted.begin();
                                 it<m_BLC_indicators_to_be_deleted.end(); ++it)
        {