liblts_bisim_dnj.h

Go to the documentation of this file.

// Author(s): David N. Jansen, Institute of Software, Chinese Academy of
// Sciences, Beijing, PR China
//
// 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)
 
 
// The file is best viewed on a screen or in a window that is 160 characters
// wide.  The left 80 columns contain the main text of the program.  The right
// 80 columns contain assertions and other code used for debugging.
 
#ifndef LIBLTS_BISIM_DNJ_H
#define LIBLTS_BISIM_DNJ_H
 
#include "mcrl2/lts/detail/liblts_scc.h"
#include "mcrl2/lts/detail/liblts_merge.h"
#include "mcrl2/lts/detail/coroutine.h"
#include "mcrl2/lts/detail/check_complexity.h"
#include "mcrl2/lts/detail/fixed_vector.h"
 
#include <cstddef>   // for std::size_t
 
// My provisional recommendation is to always use simple lists and pool
// allocators.  Using standard allocation and standard lists is 5-15% slower
// and uses perhaps 0.7% more memory.  Using standard allocation and simple
// lists is 10-20% slower and has no significant effect on memory use.  These
// numbers are based on a small set with not-so-large case studies, none of
// which includes new bottom states.
 
#define USE_SIMPLE_LIST
 
#ifndef USE_SIMPLE_LIST
    #include <list>  // for the list of block_bunch-slices
    #include <type_traits> // for std::is_trivially_destructible<class>
#endif
 
#define USE_POOL_ALLOCATOR
 
#ifdef USE_POOL_ALLOCATOR
    #ifndef NDEBUG
        #include <type_traits> // for std::is_trivially_destructible<class>
    #endif
 
    #define ONLY_IF_POOL_ALLOCATOR(...) __VA_ARGS__
    #ifndef USE_SIMPLE_LIST
        #error "Using the pool allocator also requires using the simple list"
    #endif
#else
    #define ONLY_IF_POOL_ALLOCATOR(...)
#endif
 
namespace mcrl2
{
namespace lts
{
namespace detail
{
                                                                                #ifndef NDEBUG
// state_type and trans_type are defined in check_complexity.h.                     /// mode and to nothing otherwise.
                                                                                    #define ONLY_IF_DEBUG(...) __VA_ARGS__
                                                                                #else
                                                                                    #define ONLY_IF_DEBUG(...)
                                                                                #endif
typedef std::size_t label_type;
 
template <class LTS_TYPE> class bisim_partitioner_dnj;
 
namespace bisim_dnj
{
 
template <class Iterator>
union iterator_or_counter
{
    trans_type count;
 
    Iterator begin;
 
    iterator_or_counter()  {  count = 0;  }
 
 
    void convert_to_iterator(const Iterator other)
    {
        new (&begin) Iterator(other);
    }
 
 
    ~iterator_or_counter()  {  begin.~Iterator();  }
};
 
 
class block_bunch_entry;
class action_block_entry;
 
 
 
 
 
/* ************************************************************************* */
/*                                                                           */
/*                     M E M O R Y   M A N A G E M E N T                     */
/*                                                                           */
/* ************************************************************************* */
 
 
 
 
 
#ifdef USE_POOL_ALLOCATOR
    template <class T, size_t BLOCKSIZE = 1000>
    class my_pool
    {                                                                           static_assert(std::is_trivially_destructible<T>::value);
      private:                                                                  static_assert(sizeof(void*) <= sizeof(T));
        class pool_block_t
        {
          public:
            char data[BLOCKSIZE - sizeof(pool_block_t*)];
            pool_block_t* next_block;
 
            pool_block_t(pool_block_t* const new_next_block)
              : next_block(new_next_block)
            {  }
        };                                                                      static_assert(sizeof(T) <= sizeof(pool_block_t::data));
 
        pool_block_t* first_block;
 
        void* begin_used_in_first_block;
 
        void* first_free_T;
 
        static void*& deref_void(void* addr)
        {
            return *static_cast<void**>(addr);
        }
      public:
        my_pool()
          : first_block(new pool_block_t(nullptr)),
            begin_used_in_first_block(
                                &first_block->data[sizeof(first_block->data)]),
            first_free_T(nullptr)
        {  }
 
 
        ~my_pool()
        {
            pool_block_t* block(first_block);                                   assert(nullptr != block);
            do
            {
                pool_block_t* next_block = block->next_block;
                delete block;
                block = next_block;
            }
            while(nullptr != block);
        }
 
 
      private:
        template <class U, class... Args>
        U* construct_samesize(Args&&... args)
        {                                                                       static_assert(sizeof(T) == sizeof(U));
            void* new_el;                                                       assert(nullptr != first_block);
            if (first_block->data + sizeof(U) <= begin_used_in_first_block)
            {
                begin_used_in_first_block =
                    new_el = static_cast<char*>(begin_used_in_first_block) -
                                                                     sizeof(U);
            }
            else if (nullptr != first_free_T)
            {
                // free list is tested afterwards because I expect that there
                // won't be too many elements in the free list.
                new_el = first_free_T;
                first_free_T = deref_void(new_el);
            }
            else
            {
                first_block = new pool_block_t(first_block);
                begin_used_in_first_block =
                    new_el = &first_block->data[sizeof(first_block->data) -
                                                                    sizeof(U)];
            }
            return new(new_el) U(std::forward<Args>(args)...);
        }
 
 
        template <class U, class... Args>
        U* construct_othersize(Args&&... args)
        {                                                                       static_assert(sizeof(U) != sizeof(T));
            void* new_el;                                                       assert(nullptr != first_block);
            if (first_block->data + sizeof(U) <= begin_used_in_first_block)
            {
                begin_used_in_first_block =
                    new_el = static_cast<char*>(begin_used_in_first_block) -
                                                                     sizeof(U);
            }
            else
            {
                if constexpr (sizeof(T) * 2 < sizeof(U))
                {
                    // There may be space for several T-elements
                    while (first_block->data + sizeof(T) <=
                                                     begin_used_in_first_block)
                    {
                        begin_used_in_first_block = static_cast<char*>
                                       (begin_used_in_first_block) - sizeof(T);
                        deref_void(begin_used_in_first_block) = first_free_T;
                        first_free_T = begin_used_in_first_block;
                    }
                }
                else if constexpr (sizeof(T) < sizeof(U))
                {
                    // There may be space for one T-element (but not more)
                    if (first_block->data + sizeof(T) <=
                                                     begin_used_in_first_block)
                    {
                        begin_used_in_first_block = static_cast<char*>
                                       (begin_used_in_first_block) - sizeof(T);
                        deref_void(begin_used_in_first_block) = first_free_T;
                        first_free_T = begin_used_in_first_block;
                    }
                }                                                               assert(first_block->data + sizeof(T) > begin_used_in_first_block);
                first_block = new pool_block_t(first_block);
                begin_used_in_first_block =
                    new_el = &first_block->data[sizeof(first_block->data) -
                                                                    sizeof(U)];
            }
            return new(new_el) U(std::forward<Args>(args)...);
        }
      public:
        template <class U, class... Args>
        U* construct(Args&&... args)
        {                                                                       static_assert(std::is_trivially_destructible<U>::value);
            if constexpr (sizeof(U) == sizeof(T))
            {
                return construct_samesize<U>(std::forward<Args>(args)...);
            }
            else
            {                                                                   static_assert(sizeof(U) <= sizeof(first_block->data));
                return construct_othersize<U>(std::forward<Args>(args)...);
            }
        }
 
 
        template <class U>
        void destroy(U* const old_el)
        {                                                                       static_assert(sizeof(T) == sizeof(U));
            old_el->~U();                                                       static_assert(std::is_trivially_destructible<U>::value);
                                                                                #ifndef NDEBUG
                                                                                    // ensure that old_el points to an element in some block
                                                                                    static std::less<const void*> const total_order;
                                                                                    for (const pool_block_t* block(first_block);
                                                                                                assert(nullptr != block),
                                                                                                total_order(old_el, block->data) ||
                                                                                                total_order(&block->data[sizeof(block->data)], old_el + 1);
                                                                                                                                    block = block->next_block )
                                                                                    {  }
                                                                                #endif
            deref_void(old_el) = first_free_T;
            first_free_T = static_cast<void*>(old_el);
        }
    };
#endif
 
#ifdef USE_SIMPLE_LIST
    template <class T>
    class simple_list
    {
      private:
        class empty_entry
        {
          protected:
            empty_entry* next;
 
            empty_entry* prev;
 
            empty_entry(empty_entry*const new_next, empty_entry*const new_prev)
              : next(new_next),
                prev(new_prev)
            {  }
 
            friend class simple_list;
        };
 
        empty_entry sentinel;
 
      public:
        class entry : public empty_entry
        {
          private:
            T data;
 
            friend class simple_list;
          public:
            template <class... Args>
            entry(empty_entry* const new_next, empty_entry* const new_prev,
                                                                Args&&... args)
              : empty_entry(new_next, new_prev),
                data(std::forward<Args>(args)...)
            {  }
        };
 
        class const_iterator
        {
          public:
            typedef std::bidirectional_iterator_tag iterator_category;
            typedef T value_type;
            typedef std::ptrdiff_t difference_type;
            typedef T* pointer;
            typedef T& reference;
          protected:
            empty_entry* ptr;
 
            const_iterator(const empty_entry* const new_ptr)
              : ptr(const_cast<empty_entry*>(new_ptr))
            {  }
 
            friend class simple_list;
          public:
            const_iterator() = default;
            const_iterator(const const_iterator& other) = default;
            const_iterator& operator=(const const_iterator& other) = default;
            const_iterator& operator++()  {  ptr = ptr->next;  return *this;  }
            const_iterator& operator--()  {  ptr = ptr->prev;  return *this;  }
            const T& operator*() const
            {
                return  static_cast<const entry*>(ptr)->data;
            }
            const T* operator->() const
            {
                return &static_cast<const entry*>(ptr)->data;
            }
            bool operator==(const const_iterator& other) const
            {
                return ptr == other.ptr;
            }
            bool operator!=(const const_iterator& other) const
            {
                return !operator==(other);
            }
        };
 
        class iterator : public const_iterator
        {
          public:
            typedef typename const_iterator::iterator_category
                                                             iterator_category;
            typedef typename const_iterator::value_type value_type;
            typedef typename const_iterator::difference_type difference_type;
            typedef typename const_iterator::pointer pointer;
            typedef typename const_iterator::reference reference;
          protected:
            iterator(empty_entry*const new_ptr) : const_iterator(new_ptr)  {  }
 
            friend class simple_list;
          public:
            iterator() = default;
            iterator(const iterator& other) = default;
            iterator& operator=(const iterator& other) = default;
            iterator& operator++(){const_iterator::operator++(); return *this;}
            iterator& operator--(){const_iterator::operator--(); return *this;}
            T& operator*() const
            {
                return  static_cast<entry*>(const_iterator::ptr)->data;
            }
            T* operator->() const
            {
                return &static_cast<entry*>(const_iterator::ptr)->data;
            }
        };
 
        class iterator_or_null : public iterator
        {
          public:
            typedef typename iterator::iterator_category iterator_category;
            typedef typename iterator::value_type value_type;
            typedef typename iterator::difference_type difference_type;
            typedef typename iterator::pointer pointer;
            typedef typename iterator::reference reference;
            iterator_or_null() : iterator()  {  }
            iterator_or_null(std::nullptr_t) : iterator()
            {
                 const_iterator::ptr = nullptr;
            }
            iterator_or_null(const iterator& other) : iterator(other)  {  }
            bool is_null() const  {  return nullptr == const_iterator::ptr;  }
            T& operator*() const
            {                                                                   assert(!is_null());
                return iterator::operator*();
            }
            T* operator->() const
            {                                                                   assert(!is_null());
                return iterator::operator->();
            }
            bool operator==(const const_iterator& other) const
            {
                return const_iterator::ptr == other.ptr;
            }
            bool operator!=(const const_iterator& other) const
            {
                return !operator==(other);
            }
            bool operator==(const T* const other) const
            {                                                                   assert(nullptr != other);
                // It is allowed to call this even if is_null().  Therefore, we
                // cannot use iterator_or_null::operator->().
                return const_iterator::operator->() == other;
            }
            bool operator!=(const T* const other) const
            {
                return !operator==(other);
            }
 
            void operator=(std::nullptr_t)
            {
                const_iterator::ptr = nullptr;
            }
        };
 
        simple_list()
          : sentinel(&sentinel, &sentinel)
        {                                                                       static_assert(std::is_trivially_destructible<entry>::value);
        }
 
        #ifndef USE_POOL_ALLOCATOR
            ~simple_list()
            {
                for (iterator iter = begin(); end() != iter; )
                {
                    iterator next = std::next(iter);
                    delete static_cast<entry*>(iter.ptr);
                    iter = next;
                }
            }
        #endif
 
        iterator begin()  {  return iterator(sentinel.next);  }
 
        iterator end()    {  return iterator(&sentinel);      }
 
        const_iterator cbegin() const { return const_iterator(sentinel.next); }
 
        const_iterator cend()   const { return const_iterator(&sentinel);     }
 
        const_iterator begin() const  {  return cbegin();  }
 
        const_iterator end()   const  {  return cend();    }
 
        T& front()
        {                                                                       assert(!empty());
            return static_cast<entry*>(sentinel.next)->data;
        }
 
        T& back()
        {                                                                       assert(!empty());
            return static_cast<entry*>(sentinel.prev)->data;
        }
 
        bool empty() const  {  return sentinel.next == &sentinel;  }
 
        template<class... Args>
        static iterator emplace(
                ONLY_IF_POOL_ALLOCATOR( my_pool<entry>& pool, )
                                                  iterator pos, Args&&... args)
        {
            entry* const new_entry(
                #ifdef USE_POOL_ALLOCATOR
                    pool.template construct<entry>
                #else
                    new entry
                #endif
                        (pos.ptr, pos.ptr->prev, std::forward<Args>(args)...));
            pos.ptr->prev->next = new_entry;
            pos.ptr->prev = new_entry;
            return iterator(new_entry);
        }
 
        template<class... Args>
        static iterator emplace_after(
                ONLY_IF_POOL_ALLOCATOR( my_pool<entry>& pool, )
                                                  iterator pos, Args&&... args)
        {
            entry* const new_entry(
                #ifdef USE_POOL_ALLOCATOR
                    pool.template construct<entry>
                #else
                    new entry
                #endif
                        (pos.ptr->next, pos.ptr, std::forward<Args>(args)...));
            pos.ptr->next->prev = new_entry;
            pos.ptr->next = new_entry;
            return iterator(new_entry);
        }
 
        template<class... Args>
        iterator emplace_front(
                ONLY_IF_POOL_ALLOCATOR( my_pool<entry>& pool, )
                                                                Args&&... args)
        {
            entry* const new_entry(
                #ifdef USE_POOL_ALLOCATOR
                    pool.template construct<entry>
                #else
                    new entry
                #endif
                      (sentinel.next, &sentinel, std::forward<Args>(args)...));
            sentinel.next->prev = new_entry;
            sentinel.next = new_entry;
            return iterator(new_entry);
        }
 
        template<class... Args>
        iterator emplace_back(
                ONLY_IF_POOL_ALLOCATOR( my_pool<entry>& pool, )
                                                                Args&&... args)
        {
            entry* const new_entry(
                #ifdef USE_POOL_ALLOCATOR
                    pool.template construct<entry>
                #else
                    new entry
                #endif
                      (&sentinel, sentinel.prev, std::forward<Args>(args)...));
            sentinel.prev->next = new_entry;
            sentinel.prev = new_entry;
            return iterator(new_entry);
        }
 
        static void splice(iterator const new_pos, simple_list& /* unused */,
                                                        iterator const old_pos)
        {
            old_pos.ptr->prev->next = old_pos.ptr->next;
            old_pos.ptr->next->prev = old_pos.ptr->prev;
 
            old_pos.ptr->next = new_pos.ptr->prev->next;
            old_pos.ptr->prev = new_pos.ptr->prev;
 
            old_pos.ptr->prev->next = old_pos.ptr;
            old_pos.ptr->next->prev = old_pos.ptr;
        }
 
        static void erase(
                ONLY_IF_POOL_ALLOCATOR( my_pool<entry>& pool, )
                                                            iterator const pos)
        {
            pos.ptr->prev->next = pos.ptr->next;
            pos.ptr->next->prev = pos.ptr->prev;
            #ifdef USE_POOL_ALLOCATOR
                pool.destroy(static_cast<entry*>(pos.ptr));
            #else
                delete static_cast<entry*>(pos.ptr);
            #endif
        }
    };
#else
    #define simple_list std::list
#endif
 
 
 
 
 
/* ************************************************************************* */
/*                                                                           */
/*                   R E F I N A B L E   P A R T I T I O N                   */
/*                                                                           */
/* ************************************************************************* */
 
 
 
 
 
class state_info_entry;
class permutation_entry;
 
typedef bisim_gjkw::fixed_vector<permutation_entry> permutation_t;
 
class block_t;
class bunch_t;
 
class pred_entry;
class succ_entry;
 
class block_bunch_slice_t;
typedef simple_list<block_bunch_slice_t>::iterator block_bunch_slice_iter_t;
typedef simple_list<block_bunch_slice_t>::const_iterator
                                                block_bunch_slice_const_iter_t;
#ifdef USE_SIMPLE_LIST
    typedef simple_list<block_bunch_slice_t>::iterator_or_null
                                              block_bunch_slice_iter_or_null_t;
#else
    union block_bunch_slice_iter_or_null_t
    {
      private:
        const void* null;
        block_bunch_slice_iter_t iter;
      public:
        block_bunch_slice_iter_or_null_t()
        {
            if constexpr (!std::is_trivially_destructible<
                                              block_bunch_slice_iter_t>::value)
            {
                // We still have to internally decide whether to construct
                // the iterator or not so the destructor knows what to do.
                null = nullptr;
            }
        }
 
 
        explicit block_bunch_slice_iter_or_null_t(nullptr_t)
        {
            null = nullptr;
        }
 
 
        explicit block_bunch_slice_iter_or_null_t(
                                         const block_bunch_slice_iter_t& other)
        {
            new (&iter) block_bunch_slice_iter_t(other);                        assert(nullptr != null);
        }
 
 
        // not)
        ~block_bunch_slice_iter_or_null_t()
        {
            if (!is_null())  iter.~block_bunch_slice_iter_t();
        }
 
        block_bunch_slice_t* operator->()
        {                                                                       assert(nullptr != null);
            return iter.operator->();
        }
        block_bunch_slice_t& operator*()
        {                                                                       assert(nullptr != null);
            return iter.operator*();
        }
 
        void operator=(nullptr_t)
        {
            if (!is_null())  iter.~block_bunch_slice_iter_t();
            null = nullptr;
        }
 
 
        explicit operator block_bunch_slice_iter_t() const
        {                                                                       assert(nullptr != null);
            return iter;
        }
 
 
        explicit operator block_bunch_slice_const_iter_t() const
        {                                                                       assert(nullptr != null);
            return iter;
        }
 
 
        void operator=(const block_bunch_slice_iter_t& other)
        {
            if (!is_null())  iter.~block_bunch_slice_iter_t();
            new (&iter) block_bunch_slice_iter_t(other);                        assert(nullptr != null);
        }
 
        bool operator==(const block_bunch_slice_iter_or_null_t& other) const
        {
            if constexpr (sizeof(null) == sizeof(iter))
            {
                return &*iter == &*other.iter;
            }
            else
            {
                return (is_null() && other.is_null()) ||
                    (!is_null() && !other.is_null() && &*iter == &*other.iter);
            }
        }
 
 
        bool operator!=(const block_bunch_slice_iter_or_null_t& other) const
        {
            return !operator==(other);
        }
 
 
        bool operator==(const block_bunch_slice_const_iter_t other) const
        {                                                                       // assert(nullptr != &*other); -- generates a warning
            return (sizeof(null) == sizeof(iter) || !is_null()) &&
                                                             &*iter == &*other;
        }
 
 
        bool operator!=(const block_bunch_slice_const_iter_t other) const
        {
            return !operator==(other);
        }
 
 
        bool operator==(const block_bunch_slice_t* const other) const
        {                                                                       assert(nullptr != other);
            return (sizeof(null) == sizeof(iter) || !is_null()) &&
                                                               &*iter == other;
        }
 
 
        bool operator!=(const block_bunch_slice_t* const other) const
        {
            return !operator==(other);
        }
 
 
        bool is_null() const  {  return nullptr == null;  }
    };
#endif
 
enum new_block_mode_t { new_block_is_U, new_block_is_R };
 
 
class state_info_entry
{
  public:
    iterator_or_counter<pred_entry*> pred_inert;
 
    iterator_or_counter<succ_entry*> succ_inert;
 
    union bl_t {
        pred_entry* ed_noninert_end;
        block_t* ock;
    } bl;
 
    permutation_entry* pos;
 
    iterator_or_counter<succ_entry*> untested_to_U_eqv;
                                                                                #ifndef NDEBUG
                                                                                    template<class LTS_TYPE>
                                                                                    std::string debug_id_short(const bisim_partitioner_dnj<LTS_TYPE>&
                                                                                                                                             partitioner) const
                                                                                    {   assert(&partitioner.part_st.state_info.front() <= this);
                                                                                        assert(this <= &partitioner.part_st.state_info.back());
                                                                                        return std::to_string(this - &partitioner.part_st.state_info.front());
                                                                                    }
 
                                                                                    template<class LTS_TYPE>
                                                                                    std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>&
                                                                                                                                             partitioner) const
                                                                                    {
                                                                                        return "state " + debug_id_short(partitioner);
                                                                                    }
 
                                                                                    mutable check_complexity::state_dnj_counter_t work_counter;
                                                                                #endif
};
 
 
class permutation_entry {
  public:
    state_info_entry* st;
 
 
    permutation_entry() = default;
 
 
    permutation_entry(const permutation_entry&& other) noexcept
    {
        st = other.st;
    }
 
 
    void operator=(const permutation_entry&& other) noexcept
    {
        st = other.st;
        st->pos = this;
    }
};
 
 
class block_t
{
  public:
    permutation_entry* begin;
 
    permutation_entry* marked_bottom_begin;
 
    permutation_entry* nonbottom_begin;
 
    permutation_entry* marked_nonbottom_begin;
 
    permutation_entry* end;
 
    simple_list<block_bunch_slice_t> stable_block_bunch;
 
    const state_type seqnr;
 
 
    block_t(permutation_entry* const new_begin,
                  permutation_entry* const new_end, state_type const new_seqnr)
      : begin(new_begin),
        marked_bottom_begin(new_end),
        nonbottom_begin(new_end),
        marked_nonbottom_begin(new_end),
        end(new_end),
        stable_block_bunch(),
        seqnr(new_seqnr)
    {                                                                           assert(new_begin < new_end);
    }
 
 
    state_type size() const
    {                                                                           assert(begin <= marked_bottom_begin);  assert(marked_nonbottom_begin <= end);
                                                                                assert(marked_bottom_begin <= nonbottom_begin);
                                                                                assert(nonbottom_begin <= marked_nonbottom_begin);
        return end - begin;
    }
 
 
    state_type bottom_size() const
    {                                                                           assert(begin <= marked_bottom_begin);  assert(marked_nonbottom_begin <= end);
                                                                                assert(marked_bottom_begin <= nonbottom_begin);
                                                                                assert(nonbottom_begin <= marked_nonbottom_begin);
        return nonbottom_begin - begin;
    }
 
 
    state_type marked_bottom_size() const
    {                                                                           assert(begin <= marked_bottom_begin);  assert(marked_nonbottom_begin <= end);
                                                                                assert(marked_bottom_begin <= nonbottom_begin);
                                                                                assert(nonbottom_begin <= marked_nonbottom_begin);
        return nonbottom_begin - marked_bottom_begin;
    }
 
 
    state_type marked_size() const
    {
        return end - marked_nonbottom_begin + marked_bottom_size();
    }
 
 
    state_type unmarked_bottom_size() const
    {                                                                           assert(begin <= marked_bottom_begin);  assert(marked_nonbottom_begin <= end);
                                                                                assert(marked_bottom_begin <= nonbottom_begin);
                                                                                assert(nonbottom_begin <= marked_nonbottom_begin);
        return marked_bottom_begin - begin;
    }
 
 
    state_type unmarked_nonbottom_size() const
    {                                                                           assert(begin <= marked_bottom_begin);  assert(marked_nonbottom_begin <= end);
                                                                                assert(marked_bottom_begin <= nonbottom_begin);
                                                                                assert(nonbottom_begin <= marked_nonbottom_begin);
        return marked_nonbottom_begin - nonbottom_begin;
    }
 
 
    bool mark_nonbottom(permutation_entry* const s)
    {                                                                           assert(nonbottom_begin <= s);  assert(s < end);
                                                                                // assert(this == s->st->bl.ock); -- does not hold during initialisation
                                                                                assert(begin <= marked_bottom_begin);
                                                                                assert(marked_bottom_begin <= nonbottom_begin);
                                                                                assert(nonbottom_begin <= marked_nonbottom_begin);
        if (marked_nonbottom_begin <= s) { return false; }                      assert(marked_nonbottom_begin <= end);
        std::swap(*s, *--marked_nonbottom_begin);                               assert(nonbottom_begin <= marked_nonbottom_begin);
        return true;
    }
 
 
    bool mark(permutation_entry* const s)
    {                                                                           assert(begin <= s);
        if (s < nonbottom_begin)                                                // assert(this == s->st->bl.ock); -- does not hold during initialisation
        {                                                                       assert(begin <= marked_bottom_begin);  assert(marked_nonbottom_begin <= end);
                                                                                assert(nonbottom_begin <= marked_nonbottom_begin);
            if (marked_bottom_begin <= s) { return false; }                     assert(marked_bottom_begin <= nonbottom_begin);
            std::swap(*s, *--marked_bottom_begin);                              assert(begin <= marked_bottom_begin);
            return true;
        }
        return mark_nonbottom(s);
    }
 
 
                                                                                ONLY_IF_DEBUG( template<class LTS_TYPE> )
    block_t* split_off_block(enum new_block_mode_t new_block_mode,              ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner, )
            ONLY_IF_POOL_ALLOCATOR(
                 my_pool<simple_list<block_bunch_slice_t>::entry>& storage, )
                                                         state_type new_seqnr);
                                                                                #ifndef NDEBUG
                                                                                    template<class LTS_TYPE>
                                                                                    inline std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>&
                                                                                                                                             partitioner) const
                                                                                    {   assert(&partitioner.part_st.permutation.front() <= begin);
                                                                                        assert(begin < end);  assert(begin <= marked_bottom_begin);
                                                                                        assert(marked_bottom_begin <= nonbottom_begin);
                                                                                        assert(nonbottom_begin <= marked_nonbottom_begin);
                                                                                        assert(marked_nonbottom_begin <= end);
                                                                                        assert(end <= 1 + &partitioner.part_st.permutation.back());
                                                                                        return "block [" +
                                                                                           std::to_string(begin - &partitioner.part_st.permutation.front()) +
                                                                                           "," + std::to_string(end-&partitioner.part_st.permutation.front()) +
                                                                                                                          ") (#" + std::to_string(seqnr) + ")";
                                                                                    }
 
                                                                                    mutable check_complexity::block_dnj_counter_t work_counter;
                                                                                #endif
};
 
 
class part_state_t
{
  public:
    permutation_t permutation;
 
    bisim_gjkw::fixed_vector<state_info_entry> state_info;
 
    state_type nr_of_blocks;
 
    part_state_t(state_type const num_states)
      : permutation(num_states),
        state_info(num_states),
        nr_of_blocks(0)
    {                                                                           assert(0 < num_states);
        permutation_entry* perm_iter(&permutation.front());                     ONLY_IF_POOL_ALLOCATOR(
                                                                                               static_assert(std::is_trivially_destructible<block_t>::value); )
        state_info_entry* state_iter(&state_info.front());                      assert(perm_iter <= &permutation.back());
        do
        {
            state_iter->pos = perm_iter;
            perm_iter->st = state_iter;
        }
        while (++state_iter, ++perm_iter <= &permutation.back());               assert(state_iter == 1 + &state_info.back());
    }
 
 
    #ifndef USE_POOL_ALLOCATOR
        ~part_state_t()
        {                                                                       ONLY_IF_DEBUG( state_type deleted_blocks(0); )
            permutation_entry* perm_iter(1 + &permutation.back());              assert(&permutation.front() < perm_iter);
            do
            {
                block_t* const B(perm_iter[-1].st->bl.ock);                     assert(B->end == perm_iter);
                perm_iter = B->begin;                                           ONLY_IF_DEBUG( ++deleted_blocks; )
                delete B;
            }
            while (&permutation.front() < perm_iter);                           assert(deleted_blocks == nr_of_blocks);
        }
    #endif
 
 
    state_type state_size() const  {  return permutation.size();  }
 
 
    const block_t* block(state_type const s) const
    {
        return state_info[s].bl.ock;
    }
                                                                                #ifndef NDEBUG
                                                                                  private:
                                                                                    template<class LTS_TYPE>
                                                                                    void print_block(const block_t* const B,
                                                                                                     const char* const message,
                                                                                                     const permutation_entry* begin_print,
                                                                                                     const permutation_entry* const end_print,
                                                                                                     const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
                                                                                    {   assert(B->begin <= begin_print);  assert(end_print <= B->end);
                                                                                        if (end_print == begin_print)  return;
 
                                                                                        mCRL2log(log::debug) << '\t' << message
                                                                                                             << (1 < end_print - begin_print ? "s:\n" : ":\n");
                                                                                        assert(begin_print < end_print);
                                                                                        do
                                                                                        {
                                                                                            mCRL2log(log::debug) << "\t\t"
                                                                                                                     << begin_print->st->debug_id(partitioner);
                                                                                            if (B != begin_print->st->bl.ock)
                                                                                            {
                                                                                                mCRL2log(log::debug) << ", inconsistent: points "
                                                                                                       "to " << begin_print->st->bl.ock->debug_id(partitioner);
                                                                                            }
                                                                                            if (begin_print != begin_print->st->pos)
                                                                                            {
                                                                                                mCRL2log(log::debug)
                                                                                                               << ", inconsistent pointer to state_info_entry";
                                                                                            }
                                                                                            mCRL2log(log::debug) << '\n';
                                                                                        }
                                                                                        while (++begin_print < end_print);
                                                                                    }
                                                                                  public:
                                                                                    template<class LTS_TYPE>
                                                                                    void print_part(const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
                                                                                    {
                                                                                        if (!mCRL2logEnabled(log::debug))  return;
                                                                                        const block_t* B(permutation.front().st->bl.ock);
                                                                                        do
                                                                                        {
                                                                                            mCRL2log(log::debug)<<B->debug_id(partitioner)<<":\n";
                                                                                            print_block(B, "Bottom state",
                                                                                                                B->begin, B->marked_bottom_begin, partitioner);
                                                                                            print_block(B, "Marked bottom state",
                                                                                                      B->marked_bottom_begin, B->nonbottom_begin, partitioner);
                                                                                            print_block(B, "Non-bottom state",
                                                                                                   B->nonbottom_begin, B->marked_nonbottom_begin, partitioner);
                                                                                            print_block(B, "Marked non-bottom state",
                                                                                                               B->marked_nonbottom_begin, B->end, partitioner);
                                                                                        // go to next block
                                                                                        }
                                                                                        while(B->end <= &permutation.back() && (B = B->end->st->bl.ock, true));
                                                                                    }
 
                                                                                    template<class LTS_TYPE>
                                                                                    void assert_consistency(
                                                                                                      const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
                                                                                    {
                                                                                        const permutation_entry* perm_iter(&permutation.front());
                                                                                        state_type true_nr_of_blocks(0);
                                                                                        assert(perm_iter <= &permutation.back());
                                                                                        do
                                                                                        {
                                                                                            const block_t* const block(perm_iter->st->bl.ock);
                                                                                            // block is consistent:
                                                                                            assert(block->begin == perm_iter);
                                                                                            assert(block->begin < block->marked_bottom_begin);
                                                                                            assert(block->marked_bottom_begin == block->nonbottom_begin);
                                                                                            assert(block->nonbottom_begin <= block->marked_nonbottom_begin);
                                                                                            assert(block->marked_nonbottom_begin == block->end);
                                                                                            assert(partitioner.branching||block->nonbottom_begin==block->end);
                                                                                            assert(0 <= block->seqnr);
                                                                                            assert(block->seqnr < nr_of_blocks);
                                                                                            unsigned const max_block(check_complexity::log_n -
                                                                                                                       check_complexity::ilog2(block->size()));
                                                                                            mCRL2complexity(block, no_temporary_work(max_block), partitioner);
 
                                                                                            // states in the block are consistent:
                                                                                            do
                                                                                            {
                                                                                                const state_info_entry* const state(perm_iter->st);
                                                                                                // assert(&part_tr.pred.front() < state->pred_inert.begin);
                                                                                                assert(&state_info.back() == state ||
                                                                                                         state->pred_inert.begin <= state[1].pred_inert.begin);
                                                                                                // assert(state->pred_inert.begin <= &part_tr.pred.back());
                                                                                                // assert(state->succ_inert.begin <= &part_tr.succ.back());
                                                                                                if (perm_iter < block->nonbottom_begin)
                                                                                                {
                                                                                                    assert(&state_info.back() == state || state->
                                                                                                                succ_inert.begin <= state[1].succ_inert.begin);
                                                                                                    // assert(state->succ_inert.begin==&part_tr.succ.back() ||
                                                                                                    //    state <
                                                                                                    //     state->succ_inert.begin->block_bunch->pred->source);
                                                                                                    mCRL2complexity(state, no_temporary_work(max_block, true),
                                                                                                                                                  partitioner);
                                                                                                }
                                                                                                else
                                                                                                {
                                                                                                    // assert(state->succ_inert.begin < &part_tr.succ.back());
                                                                                                    assert(&state_info.back() == state || state->
                                                                                                                 succ_inert.begin < state[1].succ_inert.begin);
                                                                                                    //assert(state ==
                                                                                                    //     state->succ_inert.begin->block_bunch->pred->source);
                                                                                                    mCRL2complexity(state, no_temporary_work(max_block, false),
                                                                                                                                                  partitioner);
                                                                                                }
                                                                                                assert(block == state->bl.ock);
                                                                                                assert(perm_iter == state->pos);
                                                                                            }
                                                                                            while (++perm_iter < block->end);
                                                                                            assert(perm_iter == block->end);
                                                                                            ++true_nr_of_blocks;
                                                                                        }
                                                                                        while (perm_iter <= &permutation.back());
                                                                                        assert(nr_of_blocks == true_nr_of_blocks);
                                                                                    }
                                                                                #endif
};
 
 
 
 
 
                                                                                #ifndef NDEBUG
/* ************************************************************************* */     static struct {
/*                                                                           */         bool operator()(const iterator_or_counter<action_block_entry*> p1,
/*                           T R A N S I T I O N S                           */                             const action_block_entry* const action_block) const
/*                                                                           */         {
/* ************************************************************************* */             return p1.begin > action_block;
                                                                                        }
                                                                                    } const action_label_greater;
                                                                                #endif
 
 
 
 
class succ_entry
{
  public:
    block_bunch_entry* block_bunch;
 
    succ_entry* begin_or_before_end;
 
 
    succ_entry* out_slice_begin(                                                ONLY_IF_DEBUG( const bisim_gjkw::fixed_vector<succ_entry>& succ )
                                );
 
 
    bunch_t* bunch() const;
                                                                                #ifndef NDEBUG
                                                                                    template <class LTS_TYPE>
                                                                                    static inline void add_work_to_out_slice(
                                                                                                  const bisim_partitioner_dnj<LTS_TYPE>& partitioner,
                                                                                                  const succ_entry* out_slice_begin,
                                                                                                  enum check_complexity::counter_type ctr, unsigned max_value);
                                                                                #endif
};
 
 
class block_bunch_entry
{
  public:
    pred_entry* pred;
 
    block_bunch_slice_iter_or_null_t slice;
};
 
 
class pred_entry
{
  public:
    action_block_entry* action_block;
 
    state_info_entry* source;
 
    state_info_entry* target;
                                                                                #ifndef NDEBUG
                                                                                    template <class LTS_TYPE>
                                                                                    std::string debug_id_short(const bisim_partitioner_dnj<LTS_TYPE>&
                                                                                                                                             partitioner) const
                                                                                    {
                                                                                        return "from " + source->debug_id_short(partitioner) +
                                                                                                                  " to " + target->debug_id_short(partitioner);
                                                                                    }
 
                                                                                    template <class LTS_TYPE>
                                                                                    std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
                                                                                                                                                          const
                                                                                    {
                                                                                        // Search for the action label in partitioner.action_label
                                                                                        label_type const label(std::lower_bound(
                                                                                            partitioner.action_label.cbegin(), partitioner.action_label.cend(),
                                                                                                                      action_block, action_label_greater) -
                                                                                                                            partitioner.action_label.cbegin());
                                                                                        assert(label < partitioner.action_label.size());
                                                                                        assert(partitioner.action_label[label].begin <= action_block);
                                                                                        assert(0==label||action_block<partitioner.action_label[label-1].begin);
                                                                                        // class lts_lts_t uses a function pp() to transform the action label
                                                                                        // to a string.
                                                                                        return pp(partitioner.aut.action_label(label)) + "-transition " +
                                                                                                                                   debug_id_short(partitioner);
                                                                                    }
 
                                                                                    mutable check_complexity::trans_dnj_counter_t work_counter;
                                                                                #endif
};
 
 
class action_block_entry
{
  public:
    succ_entry* succ;
 
    action_block_entry* begin_or_before_end;
 
 
    action_block_entry* action_block_slice_begin(                               ONLY_IF_DEBUG( const action_block_entry* const action_block_begin,
                                                                                                const action_block_entry* const action_block_orig_inert_begin )
                                                 )
    {
        action_block_entry* result(begin_or_before_end);                        assert(nullptr != result);
        if (this < result)
        {                                                                       assert(this == result->begin_or_before_end);
            result = this;                                                      // The following assertion does not always hold: the function is called
        }                                                                       // immediately after a block is refined, so it may be the case that the
                                                                                // transitions are still to be moved to different slices.
                                                                                // assert(succ->block_bunch->pred->target->bl.ock ==
                                                                                //                            result->succ->block_bunch->pred->target->bl.ock);
                                                                                assert(nullptr != succ);  assert(nullptr != result->succ);
                                                                                assert(succ->bunch() == result->succ->bunch());
                                                                                assert(result == action_block_begin || nullptr == result[-1].succ ||
                                                                                            action_block_orig_inert_begin <= result ||
                                                                                            result[-1].succ->block_bunch->pred->target->bl.ock !=
                                                                                                              result->succ->block_bunch->pred->target->bl.ock);
                                                                                // assert(this has the same action as result);
        return result;
    }
};
 
 
class part_trans_t;
 
class bunch_t
{
  public:
    action_block_entry* begin;
 
    action_block_entry* end;
 
    union next_nontrivial_and_label_t
    {
        bunch_t* next_nontrivial;
 
        label_type label;
 
 
        next_nontrivial_and_label_t()
        {
            next_nontrivial = nullptr;
        }
    } next_nontrivial_and_label;
 
 
    bunch_t(action_block_entry* const new_begin,
                                             action_block_entry* const new_end)
      : begin(new_begin),
        end(new_end),
        next_nontrivial_and_label()
    {  }
 
 
    bool is_trivial() const
    {
        return nullptr == next_nontrivial_and_label.next_nontrivial;
    }
 
 
    bunch_t* split_off_small_action_block_slice(part_trans_t& part_tr);
                                                                                #ifndef NDEBUG
                                                                                    template <class LTS_TYPE>
                                                                                    std::string debug_id_short(const bisim_partitioner_dnj<LTS_TYPE>&
                                                                                                                                             partitioner) const
                                                                                    {
                                                                                        assert(partitioner.part_tr.action_block_begin <= begin);
                                                                                        assert(end <= partitioner.part_tr.action_block_inert_begin);
                                                                                        return "bunch [" + std::to_string(begin -
                                                                                                                partitioner.part_tr.action_block_begin) + "," +
                                                                                            std::to_string(end - partitioner.part_tr.action_block_begin) + ")";
                                                                                    }
 
                                                                                    template <class LTS_TYPE>
                                                                                    std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
                                                                                                                                                          const
                                                                                    {   assert(nullptr != end[-1].succ);
                                                                                        const action_block_entry* iter(begin);  assert(iter < end);
                                                                                        assert(nullptr != iter->succ);
                                                                                        assert(iter == iter->succ->block_bunch->pred->action_block);
                                                                                        std::string result(debug_id_short(partitioner));
                                                                                        result += " containing transition";
                                                                                        result += iter < end - 1 ? "s " : " ";
                                                                                        result += iter->succ->block_bunch->pred->debug_id_short(partitioner);
                                                                                        ++iter;
                                                                                        if (end <= iter)  return result;
                                                                                        while (nullptr == iter->succ)  ++iter;
                                                                                        assert(iter < end);
                                                                                        assert(iter == iter->succ->block_bunch->pred->action_block);
                                                                                        result += ", ";
                                                                                        result += iter->succ->block_bunch->pred->debug_id_short(partitioner);
                                                                                        if (iter < end - 3)
                                                                                        {
                                                                                            result += ", ...";
                                                                                            iter = end - 3;
                                                                                        }
                                                                                        while (++iter < end)
                                                                                        {
                                                                                            if (nullptr != iter->succ)
                                                                                            {   assert(iter == iter->succ->block_bunch->pred->action_block);
                                                                                                result += ", ";
                                                                                                result += iter->succ->block_bunch->pred->debug_id_short(
                                                                                                                                                  partitioner);
                                                                                            }
                                                                                        }
                                                                                        return result;
                                                                                    }
 
                                                                                    template <class LTS_TYPE>
                                                                                    int max_work_counter(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
                                                                                                                                                          const
                                                                                    {
                                                                                        // verify that the bunch only has a single action label.
                                                                                        // Search for the action label in partitioner.action_label
                                                                                        label_type const label(std::lower_bound(
                                                                                            partitioner.action_label.cbegin(), partitioner.action_label.cend(),
                                                                                                                                begin, action_label_greater) -
                                                                                                                            partitioner.action_label.cbegin());
                                                                                        assert(label < partitioner.action_label.size());
                                                                                        assert(partitioner.action_label[label].begin <= begin);
                                                                                        assert(0 == label || begin < partitioner.action_label[label-1].begin);
                                                                                        if (0 == label || end < partitioner.action_label[label - 1].begin)
                                                                                        {
                                                                                            assert(check_complexity::ilog2(end - begin) <=
                                                                                                                                      check_complexity::log_n);
                                                                                            return check_complexity::log_n-check_complexity::ilog2(end-begin);
                                                                                        }
                                                                                        return 0;
                                                                                    }
 
                                                                                    mutable check_complexity::bunch_dnj_counter_t work_counter;
                                                                                #endif
};
 
 
class block_bunch_slice_t
{
  public:
    block_bunch_entry* end;
 
    bunch_t* bunch;
 
    block_bunch_entry* marked_begin;
 
 
    bool is_stable() const  {  return nullptr == marked_begin;  }
 
 
    void make_stable()
    {                                                                           assert(!is_stable());  assert(!empty());
        marked_begin = nullptr;
    }
 
 
    void make_unstable()
    {                                                                           assert(is_stable());
        marked_begin = end;                                                     assert(!is_stable());
    }
 
 
    block_bunch_slice_t(block_bunch_entry* const new_end,
                            bunch_t* const new_bunch, bool const new_is_stable)
      : end(new_end),
        bunch(new_bunch),
        marked_begin(nullptr)
    {
        if (!new_is_stable)  make_unstable();
    }
 
 
    bool empty() const
    {                                                                           // assert(std::less(&part_tr.block_bunch.front(), end));
                                                                                // assert(!std::less(part_tr.block_bunch_inert_begin, end));
                                                                                // assert(part_tr.block_bunch.front().slice != this);
        return end[-1].slice != this;
    }
 
 
    block_t* source_block() const
    {                                                                           assert(!empty());
        return end[-1].pred->source->bl.ock;
    }
                                                                                #ifndef NDEBUG
                                                                                    template <class LTS_TYPE>
                                                                                    std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
                                                                                                                                                          const
                                                                                    {
                                                                                        static struct {
                                                                                            bool operator()(const block_bunch_entry& p1,
                                                                                                                     const block_bunch_slice_t* const p2) const
                                                                                            {
                                                                                                return p1.slice != p2;
                                                                                            }
                                                                                        } const block_bunch_not_equal;
 
                                                                                        assert(&partitioner.part_tr.block_bunch.front() < end);
                                                                                        assert(end <= partitioner.part_tr.block_bunch_inert_begin);
                                                                                        std::string const index_string(std::to_string(end -
                                                                                                                &partitioner.part_tr.block_bunch.cbegin()[1]));
                                                                                        if (empty())
                                                                                        {   //assert(!is_stable());
                                                                                            return "empty block_bunch_slice [" + index_string + "," +
                                                                                                                                            index_string + ")";
                                                                                        }
                                                                                        const block_bunch_entry* begin(
                                                                                                                 &partitioner.part_tr.block_bunch.cbegin()[1]);
                                                                                        if (trans_type bunch_size(bunch->end - bunch->begin);
                                                                                                                       (trans_type) (end - begin) > bunch_size)
                                                                                        {
                                                                                            begin = end - bunch_size;
                                                                                        }
                                                                                        begin = std::lower_bound(begin, const_cast<const block_bunch_entry*>
                                                                                                     (is_stable() || marked_begin==end ? end-1 : marked_begin),
                                                                                                                                  this, block_bunch_not_equal);
                                                                                        assert(begin->slice == this);
                                                                                        assert(begin[-1].slice != this);
                                                                                        return (is_stable() ? "stable block_bunch-slice ["
                                                                                                            : "unstable block_bunch_slice [") +
                                                                                           std::to_string(begin-&partitioner.part_tr.block_bunch.cbegin()[1]) +
                                                                                                        "," + index_string + ") containing transitions from " +
                                                                                                                   source_block()->debug_id(partitioner) +
                                                                                                                   " in " + bunch->debug_id_short(partitioner);
                                                                                    }
 
                                                                                    template <class LTS_TYPE>
                                                                                    bool add_work_to_bottom_transns(enum check_complexity::
                                                                                                      counter_type const ctr, unsigned const max_value,
                                                                                                      const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
                                                                                    {   assert(!empty());
                                                                                        assert(1U == max_value);
                                                                                        const block_t* const block(source_block());
                                                                                        bool result(false);
                                                                                        const block_bunch_entry* block_bunch(end);
                                                                                        assert(partitioner.part_tr.block_bunch.front().slice != this);
                                                                                        assert(block_bunch[-1].slice == this);
                                                                                        do
                                                                                        {
                                                                                            --block_bunch;
                                                                                            const state_info_entry* const source(block_bunch->pred->source);
                                                                                            assert(source->bl.ock == block);
                                                                                            if (source->pos < block->nonbottom_begin /*&&
                                                                                                // the transition starts in a (new) bottom state
                                                                                                block_bunch->pred->work_counter.counters[ctr -
                                                                                                               check_complexity::TRANS_dnj_MIN] != max_value*/)
                                                                                            {
                                                                                                mCRL2complexity(block_bunch->pred, add_work(ctr, max_value),
                                                                                                                                                  partitioner);
                                                                                                result = true;
                                                                                            }
                                                                                        }
                                                                                        while (block_bunch[-1].slice == this);
                                                                                        return result;
                                                                                    }
 
                                                                                    mutable check_complexity::block_bunch_dnj_counter_t work_counter;
                                                                                #endif
};
 
 
inline succ_entry* succ_entry::out_slice_begin(                                 ONLY_IF_DEBUG( const bisim_gjkw::fixed_vector<succ_entry>& succ )
                                               )
{                                                                               assert(nullptr != begin_or_before_end);
    succ_entry* result(begin_or_before_end);                                    assert(result->block_bunch->pred->action_block->succ == result);
    if (this < result)
    {                                                                           assert(nullptr != result->begin_or_before_end);
                                                                                assert(this == result->begin_or_before_end);
        result = this;                                                          assert(result->block_bunch->pred->action_block->succ == result);
    }                                                                           assert(block_bunch->pred->source == result->block_bunch->pred->source);
                                                                                // assert(this <= result); //< holds always, based on the if() above
                                                                                assert(nullptr != result->begin_or_before_end);
                                                                                assert(this <= result->begin_or_before_end);
                                                                                assert(block_bunch->slice == result->block_bunch->slice);
                                                                                assert(&succ.cbegin()[1] == result ||
                                                                                        result[-1].block_bunch->pred->source < block_bunch->pred->source ||
                                                                                                              result[-1].bunch() != block_bunch->slice->bunch);
    return result;
}
 
 
inline bunch_t* succ_entry::bunch() const
{
    return block_bunch->slice->bunch;
}
                                                                                #ifndef NDEBUG
                                                                                    template <class LTS_TYPE>
                                                                                    /* static */ inline void succ_entry::add_work_to_out_slice(
                                                                                        const bisim_partitioner_dnj<LTS_TYPE>& partitioner,
                                                                                        const succ_entry* out_slice_begin,
                                                                                        enum check_complexity::counter_type const ctr,unsigned const max_value)
                                                                                    {
                                                                                        const succ_entry* const out_slice_before_end(
                                                                                                                         out_slice_begin->begin_or_before_end);
                                                                                        assert(nullptr != out_slice_before_end);
                                                                                        assert(out_slice_begin <= out_slice_before_end);
                                                                                        mCRL2complexity(out_slice_begin->block_bunch->pred,
                                                                                                                        add_work(ctr, max_value), partitioner);
                                                                                        while (++out_slice_begin <= out_slice_before_end)
                                                                                        {
                                                                                            // treat temporary counters specially
                                                                                            mCRL2complexity(out_slice_begin->block_bunch->pred,
                                                                                                            add_work_notemporary(ctr, max_value), partitioner);
                                                                                        }
                                                                                    }
                                                                                #endif
class part_trans_t
{
  public:
    bisim_gjkw::fixed_vector<succ_entry> succ;
 
    bisim_gjkw::fixed_vector<block_bunch_entry> block_bunch;
 
    bisim_gjkw::fixed_vector<pred_entry> pred;
 
    action_block_entry* const action_block_begin;
    action_block_entry* const action_block_end;
 
    block_bunch_entry* block_bunch_inert_begin;
 
    action_block_entry* action_block_inert_begin;
                                                                                #ifndef NDEBUG
                                                                                    const action_block_entry* action_block_orig_inert_begin;
                                                                                #endif
    simple_list<block_bunch_slice_t> splitter_list;
   private:
    bunch_t* first_nontrivial;
 
  public:
    #ifdef USE_POOL_ALLOCATOR
                                                                                static_assert(std::is_trivially_destructible<bunch_t>::value);
                                                                                static_assert(std::is_trivially_destructible<
                                                                                                              simple_list<block_bunch_slice_t>::entry>::value);
        my_pool<simple_list<block_bunch_slice_t>::entry> storage;
    #endif
 
    state_type nr_of_new_bottom_states;
 
    trans_type nr_of_bunches;
    trans_type nr_of_nontrivial_bunches;
    trans_type nr_of_action_block_slices;
    trans_type nr_of_block_bunch_slices;
 
    part_trans_t(trans_type num_transitions,
                 trans_type num_actions)
      : succ(num_transitions + 2),
        block_bunch(num_transitions + 1),
        pred(num_transitions + 2),
        action_block_begin(
                    new action_block_entry[num_transitions + num_actions - 1]),
        action_block_end(action_block_begin + (num_transitions+num_actions-1)),
        block_bunch_inert_begin(1 + &block_bunch.back()),
        action_block_inert_begin(action_block_end),
        splitter_list(),
        first_nontrivial(nullptr),
        nr_of_new_bottom_states(0),
        nr_of_bunches(0),
        nr_of_nontrivial_bunches(0),
        nr_of_action_block_slices(0),
        nr_of_block_bunch_slices(0)
    {
        succ.front().block_bunch = &block_bunch.front();
        succ.back() .block_bunch = &block_bunch.front();
        block_bunch.front().pred = &pred.front();
        block_bunch.front().slice = nullptr;
        pred.front().source = nullptr;
        pred.front().target = nullptr;
        pred.back() .source = nullptr;
        pred.back() .target = nullptr;
    }
 
 
    ~part_trans_t()
    {
        #ifndef USE_POOL_ALLOCATOR
            // The destructor also deallocates the bunches, as they are not
            // directly referenced from anywhere.  This is only necessary if we
            // do not use the pool allocator, as the latter will destroy the
            // bunches wholesale.
            action_block_entry* action_block_iter(action_block_begin);
            for (;;)
            {
                do
                {
                    if (action_block_inert_begin <= action_block_iter)
                    {                                                           assert(0 == nr_of_bunches);
                        delete [] action_block_begin;
                        return;
                    }
                }
                while (nullptr == action_block_iter->succ && (                  assert(nullptr == action_block_iter->begin_or_before_end),
                                                   ++action_block_iter, true)); assert(nullptr != action_block_iter->begin_or_before_end);
                bunch_t* const bunch(action_block_iter->succ->bunch());         assert(bunch->begin == action_block_iter);
                action_block_iter = bunch->end;
                delete bunch;                                                   ONLY_IF_DEBUG( --nr_of_bunches; )
            }
            /* unreachable                                                   */ assert(0);
        #else
            delete [] action_block_begin;
        #endif
    }
 
 
    bunch_t* get_some_nontrivial()
    {
        return first_nontrivial;
    }
 
 
    void make_nontrivial(bunch_t* const bunch)
    {                                                                           assert(1 < bunch->end - bunch->begin);  assert(bunch->is_trivial());
                                                                                // The following assertions do not necessarily hold during initialisation:
                                                                                //assert(bunch->begin <= bunch->begin->begin_or_before_end);
        bunch->next_nontrivial_and_label.next_nontrivial =
                        nullptr == first_nontrivial ? bunch : first_nontrivial; //assert(nullptr != bunch->begin->begin_or_before_end);
                                                                                //assert(nullptr != bunch->end[-1].begin_or_before_end);
                                                                                //assert(bunch->begin->begin_or_before_end <
                                                                                //                                         bunch->end[-1].begin_or_before_end);
                                                                                //assert(nullptr != end[-1].begin_or_before_end);
        first_nontrivial = bunch;                                               assert(nr_of_nontrivial_bunches < nr_of_bunches);
        ++nr_of_nontrivial_bunches;                                             //assert(end[-1].begin_or_before_end <= end);
    }
 
 
    void make_trivial(bunch_t* const bunch)
    {                                                                           assert(!bunch->is_trivial());  assert(first_nontrivial == bunch);
        first_nontrivial =
                bunch == bunch->next_nontrivial_and_label.next_nontrivial
                  ? nullptr : bunch->next_nontrivial_and_label.next_nontrivial; assert(bunch->end - 1 == bunch->begin->begin_or_before_end);
        bunch->next_nontrivial_and_label.next_nontrivial = nullptr;             assert(0 < nr_of_nontrivial_bunches);
        --nr_of_nontrivial_bunches;                                             assert(bunch->begin == bunch->end[-1].begin_or_before_end);
    }
 
 
    void first_move_transition_to_new_bunch(
                                   action_block_entry* const action_block_iter,
                                   bunch_t* const bunch_T_a_Bprime,
                                   bool const first_transition_of_state)
    {
 
        /* -  -  -  -  -  -  -  - adapt part_tr.succ -  -  -  -  -  -  -  - */
 
        succ_entry* const old_succ_pos(action_block_iter->succ);                assert(nullptr != old_succ_pos);
                                                                                assert(old_succ_pos->block_bunch->pred->action_block == action_block_iter);
        succ_entry* const out_slice_begin(old_succ_pos->out_slice_begin(        ONLY_IF_DEBUG( succ )
                                                                  ));           assert(out_slice_begin->block_bunch->pred->action_block->succ ==
                                                                                                                                              out_slice_begin);
        succ_entry* const new_succ_pos(out_slice_begin->begin_or_before_end);   assert(nullptr != new_succ_pos);
                                                                                assert(out_slice_begin == new_succ_pos->begin_or_before_end);
                                                                                assert(new_succ_pos<old_succ_pos->block_bunch->pred->source->succ_inert.begin);
        /* move the transition to the end of its out-slice                   */ assert(new_succ_pos->block_bunch->pred->action_block->succ == new_succ_pos);
        if (old_succ_pos < new_succ_pos)
        {
            std::swap(old_succ_pos->block_bunch, new_succ_pos->block_bunch);
            old_succ_pos->block_bunch->pred->action_block->succ = old_succ_pos; assert(action_block_iter == new_succ_pos->block_bunch->pred->action_block);
            action_block_iter->succ = new_succ_pos;
        }                                                                       else  assert(old_succ_pos == new_succ_pos);
 
        // adapt the old out-slice immediately
            // If the old out-slice becomes empty, then out_slice_begin ==
            // new_succ_pos, so the two following assignments will assign the
            // same variable.  The second assignment is the relevant one.
        out_slice_begin->begin_or_before_end = new_succ_pos - 1;
 
        // adapt the new out-slice, as far as is possible now:
            // make the begin_or_before_end pointers of the first and last
            // transition in the slice correct immediately.  The other
            // begin_or_before_end pointers need to be corrected after all
            // transitions in the new bunch have been positioned correctly.
        if (first_transition_of_state)
        {
            new_succ_pos->begin_or_before_end = new_succ_pos;
        }
        else
        {
            succ_entry* const out_slice_before_end(
                                          new_succ_pos[1].begin_or_before_end); assert(nullptr != out_slice_before_end);
                                                                                assert(new_succ_pos < out_slice_before_end);
                                                                                assert(out_slice_before_end->block_bunch->pred->action_block->succ ==
                                                                                                                                         out_slice_before_end);
                                                                                assert(new_succ_pos + 1 == out_slice_before_end->begin_or_before_end);
            out_slice_before_end->begin_or_before_end = new_succ_pos;           assert(out_slice_before_end <
                                                                                                    new_succ_pos->block_bunch->pred->source->succ_inert.begin);
            new_succ_pos->begin_or_before_end = out_slice_before_end;           assert(bunch_T_a_Bprime == out_slice_before_end->bunch());
        }
 
        /* -  -  -  -  -  -  - adapt part_tr.block_bunch -  -  -  -  -  -  - */ assert(new_succ_pos == action_block_iter->succ);
 
        block_bunch_entry* const old_block_bunch_pos(
                                                    new_succ_pos->block_bunch); assert(old_block_bunch_pos->pred->action_block == action_block_iter);
        block_t*const source_block = old_block_bunch_pos->pred->source->bl.ock; assert(!old_block_bunch_pos->slice.is_null());
        block_bunch_slice_iter_t const old_block_bunch_slice(
                                                   old_block_bunch_pos->slice);
        block_bunch_entry* const new_block_bunch_pos(
                                               old_block_bunch_slice->end - 1); assert(nullptr != new_block_bunch_pos->pred->action_block->succ);
                                                                                assert(new_block_bunch_pos->pred->action_block->succ->block_bunch ==
                                                                                                                                          new_block_bunch_pos);
        // create or adapt the new block_bunch-slice
        block_bunch_slice_iter_t new_block_bunch_slice;
        if (new_block_bunch_pos + 1 >= block_bunch_inert_begin ||
                       (new_block_bunch_slice = (block_bunch_slice_iter_t)
                                                new_block_bunch_pos[1].slice,   assert(!new_block_bunch_pos[1].slice.is_null()),
                        bunch_T_a_Bprime != new_block_bunch_slice->bunch ||
                        source_block != new_block_bunch_slice->source_block()))
        {                                                                       assert(first_transition_of_state);
            // This is the first transition in the block_bunch-slice.
            // The old block_bunch-slice becomes unstable, and the new
            // block_bunch-slice is created unstable.
 
            // Note that the new block_bunch-slice should precede the old one.
 
            #ifdef USE_SIMPLE_LIST
                new_block_bunch_slice = splitter_list.emplace_back(
                            ONLY_IF_POOL_ALLOCATOR( storage, )
                             new_block_bunch_pos + 1, bunch_T_a_Bprime, false);
            #else
                splitter_list.emplace_back(new_block_bunch_pos + 1,
                                                      bunch_T_a_Bprime, false);
                new_block_bunch_slice = std::prev(splitter_list.end());
            #endif
            ++nr_of_block_bunch_slices;                                         ONLY_IF_DEBUG( new_block_bunch_slice->work_counter =
                                                                                                                         old_block_bunch_slice->work_counter; )
            splitter_list.splice(splitter_list.end(),
                      source_block->stable_block_bunch, old_block_bunch_slice);
            old_block_bunch_slice->make_unstable();
        }                                                                       assert(!new_block_bunch_slice->is_stable());
 
        // move the transition to the end of its block_bunch-slice
        if (old_block_bunch_pos < new_block_bunch_pos)
        {
            std::swap(old_block_bunch_pos->pred, new_block_bunch_pos->pred);    assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
            old_block_bunch_pos->pred->action_block->succ->block_bunch =
                                                           old_block_bunch_pos; assert(new_succ_pos == new_block_bunch_pos->pred->action_block->succ);
            new_succ_pos->block_bunch = new_block_bunch_pos;
        }                                                                       else  assert(new_block_bunch_pos == old_block_bunch_pos);
                                                                                assert(new_block_bunch_pos->slice == old_block_bunch_slice);
        new_block_bunch_pos->slice = new_block_bunch_slice;
 
        /* adapt the old block_bunch-slice                                   */ assert(new_block_bunch_pos + 1 == old_block_bunch_slice->marked_begin);
        old_block_bunch_slice->end = new_block_bunch_pos;
        old_block_bunch_slice->marked_begin = new_block_bunch_pos;              assert(nullptr != new_block_bunch_pos);
        if (old_block_bunch_slice->empty())
        {                                                                       assert(!old_block_bunch_slice->is_stable());
            splitter_list.erase(  ONLY_IF_POOL_ALLOCATOR( storage, )
                                                        old_block_bunch_slice); assert(!new_block_bunch_slice->is_stable());
            --nr_of_block_bunch_slices;
 
            // Because now every bottom state has a transition in the new
            // bunch, and no state has a transition in the old bunch, there
            // is no need to refine this block.  So we make this
            // block_bunch-slice stable again.
            source_block->stable_block_bunch.splice(
                                        source_block->stable_block_bunch.end(),
                                        splitter_list, new_block_bunch_slice);
            new_block_bunch_slice->make_stable();
 
            // unmark the states
                // (This transition must be the last transition from
                // source_block in the new bunch, so unmarking the states now
                // will not be undone by later markings of other states.)
            source_block->marked_nonbottom_begin = source_block->end;           assert(source_block->marked_bottom_begin == source_block->begin);
            source_block->marked_bottom_begin = source_block->nonbottom_begin;
        }
    }
 
 
                                                                                ONLY_IF_DEBUG( template <class LTS_TYPE> )
    void second_move_transition_to_new_bunch(
                                   action_block_entry* const action_block_iter, ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner,
                                                                                                                             bunch_t* const bunch_T_a_Bprime, )
                                   bunch_t* const large_splitter_bunch)
    {                                                                           assert(nullptr != bunch_T_a_Bprime);
 
        /* -  -  -  -  -  -  -  - adapt part_tr.succ -  -  -  -  -  -  -  - */
 
            // We already moved the transition in part_tr.succ to the correct
            // place in first_move_transition_to_new_bunch(); now we have to
            // set begin_or_before_end.
        succ_entry* const new_succ_pos(action_block_iter->succ);                assert(nullptr != new_succ_pos);
                                                                                assert(new_succ_pos->block_bunch->pred->action_block == action_block_iter);
        state_info_entry* const source(
                                      new_succ_pos->block_bunch->pred->source); assert(source->pos->st == source);
                                                                                assert(new_succ_pos < source->succ_inert.begin);
                                                                                assert(source == &partitioner.part_st.state_info.front() ||
                                                                                                                  source[-1].succ_inert.begin <= new_succ_pos);
                                                                                assert(nullptr != new_succ_pos->begin_or_before_end);
        succ_entry* const new_begin_or_before_end(
                       new_succ_pos->begin_or_before_end->begin_or_before_end); assert(nullptr != new_begin_or_before_end);
                                                                                assert(new_begin_or_before_end->block_bunch->pred->action_block->succ ==
                                                                                                                                      new_begin_or_before_end);
        if (new_begin_or_before_end < new_succ_pos)
        {                                                                       assert(source == &partitioner.part_st.state_info.front() ||
                                                                                                       source[-1].succ_inert.begin <= new_begin_or_before_end);
            new_succ_pos->begin_or_before_end = new_begin_or_before_end;
        }
        else
        {                                                                       assert(new_begin_or_before_end == new_succ_pos);
            // This is the first or the last transition in the out-slice.
            const succ_entry* const new_before_end(
                                 new_begin_or_before_end->begin_or_before_end); assert(nullptr != new_before_end);
            if (new_begin_or_before_end <= new_before_end)
            {                                                                   assert(&partitioner.part_tr.succ.cbegin()[1] == new_begin_or_before_end ||
                /* This is the first transition in the new out-slice.        */             new_begin_or_before_end[-1].block_bunch->pred->source < source ||
                /* If there is still a transition in the old out-slice,      */                       new_begin_or_before_end[-1].bunch() != bunch_T_a_Bprime);
                /* we prepay for it.                                         */ assert(new_before_end + 1 == source->succ_inert.begin ||
                                                                                                                bunch_T_a_Bprime != new_before_end[1].bunch());
                if (source == new_succ_pos[-1].block_bunch->pred->source &&
                              new_succ_pos[-1].bunch() == large_splitter_bunch)
                {
                    // Mark one transition in the large slice
                    block_bunch_entry* const old_block_bunch_pos(
                                                 new_succ_pos[-1].block_bunch); assert(!old_block_bunch_pos->slice.is_null());
                                                                                assert(old_block_bunch_pos->pred->action_block->succ == new_succ_pos - 1);
                    block_bunch_slice_iter_t const large_splitter_slice(
                                                   old_block_bunch_pos->slice);
                    if (!large_splitter_slice->is_stable())
                    {
                        block_bunch_entry* const new_block_bunch_pos(
                                       large_splitter_slice->marked_begin - 1); assert(nullptr != new_block_bunch_pos->pred->action_block->succ);
                                                                                assert(new_block_bunch_pos->pred->action_block->succ->block_bunch ==
                                                                                                                                          new_block_bunch_pos);
                        if (old_block_bunch_pos < new_block_bunch_pos)
                        {
                            std::swap(old_block_bunch_pos->pred,
                                                    new_block_bunch_pos->pred); // assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
                            old_block_bunch_pos->pred->action_block->
                                       succ->block_bunch = old_block_bunch_pos; assert(new_block_bunch_pos->pred->action_block->succ == new_succ_pos - 1);
                            new_succ_pos[-1].block_bunch = new_block_bunch_pos;
                        }
                        large_splitter_slice->marked_begin=new_block_bunch_pos; assert(nullptr != new_block_bunch_pos);
                    }                                                           else assert(1 >= source->bl.ock->size());
                }
            }                                                                   else assert(source == &partitioner.part_st.state_info.front() ||
                                                                                                                source[-1].succ_inert.begin <= new_before_end);
        }
                                                                                #ifndef NDEBUG
        /* -  -  -  -  -  -  - adapt part_tr.block_bunch -  -  -  -  -  -  - */     const block_bunch_entry* new_block_bunch_pos(new_succ_pos->block_bunch);
                                                                                    assert(new_block_bunch_pos->pred->action_block->succ == new_succ_pos);
                                                                                    assert(!new_block_bunch_pos->slice.is_null());
        /* Nothing needs to be done.                                         */     block_bunch_slice_const_iter_t const new_block_bunch_slice(
                                                                                                                                   new_block_bunch_pos->slice);
                                                                                    assert(new_block_bunch_pos < new_block_bunch_slice->end);
                                                                                    assert(bunch_T_a_Bprime == new_block_bunch_slice->bunch);
                                                                                    if (new_block_bunch_pos + 1 < new_block_bunch_slice->end)  return;
 
                                                                                    // This transition is the last in the block_bunch-slice.  If there
                                                                                    // were some task that would need to be done exactly once per
                                                                                    // block_bunch-slice, this would be the moment.
                                                                                    do  assert(source->bl.ock == new_block_bunch_pos->pred->source->bl.ock);
                                                                                    while ((--new_block_bunch_pos)->slice == new_block_bunch_slice);
                                                                                    assert(new_block_bunch_pos <= &partitioner.part_tr.block_bunch.front() ||
                                                                                                source->bl.ock != new_block_bunch_pos->pred->source->bl.ock ||
                                                                                                        bunch_T_a_Bprime != new_block_bunch_pos->slice->bunch);
                                                                                #endif
    }
 
 
  private:
                                                                                ONLY_IF_DEBUG( template <class LTS_TYPE> )
    succ_entry* move_out_slice_to_new_block(
                               succ_entry* out_slice_end,                       ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner, )
                               #ifndef USE_SIMPLE_LIST
                                   block_t* const old_block,
                               #endif
                               block_bunch_slice_const_iter_t const splitter_T)
    {                                                                           assert(&succ.cbegin()[1] < out_slice_end);
        succ_entry* const out_slice_begin(
                                        out_slice_end[-1].begin_or_before_end); assert(nullptr != out_slice_begin);
                                                                                assert(out_slice_begin < out_slice_end);
                                                                                assert(out_slice_begin->block_bunch->pred->action_block->succ ==
                                                                                                                                              out_slice_begin);
        block_bunch_entry* old_block_bunch_pos(out_slice_end[-1].block_bunch);  assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
                                                                                assert(!old_block_bunch_pos->slice.is_null());
        block_bunch_slice_iter_t const old_block_bunch_slice(
                                                   old_block_bunch_pos->slice); assert(old_block_bunch_pos->pred->action_block->succ->block_bunch ==
                                                                                                                                          old_block_bunch_pos);
        if (&*splitter_T == &*old_block_bunch_slice)  return out_slice_begin;
 
        block_bunch_entry* old_block_bunch_slice_end(
                                                   old_block_bunch_slice->end);
        state_info_entry* const source(old_block_bunch_pos->pred->source);      assert(out_slice_end <= source->succ_inert.begin);
                                                                                assert(&partitioner.part_st.state_info.front() == source ||
                                                                                                                  source[-1].succ_inert.begin < out_slice_end);
        block_t* const new_block(source->bl.ock);                               assert(source == out_slice_begin->block_bunch->pred->source);
        block_bunch_slice_iter_t new_block_bunch_slice;                         assert(source->pos->st == source);
        if (old_block_bunch_slice_end >= block_bunch_inert_begin ||
            new_block != old_block_bunch_slice_end->pred->source->bl.ock ||
                (new_block_bunch_slice = (block_bunch_slice_iter_t)
                                         old_block_bunch_slice_end->slice,      assert(!old_block_bunch_slice_end->slice.is_null()),
                 old_block_bunch_slice->bunch != new_block_bunch_slice->bunch))
        {
            // the new block_bunch-slice is not suitable; create a new one and
            // insert it into the correct list.
            if (old_block_bunch_slice->is_stable())
            {
                // In most cases, but not always, the source is a bottom state.
                #ifdef USE_SIMPLE_LIST
                    new_block_bunch_slice =
                        new_block->stable_block_bunch.emplace_front(
                                ONLY_IF_POOL_ALLOCATOR( storage, )
                                           old_block_bunch_slice->end,
                                           old_block_bunch_slice->bunch, true);
                #else
                    new_block->stable_block_bunch.emplace_front(
                                           old_block_bunch_slice->end,
                                           old_block_bunch_slice->bunch, true);
                    new_block_bunch_slice =
                                         new_block->stable_block_bunch.begin();
                #endif
            }
            else
            {
                #ifdef USE_SIMPLE_LIST
                    new_block_bunch_slice = splitter_list.emplace_after(
                            ONLY_IF_POOL_ALLOCATOR( storage, )
                                          old_block_bunch_slice,
                                          old_block_bunch_slice->end,
                                          old_block_bunch_slice->bunch, false);
                #else
                    new_block_bunch_slice = splitter_list.emplace(
                                          std::next(old_block_bunch_slice),
                                          old_block_bunch_slice->end,
                                          old_block_bunch_slice->bunch, false);
                #endif
            }
            ++nr_of_block_bunch_slices;                                         ONLY_IF_DEBUG( new_block_bunch_slice->work_counter =
                                                                                                                         old_block_bunch_slice->work_counter; )
        }
                                                                                ONLY_IF_DEBUG( unsigned max_counter = check_complexity::log_n -
                                                                                                                  check_complexity::ilog2(new_block->size()); )
        /* move all transitions in this out-slice to the new block_bunch     */ assert(out_slice_begin < out_slice_end);
        do
        {                                                                       assert(old_block_bunch_pos == out_slice_end[-1].block_bunch);
            --out_slice_end;                                                    assert(old_block_bunch_pos->slice == old_block_bunch_slice);
                                                                                assert(source == out_slice_end->block_bunch->pred->source);
            --old_block_bunch_slice_end;                                        // assign work already now because the transition may be moved to several
                                                                                // places:
            old_block_bunch_slice_end->slice = new_block_bunch_slice;           mCRL2complexity(old_block_bunch_pos->pred, add_work(
                                                                                     check_complexity::move_out_slice_to_new_block, max_counter), partitioner);
            if (old_block_bunch_slice->is_stable() || (                         assert(!new_block_bunch_slice->is_stable()),
                 old_block_bunch_slice->marked_begin >
                                                 old_block_bunch_slice_end &&
                 (/* As the old block_bunch-slice has no marked              */ assert(nullptr != old_block_bunch_slice_end),
                  // transitions, it is enough to adapt its marked_begin
                  // and then do a simple (two-way) swap.
                  old_block_bunch_slice->marked_begin =
                                             old_block_bunch_slice_end, true)))
            {
                // The old block_bunch-slice is stable, or it has no
                // marked transitions.
                std::swap(old_block_bunch_pos->pred,
                                              old_block_bunch_slice_end->pred);
            }
            else
            {
                // The old block_bunch-slice is unstable and has marked
                // transitions.
                pred_entry* const old_pred = old_block_bunch_pos->pred;
                if (old_block_bunch_pos < old_block_bunch_slice->marked_begin)
                {
                    // The transition is not marked, but there are other
                    // marked transitions in the old block_bunch-slice.
                    // Move the transition to the non-marked part of the
                    // new block_bunch-slice.
                    block_bunch_entry* const old_marked_begin =
                                       old_block_bunch_slice->marked_begin - 1; assert(old_block_bunch_pos < old_block_bunch_slice_end);
                    old_block_bunch_slice->marked_begin = old_marked_begin;
 
                    old_block_bunch_pos->pred = old_marked_begin->pred;
                    old_marked_begin->pred = old_block_bunch_slice_end->pred;
                    old_block_bunch_slice_end->pred = old_pred;                 assert(nullptr != old_marked_begin->pred->action_block->succ);
 
                    old_marked_begin->pred->action_block->succ->
                                                block_bunch = old_marked_begin;
                }
                else
                {
                    // The transition is marked. Move to the marked part
                    // of the new block_bunch-slice.
                    block_bunch_entry* const new_marked_begin =
                                       new_block_bunch_slice->marked_begin - 1;
                    new_block_bunch_slice->marked_begin = new_marked_begin;     assert(old_block_bunch_pos < new_marked_begin ||
                                                                                                             old_block_bunch_pos == old_block_bunch_slice_end);
                    old_block_bunch_pos->pred=old_block_bunch_slice_end->pred;  assert(old_block_bunch_slice_end <= new_marked_begin);
                    old_block_bunch_slice_end->pred = new_marked_begin->pred;
                    new_marked_begin->pred = old_pred;                          assert(out_slice_end == new_marked_begin->pred->action_block->succ);
 
                    out_slice_end->block_bunch = new_marked_begin;
                }
            }                                                                   assert(nullptr != old_block_bunch_slice_end->pred->action_block->succ);
            old_block_bunch_slice_end->pred->action_block->succ->block_bunch =
                                                     old_block_bunch_slice_end; assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
            old_block_bunch_pos->pred->action_block->succ->block_bunch =
                                                           old_block_bunch_pos;
        }
        while (out_slice_begin < out_slice_end &&
                  (old_block_bunch_pos = out_slice_end[-1].block_bunch, true));
        old_block_bunch_slice->end = old_block_bunch_slice_end;
 
        if (old_block_bunch_slice->empty())
        {
            #ifdef USE_SIMPLE_LIST
                simple_list<block_bunch_slice_t>::erase(
                            ONLY_IF_POOL_ALLOCATOR( storage, )
                                                        old_block_bunch_slice);
            #else
                if (old_block_bunch_slice->is_stable())
                {
                    // If the new block is R, then the old (U) block loses
                    // exactly one stable block_bunch-slice, namely the one we
                    // just stabilised for (`splitter_T`).  We could perhaps
                    // optimize this by moving that slice as a whole to the new
                    // block -- perhaps later.
                    //
                    // If the new block is U, then the old (R) block loses
                    // no stable block_bunch-slices if it contains any bottom
                    // state.  If it doesn't contain any bottom state, it will
                    // definitely keep `splitter_T`, but nothing else can be
                    // guaranteed.
                    //
                    // So old_block_bunch_slice may be deleted, in particular
                    // if the new block is U, but not exclusively.
                    old_block->stable_block_bunch.erase(old_block_bunch_slice);
                }
                else
                {
                    splitter_list.erase(old_block_bunch_slice);
                }
            #endif
            --nr_of_block_bunch_slices;
        }
        return out_slice_begin;
    }
 
 
    void first_move_transition_to_new_action_block(pred_entry* const pred_iter)
    {
        action_block_entry* const old_action_block_pos(
                                                      pred_iter->action_block); assert(nullptr != old_action_block_pos->succ);
                                                                                assert(old_action_block_pos->succ->block_bunch->pred == pred_iter);
        action_block_entry* const action_block_slice_begin(
                             old_action_block_pos->action_block_slice_begin(    ONLY_IF_DEBUG( action_block_begin, action_block_orig_inert_begin )
                                                                            )); assert(nullptr != action_block_slice_begin->succ);
                                                                                assert(action_block_slice_begin->succ->block_bunch->pred->action_block ==
                                                                                                                                     action_block_slice_begin);
        action_block_entry* const new_action_block_pos(
                                action_block_slice_begin->begin_or_before_end); assert(nullptr != new_action_block_pos);
                                                                                assert(action_block_slice_begin == new_action_block_pos->begin_or_before_end);
                                                                                assert(nullptr != new_action_block_pos->succ);
                                                                                assert(new_action_block_pos->succ->block_bunch->pred->action_block ==
        /* move the transition to the end of the action_block-slice          */                                                          new_action_block_pos);
        if (old_action_block_pos < new_action_block_pos)
        {
            succ_entry* const temp(new_action_block_pos->succ);                 assert(nullptr != temp);  assert(nullptr != old_action_block_pos->succ);
            new_action_block_pos->succ = old_action_block_pos->succ;
            old_action_block_pos->succ = temp;
            temp->block_bunch->pred->action_block = old_action_block_pos;       assert(pred_iter == new_action_block_pos->succ->block_bunch->pred);
            pred_iter->action_block = new_action_block_pos;
 
        // adapt the old action_block-slice immediately
            action_block_slice_begin->begin_or_before_end =
                                                      new_action_block_pos - 1;
        }
        else
        {                                                                       assert(old_action_block_pos == new_action_block_pos);
            if (action_block_slice_begin < new_action_block_pos)
            {
                // The old action_block-slice is not empty, so we have to adapt
                // the pointer at the beginning.  (If it is empty, it may
                // happen that `new_action_block_pos - 1` is an illegal value.)
                action_block_slice_begin->begin_or_before_end =
                                                      new_action_block_pos - 1;
            }
            else  --nr_of_action_block_slices;
        }                                                                       assert(nullptr != new_action_block_pos->succ);
                                                                                assert(pred_iter == new_action_block_pos->succ->block_bunch->pred);
        // adapt the new action_block-slice, as far as is possible now
            // make the begin_or_before_end pointers of the first and last
            // transition in the slice correct immediately.  The other
            // begin_or_before_end pointers need to be corrected after all
            // transitions in the new bunch have been positioned correctly.
        if (new_action_block_pos + 1 >= action_block_inert_begin ||
            nullptr == new_action_block_pos[1].succ ||
            new_action_block_pos[1].succ->bunch() !=
                                         new_action_block_pos->succ->bunch() ||
            new_action_block_pos[1].succ->block_bunch->pred->target->bl.ock !=
                                                     pred_iter->target->bl.ock)
        {
            // This is the first transition that moves to this new
            // action_block-slice.
            new_action_block_pos->begin_or_before_end = new_action_block_pos;
            ++nr_of_action_block_slices;
        }
        else
        {
            action_block_entry* const action_block_slice_before_end(
                                  new_action_block_pos[1].begin_or_before_end); assert(nullptr != action_block_slice_before_end);
                                                                                assert(new_action_block_pos < action_block_slice_before_end);
                                                                                assert(nullptr != action_block_slice_before_end->succ);
                                                                                assert(action_block_slice_before_end->succ->block_bunch->pred->action_block ==
                                                                                                                                action_block_slice_before_end);
                                                                                assert(new_action_block_pos + 1 ==
                                                                                                           action_block_slice_before_end->begin_or_before_end);
            action_block_slice_before_end->begin_or_before_end =
                                                          new_action_block_pos; assert(action_block_slice_before_end->succ->block_bunch->
                                                                                                            pred->target->bl.ock == pred_iter->target->bl.ock);
            new_action_block_pos->begin_or_before_end =
                                                 action_block_slice_before_end; assert(action_block_slice_before_end < action_block_inert_begin);
        }
    }
 
 
    void second_move_transition_to_new_action_block(
                                                   pred_entry* const pred_iter)
    {
        action_block_entry* const new_action_block_pos(
                                                      pred_iter->action_block); assert(nullptr != new_action_block_pos->succ);
                                                                                assert(new_action_block_pos->succ->block_bunch->pred == pred_iter);
        action_block_entry* const old_begin_or_before_end(
                                    new_action_block_pos->begin_or_before_end); assert(nullptr != old_begin_or_before_end);
                                                                                assert(nullptr != old_begin_or_before_end->succ);
                                                                                assert(old_begin_or_before_end->succ->block_bunch->pred->action_block ==
                                                                                                                                      old_begin_or_before_end);
        if (action_block_entry* const new_begin_or_before_end(
                                 old_begin_or_before_end->begin_or_before_end); assert(nullptr != new_begin_or_before_end),
                                                                                assert(nullptr != new_begin_or_before_end->succ),
                                                                                assert(new_begin_or_before_end->succ->block_bunch->pred->action_block ==
                                                                                                                                      new_begin_or_before_end),
                                new_begin_or_before_end < new_action_block_pos)
        {                                                                       assert(old_begin_or_before_end==new_begin_or_before_end->begin_or_before_end);
            new_action_block_pos->begin_or_before_end =
                                                       new_begin_or_before_end; assert(new_action_block_pos <= old_begin_or_before_end);
            return;
        }                                                                       else  assert(new_begin_or_before_end == new_action_block_pos);
        if (old_begin_or_before_end < new_action_block_pos)  return;
 
        // this is the first transition in the new action_block-slice.
        // Check whether the bunch it belongs to has become nontrivial.
        bunch_t* const bunch(new_action_block_pos->succ->bunch());
        if (!bunch->is_trivial()) { return; }                                    assert(old_begin_or_before_end + 1 == bunch->end);
        if (bunch->begin < new_action_block_pos)
        {
            make_nontrivial(bunch);
        }
    }
 
 
    bool make_noninert(pred_entry* const old_pred_pos,
          block_bunch_slice_iter_or_null_t* const new_noninert_block_bunch_ptr)
    {
        state_info_entry* const source(old_pred_pos->source);                   assert(source->pos->st == source);
        state_info_entry* const target(old_pred_pos->target);                   assert(target->pos->st == target);
 
        action_block_entry* const new_action_block_pos(
                                                   action_block_inert_begin++); assert(nullptr != new_action_block_pos->succ);
                                                                                assert(new_action_block_pos->succ->block_bunch->pred->action_block ==
                                                                                                                                         new_action_block_pos);
        succ_entry* const new_succ_pos(source->succ_inert.begin++);             assert(new_succ_pos->block_bunch->pred->action_block->succ == new_succ_pos);
        block_bunch_entry* const new_block_bunch_pos(
                                                    block_bunch_inert_begin++); assert(nullptr != new_block_bunch_pos->pred->action_block->succ);
                                                                                assert(new_block_bunch_pos->pred->action_block->succ->block_bunch ==
                                                                                                                                          new_block_bunch_pos);
        action_block_entry* const old_action_block_pos(
                                                   old_pred_pos->action_block); assert(new_action_block_pos <= old_action_block_pos);
 
        succ_entry* const old_succ_pos(old_action_block_pos->succ);             assert(nullptr != old_succ_pos);
        block_bunch_entry* const old_block_bunch_pos(
                                                    old_succ_pos->block_bunch); assert(old_pred_pos == old_block_bunch_pos->pred);
        pred_entry* const new_pred_pos(target->pred_inert.begin++);             assert(nullptr != new_pred_pos->action_block->succ);
                                                                                assert(new_pred_pos->action_block->succ->block_bunch->pred == new_pred_pos);
 
        /* adapt action_block                                                */ assert(nullptr == new_action_block_pos->begin_or_before_end);
        if (new_action_block_pos < old_action_block_pos)
        {                                                                       assert(nullptr == old_action_block_pos->begin_or_before_end);
            old_action_block_pos->succ = new_action_block_pos->succ;            assert(nullptr != old_action_block_pos->succ);
                                                                                assert(old_action_block_pos->succ->block_bunch->pred->action_block ==
                                                                                                                                         new_action_block_pos);
            old_action_block_pos->succ->block_bunch->pred->action_block =
                                                          old_action_block_pos;
        }                                                                       else  assert(new_action_block_pos == old_action_block_pos);
        new_action_block_pos->succ = new_succ_pos;                              assert(nullptr != new_succ_pos);
        // new_action_block_pos->begin_or_before_end = ...; -- see below
 
        /* adapt succ                                                        */ assert(nullptr == new_succ_pos->begin_or_before_end);
        if (new_succ_pos < old_succ_pos)
        {                                                                       assert(nullptr == old_succ_pos->begin_or_before_end);
            old_succ_pos->block_bunch = new_succ_pos->block_bunch;              assert(old_succ_pos->block_bunch->pred->action_block->succ == new_succ_pos);
            old_succ_pos->block_bunch->pred->action_block->succ = old_succ_pos; assert(nullptr != old_succ_pos);
        }                                                                       else  assert(new_succ_pos == old_succ_pos);
        new_succ_pos->block_bunch = new_block_bunch_pos;
        // new_succ_pos->begin_or_before_end = ...; -- see below
 
        /* adapt block_bunch                                                 */ assert(new_block_bunch_pos->slice.is_null());
        if (new_block_bunch_pos < old_block_bunch_pos)
        {                                                                       assert(old_block_bunch_pos->slice.is_null());
                                                                                assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
            old_block_bunch_pos->pred = new_block_bunch_pos->pred;              assert(old_block_bunch_pos->pred->action_block->succ->block_bunch ==
                                                                                                                                          new_block_bunch_pos);
                                                                                assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
            old_block_bunch_pos->pred->action_block->succ->block_bunch =
                                                           old_block_bunch_pos;
        }                                                                       else  assert(new_block_bunch_pos == old_block_bunch_pos);
        new_block_bunch_pos->pred = new_pred_pos;
        // new_block_bunch_pos->slice = ...; -- see below
 
        // adapt pred
        if (new_pred_pos < old_pred_pos)
        {
            // We need std::swap here to swap the whole content, including
            // work counters in case we measure the work.
            std::swap(*old_pred_pos, *new_pred_pos);                            assert(nullptr != old_pred_pos->action_block->succ);
                                                                                assert(old_pred_pos->action_block->succ->block_bunch->pred == new_pred_pos);
            old_pred_pos->action_block->succ->block_bunch->pred = old_pred_pos;
        }                                                                       else  assert(new_pred_pos == old_pred_pos);
        new_pred_pos->action_block = new_action_block_pos;
 
        /* make the state a bottom state if necessary                        */ assert(source->bl.ock->nonbottom_begin <= source->pos);
        bool became_bottom(false);                                              assert(succ.back().block_bunch->pred->source != source);
        if (source != source->succ_inert.begin->block_bunch->pred->source)
        {
            block_t* const source_block(source->bl.ock);
            // make the state a marked bottom state
            if (source->pos >= source_block->marked_nonbottom_begin)
            {
                std::swap(*source->pos,
                                      *source_block->marked_nonbottom_begin++);
            }                                                                   assert(source->pos < source_block->marked_nonbottom_begin);
            std::swap(*source->pos, *source_block->nonbottom_begin++);
            ++nr_of_new_bottom_states;
            became_bottom = true;
        }
 
        bunch_t* new_noninert_bunch;                                            assert(nullptr != new_action_block_pos);
        if (!new_noninert_block_bunch_ptr->is_null())
        {
            // There is already some new non-inert transition from this block.
            // So we can reuse this block_bunch and its bunch.
            // (However, it may be the case that the current transition goes to
            // another block; in the latter case, we have to create a new
            // action_block-slice.)
 
            // extend the bunch
            new_noninert_bunch = (*new_noninert_block_bunch_ptr)->bunch;        assert(new_action_block_pos >= new_noninert_bunch->end);
                                                                                ONLY_IF_DEBUG(
                                                                                    for (const action_block_entry*temp_action_block_pos=new_action_block_pos ;
                                                                                                            temp_action_block_pos > new_noninert_bunch->end ; )
                                                                                    {
                                                                                        assert(nullptr == (--temp_action_block_pos)->succ);
                                                                                    }
                                                                                )
            new_noninert_bunch->end = action_block_inert_begin;
            /* extend the block_bunch-slice                                  */ assert((*new_noninert_block_bunch_ptr)->end == new_block_bunch_pos);
            (*new_noninert_block_bunch_ptr)->end = block_bunch_inert_begin;
            if (!(*new_noninert_block_bunch_ptr)->is_stable())
            {                                                                   assert((*new_noninert_block_bunch_ptr)->marked_begin == new_block_bunch_pos);
                (*new_noninert_block_bunch_ptr)->marked_begin =
                                                       block_bunch_inert_begin;
            }
            new_block_bunch_pos->slice = *new_noninert_block_bunch_ptr;
 
            /* adapt the action_block-slice                                  */ assert(new_noninert_bunch->begin < new_action_block_pos);
            if (nullptr != new_action_block_pos[-1].succ &&
                target->bl.ock == new_action_block_pos[-1].
                                       succ->block_bunch->pred->target->bl.ock)
            {
                // the action_block-slice is suitable: extend it
                action_block_entry* const action_block_slice_begin(
                                 new_action_block_pos[-1].begin_or_before_end); assert(nullptr != action_block_slice_begin);
                                                                                assert(new_action_block_pos-1==action_block_slice_begin->begin_or_before_end);
                                                                                assert(nullptr != action_block_slice_begin->succ);
                                                                                assert(action_block_slice_begin->succ->block_bunch->pred->action_block ==
                                                                                                                                     action_block_slice_begin);
                action_block_slice_begin->begin_or_before_end =
                                                          new_action_block_pos;
                new_action_block_pos->begin_or_before_end =
                                                      action_block_slice_begin;
            }
            else
            {
                // create a new action_block-slice
                new_action_block_pos->begin_or_before_end=new_action_block_pos;
                if (new_noninert_bunch->is_trivial())
                {                                                               // Only during initialisation, it may happen that we add new non-inert
                    make_nontrivial(new_noninert_bunch);                        // transitions to a nontrivial bunch:
                }
                                                                                #ifndef NDEBUG
                                                                                    else
                                                                                    {
                                                                                        // We make sure that new_noninert_bunch is the first bunch in
                                                                                        // action_block (and because it's always the last one, it will be the
                                                                                        // only one, so there is only one bunch, as ).
                                                                                        for (const action_block_entry* iter = action_block_begin;
                                                                                                                      iter < new_noninert_bunch->begin; ++iter)
                                                                                        {
                                                                                            assert(nullptr == iter->succ);
                                                                                            assert(nullptr == iter->begin_or_before_end);
                                                                                        }
                                                                                    }
                                                                                #endif
                ++nr_of_action_block_slices;
            }
 
            /* adapt the out-slice                                           */ assert(source != succ.front().block_bunch->pred->source);
            if (source == new_succ_pos[-1].block_bunch->pred->source &&
                                new_succ_pos[-1].bunch() == new_noninert_bunch)
            {
                // the out-slice is suitable: extend it.
                succ_entry* const out_slice_begin(
                                         new_succ_pos[-1].begin_or_before_end); assert(nullptr != out_slice_begin);
                                                                                assert(new_succ_pos - 1 == out_slice_begin->begin_or_before_end);
                out_slice_begin->begin_or_before_end = new_succ_pos;            assert(out_slice_begin->block_bunch->pred->action_block->succ ==
                                                                                                                                              out_slice_begin);
                new_succ_pos->begin_or_before_end = out_slice_begin;
                return became_bottom;
            }
        }
        else
        {
            // create a new bunch for noninert transitions
            new_noninert_bunch =
                #ifdef USE_POOL_ALLOCATOR
                    storage.template construct<bunch_t>
                #else
                    new bunch_t
                #endif
                              (new_action_block_pos, action_block_inert_begin);
            ++nr_of_bunches;
 
            // create a new block_bunch-slice
            #ifdef USE_SIMPLE_LIST
                block_bunch_slice_iter_t new_noninert_block_bunch(
                    splitter_list.emplace_back(
                        ONLY_IF_POOL_ALLOCATOR( storage, )
                          block_bunch_inert_begin, new_noninert_bunch, false));
            #else
                splitter_list.emplace_back(block_bunch_inert_begin,
                                                    new_noninert_bunch, false);
                block_bunch_slice_iter_t new_noninert_block_bunch(
                                               std::prev(splitter_list.end()));
            #endif
            ++nr_of_block_bunch_slices;
            new_block_bunch_pos->slice = new_noninert_block_bunch;
            *new_noninert_block_bunch_ptr = new_noninert_block_bunch;
 
            // create a new action_block-slice
            new_action_block_pos->begin_or_before_end = new_action_block_pos;
            ++nr_of_action_block_slices;
        }                                                                       assert(&succ.cbegin()[1] == new_succ_pos ||
                                                                                                new_succ_pos[-1].block_bunch->pred->source < source ||
        /* create a new out-slice                                            */                                new_succ_pos[-1].bunch() != new_noninert_bunch);
        new_succ_pos->begin_or_before_end = new_succ_pos;
        return became_bottom;
    }
 
 
  public:
                                                                                ONLY_IF_DEBUG( template<class LTS_TYPE> )
    void adapt_transitions_for_new_block(
                  block_t* const new_block,
                  block_t* const old_block,                                     ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner, )
                  bool const add_new_noninert_to_splitter,
                  const block_bunch_slice_iter_t splitter_T,
                  enum new_block_mode_t const new_block_mode)
    {                                                                           assert(splitter_T->is_stable());
        // We begin with a bottom state so the new block gets a sorted list of
        // stable block_bunch-slices.
        permutation_entry* s_iter(new_block->begin);                            assert(s_iter < new_block->end);
        do
        {
            state_info_entry* const s(s_iter->st);                              assert(new_block == s->bl.ock);
                                                                                assert(s->pos == s_iter);
            /* -  -  -  -  -  -  adapt part_tr.block_bunch  -  -  -  -  -  - */
                                                                                assert(s != succ.front().block_bunch->pred->source);
            for (succ_entry* succ_iter(s->succ_inert.begin);
                                s == succ_iter[-1].block_bunch->pred->source; )
            {
                succ_iter = move_out_slice_to_new_block(succ_iter,              ONLY_IF_DEBUG( partitioner, )
                                                    #ifndef USE_SIMPLE_LIST
                                                        old_block,
                                                    #endif
                                                                   splitter_T); assert(succ_iter->block_bunch->pred->action_block->succ == succ_iter);
                                                                                assert(s == succ_iter->block_bunch->pred->source);
                                                                                // add_work_to_out_slice(succ_iter, ...) -- subsumed in the call below
            }
 
            /*-  -  -  -  -  -  adapt part_tr.action_block  -  -  -  -  -  -*/
                                                                                assert(s != pred.front().target);
            for (pred_entry* pred_iter(s->pred_inert.begin);
                                                  s == (--pred_iter)->target; )
            {                                                                   assert(&pred.front() < pred_iter);
                                                                                assert(nullptr != pred_iter->action_block->succ);
                                                                                assert(pred_iter->action_block->succ->block_bunch->pred == pred_iter);
                first_move_transition_to_new_action_block(pred_iter);           // mCRL2complexity(pred_iter, ...) -- subsumed in the call below
            }                                                                   // mCRL2complexity(s, ...) -- subsumed in the call at the end
        }
        while (++s_iter < new_block->end);
 
        if (new_block_is_R == new_block_mode)
        {                                                                       assert(splitter_T->source_block() == new_block);
            // The `splitter_T` slice moves completely from the old to the new
            // block.  We move it as a whole to the new block_bunch list.
            new_block->stable_block_bunch.splice(
                    new_block->stable_block_bunch.begin(),
                                    old_block->stable_block_bunch, splitter_T);
        }                                                                       else  assert(splitter_T->source_block() == old_block);
 
        // We cannot join the loop above with the one below because transitions
        // in the action_block-slices need to be handled in two phases.
 
        s_iter = new_block->begin;                                              assert(s_iter < new_block->end);
        do
        {
            state_info_entry* const s(s_iter->st);                              assert(s->pos == s_iter);  assert(s != pred.front().target);
            for (pred_entry* pred_iter(s->pred_inert.begin);
                                                  s == (--pred_iter)->target; )
            {                                                                   assert(&pred.front() < pred_iter);
                                                                                assert(nullptr != pred_iter->action_block->succ);
                                                                                assert(pred_iter->action_block->succ->block_bunch->pred == pred_iter);
                second_move_transition_to_new_action_block(pred_iter);          // mCRL2complexity(pred_iter, ...) -- subsumed in the call below
            }                                                                   // mCRL2complexity(s, ...) -- subsumed in the call at the end
        }
        while (++s_iter < new_block->end);
                                                                                assert(0 == new_block->marked_size());  assert(0 == old_block->marked_size());
        /* -  -  -  -  -  - find new non-inert transitions -  -  -  -  -  - */  assert(1 + &block_bunch.back() - block_bunch_inert_begin ==
                                                                                                                  action_block_end - action_block_inert_begin);
        if (block_bunch_inert_begin <= &block_bunch.back())
        {
            block_bunch_slice_iter_or_null_t new_noninert_block_bunch;
            if (add_new_noninert_to_splitter)
            {
                new_noninert_block_bunch = splitter_T;
            }
            else
            {
                new_noninert_block_bunch = nullptr;
            }
            if (new_block_is_U == new_block_mode)
            {                                                                   assert(old_block == new_block->end->st->bl.ock);
                                                                                assert(new_block->end <= &partitioner.part_st.permutation.back());
                permutation_entry* target_iter(new_block->begin);               assert(target_iter < new_block->end);
                do
                {
                    state_info_entry* const s(target_iter->st);                 assert(s->pos == target_iter);
                    // check all incoming inert transitions of s, whether they
                    /* still start in new_block                              */ assert(s != pred.back().target);
                    for (pred_entry* pred_iter(s->pred_inert.begin);
                                           s == pred_iter->target; ++pred_iter)
                    {                                                           assert(pred_iter < &pred.back());
                                                                                assert(nullptr != pred_iter->action_block->succ);
                        state_info_entry* const t(pred_iter->source);           assert(pred_iter->action_block->succ->block_bunch->pred == pred_iter);
                                                                                assert(t->pos->st == t);
                        if (new_block != t->bl.ock)
                        {                                                       assert(old_block == t->bl.ock);
                            if (!make_noninert(pred_iter,
                                                    &new_noninert_block_bunch))
                                       // make_noninert() may modify *pred_iter
                            {
                                old_block->mark_nonbottom(t->pos);
                            }
                        }                                                       // mCRL2complexity(old value of *pred_iter, ...) -- overapproximated by the
                                                                                // call below
                    }                                                           // mCRL2complexity(s, ...) -- subsumed in the call at the end
                }
                while (++target_iter < new_block->end);                         assert(0 < old_block->bottom_size());
            }
            else
            {                                                                   assert(new_block_is_R == new_block_mode);
                    /* We have to be careful because make_noninert may move  */ assert(&partitioner.part_st.permutation.front() < new_block->begin);
                    /* a state either forward (to the marked states) or      */ assert(old_block == new_block->begin[-1].st->bl.ock);
                    /* back (to the bottom states).                          */ assert(0 < old_block->bottom_size());
                for(permutation_entry* source_iter(new_block->nonbottom_begin);
                             source_iter < new_block->marked_nonbottom_begin; )
                {
                    state_info_entry* const s(source_iter->st);                 assert(s->pos == source_iter);
                    // check all outgoing inert transitions of s, whether they
                    /* still end in new_block.                               */ assert(succ.back().block_bunch->pred->source != s);
                    succ_entry* succ_iter(s->succ_inert.begin);                 assert(succ_iter < &succ.back());
                    bool dont_mark(true);                                       assert(s == succ_iter->block_bunch->pred->source);
                    do
                    {                                                           assert(succ_iter->block_bunch->pred->action_block->succ == succ_iter);
                        if (new_block !=
                                  succ_iter->block_bunch->pred->target->bl.ock)
                        {                                                       assert(old_block == succ_iter->block_bunch->pred->target->bl.ock);
                            dont_mark = make_noninert(
                                                  succ_iter->block_bunch->pred,
                                                    &new_noninert_block_bunch);
                        }                                                       // mCRL2complexity(succ_iter->block_bunch->pred, ...) -- overapproximated by
                                                                                // the call below
                    }
                    while (s == (++succ_iter)->block_bunch->pred->source);
                    if (dont_mark)  ++source_iter;
                    else
                    {                                                           assert(s->pos == source_iter);
                        new_block->mark_nonbottom(source_iter);
                    }                                                           assert(new_block->nonbottom_begin <= source_iter);
                                                                                // mCRL2complexity(s, ...) -- overapproximated by the call at the end
                }
            }
        }                                                                       else  assert(block_bunch_inert_begin == 1 + &block_bunch.back());
                                                                                mCRL2complexity(new_block, add_work(check_complexity::
                                                                                    adapt_transitions_for_new_block, check_complexity::log_n -
                                                                                                     check_complexity::ilog2(new_block->size())), partitioner);
    }
                                                                                #ifndef NDEBUG
                                                                                    template <class LTS_TYPE>
                                                                                    void print_trans(const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
                                                                                    {
                                                                                        if (!mCRL2logEnabled(log::debug))  return;
                                                                                        // print all outgoing transitions grouped per successor and out-slice
                                                                                        const succ_entry* succ_iter(&succ.cbegin()[1]);
                                                                                        if (succ_iter >= &succ.back())
                                                                                        {
                                                                                            mCRL2log(log::debug) << "No transitions.\n";
                                                                                            return;
                                                                                        }
                                                                                        const state_info_entry* source(succ_iter->block_bunch->pred->source);
                                                                                        mCRL2log(log::debug) << source->debug_id(partitioner) << ":\n";
                                                                                        block_bunch_slice_iter_or_null_t current_out_bunch(
                                                                                                         const_cast<part_trans_t*>(this)->splitter_list.end());
                                                                                        do
                                                                                        {
                                                                                            if (source != succ_iter->block_bunch->pred->source)
                                                                                            {   assert(source < succ_iter->block_bunch->pred->source);
                                                                                                source = succ_iter->block_bunch->pred->source;
                                                                                                mCRL2log(log::debug)
                                                                                                    << source->debug_id(partitioner) << ":\n";
                                                                                                current_out_bunch =
                                                                                                          const_cast<part_trans_t*>(this)->splitter_list.end();
                                                                                            }
                                                                                            if (succ_iter->block_bunch->slice != current_out_bunch)
                                                                                            {   assert(!current_out_bunch.is_null());
                                                                                                if (succ_iter->block_bunch->slice.is_null())
                                                                                                {   assert(succ_iter == source->succ_inert.begin);
                                                                                                    mCRL2log(log::debug)<<"\tInert successors:\n";
                                                                                                    current_out_bunch = nullptr;
                                                                                                }
                                                                                                else
                                                                                                {   assert(succ_iter < source->succ_inert.begin);
                                                                                                    assert(!current_out_bunch.is_null());
                                                                                                    assert(current_out_bunch == splitter_list.end() ||
                                                                                                               current_out_bunch->bunch != succ_iter->bunch());
                                                                                                    mCRL2log(log::debug) << "\tSuccessors in "
                                                                                                      <<succ_iter->bunch()->debug_id_short(partitioner)<<":\n";
                                                                                                    current_out_bunch = succ_iter->block_bunch->slice;
                                                                                                }
                                                                                            }
                                                                                            mCRL2log(log::debug) << "\t\t"
                                                                                                << succ_iter->block_bunch->pred->debug_id(partitioner) << '\n';
                                                                                        }
                                                                                        while (++succ_iter < &succ.back());
 
                                                                                        // print all transitions grouped per bunch and action_block-slice
                                                                                        const action_block_entry* action_block_iter(action_block_begin);
                                                                                        do  assert(action_block_iter < action_block_end);
                                                                                        while (nullptr == action_block_iter->succ &&
                                                                                                   (assert(nullptr == action_block_iter->begin_or_before_end),
                                                                                                    ++action_block_iter, true));
                                                                                        do
                                                                                        {
                                                                                            const action_block_entry* bunch_end;
                                                                                            const action_block_entry* action_block_slice_end;
                                                                                            assert(nullptr != action_block_iter->succ);
                                                                                            if (action_block_iter->succ->block_bunch->slice.is_null())
                                                                                            {   assert(action_block_iter == action_block_inert_begin);
                                                                                                mCRL2log(log::debug) <<"Inert transition slice [";
                                                                                                action_block_slice_end = bunch_end = action_block_end;
                                                                                            }
                                                                                            else
                                                                                            {
                                                                                                const bunch_t* const bunch(action_block_iter->succ->bunch());
                                                                                                assert(nullptr != bunch);
                                                                                                mCRL2log(log::debug) << bunch->debug_id_short(
                                                                                                                   partitioner) << ":\n\taction_block-slice [";
                                                                                                assert(bunch->begin == action_block_iter);
                                                                                                bunch_end = bunch->end;
                                                                                                assert(bunch_end <= action_block_inert_begin);
                                                                                                assert(nullptr != action_block_iter->begin_or_before_end);
                                                                                                action_block_slice_end =
                                                                                                                  action_block_iter->begin_or_before_end + 1;
                                                                                            }
                                                                                            assert(action_block_slice_end <= bunch_end);
                                                                                            // for all action_block-slices in bunch
                                                                                            for (;;)
                                                                                            {
                                                                                                mCRL2log(log::debug) << (action_block_iter -
                                                                                                                                     action_block_begin) << ","
                                                                                                    << (action_block_slice_end - action_block_begin) << "):\n";
                                                                                                // for all transitions in the action_block-slice
                                                                                                assert(action_block_iter < action_block_slice_end);
                                                                                                do
                                                                                                {
                                                                                                    assert(nullptr != action_block_iter->succ);
                                                                                                    mCRL2log(log::debug) << "\t\t"
                                                                                                            << action_block_iter->succ->block_bunch->
                                                                                                                           pred->debug_id(partitioner) << '\n';
                                                                                                }
                                                                                                while (++action_block_iter < action_block_slice_end);
                                                                                                // go to next action_block-slice in the same bunch
                                                                                                while (action_block_iter < bunch_end &&
                                                                                                                            nullptr == action_block_iter->succ)
                                                                                                {
                                                                                                    assert(nullptr == action_block_iter->begin_or_before_end);
                                                                                                    ++action_block_iter;
                                                                                                    assert(action_block_iter < bunch_end);
                                                                                                }
                                                                                                if (action_block_iter >= bunch_end)  break;
                                                                                                assert(nullptr != action_block_iter->begin_or_before_end);
                                                                                                action_block_slice_end =
                                                                                                                  action_block_iter->begin_or_before_end + 1;
                                                                                                mCRL2log(log::debug) << "\taction_block-slice [";
                                                                                            }
                                                                                            // go to next bunch
                                                                                            assert(action_block_iter == bunch_end);
                                                                                            while (action_block_iter < action_block_end &&
                                                                                                                            nullptr == action_block_iter->succ)
                                                                                            {
                                                                                                assert(nullptr == action_block_iter->begin_or_before_end);
                                                                                                ++action_block_iter;
                                                                                            }
                                                                                        }
                                                                                        while (action_block_iter < action_block_end);
                                                                                    }
                                                                                #endif
};
 
 
                                                                                ONLY_IF_DEBUG( template<class LTS_TYPE> )
inline block_t* block_t::split_off_block(
        enum new_block_mode_t const new_block_mode,                             ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner, )
        ONLY_IF_POOL_ALLOCATOR(
                  my_pool<simple_list<block_bunch_slice_t>::entry>& storage, )
                                                    state_type const new_seqnr)
{                                                                               assert(0 < marked_size());  assert(0 < unmarked_bottom_size());
    // create a new block
    block_t* new_block;
    state_type swapcount(std::min(marked_bottom_size(),
                                                   unmarked_nonbottom_size()));
    if (permutation_entry* const splitpoint(marked_bottom_begin +
                                                    unmarked_nonbottom_size()); assert(begin < splitpoint),  assert(splitpoint < end),
                                                                                assert(splitpoint->st->pos == splitpoint),
                                              new_block_is_U == new_block_mode)
    {                                                                           assert((state_type) (splitpoint - begin) <= size()/2);
        new_block =
                    #ifdef USE_POOL_ALLOCATOR
                        storage.template construct<block_t>
                    #else
                        new block_t
                    #endif
                                                (begin, splitpoint, new_seqnr);
        new_block->nonbottom_begin = marked_bottom_begin;
 
        // adapt the old block: it only keeps the R-states
        begin = splitpoint;
        nonbottom_begin = marked_nonbottom_begin;
    }
    else
    {                                                                           assert(new_block_is_R == new_block_mode);
        new_block =
                    #ifdef USE_POOL_ALLOCATOR
                        storage.template construct<block_t>
                    #else
                        new block_t
                    #endif
                                                  (splitpoint, end, new_seqnr);
        new_block->nonbottom_begin = marked_nonbottom_begin;                    assert((state_type) (end - splitpoint) <= size()/2);
 
        // adapt the old block: it only keeps the U-states
        end = splitpoint;
        nonbottom_begin = marked_bottom_begin;
    }                                                                           ONLY_IF_DEBUG( new_block->work_counter = work_counter; )
 
    // swap contents
 
    // The structure of a block is
    // |  unmarked  |   marked   |  unmarked  |   marked   |
    // |   bottom   |   bottom   | non-bottom | non-bottom |
    // We have to swap the marked bottom with the unmarked non-bottom
    // states.
    //
    // It is not necessary to reset the untested_to_U counters; these
    // counters are anyway only valid for the states in the respective
    // slice.
 
    if (0 < swapcount)
    {
        // vector swap the states:
        permutation_entry* pos1(marked_bottom_begin);
        permutation_entry* pos2(marked_nonbottom_begin);                        assert(pos1 < pos2);
        permutation_entry const temp(std::move(*pos1));
        for (;;)
        {
            --pos2;                                                             assert(pos1 < pos2);
            *pos1 = std::move(*pos2);
            ++pos1;
            if (0 >= --swapcount) { break; }                                    assert(pos1 < pos2);
            *pos2 = std::move(*pos1);                                           // mCRL2complexity(new_block_is_U == new_block_mode ? pos1[-1] : *pos2, ...)
        }                                                                       // -- overapproximated by the call at the end
        *pos2 = std::move(temp);                                                // mCRL2complexity(new_block_is_U == new_block_mode ? pos1[-1] : *pos2, ...)
    }                                                                           // -- overapproximated by the call at the end
                                                                                #ifndef NDEBUG
                                                                                    { const permutation_entry* s_iter(begin);  assert(s_iter < end);
                                                                                    do  assert(s_iter->st->pos == s_iter);
                                                                                    while (++s_iter < end); }
                                                                                #endif
    // unmark all states in both blocks
    marked_nonbottom_begin = end;
    marked_bottom_begin = nonbottom_begin;
    new_block->marked_bottom_begin = new_block->nonbottom_begin;                assert(new_block->size() <= size());
 
    /* set the block pointer of states in the new block                      */ assert(new_block->marked_nonbottom_begin == new_block->end);
    permutation_entry* s_iter(new_block->begin);                                assert(s_iter < new_block->end);
    do
    {                                                                           assert(s_iter->st->pos == s_iter);
        s_iter->st->bl.ock = new_block;                                         // mCRL2complexity (*s_iter, ...) -- subsumed in the call below
    }
    while (++s_iter < new_block->end);                                          mCRL2complexity(new_block, add_work(check_complexity::split_off_block,
                                                                                       check_complexity::log_n - check_complexity::ilog2(new_block->size())),
                                                                                                                                                  partitioner);
    return new_block;
}
 
 
inline bunch_t* bunch_t::split_off_small_action_block_slice(
                                                         part_trans_t& part_tr)
{                                                                               assert(begin < end);  assert(nullptr != begin->succ);
                                                                                assert(nullptr != begin->begin_or_before_end);
    action_block_entry* const first_slice_end(begin->begin_or_before_end + 1);  assert(nullptr != end[-1].succ);  assert(nullptr!=end[-1].begin_or_before_end);
    action_block_entry* const last_slice_begin(end[-1].begin_or_before_end);    assert(begin < first_slice_end);  assert(first_slice_end <= last_slice_begin);
    bunch_t* bunch_T_a_Bprime;
        /* Line 2.6: Select some a in Act and B' in Pi_s such that           */ assert(last_slice_begin < end);  assert(nullptr != first_slice_end[-1].succ);
        /*            |T--a-->B'| < 1/2 |T|                                  */ assert(nullptr != last_slice_begin->succ);
    if (first_slice_end - begin > end - last_slice_begin)
    {
        // Line 2.7: Pi_t := Pi_t \ {T} union { T--a-->B', T \ T--a-->B' }
        bunch_T_a_Bprime =
                            #ifdef USE_POOL_ALLOCATOR
                                 part_tr.storage.template construct<bunch_t>
                            #else
                                new bunch_t
                            #endif
                                                       (last_slice_begin, end); assert(nullptr != bunch_T_a_Bprime);
        end = last_slice_begin;
        while (nullptr == end[-1].succ)
        {
            --end;                                                              assert(first_slice_end <= end);  assert(nullptr == end->begin_or_before_end);
        }                                                                       assert(nullptr != end[-1].begin_or_before_end);
        if (first_slice_end == end)  part_tr.make_trivial(this);
    }
    else
    {
        // Line 2.7: Pi_t := Pi_t \ {T} union { T--a-->B', T \ T--a-->B' }
        bunch_T_a_Bprime =
                            #ifdef USE_POOL_ALLOCATOR
                                 part_tr.storage.template construct<bunch_t>
                            #else
                                new bunch_t
                            #endif
                                                      (begin, first_slice_end); assert(nullptr != bunch_T_a_Bprime);
        begin = first_slice_end;
        while (nullptr == begin->succ)
        {                                                                       assert(nullptr == begin->begin_or_before_end);
            ++begin;                                                            assert(begin <= last_slice_begin);
        }                                                                       assert(nullptr != begin->begin_or_before_end);
        if (begin == last_slice_begin)  part_tr.make_trivial(this);
    }                                                                           ONLY_IF_DEBUG( bunch_T_a_Bprime->work_counter = work_counter; )
    ++part_tr.nr_of_bunches;
    return bunch_T_a_Bprime;
}
 
} // end namespace bisim_dnj
 
 
 
 
 
/* ************************************************************************* */
/*                                                                           */
/*                            A L G O R I T H M S                            */
/*                                                                           */
/* ************************************************************************* */
 
 
 
 
 
 
 
 
/*=============================================================================
=                                 main class                                  =
=============================================================================*/
 
 
 
 
 
template <class LTS_TYPE>
class bisim_partitioner_dnj
{
  private:
    enum refine_mode_t{extend_from_marked_states,
                       extend_from_marked_states__add_new_noninert_to_splitter,
                       extend_from_splitter };
 
    LTS_TYPE& aut;
                                                                                ONLY_IF_DEBUG( public: )
    bisim_dnj::part_state_t part_st;
 
    bisim_dnj::part_trans_t part_tr;
  private:
    bisim_gjkw::fixed_vector<bisim_dnj::iterator_or_counter<
                                bisim_dnj::action_block_entry*> > action_label;
                                                                                ONLY_IF_DEBUG( public: )
    bool const branching;
  private:
    bool const preserve_divergence;
                                                                                #ifndef NDEBUG
                                                                                    friend class bisim_dnj::pred_entry;
                                                                                    friend class bisim_dnj::bunch_t;
                                                                                #endif
  public:
    bisim_partitioner_dnj(LTS_TYPE& new_aut, bool const new_branching = false,
                                    bool const new_preserve_divergence = false)
      : aut(new_aut),
        part_st(new_aut.num_states()),
        part_tr(new_aut.num_transitions(), new_aut.num_action_labels()),
        action_label(new_aut.num_action_labels()),
        branching(new_branching),
        preserve_divergence(new_preserve_divergence)
    {                                                                           assert(branching || !preserve_divergence);
 
mCRL2log(log::verbose) << "Start initialisation.\n";
        create_initial_partition();                                             ONLY_IF_DEBUG( part_tr.action_block_orig_inert_begin =
                                                                                                                       part_tr.action_block_inert_begin; )
mCRL2log(log::verbose) << "Start refining\n";
        refine_partition_until_it_becomes_stable();
    }
 
 
    state_type num_eq_classes() const
    {
        return part_st.nr_of_blocks;
    }
 
 
    state_type get_eq_class(state_type const s) const
    {
        return part_st.block(s)->seqnr;
    }
 
 
    void finalize_minimized_LTS()
    {
        // The labels have already been stored in
        // next_nontrivial_and_label.label by
        // refine_partition_until_it_becomes_stable().
 
        // for all blocks
        const bisim_dnj::permutation_entry*
                                          s_iter(&part_st.permutation.front()); assert(s_iter <= &part_st.permutation.back());
        do
        {
            const bisim_dnj::block_t* const B(s_iter->st->bl.ock);
            // for all block_bunch-slices of the block
            for (const bisim_dnj::block_bunch_slice_t& block_bunch :
                                                         B->stable_block_bunch)
            {                                                                   assert(block_bunch.is_stable());  assert(!block_bunch.empty());
                const bisim_dnj::pred_entry* const
                                                pred(block_bunch.end[-1].pred); assert(pred->source->bl.ock == B);
                                                                                assert(nullptr != pred->action_block->succ);
                /* add a transition from the source block to the goal block  */ assert(pred->action_block->succ->block_bunch->pred == pred);
                /* with the indicated label.                                 */ assert(pred->action_block->succ->block_bunch->slice == &block_bunch);
                label_type const
                     label(block_bunch.bunch->next_nontrivial_and_label.label); assert(0 <= label);  assert(label < action_label.size());
                aut.add_transition(transition(B->seqnr, label,
                                                 pred->target->bl.ock->seqnr));
            }
            s_iter = B->end;
        }
        while (s_iter <= &part_st.permutation.back());
 
        // Merge the states, by setting the state labels of each state to the
        // concatenation of the state labels of its equivalence class.
 
        if (aut.has_state_info())   /* If there are no state labels
                                                    this step can be ignored */
        {
            /* Create a vector for the new labels */
            bisim_gjkw::fixed_vector<typename LTS_TYPE::state_label_t>
                                                  new_labels(num_eq_classes());
 
            state_type i(aut.num_states());                                     assert(0 < i);
            do
            {
                --i;
                const state_type new_index(get_eq_class(i));
                new_labels[new_index]=new_labels[new_index]+aut.state_label(i);
            }
            while (0 < i);
 
            aut.set_num_states(num_eq_classes());
            i = 0;                                                              assert(i < num_eq_classes());
            do
            {
                aut.set_state_label(i, new_labels[i]);
            }
            while (++i < num_eq_classes());
        }
        else
        {
            aut.set_num_states(num_eq_classes());
        }
 
        aut.set_initial_state(get_eq_class(aut.initial_state()));
    }
 
 
    bool in_same_class(state_type const s, state_type const t) const
    {
        return part_st.block(s) == part_st.block(t);
    }
  private:
 
    /*--------------------------- main algorithm ----------------------------*/
 
    void create_initial_partition()
    {
        mCRL2log(log::verbose) << "An O(m log n) "
             << (branching ? (preserve_divergence
                                           ? "divergence-preserving branching "
                                           : "branching ")
                           : "")
             << "bisimulation partitioner created for " << part_st.state_size()
             << " states and " << aut.num_transitions() << " transitions.\n";
 
        if (part_st.state_size() > 2 * aut.num_transitions() + 1)
        {
            mCRL2log(log::warning) << "There are several isolated states "
                "without incoming or outgoing transition. It is not "
                "guaranteed that branching bisimulation minimisation runs in "
                "time O(m log n).\n";
        }
 
sort_transitions(aut.get_transitions(), tgt_lbl_src);
mCRL2log(log::verbose) << "Carried out sorting\n";
        // create one block for all states
        bisim_dnj::block_t* B(
                #ifdef USE_POOL_ALLOCATOR
                    part_tr.storage.template construct<bisim_dnj::block_t>
                #else
                    new bisim_dnj::block_t
                #endif
                    (&part_st.permutation.front(),
                     1 + &part_st.permutation.back(), part_st.nr_of_blocks++));
 
        // Iterate over the transitions to count how to order them in
        // part_trans_t
 
        // counters for the non-inert outgoing and incoming transitions per
        // state are provided in part_st.state_info.  These counters have been
        // initialised to zero in the constructor of part_state_t.
        // counters for the non-inert transition per label are stored in
        // action_label.
                                                                                assert(action_label.size() == aut.num_action_labels());
        // counter for the total number of inert transitions:
        trans_type inert_transitions(0);
        for (const transition& t: aut.get_transitions())
        {
            if (branching&&aut.is_tau(aut.apply_hidden_label_map(t.label()))&&  ((
                                                            t.from() != t.to())   || (assert(preserve_divergence), false)))
            {
                // The transition is inert.
                ++part_st.state_info[t.from()].succ_inert.count;
                ++inert_transitions;
 
                // The source state should become non-bottom:
                if (part_st.state_info[t.from()].pos < B->nonbottom_begin)
                {
                    std::swap(*part_st.state_info[t.from()].pos,
                                                        *--B->nonbottom_begin);
                    // we do not yet update the marked_bottom_begin pointer
                }
            }
            else
            {
                // The transition is non-inert.  (It may be a self-loop).
                ++part_st.state_info[t.from()].untested_to_U_eqv.count;
                ++action_label[aut.apply_hidden_label_map(t.label())].count;
            }
            ++part_st.state_info[t.to()].pred_inert.count;
        }
        // Now we update the marked_bottom_begin pointer:
        B->marked_bottom_begin = B->nonbottom_begin;
 
        // set the pointers to transition slices in the state info entries
 
        // We set them all to the end of the respective slice here.  Then, with
        // every transition, the pointer will be reduced by one, so that after
        // placing all transitions it will point to the beginning of the slice.
 
        bisim_dnj::pred_entry* next_pred_begin(&part_tr.pred.begin()[1]);
        bisim_dnj::succ_entry* next_succ_begin(&part_tr.succ.begin()[1]);
        bisim_dnj::state_info_entry* state_iter(&part_st.state_info.front());   assert(state_iter <= &part_st.state_info.back());
        do
        {
            state_iter->bl.ed_noninert_end = next_pred_begin;
            next_pred_begin += state_iter->pred_inert.count;
            state_iter->pred_inert.convert_to_iterator(next_pred_begin);
 
            // create slice descriptors in part_tr.succ for each state with
            /* outgoing transitions.                                         */ assert(nullptr != next_succ_begin);
            state_iter->untested_to_U_eqv.convert_to_iterator(
                        next_succ_begin + state_iter->untested_to_U_eqv.count);
            if (next_succ_begin < state_iter->untested_to_U_eqv.begin)
            {                                                                   assert(nullptr != state_iter->untested_to_U_eqv.begin);
                next_succ_begin->begin_or_before_end =
                                       state_iter->untested_to_U_eqv.begin - 1;
                for (bisim_dnj::succ_entry* const
                                              out_slice_begin(next_succ_begin);
                     ++next_succ_begin < state_iter->untested_to_U_eqv.begin; )
                {
                    next_succ_begin->begin_or_before_end = out_slice_begin;     // mCRL2complexity(next_succ_begin->block_bunch->pred, ...) -- subsumed in the
                }                                                               // call below
 
                B->mark(state_iter->pos);
            }
            state_iter->succ_inert.convert_to_iterator(next_succ_begin +
                                                 state_iter->succ_inert.count);
                                                                                #ifndef NDEBUG
                                                                                    while (next_succ_begin < state_iter->succ_inert.begin)
                                                                                    {   assert(nullptr == next_succ_begin->begin_or_before_end);
                                                                                        ++next_succ_begin;
                                                                                    }
                                                                                #endif
            next_succ_begin = state_iter->succ_inert.begin;                     // mCRL2complexity(*state_iter, ...) -- subsumed in the call at the end
        }
        while (++state_iter <= &part_st.state_info.back());
 
        // Line 2.4: Pi_t := { { all non-inert transitions } }
        part_tr.action_block_inert_begin =
                                  part_tr.action_block_end - inert_transitions; assert(part_tr.action_block_begin <= part_tr.action_block_inert_begin);
        part_tr.block_bunch_inert_begin =
                           1 + &part_tr.block_bunch.back() - inert_transitions; assert(1 + &part_tr.block_bunch.front() <= part_tr.block_bunch_inert_begin);
        bisim_dnj::bunch_t* bunch(nullptr);
 
        if (1 + &part_tr.block_bunch.front() < part_tr.block_bunch_inert_begin)
        {                                                                       assert(part_tr.action_block_begin < part_tr.action_block_inert_begin);
            // create a single bunch containing all non-inert transitions
            bunch =
                #ifdef USE_POOL_ALLOCATOR
                    part_tr.storage.template construct<bisim_dnj::bunch_t>
                #else
                    new bisim_dnj::bunch_t
                #endif
                                            (part_tr.action_block_begin,
                                             part_tr.action_block_inert_begin); assert(nullptr != bunch);  assert(part_tr.splitter_list.empty());
            ++part_tr.nr_of_bunches;                                            assert(1 == part_tr.nr_of_bunches);
 
            // create a single block_bunch entry for all non-inert transitions
            part_tr.splitter_list.emplace_front(
                    ONLY_IF_POOL_ALLOCATOR( part_tr.storage, )
                                part_tr.block_bunch_inert_begin, bunch, false); assert(!part_tr.splitter_list.empty());
            ++part_tr.nr_of_block_bunch_slices;                                 assert(1 == part_tr.nr_of_block_bunch_slices);
        }
 
        // create slice descriptors in part_tr.action_block for each label
 
        // The action_block array shall have the tau transitions at the end:
        // first the non-inert tau transitions (during initialisation, that are
        // only the tau self-loops), then the tau transitions that have become
        // non-inert and finally the inert transitions.
        // Transitions with other labels are placed from beginning to end.
        // Every such transition block except the last one ends with a dummy
        /* entry.  If there are transition labels without transitions,       */ assert((size_t) (part_tr.action_block_end - part_tr.action_block_begin) ==
        /* multiple dummy entries will be placed side-by-side.               */                               aut.num_transitions() + action_label.size() - 1);
        bisim_dnj::action_block_entry*
                           next_action_label_begin(part_tr.action_block_begin);
        trans_type const n_square(part_st.state_size() * part_st.state_size()); ONLY_IF_DEBUG( trans_type max_transitions = n_square; )
        label_type label(action_label.size());                                  assert(0 < label);
        do
        {
            --label;
            if (0 < action_label[label].count)
            {                                                                   assert(nullptr != bunch);
                if (++part_tr.nr_of_action_block_slices == 2)
                {
                    // This is the second action_block-slice, so the bunch is
                    // not yet marked as nontrivial but it should be.
                    part_tr.make_nontrivial(bunch);
                }
                if (n_square < action_label[label].count)
                {
                    mCRL2log(log::warning) << "There are "
                        << action_label[label].count << ' '
                        << pp(aut.action_label(label)) << "-transitions.  "
                        "This is more than n^2 (= " << n_square << "). It is "
                        "not guaranteed that branching bisimulation "
                        "minimisation runs in time O(m log n).\n";              ONLY_IF_DEBUG(  if (max_transitions < action_label[label].count)
                                                                                                {   max_transitions = action_label[label].count;   }  )
                }
                // initialise begin_or_before_end pointers for this
                // action_block-slice
                action_label[label].convert_to_iterator(
                          next_action_label_begin + action_label[label].count);
                next_action_label_begin->begin_or_before_end =
                                                 action_label[label].begin - 1; assert(nullptr != next_action_label_begin->begin_or_before_end);
                bisim_dnj::action_block_entry* const
                             action_block_slice_begin(next_action_label_begin); assert(nullptr != action_block_slice_begin);
                while (++next_action_label_begin < action_label[label].begin)
                {
                    next_action_label_begin->begin_or_before_end =
                                                      action_block_slice_begin; // mCRL2complexity(next_action_label_begin->succ->block_bunch->pred, ...) --
                }                                                               // subsumed in the call at the end
            }
            else
            {
                action_label[label].convert_to_iterator(
                                                      next_action_label_begin);
                if (0 != label && aut.num_transitions() < action_label.size())
                {
                    mCRL2log(log::warning) << "Action label "
                        << pp(aut.action_label(label)) << " has no "
                        "transitions, and the number of action labels exceeds "
                        "the number of transitions. It is not guaranteed that "
                        "branching bisimulation minimisation runs in time "
                        "O(m log n).\n";
                }
            }
        }
        while (0 < label && (/* insert a dummy entry                         */ assert(next_action_label_begin < part_tr.action_block_inert_begin),
                     next_action_label_begin->succ = nullptr,
                     next_action_label_begin->begin_or_before_end = nullptr,
                                             ++next_action_label_begin, true)); assert(next_action_label_begin == part_tr.action_block_inert_begin);
 
        /* distribute the transitions over the data structures               */ ONLY_IF_DEBUG( check_complexity::init(2 * max_transitions); )
 
        bisim_dnj::block_bunch_entry*
                            next_block_bunch(1 + &part_tr.block_bunch.front());
        for (const transition& t: aut.get_transitions())
        {
            bisim_dnj::state_info_entry* const
                                source(&part_st.state_info.front() + t.from());
            bisim_dnj::state_info_entry* const
                                target(&part_st.state_info.front() + t.to());
            bisim_dnj::succ_entry* succ_pos;
            bisim_dnj::block_bunch_entry* block_bunch_pos;
            bisim_dnj::pred_entry* pred_pos;
            bisim_dnj::action_block_entry* action_block_pos;
 
            if (branching&&aut.is_tau(aut.apply_hidden_label_map(t.label()))&&  ((
                                                            t.from() != t.to())   || (assert(preserve_divergence), false)))
            {
                // It is a (normal) inert transition: place near the end of the
                // respective pred/succ slices, just before the other inert
                // transitions.
                succ_pos = --source->succ_inert.begin;                          assert(nullptr == succ_pos->begin_or_before_end);
                block_bunch_pos = 1 + &part_tr.block_bunch.back() -
                                                             inert_transitions; assert(block_bunch_pos >= part_tr.block_bunch_inert_begin);
                pred_pos = --target->pred_inert.begin;                          assert(block_bunch_pos->slice.is_null());
                action_block_pos = part_tr.action_block_end-inert_transitions;  assert(action_block_pos >= part_tr.action_block_inert_begin);
                action_block_pos->begin_or_before_end = nullptr;
                --inert_transitions;
            }
            else
            {
                // It is a non-inert transition (possibly a self-loop): place
                // at the end of the respective succ slice and at the beginning
                // of the respective pred slice.
                succ_pos =
                        --part_st.state_info[t.from()].untested_to_U_eqv.begin; assert(nullptr != succ_pos->begin_or_before_end);
                                                                                assert(nullptr != succ_pos->begin_or_before_end->begin_or_before_end);
                                                                                assert(succ_pos->begin_or_before_end <= succ_pos ||
                                                                                               succ_pos->begin_or_before_end->begin_or_before_end == succ_pos);
                block_bunch_pos = next_block_bunch++;                           assert(block_bunch_pos < part_tr.block_bunch_inert_begin);
                pred_pos = target->bl.ed_noninert_end++;
                action_block_pos =
                   --action_label[aut.apply_hidden_label_map(t.label())].begin; assert(nullptr != action_block_pos->begin_or_before_end);
                                                                                assert(nullptr != action_block_pos->begin_or_before_end->begin_or_before_end);
                                                                                assert(action_block_pos->begin_or_before_end <= action_block_pos ||
                                                                                                action_block_pos->begin_or_before_end->
                                                                                                                      begin_or_before_end == action_block_pos);
                                                                                assert(!part_tr.splitter_list.empty());
                block_bunch_pos->slice = part_tr.splitter_list.begin();         assert(action_block_pos < part_tr.action_block_inert_begin);
            }                                                                   assert(target->bl.ed_noninert_end <= target->pred_inert.begin);
            succ_pos->block_bunch = block_bunch_pos;
            block_bunch_pos->pred = pred_pos;
            pred_pos->action_block = action_block_pos;
            pred_pos->source = source;
            pred_pos->target = target;                                          assert(nullptr != succ_pos);
            action_block_pos->succ = succ_pos;                                  // mCRL2complexity(pred_pos, ...) -- subsumed in the call at the end
        }                                                                       assert(0 == inert_transitions);
        /* delete transitions already -- they are no longer needed.  We will */ assert(next_block_bunch == part_tr.block_bunch_inert_begin);
        // add new transitions at the end of minimisation.
        aut.clear_transitions();
 
        state_iter = &part_st.state_info.front();                               assert(state_iter <= &part_st.state_info.back());
        do
        {
            state_iter->bl.ock = B;
        }
        while (++state_iter <= &part_st.state_info.back());
 
        if (nullptr != bunch)
        {
            while (nullptr == bunch->begin->succ)
            {                                                                   assert(nullptr == bunch->begin->begin_or_before_end);
                ++bunch->begin;                                                 assert(bunch->begin < bunch->end);
            }                                                                   assert(nullptr != bunch->begin->begin_or_before_end);
            while (nullptr == bunch->end[-1].succ)
            {                                                                   assert(nullptr == bunch->end[-1].begin_or_before_end);
                --bunch->end;                                                   assert(bunch->begin < bunch->end);
            }                                                                   assert(nullptr != bunch->end[-1].begin_or_before_end);
 
            /* Line 2.2: B_vis := { s in S | there exists a visible          */ mCRL2complexity(B, add_work(check_complexity::
            /*                               transition that is reachable    */                                          create_initial_partition, 1U), *this);
            //                               from s }
            //           B_invis := S \ B_vis
            // Line 2.3: Pi_s := { B_vis, B_invis } \ { emptyset }
                // At this point, all states with a visible transition are
                // marked.
            if (0 < B->marked_size())
            {                                                                   ONLY_IF_DEBUG( part_st.print_part(*this);
                                                                                               part_tr.print_trans(*this); )
                bisim_dnj::block_bunch_slice_iter_t slice =
                                                 part_tr.splitter_list.begin();
                if (1 < B->size())
                {
                    B = split(B, /* splitter block_bunch */ slice,
                      extend_from_marked_states__add_new_noninert_to_splitter);
                    // We can ignore possible new non-inert transitions, as
                    // every R-bottom state already has a transition in bunch.
                    B->marked_nonbottom_begin = B->end;
                }
                else
                {                                                               assert(B->nonbottom_begin == B->end);
                    /* A block with 1 state will not be split.  However, we  */ assert(B->marked_nonbottom_begin == B->end);
                    // still have to make the splitter stable.
                    B->stable_block_bunch.splice(B->stable_block_bunch.end(),
                                                 part_tr.splitter_list, slice);
                    slice->make_stable();
                }                                                               assert(!B->stable_block_bunch.empty());  assert(part_tr.splitter_list.empty());
                                                                                assert(B->stable_block_bunch.front().end <= part_tr.block_bunch_inert_begin);
                                                                                assert(1 + &part_tr.block_bunch.front() < B->stable_block_bunch.front().end);
                B->marked_bottom_begin = B->nonbottom_begin;                    assert(!B->stable_block_bunch.front().empty());
            }
        }                                                                       else  assert(0 == B->marked_size());
    }
                                                                                #ifndef NDEBUG
                                                                                    void assert_stability() const
                                                                                    {
                                                                                        part_st.assert_consistency(*this);
 
                                                                                        assert(part_tr.succ.size() == part_tr.block_bunch.size() + 1);
                                                                                        assert(part_tr.pred.size() == part_tr.block_bunch.size() + 1);
                                                                                        assert((size_t)(part_tr.action_block_end-part_tr.action_block_begin) ==
                                                                                                         part_tr.block_bunch.size() + action_label.size() - 2);
                                                                                        if (part_tr.block_bunch.empty())  return;
 
                                                                                        assert(part_tr.splitter_list.empty());
                                                                                        /* for (const block_bunch_slice_t& block_bunch : part_tr.splitter_list)
                                                                                        {
                                                                                            assert(!block_bunch.is_stable());
                                                                                        } */
 
                                                                                        trans_type true_nr_of_block_bunch_slices(0);
                                                                                        // for all blocks
                                                                                        const bisim_dnj::permutation_entry*
                                                                                                                       perm_iter(&part_st.permutation.front());
                                                                                        assert(perm_iter <= &part_st.permutation.back());
                                                                                        do
                                                                                        {
                                                                                            const bisim_dnj::block_t* const block(perm_iter->st->bl.ock);
                                                                                            unsigned const max_block(check_complexity::log_n -
                                                                                                                       check_complexity::ilog2(block->size()));
                                                                                            // iterators have no predefined hash, so we store pointers:
                                                                                            std::unordered_set<const bisim_dnj::block_bunch_slice_t*>
                                                                                                                                         block_bunch_check_set;
                                                                                            #ifndef USE_SIMPLE_LIST
                                                                                                block_bunch_check_set.reserve(
                                                                                                                             block->stable_block_bunch.size());
                                                                                            #endif
 
                                                                                            // for all stable block_bunch-slices of the block
                                                                                            for (const bisim_dnj::block_bunch_slice_t& block_bunch :
                                                                                                                                     block->stable_block_bunch)
                                                                                            {
                                                                                                assert(block_bunch.source_block() == block);
                                                                                                assert(block_bunch.is_stable());
                                                                                                block_bunch_check_set.insert(&block_bunch);
                                                                                                mCRL2complexity(&block_bunch, no_temporary_work(
                                                                                                           block_bunch.bunch->max_work_counter(*this)), *this);
                                                                                                ++true_nr_of_block_bunch_slices;
                                                                                            }
 
                                                                                            // for all states in the block
                                                                                            do
                                                                                            {
                                                                                                trans_type block_bunch_count(0);
                                                                                                const bisim_dnj::state_info_entry* const state(perm_iter->st);
                                                                                                assert(state!=part_tr.succ.front().block_bunch->pred->source);
                                                                                                // for all out-slices of the state
                                                                                                for (const bisim_dnj::succ_entry*
                                                                                                                        out_slice_end(state->succ_inert.begin);
                                                                                                        state == out_slice_end[-1].block_bunch->pred->source; )
                                                                                                {   assert(!out_slice_end[-1].block_bunch->slice.is_null());
                                                                                                    bisim_dnj::block_bunch_slice_const_iter_t const
                                                                                                       block_bunch_slice(out_slice_end[-1].block_bunch->slice);
                                                                                                    const bisim_dnj::bunch_t* const bunch(
                                                                                                                                     block_bunch_slice->bunch);
                                                                                                    assert(block == block_bunch_slice->source_block());
                                                                                                    if (block_bunch_slice->is_stable())
                                                                                                    {
                                                                                                        assert(1 == block_bunch_check_set.count(
                                                                                                                                         &*block_bunch_slice));
                                                                                                        ++block_bunch_count;
                                                                                                    }
                                                                                                    else  assert(0); // i. e. all block_bunch-slices should
                                                                                                                         // be stable
                                                                                                    const bisim_dnj::succ_entry* const out_slice_begin(
                                                                                                                        out_slice_end[-1].begin_or_before_end);
                                                                                                    assert(nullptr != out_slice_begin);
                                                                                                    assert(out_slice_begin < out_slice_end);
                                                                                                    assert(nullptr != out_slice_begin->begin_or_before_end);
                                                                                                    assert(out_slice_begin->begin_or_before_end + 1 ==
                                                                                                                                                out_slice_end);
 
                                                                                                    // for all transitions in the out-slice
                                                                                                    do
                                                                                                    {
                                                                                                        --out_slice_end;
                                                                                                        assert(bunch->begin <=
                                                                                                               out_slice_end->block_bunch->pred->action_block);
                                                                                                        assert(out_slice_end->block_bunch->pred->
                                                                                                                                    action_block < bunch->end);
                                                                                                        assert(out_slice_end->block_bunch->slice ==
                                                                                                                                            block_bunch_slice);
                                                                                                        assert(nullptr != out_slice_end->begin_or_before_end);
                                                                                                        if (out_slice_end->block_bunch + 1 !=
                                                                                                                                        block_bunch_slice->end)
                                                                                                        {
                                                                                                            assert(out_slice_end->block_bunch + 1 <
                                                                                                                                       block_bunch_slice->end);
                                                                                                            assert(out_slice_end->block_bunch[1].slice ==
                                                                                                                                            block_bunch_slice);
                                                                                                        }
                                                                                                        mCRL2complexity(out_slice_end->block_bunch->pred,
                                                                                                            no_temporary_work(max_block,
                                                                                                                    check_complexity::log_n -
                                                                                                                    check_complexity::ilog2(out_slice_end->
                                                                                                                    block_bunch->pred->target->bl.ock->size()),
                                                                                                                    perm_iter < block->nonbottom_begin),*this);
                                                                                                    }
                                                                                                    while (out_slice_begin < out_slice_end &&
                                                                                                           (assert(out_slice_begin ==
                                                                                                                   out_slice_end->begin_or_before_end), true));
                                                                                                }
                                                                                                if (perm_iter < block->nonbottom_begin)
                                                                                                {
                                                                                                    assert(block_bunch_check_set.size() == block_bunch_count);
                                                                                                }
                                                                                            }
                                                                                            while (++perm_iter < block->end);
                                                                                        }
                                                                                        while (perm_iter <= &part_st.permutation.back());
                                                                                        assert(part_tr.nr_of_block_bunch_slices ==
                                                                                                                                true_nr_of_block_bunch_slices);
                                                                                        assert(part_tr.action_block_begin <= part_tr.action_block_inert_begin);
                                                                                        assert(&part_tr.block_bunch.front() < part_tr.block_bunch_inert_begin);
                                                                                        if (branching)
                                                                                        {   assert(part_tr.action_block_inert_begin<=part_tr.action_block_end);
                                                                                            assert(part_tr.block_bunch_inert_begin <=
                                                                                                                              1 + &part_tr.block_bunch.back());
                                                                                            assert(1 + &part_tr.block_bunch.back() -
                                                                                                                             part_tr.block_bunch_inert_begin ==
                                                                                                  part_tr.action_block_end - part_tr.action_block_inert_begin);
 
                                                                                            // for all inert transitions
                                                                                            for (const bisim_dnj::action_block_entry* action_block(
                                                                                                                             part_tr.action_block_inert_begin);
                                                                                                                       action_block < part_tr.action_block_end;
                                                                                                                                                ++action_block)
                                                                                            {   assert(nullptr == action_block->begin_or_before_end);
                                                                                                const bisim_dnj::succ_entry* const
                                                                                                                                 succ_iter(action_block->succ);
                                                                                                assert(nullptr != succ_iter);
                                                                                                assert(succ_iter->block_bunch->slice.is_null());
                                                                                                const bisim_dnj::pred_entry* const
                                                                                                                       pred_iter(succ_iter->block_bunch->pred);
                                                                                                assert(action_block == pred_iter->action_block);
                                                                                                assert(part_tr.block_bunch_inert_begin <=
                                                                                                                                       succ_iter->block_bunch);
                                                                                                assert(pred_iter->source != pred_iter->target);
                                                                                                assert(pred_iter->source->bl.ock == pred_iter->target->bl.ock);
                                                                                                assert(pred_iter->source->succ_inert.begin <= succ_iter);
                                                                                                assert(pred_iter->source->succ_inert.begin == succ_iter ||
                                                                                                   succ_iter[-1].block_bunch->pred->source==pred_iter->source);
                                                                                                assert(pred_iter->target->pred_inert.begin <= pred_iter);
                                                                                                assert(pred_iter->target->pred_inert.begin == pred_iter ||
                                                                                                                    pred_iter[-1].target == pred_iter->target);
                                                                                                unsigned const max_block(check_complexity::log_n -
                                                                                                   check_complexity::ilog2(pred_iter->target->bl.ock->size()));
                                                                                                mCRL2complexity(pred_iter, no_temporary_work(max_block,
                                                                                                                                     max_block, false), *this);
                                                                                            }
                                                                                        }
                                                                                        else
                                                                                        {
                                                                                            assert(!preserve_divergence);
                                                                                            assert(part_tr.action_block_inert_begin==part_tr.action_block_end);
                                                                                            assert(part_tr.block_bunch_inert_begin ==
                                                                                                                              1 + &part_tr.block_bunch.back());
                                                                                        }
                                                                                        const bisim_dnj::action_block_entry*
                                                                                                            action_slice_end(part_tr.action_block_inert_begin);
                                                                                        trans_type true_nr_of_bunches(0);
                                                                                        trans_type true_nr_of_nontrivial_bunches(0);
                                                                                        trans_type true_nr_of_action_block_slices(0);
                                                                                        // for all action labels and bunches
                                                                                        label_type label(0);
                                                                                        assert(label < action_label.size());
                                                                                        const bisim_dnj::bunch_t* previous_bunch(nullptr);
                                                                                        do
                                                                                        {
                                                                                            assert(part_tr.action_block_begin <= action_label[label].begin);
                                                                                            assert(action_label[label].begin <= action_slice_end);
                                                                                            assert(action_slice_end <= part_tr.action_block_inert_begin);
                                                                                            // for all action_block slices
                                                                                            for (const bisim_dnj::action_block_entry*
                                                                                                                     action_block_slice_end(action_slice_end);
                                                                                                          action_label[label].begin < action_block_slice_end; )
                                                                                            {
                                                                                                const bisim_dnj::action_block_entry* const
                                                                                                        action_block_slice_begin(
                                                                                                               action_block_slice_end[-1].begin_or_before_end);
                                                                                                assert(nullptr != action_block_slice_begin);
                                                                                                assert(action_block_slice_begin < action_block_slice_end);
                                                                                                assert(action_block_slice_end <= action_slice_end);
                                                                                                assert(nullptr != action_block_slice_begin->succ);
                                                                                                const bisim_dnj::block_t* const
                                                                                                        target_block(action_block_slice_begin->
                                                                                                                      succ->block_bunch->pred->target->bl.ock);
                                                                                                const bisim_dnj::bunch_t* const
                                                                                                                bunch(action_block_slice_begin->succ->bunch());
                                                                                                if (previous_bunch != bunch)
                                                                                                {
                                                                                                    assert(nullptr == previous_bunch);
                                                                                                    previous_bunch = bunch;
                                                                                                    assert(bunch->end == action_block_slice_end);
                                                                                                    if (bunch->begin == action_block_slice_begin)
                                                                                                    {
                                                                                                        // Perhaps this does not always hold; sometimes, an
                                                                                                        // action_block slice disappears but the bunch cannot
                                                                                                        // be made trivial.
                                                                                                        assert(bunch->is_trivial());
                                                                                                    }
                                                                                                    else
                                                                                                    {
                                                                                                        assert(!bunch->is_trivial());
                                                                                                        ++true_nr_of_nontrivial_bunches;
                                                                                                    }
                                                                                                    mCRL2complexity(bunch, no_temporary_work(
                                                                                                                       bunch->max_work_counter(*this)), *this);
                                                                                                    ++true_nr_of_bunches;
                                                                                                }
                                                                                                if(bunch->begin == action_block_slice_begin)
                                                                                                {
                                                                                                    previous_bunch = nullptr;
                                                                                                }
                                                                                                else  assert(bunch->begin < action_block_slice_begin);
 
                                                                                                assert(action_block_slice_begin->begin_or_before_end + 1 ==
                                                                                                                                       action_block_slice_end);
                                                                                                // for all transitions in the action_block slice
                                                                                                const bisim_dnj::action_block_entry*
                                                                                                                          action_block(action_block_slice_end);
                                                                                                do
                                                                                                {
                                                                                                    --action_block;
                                                                                                    const bisim_dnj::succ_entry* const
                                                                                                                                 succ_iter(action_block->succ);
                                                                                                    assert(nullptr != succ_iter);
                                                                                                    const bisim_dnj::pred_entry* const
                                                                                                                       pred_iter(succ_iter->block_bunch->pred);
                                                                                                    assert(action_block == pred_iter->action_block);
                                                                                                    assert(succ_iter->block_bunch <
                                                                                                                              part_tr.block_bunch_inert_begin);
                                                                                                    assert(!branching || !aut.is_tau(label) ||
                                                                                                        pred_iter->source->bl.ock!=pred_iter->target->bl.ock ||
                                                                                                                     (preserve_divergence &&
                                                                                                                      pred_iter->source == pred_iter->target));
                                                                                                    assert(succ_iter < pred_iter->source->succ_inert.begin);
                                                                                                    assert(succ_iter+1==pred_iter->source->succ_inert.begin ||
                                                                                                                succ_iter[1].block_bunch->pred->source ==
                                                                                                                                            pred_iter->source);
                                                                                                    assert(pred_iter < pred_iter->target->pred_inert.begin);
                                                                                                    assert(pred_iter+1==pred_iter->target->pred_inert.begin ||
                                                                                                                     pred_iter[1].target == pred_iter->target);
                                                                                                    assert(target_block == pred_iter->target->bl.ock);
                                                                                                    assert(bunch == succ_iter->bunch());
                                                                                                }
                                                                                                while (action_block_slice_begin < action_block &&
                                                                                                   (// some properties only need to be checked for states that
                                                                                                    // are not the first one:
                                                                                                    assert(action_block->begin_or_before_end ==
                                                                                                                             action_block_slice_begin), true));
                                                                                                action_block_slice_end = action_block_slice_begin;
                                                                                                ++true_nr_of_action_block_slices;
                                                                                            }
                                                                                            if (action_slice_end < part_tr.action_block_inert_begin)
                                                                                            {
                                                                                                // there is a dummy transition between action labels
                                                                                                assert(nullptr == action_slice_end->succ);
                                                                                                assert(nullptr == action_slice_end->begin_or_before_end);
                                                                                            }
                                                                                        }
                                                                                        while (++label < action_label.size() &&
                                                                                                 (action_slice_end = action_label[label - 1].begin - 1, true));
                                                                                        assert(nullptr == previous_bunch);
                                                                                        assert(part_tr.nr_of_bunches == true_nr_of_bunches);
                                                                                        assert(part_tr.nr_of_nontrivial_bunches ==
                                                                                                                                true_nr_of_nontrivial_bunches);
                                                                                        assert(part_tr.nr_of_action_block_slices ==
                                                                                                                               true_nr_of_action_block_slices);
                                                                                    }
                                                                                #endif
    void refine_partition_until_it_becomes_stable()
    {
        // Line 2.5: for all non-trivial bunches bunch_T in Pi_t do
        clock_t next_print_time = clock();
        const clock_t rounded_start_time = next_print_time - CLOCKS_PER_SEC/2;
        // const double log_initial_nr_of_action_block_slices =
        //                   100 / std::log(part_tr.nr_of_action_block_slices);
        for (;;)
        {                                                                       // mCRL2complexity(...) -- this loop will be ascribed to (the transitions in)
                                                                                // the new bunch below.
            /*------------------ find a non-trivial bunch -------------------*/ ONLY_IF_DEBUG( part_st.print_part(*this);  part_tr.print_trans(*this);