liblts_bisim_gjkw.h

Go to the documentation of this file.

// Author(s): David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands
//
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
 
 
#ifndef _LIBLTS_BISIM_GJKW_H
#define _LIBLTS_BISIM_GJKW_H
 
#include <unordered_map> // used during initialisation
#include <list>          // for the list of B_to_C_descriptors
 
#include "mcrl2/lts/detail/liblts_scc.h"
#include "mcrl2/lts/detail/liblts_merge.h"
#include "mcrl2/lts/detail/check_complexity.h"
#include "mcrl2/lts/detail/fixed_vector.h"
 
namespace mcrl2
{
namespace lts
{
namespace detail
{
                                                                                #ifndef NDEBUG
                                                                                    #define ONLY_IF_DEBUG(...) __VA_ARGS__
                                                                                #else
                                                                                    #define ONLY_IF_DEBUG(...)
                                                                                #endif
// state_type and trans_type are defined in check_complexity.h.
 
typedef std::size_t label_type;
 
 
 
 
 
/* ************************************************************************* */
/*                                                                           */
/*                   R E F I N A B L E   P A R T I T I O N                   */
/*                                                                           */
/* ************************************************************************* */
 
 
 
 
 
 
namespace bisim_gjkw
{
 
class state_info_entry;
 
typedef state_info_entry* state_info_ptr;
typedef const state_info_entry* state_info_const_ptr;
 
typedef fixed_vector<state_info_ptr> permutation_t;
typedef permutation_t::iterator permutation_iter_t;
typedef permutation_t::const_iterator permutation_const_iter_t;
 
class block_t;
class constln_t;
 
class B_to_C_entry;
class pred_entry;
class succ_entry;
typedef fixed_vector<B_to_C_entry>::iterator B_to_C_iter_t;
typedef fixed_vector<pred_entry>::iterator pred_iter_t;
typedef fixed_vector<succ_entry>::iterator succ_iter_t;
 
typedef fixed_vector<B_to_C_entry>::const_iterator B_to_C_const_iter_t;
typedef fixed_vector<pred_entry>::const_iterator pred_const_iter_t;
typedef fixed_vector<succ_entry>::const_iterator succ_const_iter_t;
class B_to_C_descriptor;
typedef std::list<B_to_C_descriptor> B_to_C_desc_list;
typedef B_to_C_desc_list::iterator B_to_C_desc_iter_t;
typedef B_to_C_desc_list::const_iterator B_to_C_desc_const_iter_t;
 
class state_info_entry
{
  private:
    pred_iter_t state_in_begin;
 
    succ_iter_t state_out_begin;
 
    pred_iter_t state_inert_in_begin;
 
    succ_iter_t state_inert_out_begin;
 
    succ_iter_t state_inert_out_end;
  public:
    block_t* block;
 
    permutation_iter_t pos;
 
    state_type notblue;
  private:
    succ_iter_t int_current_constln;
  public:
    const constln_t* constln() const;
    constln_t* constln();
 
    succ_const_iter_t current_constln() const {  return int_current_constln;  }
    succ_iter_t current_constln()  {  return int_current_constln;  }
    void set_current_constln(succ_iter_t const new_current_constln)
    {
        int_current_constln = new_current_constln;                              // current_constln points to a successor transition of this state:
                                                                                assert(succ_begin() <= int_current_constln);
                                                                                assert(int_current_constln <= succ_end());
                                                                                // it points to a place where a constellation slice starts or ends:
                                                                                // (This assertion cannot be tested because the types are not yet
                                                                                // complete.)
                                                                                // assert(succ_begin() == int_current_constln ||
                                                                                //     succ_end() == int_current_constln ||
                                                                                //     int_current_constln[-1].constln_slice !=
                                                                                //                                 int_current_constln->constln_slice);
                                                                                // it points to the relevant constellation:
                                                                                // The following assertions cannot be executed immediately after each
                                                                                // call.
                                                                                // assert(succ_begin() == current_constln() ||
                                                                                //                   *current_constln()[-1].target->constln() <= *SpC);
                                                                                // assert(succ_end() == current_constln() ||
                                                                                //                      *SpC <= *current_constln()->target->constln());
    }
 
    pred_const_iter_t pred_begin() const  {  return state_in_begin;  }
    pred_iter_t pred_begin()  {  return state_in_begin;  }
    void set_pred_begin(pred_iter_t new_in_begin)
    {
        state_in_begin = new_in_begin;
    }
 
    pred_const_iter_t pred_end() const
    {                                                                           assert(s_i_begin <= this);  assert(this < s_i_end);
        return this[1].state_in_begin;
    }
    pred_iter_t pred_end()
    {                                                                           assert(s_i_begin <= this);  assert(this < s_i_end);
        return this[1].state_in_begin;
    }
    void set_pred_end(pred_iter_t new_in_end)
    {                                                                           assert(s_i_begin <= this);  assert(this < s_i_end);
        this[1].set_pred_begin(new_in_end);
    }
 
    pred_const_iter_t noninert_pred_begin() const  {  return state_in_begin;  }
    pred_iter_t noninert_pred_begin()  {  return state_in_begin;  }
 
    pred_const_iter_t noninert_pred_end() const  { return inert_pred_begin(); }
    pred_iter_t noninert_pred_end()  {  return inert_pred_begin();  }
 
    pred_const_iter_t inert_pred_begin() const { return state_inert_in_begin; }
    pred_iter_t inert_pred_begin()  {  return state_inert_in_begin;  }
    void set_inert_pred_begin(pred_iter_t new_inert_in_begin)
    {
        state_inert_in_begin = new_inert_in_begin;                              assert(pred_begin() <= inert_pred_begin());
                                                                                assert(inert_pred_begin() <= pred_end());
    }
 
    pred_const_iter_t inert_pred_end() const { return pred_end(); }
    pred_iter_t inert_pred_end()  {  return pred_end();  }
 
    succ_const_iter_t succ_begin() const  {  return state_out_begin;  }
    succ_iter_t succ_begin()  {  return state_out_begin;  }
    void set_succ_begin(succ_iter_t new_out_begin)
    {
        state_out_begin = new_out_begin;
    }
 
    succ_const_iter_t succ_end() const
    {                                                                           assert(s_i_begin <= this);  assert(this < s_i_end);
        return this[1].state_out_begin;
    }
    succ_iter_t succ_end()
    {                                                                           assert(s_i_begin <= this);  assert(this < s_i_end);
        return this[1].state_out_begin;
    }
    void set_succ_end(succ_iter_t new_out_end)
    {                                                                           assert(s_i_begin <= this);  assert(this < s_i_end);
        this[1].set_succ_begin(new_out_end);                                    assert(succ_begin() <= succ_end());
    }
 
    succ_const_iter_t inert_succ_begin() const  {return state_inert_out_begin;}
    succ_iter_t inert_succ_begin()  {  return state_inert_out_begin;  }
    void set_inert_succ_begin(succ_iter_t const new_inert_out_begin)
    {                                                                           // The following assertions cannot be tested because the respective
                                                                                // types are not yet complete.
                                                                                // if (new_inert_out_begin > inert_succ_begin())
                                                                                // {
                                                                                //     assert(*new_inert_out_begin[-1].target->constln()<=*constln());
                                                                                //     assert(new_inert_out_begin[-1].target->block != block);
                                                                                // }
                                                                                // else if (new_inert_out_begin < inert_succ_begin())
                                                                                // {
                                                                                //     assert(new_inert_out_begin->target->block == block);
                                                                                // }
        state_inert_out_begin = new_inert_out_begin;                            assert(succ_begin() <= inert_succ_begin());
                                                                                assert(inert_succ_begin() <= inert_succ_end());
    }
 
    succ_const_iter_t inert_succ_end() const  {  return state_inert_out_end;  }
    succ_iter_t inert_succ_end()  {  return state_inert_out_end;  }
 
    void set_inert_succ_begin_and_end(succ_iter_t new_inert_out_begin,
                                                 succ_iter_t new_inert_out_end)
    {
        state_inert_out_begin = new_inert_out_begin;
        state_inert_out_end = new_inert_out_end;                                assert(succ_begin() <= inert_succ_begin());
                                                                                assert(inert_succ_begin() <= inert_succ_end());
                                                                                assert(inert_succ_end() <= succ_end());
                                                                                // The following assertions cannot be tested always, as the function
                                                                                // may be called earlier than the assertions are reestablished.
                                                                                // assert(succ_begin() == inert_succ_begin() ||
                                                                                //            *inert_succ_begin()[-1].target->constln() <= *constln());
                                                                                // assert(succ_begin() == inert_succ_begin() ||
                                                                                //                      inert_succ_begin()[-1].target->block != block);
                                                                                // assert(inert_succ_begin() == inert_succ_end() ||
                                                                                //                      (inert_succ_begin()->target->block == block &&
                                                                                //                       inert_succ_end()[-1].target->block == block));
                                                                                // assert(succ_end() == inert_succ_end() ||
                                                                                //                  *constln() < *inert_succ_end()->target->constln());
    }
 
    bool surely_has_transition_to(const constln_t* SpC) const;
    bool surely_has_no_transition_to(const constln_t* SpC) const;
                                                                                #ifndef NDEBUG
                                                                                    std::string debug_id_short() const
                                                                                    {
                                                                                        assert(s_i_begin <= this);
                                                                                        assert(this < s_i_end);
                                                                                        return std::to_string(this - s_i_begin);
                                                                                    }
 
                                                                                    std::string debug_id() const
                                                                                    {
                                                                                        return "state " + debug_id_short();
                                                                                    }
                                                                                  private:
                                                                                    static state_info_const_ptr s_i_begin;
 
                                                                                    static state_info_const_ptr s_i_end;
 
                                                                                    friend class part_state_t;
                                                                                  public:
                                                                                    mutable check_complexity::state_counter_t work_counter;
                                                                                #endif
};
 
 
static inline void swap_permutation(permutation_iter_t s1,
                                                        permutation_iter_t s2)
{
    // swap contents of permutation array
    std::swap(*s1, *s2);
    // swap pointers to permutation array
    (*s1)->pos = s1;
    (*s2)->pos = s2;
}
 
class block_t
{
  private:
    permutation_iter_t int_end;
 
    permutation_iter_t int_begin;
 
    permutation_iter_t int_marked_nonbottom_begin;
 
    permutation_iter_t int_bottom_begin;
 
    permutation_iter_t int_marked_bottom_begin;
 
    B_to_C_iter_t int_inert_begin;
 
    B_to_C_iter_t int_inert_end;
  public:
    B_to_C_desc_list to_constln;
  private:
    constln_t* int_constln;
 
    block_t* refinable_next;
 
    static block_t* refinable_first;
 
    state_type int_seqnr;
 
#define BLOCK_NO_SEQNR ((state_type) -1)
 
  public:
    static state_type nr_of_blocks;
 
    block_t(constln_t* const constln_, permutation_iter_t const begin_,
                                                 permutation_iter_t const end_)
      : int_end(end_),
        int_begin(begin_),
        int_marked_nonbottom_begin(begin_), // no non-bottom state is marked
        int_bottom_begin(begin_), // all states are bottom states
        int_marked_bottom_begin(end_), // no bottom state is marked
        // int_inert_begin -- is initialised by part_trans_t::create_new_block
        // int_inert_end -- is initialised by part_trans_t::create_new_block
        to_constln(), // empty list
        int_constln(constln_),
        refinable_next(nullptr),
        int_seqnr(BLOCK_NO_SEQNR)
    {                                                                           // The following assertions hold trivially.
                                                                                // assert(int_begin <= int_marked_nonbottom_begin);
                                                                                // assert(int_marked_nonbottom_begin <= int_bottom_begin);
                                                                                // assert(int_bottom_begin <= int_marked_bottom_begin);
                                                                                // assert(int_marked_bottom_begin <= int_end);
                                                                                assert(int_bottom_begin < int_end);
                                                                                // The following assertions cannot be tested because constln_t is not
                                                                                // yet complete.
                                                                                // assert(int_constln->begin() <= int_begin);
                                                                                // assert(int_end <= int_constln->end());
    }
 
    ~block_t()  {  }
 
    void assign_seqnr()
    {                                                                           assert(BLOCK_NO_SEQNR == int_seqnr);
        int_seqnr = nr_of_blocks++;
    }
 
    state_type seqnr() const  {  return int_seqnr;  }
 
    static block_t* get_some_refinable()  {  return refinable_first;  }
 
    bool is_refinable() const  {  return nullptr != refinable_next;  }
 
    bool make_refinable()
    {
        if (is_refinable())
        {
            return false;
        }
        refinable_next = nullptr == refinable_first ? this : refinable_first;
        refinable_first = this;
        return true;
    }
 
    void make_nonrefinable()
    {                                                                           assert(refinable_first == this);
        refinable_first = refinable_next == this ? nullptr : refinable_next;
        refinable_next = nullptr;
    }
 
    state_type size() const  {  return int_end - int_begin;  }
 
    state_type marked_bottom_size() const
    {
        return marked_bottom_end() - marked_bottom_begin();
    }
 
    state_type marked_size() const
    {
        return marked_nonbottom_end() - marked_nonbottom_begin() +
                                                        marked_bottom_size();
    }
 
    state_type unmarked_bottom_size() const
    {
        return unmarked_bottom_end() - unmarked_bottom_begin();
    }
 
    bool operator<(const block_t& other) const
    {
        return begin() < other.begin();
    }
 
    const constln_t* constln() const  {  return int_constln;  }
    constln_t* constln()  {  return int_constln;  }
    void set_constln(constln_t* new_constln)
    {                                                                           // The following assertion cannot be tested because the type constln_t
        int_constln = new_constln;                                              // is not yet complete.
                                                                                // assert(nullptr == int_constln ||
                                                                                //                             (int_constln->begin() <= int_begin &&
                                                                                //                                     int_end <= int_constln->end()));
    }
 
    B_to_C_descriptor* FromRed(const constln_t* SpC);
 
    void SetFromRed(B_to_C_desc_iter_t new_fromred);
 
    permutation_const_iter_t begin()  const  {  return int_begin;  }
    permutation_iter_t begin()  {  return int_begin;  }
    void set_begin(permutation_iter_t new_begin)
    {
        int_begin = new_begin;                                                  assert(int_begin <= int_marked_nonbottom_begin);
    }
 
    permutation_const_iter_t end()  const  {  return int_end;  }
    permutation_iter_t end()  {  return int_end;  }
    void set_end(permutation_iter_t new_end)
    {
        int_end = new_end;                                                      assert(int_marked_bottom_begin <= int_end); assert(int_bottom_begin < int_end);
    }
 
    permutation_const_iter_t nonbottom_begin()  const  {  return int_begin;  }
    permutation_iter_t nonbottom_begin()  {  return int_begin;  }
 
    permutation_const_iter_t nonbottom_end() const { return int_bottom_begin; }
    permutation_iter_t nonbottom_end()  {  return int_bottom_begin;  }
    void set_nonbottom_end(permutation_iter_t new_nonbottom_end)
    {
        int_bottom_begin = new_nonbottom_end;                                   assert(int_marked_nonbottom_begin <= int_bottom_begin);
                                                                                assert(int_bottom_begin <= int_marked_bottom_begin);
                                                                                assert(int_bottom_begin < int_end);
    }
 
    permutation_const_iter_t bottom_begin() const  { return int_bottom_begin; }
    permutation_iter_t bottom_begin()  {  return int_bottom_begin;  }
    void set_bottom_begin(permutation_iter_t new_bottom_begin)
    {
        int_bottom_begin = new_bottom_begin;                                    assert(int_marked_nonbottom_begin <= int_bottom_begin);
                                                                                assert(int_bottom_begin <= int_marked_bottom_begin);
                                                                                // assert(int_bottom_begin < int_end);
    }
 
    permutation_const_iter_t bottom_end() const  {  return int_end;  }
    permutation_iter_t bottom_end()  {  return int_end;  }
 
    permutation_const_iter_t unmarked_nonbottom_begin()const{return int_begin;}
    permutation_iter_t unmarked_nonbottom_begin()  {  return int_begin;  }
 
    permutation_const_iter_t unmarked_nonbottom_end() const
    {
        return int_marked_nonbottom_begin;
    }
    permutation_iter_t unmarked_nonbottom_end()
    {
        return int_marked_nonbottom_begin;
    }
    void set_unmarked_nonbottom_end(permutation_iter_t
                                                    new_unmarked_nonbottom_end)
    {
        int_marked_nonbottom_begin = new_unmarked_nonbottom_end;                assert(int_begin <= int_marked_nonbottom_begin);
                                                                                assert(int_marked_nonbottom_begin <= int_bottom_begin);
    }
 
    permutation_const_iter_t marked_nonbottom_begin() const
    {
        return int_marked_nonbottom_begin;
    }
    permutation_iter_t marked_nonbottom_begin()
    {
        return int_marked_nonbottom_begin;
    }
    void set_marked_nonbottom_begin(permutation_iter_t
                                                    new_marked_nonbottom_begin)
    {
        int_marked_nonbottom_begin = new_marked_nonbottom_begin;                assert(int_begin <= int_marked_nonbottom_begin);
                                                                                assert(int_marked_nonbottom_begin <= int_bottom_begin);
    }
 
    permutation_const_iter_t marked_nonbottom_end() const
    {
        return int_bottom_begin;
    }
    permutation_iter_t marked_nonbottom_end()  {  return int_bottom_begin;  }
 
    permutation_const_iter_t unmarked_bottom_begin() const
    {
        return int_bottom_begin;
    }
    permutation_iter_t unmarked_bottom_begin()  {  return int_bottom_begin;  }
 
    permutation_const_iter_t unmarked_bottom_end() const
    {
        return int_marked_bottom_begin;
    }
    permutation_iter_t unmarked_bottom_end()  {return int_marked_bottom_begin;}
    void set_unmarked_bottom_end(permutation_iter_t new_unmarked_bottom_end)
    {
        int_marked_bottom_begin = new_unmarked_bottom_end;                      assert(int_bottom_begin <= int_marked_bottom_begin);
                                                                                assert(int_marked_bottom_begin <= int_end);
    }
 
    permutation_const_iter_t marked_bottom_begin() const
    {
        return int_marked_bottom_begin;
    }
    permutation_iter_t marked_bottom_begin()  {return int_marked_bottom_begin;}
    void set_marked_bottom_begin(permutation_iter_t new_marked_bottom_begin)
    {
        int_marked_bottom_begin = new_marked_bottom_begin;                      assert(int_bottom_begin <= int_marked_bottom_begin);
                                                                                assert(int_marked_bottom_begin <= int_end);
    }
 
    permutation_const_iter_t marked_bottom_end() const  {  return int_end;  }
    permutation_iter_t marked_bottom_end()  {  return int_end;  }
 
    B_to_C_const_iter_t inert_begin() const  {  return int_inert_begin;  }
    B_to_C_iter_t inert_begin()  {  return int_inert_begin;  }
    void set_inert_begin(B_to_C_iter_t new_inert_begin)
    {
        int_inert_begin = new_inert_begin;                                      assert(int_inert_begin <= int_inert_end);
    }
 
    B_to_C_const_iter_t inert_end() const  {  return int_inert_end;  }
    B_to_C_iter_t inert_end()  {  return int_inert_end;  }
    void set_inert_end(B_to_C_iter_t new_inert_end)
    {
        int_inert_end = new_inert_end;                                          assert(int_inert_begin <= int_inert_end);
    }
    void set_inert_begin_and_end(B_to_C_iter_t new_inert_begin,
                                                   B_to_C_iter_t new_inert_end)
    {
        int_inert_begin = new_inert_begin;
        int_inert_end = new_inert_end;                                          assert(int_inert_begin <= int_inert_end);
    }
 
    bool mark_nonbottom(state_info_ptr s)
    {                                                                           assert(s->pos < nonbottom_end());  assert(nonbottom_begin() <= s->pos);
        if (marked_nonbottom_begin() <= s->pos)  return false;
        set_marked_nonbottom_begin(marked_nonbottom_begin() - 1);
        swap_permutation(s->pos, marked_nonbottom_begin());
        return true;
    }
 
    bool mark(state_info_ptr s)
    {                                                                           assert(s->pos < end());
        if (bottom_begin() <= s->pos)
        {
            if (marked_bottom_begin() <= s->pos)  return false;
            set_marked_bottom_begin(marked_bottom_begin() - 1);
            swap_permutation(s->pos, marked_bottom_begin());
            return true;
        }
        return mark_nonbottom(s);
    }
 
    block_t* split_off_blue(permutation_iter_t blue_nonbottom_end);
 
    block_t* split_off_red(permutation_iter_t red_nonbottom_begin);
                                                                                #ifndef NDEBUG
                                                                                    std::string debug_id() const
                                                                                    {
                                                                                        return "block [" + std::to_string(begin() - perm_begin) + "," +
                                                                                            std::to_string(end() - perm_begin) + ")" +
                                                                                            (BLOCK_NO_SEQNR != seqnr() ?" (#"+std::to_string(seqnr())+")" :"");
                                                                                    }
 
                                                                                    static permutation_const_iter_t permutation_begin()  { return perm_begin; }
 
                                                                                    mutable check_complexity::block_counter_t work_counter;
                                                                                  private:
                                                                                    static permutation_const_iter_t perm_begin;
 
                                                                                    friend class part_state_t;
                                                                                #endif
};
 
 
class constln_t
{
  private:
    permutation_iter_t int_end;
 
    permutation_iter_t int_begin;
 
    constln_t* nontrivial_next;
 
    static constln_t* nontrivial_first;
  public:
    B_to_C_iter_t postprocess_begin;
 
    B_to_C_iter_t postprocess_end;
 
    const state_type sort_key;
 
    constln_t(state_type sort_key_, permutation_iter_t begin_,
                       permutation_iter_t end_, B_to_C_iter_t postprocess_none)
      : int_end(end_),
        int_begin(begin_),
        nontrivial_next(nullptr),
        postprocess_begin(postprocess_none),
        postprocess_end(postprocess_none),
        sort_key(sort_key_)
    {                                                                           assert(int_begin<int_end);  assert((state_type)(int_end-int_begin)<=sort_key);
    }
 
    ~constln_t()  {  }
 
    static constln_t* get_some_nontrivial()  {  return nontrivial_first;  }
 
    const constln_t* get_nontrivial_next() const  {  return nontrivial_next;  }
 
    void make_trivial()
    {                                                                           assert(nontrivial_first == this);
        nontrivial_first = nontrivial_next == this ? nullptr : nontrivial_next;
        nontrivial_next = nullptr;
    }
 
    void make_nontrivial()
    {
        if (nullptr == nontrivial_next)
        {
            nontrivial_next = nullptr == nontrivial_first ? this
                                                          : nontrivial_first;
            nontrivial_first = this;
        }
    }
 
    bool is_trivial() const
    {
        return nullptr == nontrivial_next;
    }
 
    permutation_const_iter_t begin() const  {  return int_begin;  }
    permutation_iter_t begin()  {  return int_begin;  }
    void set_begin(permutation_iter_t new_begin)
    {
        int_begin = new_begin;                                                  assert(int_begin < int_end);
    }
 
    permutation_const_iter_t end() const  {  return int_end;  }
    permutation_iter_t end()  {  return int_end;  }
    void set_end(permutation_iter_t new_end)
    {
        int_end = new_end;                                                      assert(int_begin < int_end);
    }
 
    state_type size() const  {  return int_end - int_begin;  }
 
    bool operator<(const constln_t& other) const
    {
        return sort_key < other.sort_key;
    }
    bool operator> (const constln_t& other) const  {  return other < *this;  }
    bool operator<=(const constln_t& other) const  { return !(other < *this); }
    bool operator>=(const constln_t& other) const  { return !(*this < other); }
 
    block_t* split_off_small_block()
    {                                                                           assert(begin() < end());
        block_t* const FirstB = (*begin())->block;
        block_t* const LastB = end()[-1]->block;                                assert(FirstB != LastB);
        if (FirstB->end() == LastB->begin()) { make_trivial(); }                assert(FirstB->constln() == this);  assert(LastB->constln() == this);
                                                                                assert(postprocess_begin == postprocess_end);
        // 2.5: Choose a small splitter block SpB subset of SpC from P,
        //      i.e. |SpB| <= 1/2*|SpC|
        if (FirstB->size() > LastB->size())
        {
            // 2.6: Create a new constellation NewC
            // 2.6: ... and move SpB from SpC to NewC
            constln_t* NewC =
                    new constln_t(sort_key - (LastB->begin() - begin()),
                                       LastB->begin(), end(), postprocess_end);
            set_end(LastB->begin());
            LastB->set_constln(NewC);
            return LastB;
        }
        else
        {
            // 2.6: Create a new constellation NewC
            // 2.6: ... and move SpB from SpC to NewC
            constln_t* NewC =
                    new constln_t(sort_key - (end() - FirstB->end()), begin(),
                                               FirstB->end(), postprocess_end);
            set_begin(FirstB->end());
            FirstB->set_constln(NewC);
            return FirstB;
        }
    }
                                                                                #ifndef NDEBUG
                                                                                    std::string debug_id() const
                                                                                    {
                                                                                        return "constellation [" +
                                                                                                   std::to_string(begin() - block_t::permutation_begin()) +
                                                                                                   "," + std::to_string(end() - block_t::permutation_begin()) +
                                                                                                   ") (#" + std::to_string(sort_key) + ")";
                                                                                    }
                                                                                #endif
};
 
 
template <class LTS_TYPE>
class bisim_partitioner_gjkw_initialise_helper;
 
class part_trans_t;
 
class part_state_t
{
  public:
    permutation_t permutation;
 
  private:
    fixed_vector<state_info_entry> state_info;
 
    template <class LTS_TYPE>
    friend class bisim_partitioner_gjkw_initialise_helper;
  public:
    part_state_t(state_type n)
      : permutation(n),
        state_info(n+1) //< an additional ``state'' is needed to store pointers
            // to the end of the slices of transitions of the last state
    {                                                                           assert(0 == block_t::nr_of_blocks);
                                                                                #ifndef NDEBUG
                                                                                    block_t::perm_begin = permutation.begin();
                                                                                    state_info_entry::s_i_begin = state_info.data();
                                                                                    state_info_entry::s_i_end = state_info_entry::s_i_begin + n;
                                                                                #endif
    }
 
    ~part_state_t()
    {                                                                           assert(state_info.empty());  assert(permutation.empty());
    }
 
    void clear()
    {
        // We have to deallocate constellations first because deallocating
        // blocks makes the constellations inaccessible.
        for (permutation_iter_t permutation_iter = permutation.end();
                                     permutation.begin() != permutation_iter; )
        {
            constln_t* const C = permutation_iter[-1]->constln();               assert(C->end() == permutation_iter);
            // permutation_iter[-1]->block->set_constln(nullptr);               // assert that constellation is trivial:
                                                                                assert(permutation_iter[-1]->block->begin() == C->begin());
            permutation_iter = C->begin();
            delete C;
        }
                                                                                #ifndef NDEBUG
                                                                                    state_type deleted_blocks = 0;
                                                                                #endif
        for (permutation_iter_t permutation_iter = permutation.end();
                                     permutation.begin() != permutation_iter; )
        {
            block_t* const B = permutation_iter[-1]->block;                     assert(B->end() == permutation_iter);
            permutation_iter = B->begin();
                                                                                #ifndef NDEBUG
                                                                                    if (BLOCK_NO_SEQNR != B->seqnr())  ++deleted_blocks;
                                                                                    else                               assert(0 == deleted_blocks);
                                                                                #endif
            delete B;
        }                                                                       assert(deleted_blocks == block_t::nr_of_blocks);
        block_t::nr_of_blocks = 0;
        state_info.clear();
        permutation.clear();
    }
 
    state_type state_size() const  {  return permutation.size();  }
 
    const block_t* block(state_type s) const
    {
        return state_info[s].block;
    }
                                                                                #ifndef NDEBUG
                                                                                  private:
                                                                                    void print_block(const char* message, const block_t* B,
                                                                                        permutation_const_iter_t begin, permutation_const_iter_t end) const;
                                                                                  public:
                                                                                    void print_part(const part_trans_t& part_tr) const;
 
                                                                                    void print_trans() const;
                                                                                #endif
};
 
 
 
 
 
 
/* ************************************************************************* */
/*                                                                           */
/*                           T R A N S I T I O N S                           */
/*                                                                           */
/* ************************************************************************* */
 
 
 
 
 
 
 
/* pred_entry, succ_entry, and B_to_C_entry contain the data that is stored
about a transition.  Every transition has one of each data structure; the three
structures are linked through the iterators (used here as pointers). */
class succ_entry
{
  public:
    B_to_C_iter_t B_to_C;
    state_info_ptr target;
 
  private:
    succ_iter_t int_slice_begin_or_before_end;
  public:
 
    succ_iter_t slice_begin_or_before_end()
    {
        return int_slice_begin_or_before_end;
    }
 
    succ_const_iter_t slice_begin_or_before_end() const
    {
        return int_slice_begin_or_before_end;
    }
 
    void set_slice_begin_or_before_end(succ_iter_t new_value)
    {
        int_slice_begin_or_before_end = new_value;
    }
 
 
    succ_iter_t slice_begin()
    {
        if (this < &*int_slice_begin_or_before_end)
        {                                                                       assert(&*int_slice_begin_or_before_end->int_slice_begin_or_before_end <= this);
            return int_slice_begin_or_before_end->
                                                 int_slice_begin_or_before_end;
        }                                                                       assert(&*int_slice_begin_or_before_end->int_slice_begin_or_before_end == this);
        return int_slice_begin_or_before_end;
    }
 
    succ_const_iter_t slice_begin() const
    {
        if (this < &*int_slice_begin_or_before_end)
        {                                                                       assert(&*int_slice_begin_or_before_end->int_slice_begin_or_before_end <= this);
            return int_slice_begin_or_before_end->
                                                 int_slice_begin_or_before_end;
        }                                                                       assert(&*int_slice_begin_or_before_end->int_slice_begin_or_before_end == this);
        return int_slice_begin_or_before_end;
    }
 
    static succ_iter_t slice_end(succ_iter_t this_)
    {
        if (this_ < this_->int_slice_begin_or_before_end)
        {                                                                       assert(this_->int_slice_begin_or_before_end->
                                                                                                                       int_slice_begin_or_before_end <= this_);
            return this_->int_slice_begin_or_before_end + 1;
        }                                                                       assert(this_->int_slice_begin_or_before_end->
                                                                                                                       int_slice_begin_or_before_end == this_);
        // The following line requires an iterator but a normal method would
        // only have a pointer, not an iterator.  That's why we need to jump
        // through the `static` hoop.
        return this_ + 1;
    }
 
    static succ_const_iter_t slice_end(succ_const_iter_t this_)
    {
        if (this_ < this_->int_slice_begin_or_before_end)
        {                                                                       assert(this_->int_slice_begin_or_before_end->
                                                                                                                       int_slice_begin_or_before_end <= this_);
            return this_->int_slice_begin_or_before_end + 1;
        }                                                                       assert(this_->int_slice_begin_or_before_end->
                                                                                                                       int_slice_begin_or_before_end == this_);
        // The following line requires an iterator but a normal method would
        // only have a pointer, not an iterator.  That's why we need to jump
        // through the `static` hoop.
        return this_ + 1;
    }
                                                                                #ifndef NDEBUG
                                                                                    static void slice_add_work_to_transns(succ_const_iter_t this_,
                                                                                                  enum check_complexity::counter_type ctr, unsigned max_value);
                                                                                #endif
};
 
 
class pred_entry
{
  public:
    succ_iter_t succ;
    state_info_ptr source;
                                                                                #ifndef NDEBUG
                                                                                    std::string debug_id_short() const
                                                                                    {
                                                                                        return "from " + source->debug_id_short() + " to " +
                                                                                                                                succ->target->debug_id_short();
                                                                                    }
 
                                                                                    std::string debug_id() const
                                                                                    {
                                                                                        return "transition " + debug_id_short();
                                                                                    }
 
                                                                                    mutable check_complexity::trans_counter_t work_counter;
                                                                                #endif
};
 
 
class B_to_C_entry
{
  public:
    pred_iter_t pred;
    B_to_C_desc_iter_t B_to_C_slice;
};
                                                                                #ifndef NDEBUG
                                                                                    inline void succ_entry::slice_add_work_to_transns(succ_const_iter_t this_,
                                                                                                   enum check_complexity::counter_type ctr, unsigned max_value)
                                                                                    {
                                                                                        succ_const_iter_t iter = this_->slice_begin();
                                                                                        succ_const_iter_t end = slice_end(this_);
                                                                                        assert(iter < end);
                                                                                        mCRL2complexity(iter->B_to_C->pred, add_work(ctr, max_value), );
                                                                                        while (++iter != end)
                                                                                        {
                                                                                            // treat temporary counters specially
                                                                                            mCRL2complexity(iter->B_to_C->pred,
                                                                                                                       add_work_notemporary(ctr, max_value), );
                                                                                        }
                                                                                    }
                                                                                #endif
/* B_to_C_descriptor is a data type that indicates which slice of states
belongs together. */
class B_to_C_descriptor
{
  public:
    B_to_C_iter_t end, begin;
 
    B_to_C_descriptor(B_to_C_iter_t begin_, B_to_C_iter_t end_)
      : end(end_),
        begin(begin_)
    {  }
 
    const block_t* from_block() const
    {                                                                           assert(begin < end);  assert(begin->pred->succ->B_to_C == begin);
        return begin->pred->source->block;
    }
    block_t* from_block()
    {                                                                           assert(begin < end);  assert(begin->pred->succ->B_to_C == begin);
        return begin->pred->source->block;
    }
 
    const constln_t* to_constln() const
    {                                                                           assert(begin < end);  assert(begin->pred->succ->B_to_C == begin);
        return begin->pred->succ->target->constln();
    }
    constln_t* to_constln()
    {                                                                           assert(begin < end);  assert(begin->pred->succ->B_to_C == begin);
        return begin->pred->succ->target->constln();
    }
 
    bool needs_postprocessing() const
    {                                                                           assert(to_constln()->postprocess_end <= begin ||
                                                                                                                         end <= to_constln()->postprocess_end);
                                                                                assert(to_constln()->postprocess_begin <= begin ||
                                                                                                                       end <= to_constln()->postprocess_begin);
        return to_constln()->postprocess_begin <= begin &&
                                          end <= to_constln()->postprocess_end;
    }
                                                                                #ifndef NDEBUG
                                                                                    std::string debug_id() const
                                                                                    {
                                                                                        assert(begin < end);
                                                                                        std::string result("slice containing transition");
                                                                                        if (end - begin > 1)
                                                                                            result += "s ";
                                                                                        else
                                                                                            result += " ";
                                                                                        B_to_C_const_iter_t iter = begin;
                                                                                        assert(iter->pred->succ->B_to_C == iter);
                                                                                        result += iter->pred->debug_id_short();
                                                                                        if (end - iter > 4)
                                                                                        {
                                                                                            assert(iter[1].pred->succ->B_to_C == iter+1);
                                                                                            result += ", ";
                                                                                            result += iter[1].pred->debug_id_short();
                                                                                            result += ", ...";
                                                                                            iter = end - 3;
                                                                                        }
                                                                                        while (++iter != end)
                                                                                        {
                                                                                            assert(iter->pred->succ->B_to_C == iter);
                                                                                            result += ", ";
                                                                                            result += iter->pred->debug_id_short();
                                                                                        }
                                                                                        return result;
                                                                                    }
 
                                                                                    bool add_work_to_bottom_transns(enum check_complexity::counter_type ctr,
                                                                                                                                            unsigned max_value)
                                                                                    {
                                                                                        bool added = false;
 
                                                                                        for (B_to_C_const_iter_t iter = begin; iter != end; ++iter)
                                                                                        {
                                                                                            if (iter->pred->source->pos >=
                                                                                                                     iter->pred->source->block->bottom_begin())
                                                                                            {
                                                                                                // source state of the transition is a bottom state
                                                                                                mCRL2complexity(iter->pred, add_work(ctr, max_value), );
                                                                                                added = true;
                                                                                            }
                                                                                        }
                                                                                        return added;
                                                                                    }
 
                                                                                    mutable check_complexity::B_to_C_counter_t work_counter;
                                                                                #endif
};
 
 
/* part_trans_t collects and organises all data for the transitions. */
class part_trans_t
{
  private:
    fixed_vector<pred_entry> pred;
    fixed_vector<succ_entry> succ;
    fixed_vector<B_to_C_entry> B_to_C;
 
    template <class LTS_TYPE>
    friend class bisim_partitioner_gjkw_initialise_helper;
 
    void swap_in(B_to_C_iter_t const pos1, B_to_C_iter_t const pos2)
    {                                                                           assert(B_to_C.end() > pos1);  assert(pos1->pred->succ->B_to_C == pos1);
                                                                                assert(B_to_C.end() > pos2);  assert(pos2->pred->succ->B_to_C == pos2);
        // swap contents
        pred_entry const temp_entry(*pos1->pred);
        *pos1->pred = *pos2->pred;
        *pos2->pred = temp_entry;
        // swap pointers to contents
        pred_iter_t const temp_iter(pos1->pred);
        pos1->pred = pos2->pred;
        pos2->pred = temp_iter;                                                 assert(B_to_C.end() > pos1);  assert(pos1->pred->succ->B_to_C == pos1);
                                                                                assert(B_to_C.end() > pos2);  assert(pos2->pred->succ->B_to_C == pos2);
    }
 
    void swap_out(pred_iter_t const pos1, pred_iter_t const pos2)
    {                                                                           assert(pred.end() > pos1);  assert(pos1->succ->B_to_C->pred == pos1);
                                                                                assert(pred.end() > pos2);  assert(pos2->succ->B_to_C->pred == pos2);
                                                                                assert(pos1->succ->slice_begin() == pos2->succ->slice_begin());
                                                                                assert(succ_entry::slice_end(pos1->succ) == succ_entry::slice_end(pos2->succ));
        // swap contents, but do not swap slice_begin_or_before_end
        B_to_C_iter_t const temp_B_to_C(pos1->succ->B_to_C);
        state_info_ptr const temp_target(pos1->succ->target);
        pos1->succ->B_to_C = pos2->succ->B_to_C;
        pos1->succ->target = pos2->succ->target;
        pos2->succ->B_to_C = temp_B_to_C;
        pos2->succ->target = temp_target;
        // swap pointers to contents
        succ_iter_t const temp_iter(pos1->succ);
        pos1->succ = pos2->succ;
        pos2->succ = temp_iter;                                                 assert(pred.end() > pos1);  assert(pos1->succ->B_to_C->pred == pos1);
                                                                                assert(pred.end() > pos2);  assert(pos2->succ->B_to_C->pred == pos2);
                                                                                assert(pos1->succ->slice_begin() == pos2->succ->slice_begin());
                                                                                assert(succ_entry::slice_end(pos1->succ) == succ_entry::slice_end(pos2->succ));
    }
 
    void swap_B_to_C(succ_iter_t const pos1, succ_iter_t const pos2)
    {                                                                           assert(succ.end() > pos1);  assert(pos1->B_to_C->pred->succ == pos1);
                                                                                assert(succ.end() > pos2);  assert(pos2->B_to_C->pred->succ == pos2);
        // swap contents
        B_to_C_entry const temp_entry(*pos1->B_to_C);
        *pos1->B_to_C = *pos2->B_to_C;
        *pos2->B_to_C = temp_entry;
        // swap pointers to contents
        B_to_C_iter_t const temp_iter(pos1->B_to_C);
        pos1->B_to_C = pos2->B_to_C;
        pos2->B_to_C = temp_iter;                                               assert(succ.end() > pos1);  assert(pos1->B_to_C->pred->succ == pos1);
                                                                                assert(succ.end() > pos2);  assert(pos2->B_to_C->pred->succ == pos2);
    }
 
    // *pos1 -> *pos2 -> *pos3 -> *pos1
    void swap3_B_to_C(succ_iter_t const pos1, succ_iter_t const pos2,
                                                        succ_iter_t const pos3)
    {                                                                           assert(succ.end() > pos1);  assert(pos1->B_to_C->pred->succ == pos1);
                                                                                assert(succ.end() > pos2);  assert(pos2->B_to_C->pred->succ == pos2);
                                                                                assert(succ.end() > pos3);  assert(pos3->B_to_C->pred->succ == pos3);
                                                                                assert(pos1 != pos2 || pos1 == pos3);
        // swap contents
        B_to_C_entry const temp_entry(*pos1->B_to_C);
        *pos1->B_to_C = *pos3->B_to_C;
        *pos3->B_to_C = *pos2->B_to_C;
        *pos2->B_to_C = temp_entry;
        // swap pointers to contents
        B_to_C_iter_t const temp_iter(pos2->B_to_C);
        pos2->B_to_C = pos3->B_to_C;
        pos3->B_to_C = pos1->B_to_C;
        pos1->B_to_C = temp_iter;                                               assert(succ.end() > pos1);  assert(pos1->B_to_C->pred->succ == pos1);
                                                                                assert(succ.end() > pos2);  assert(pos2->B_to_C->pred->succ == pos2);
                                                                                assert(succ.end() > pos3);  assert(pos3->B_to_C->pred->succ == pos3);
    }
  public:
    part_trans_t(trans_type m)
      : pred(m),
        succ(m),
        B_to_C(m)
    {  }
    ~part_trans_t()
    {                                                                           assert(B_to_C.empty());  assert(succ.empty());  assert(pred.empty());
    }
 
    void clear()
    {
        // B_to_C_descriptors are deallocated when their respective lists are
        // deallocated by destructing the blocks.
        B_to_C.clear();
        succ.clear();
        pred.clear();
    }
 
    trans_type trans_size() const  {  return pred.size();  }
 
    /* split_inert_to_C splits the B_to_C slice of block b to its own
    constellation into two slices: one for the inert and one for the non-inert
    transitions.  It is called with SpB just after a constellation is split, as
    the transitions from SpB to itself (= the inert transitions) now go to a
    different constellation than the other transitions from SpB to its old
    constellation.  It does, however, not adapt the other transition arrays to
    reflect that noninert and inert transitions from block b would go to
    different constellations.
    Its time complexity is O(1+min {|out_noninert(b-->C)|, |out_inert(b)|}). */
    void split_inert_to_C(block_t* B);
 
    /* part_trans_t::change_to_C has to be called after a transition target has
    changed its constellation.  The member function will adapt the transition
    data structure.  It assumes that the transition is non-inert and that the
    new constellation does not (yet) have inert incoming transitions.  It
    returns the boundary between transitions to OldC and transitions to NewC in
    the state's outgoing transition array. */
    succ_iter_t change_to_C(pred_iter_t pred_iter,                              ONLY_IF_DEBUG( constln_t* SpC, constln_t* NewC, )
               bool first_transition_of_state, bool first_transition_of_block);
 
    /* split_s_inert_out splits the outgoing transitions from s to its own
    constellation into two:  the inert transitions become transitions to the
    new constellation of which s is now part;  the non-inert transitions remain
    transitions to OldC.  It returns the boundary between transitions to
    OldC and transitions to NewC in the outgoing transition array of s.
    Its time complexity is O(1 + min { |out_\nottau(s)|, |out_\tau(s)| }). */
    bool split_s_inert_out(state_info_ptr s                                     ONLY_IF_DEBUG(, constln_t* OldC)
                                           );
 
    /* part_trans_t::make_noninert makes the transition identified by succ_iter
    noninert. */
    void make_noninert(succ_iter_t const succ_iter)
    {
        // change B_to_C
        B_to_C_iter_t const other_B_to_C =
                    succ_iter->B_to_C->pred->source->block->inert_begin();      assert(succ_iter->B_to_C->B_to_C_slice->begin <= other_B_to_C);
                                                                                assert(other_B_to_C <= succ_iter->B_to_C);
                                                                                assert(succ_iter->B_to_C < succ_iter->B_to_C->B_to_C_slice->end);
        swap_B_to_C(succ_iter, other_B_to_C->pred->succ);
        succ_iter->B_to_C->pred->source->block->set_inert_begin(other_B_to_C +
                                                                            1);
        // change pred
        pred_iter_t const other_pred = succ_iter->target->inert_pred_begin();   assert(succ_iter->target->pred_begin() <= other_pred);
                                                                                assert(other_pred <= succ_iter->B_to_C->pred);
                                                                                assert(succ_iter->B_to_C->pred < succ_iter->target->pred_end());
        swap_in(succ_iter->B_to_C, other_pred->succ->B_to_C);
        succ_iter->target->set_inert_pred_begin(other_pred + 1);
        // change succ
        succ_iter_t const other_succ =
                           succ_iter->B_to_C->pred->source->inert_succ_begin(); assert(succ_iter->B_to_C->pred->source->succ_begin() <= other_succ);
                                                                                assert(other_succ <= succ_iter);
                                                                                assert(succ_iter < succ_iter->B_to_C->pred->source->succ_end());
        swap_out(succ_iter->B_to_C->pred, other_succ->B_to_C->pred);
        succ_iter->B_to_C->pred->source->set_inert_succ_begin(other_succ + 1);
    }
 
    /* part_trans_t::new_block_created splits the B_to_C-slices to reflect that
    some transitions now start in the new block NewB.  They can no longer be in
    the same slice as the transitions that start in the old block.
    
    We need separate functions for blue and red blocks because the B_to_C-slice
    of the red block should come after the B_to_C-slice of the blue block,
    at least while postprocessing.
 
    Its time complexity is O(1 + |out(NewB)|). */
    void new_blue_block_created(block_t* OldB, block_t* NewB);
    void new_red_block_created(block_t*OldB,block_t*NewB, bool postprocessing);
 
    B_to_C_const_iter_t B_to_C_begin() const  {  return B_to_C.begin();  }
    B_to_C_iter_t       B_to_C_end  ()        {  return B_to_C.end  ();  }
    pred_const_iter_t pred_end() const  {  return pred.end();  }
    succ_const_iter_t succ_end() const  {  return succ.end();  }
                                                                                #ifndef NDEBUG
                                                                                    void assert_stability(const part_state_t& part_st) const;
                                                                                #endif
};
 
 
 
 
 
 
 
/* ************************************************************************* */
/*                                                                           */
/*                            A L G O R I T H M S                            */
/*                                                                           */
/* ************************************************************************* */
 
 
 
 
 
 
 
 
/*=============================================================================
=                create initial partition and data structures                 =
=============================================================================*/
 
 
 
template<class LTS_TYPE>
class bisim_partitioner_gjkw_initialise_helper
{
  private:
    LTS_TYPE& aut;
    state_type nr_of_states;
    const state_type orig_nr_of_states;
    trans_type nr_of_transitions;
 
    // key and hash function for (action, target state) pair. Required since
    // unordered_map does not directly allow to use pair keys
    class Key 
    {
      public:
        label_type first;
        state_type second;
 
        Key(const label_type& f, const state_type& s)
          : first(f),
            second(s)
        {} 
 
        bool operator==(const Key &other) const 
        {
            return first == other.first && second == other.second;
        }
    };
 
    class KeyHasher 
    {
      public:
        std::size_t operator()(const Key& k) const
        {
            return std::hash<label_type>()(k.first) ^
                                      (std::hash<state_type>()(k.second) << 1);
        }
    };
    // Map used to convert LTS to Kripke structure
    // (also used when converting Kripke structure back to LTS)
    std::unordered_map<Key, state_type, KeyHasher> extra_kripke_states;
 
    // temporary map to keep track of blocks. maps transition labels (different
    // from tau) to blocks
    std::unordered_map<label_type, state_type> action_block_map;
 
    std::vector<state_type> noninert_out_per_state, inert_out_per_state;
    std::vector<state_type> noninert_in_per_state, inert_in_per_state;
    std::vector<state_type> noninert_out_per_block, inert_out_per_block;
    std::vector<state_type> states_per_block;
    state_type nr_of_nonbottom_states;
  public:
    bisim_partitioner_gjkw_initialise_helper(LTS_TYPE& l, bool branching,
                                                     bool preserve_divergence);
 
    void init_transitions(part_state_t& part_st, part_trans_t& part_tr,
                                     bool branching, bool preserve_divergence);
 
    // replace_transition_system() replaces the transitions of the LTS stored here by
    // those of its bisimulation quotient.  However, it does not change
    // anything else; in particular, it does not change the number of states of
    // the LTS.
    void replace_transition_system(const part_state_t& part_st,                 ONLY_IF_DEBUG( bool branching, )
                                   bool preserve_divergence);
 
    state_type get_nr_of_states() const  {  return nr_of_states;  }
 
    trans_type get_nr_of_transitions() const  {  return nr_of_transitions;  }
};
 
 
 
/*=============================================================================
=                                 main class                                  =
=============================================================================*/
 
 
 
struct refine_shared_t;
 
} // end namespace bisim_gjkw
 
template <class LTS_TYPE>
class bisim_partitioner_gjkw
{
  private:
    bisim_gjkw::bisim_partitioner_gjkw_initialise_helper<LTS_TYPE> init_helper;
    bisim_gjkw::part_state_t part_st;
    bisim_gjkw::part_trans_t part_tr;
  public:
    // The constructor constructs the data structures and immediately
    // calculates the bisimulation quotient.  However, it does not change the
    // LTS.
    bisim_partitioner_gjkw(LTS_TYPE& l, bool branching = false,
                                        bool preserve_divergence = false)
      : init_helper(l, branching, preserve_divergence),
        part_st(init_helper.get_nr_of_states()),
        part_tr(init_helper.get_nr_of_transitions())
    {                                                                           assert(branching || !preserve_divergence);
        create_initial_partition_gjkw(branching, preserve_divergence);
        refine_partition_until_it_becomes_stable_gjkw();
    }
    ~bisim_partitioner_gjkw()
    {
        part_tr.clear();
        part_st.clear();
    }
 
    // replace_transition_system() replaces the transitions of the LTS stored here by
    // those of its bisimulation quotient.  However, it does not change
    // anything else; in particular, it does not change the number of states of
    // the LTS.
    void replace_transition_system(bool branching, bool preserve_divergence)
    {
        (void) branching; // avoid warning about unused parameter.
        init_helper.replace_transition_system(part_st,                          ONLY_IF_DEBUG( branching, )
                                                       preserve_divergence);
    }
 
    static state_type num_eq_classes()
    {
        return bisim_gjkw::block_t::nr_of_blocks;
    }
 
    state_type get_eq_class(state_type s) const
    {
        return part_st.block(s)->seqnr();
    }
 
    bool in_same_class(state_type s, state_type t) const
    {
        return part_st.block(s) == part_st.block(t);
    }
 
  private:
 
    /*-------- dbStutteringEquivalence -- Algorithm 2 of [GJKW 2017] --------*/
 
    void create_initial_partition_gjkw(bool branching,
                                                     bool preserve_divergence);
    void refine_partition_until_it_becomes_stable_gjkw();
 
    /*----------------- Refine -- Algorithm 3 of [GJKW 2017] ----------------*/
 
    bisim_gjkw::block_t* refine(bisim_gjkw::block_t* RfnB,
              const bisim_gjkw::constln_t* SpC,
              const bisim_gjkw::B_to_C_descriptor* FromRed,
              bool postprocessing                                               ONLY_IF_DEBUG( , const bisim_gjkw::constln_t* NewC = nullptr )
                                 );
 
    /*--------- PostprocessNewBottom -- Algorithm 4 of [GJKW 2017] ----------*/
 
    bisim_gjkw::block_t* postprocess_new_bottom(bisim_gjkw::block_t* RedB);
};
 
 
 
 
 
 
/* ************************************************************************* */
/*                                                                           */
/*                             I N T E R F A C E                             */
/*                                                                           */
/* ************************************************************************* */
 
 
 
 
 
 
template <class LTS_TYPE>
void bisimulation_reduce_gjkw(LTS_TYPE& l, bool branching = false,
                                            bool preserve_divergence = false);
 
template <class LTS_TYPE>
bool destructive_bisimulation_compare_gjkw(LTS_TYPE& l1, LTS_TYPE& l2,
                    bool branching = false, bool preserve_divergence = false,
                                    bool generate_counter_examples = false);
 
template <class LTS_TYPE>
bool bisimulation_compare_gjkw(const LTS_TYPE& l1, const LTS_TYPE& l2,
                    bool branching = false, bool preserve_divergence = false);
 
template <class LTS_TYPE>
void bisimulation_reduce_gjkw(LTS_TYPE& l, bool const branching /* = false */,
                                  bool const preserve_divergence /* = false */)
{
  // First, remove tau loops in case of branching bisimulation.
  if (branching)
  {
    scc_reduce(l, preserve_divergence);
  }
 
  // Second, apply the branching bisimulation reduction algorithm. If there are
  // no taus, this will automatically yield strong bisimulation.
  detail::bisim_partitioner_gjkw<LTS_TYPE> bisim_part(l, branching,
                                                          preserve_divergence);
 
  // Assign the reduced LTS
  bisim_part.replace_transition_system(branching, preserve_divergence);
}
 
template <class LTS_TYPE>
inline bool bisimulation_compare_gjkw(const LTS_TYPE& l1, const LTS_TYPE& l2,
          bool branching /* = false */, bool preserve_divergence /* = false */)
{
  LTS_TYPE l1_copy(l1);
  LTS_TYPE l2_copy(l2);
  return destructive_bisimulation_compare_gjkw(l1_copy, l2_copy, branching,
                                                          preserve_divergence);
}
 
template <class LTS_TYPE>
bool destructive_bisimulation_compare_gjkw(LTS_TYPE& l1, LTS_TYPE& l2,
          bool branching /* = false */, bool preserve_divergence /* = false */,
                                           bool generate_counter_examples /* = false */,
                                           const std::string& /*counter_example_file = "" */,
                                           bool /*structured_output = false */)
{
  if (generate_counter_examples)
  {
    mCRL2log(log::warning) << "The GJKW branching bisimulation algorithm does "
                                            "not generate counterexamples.\n";
  }
  state_type init_l2 = l2.initial_state() + l1.num_states();
  mcrl2::lts::detail::merge(l1, l2);
  l2.clear(); // No use for l2 anymore.
 
  // First remove tau loops in case of branching bisimulation.
  if (branching)
  {
    detail::scc_partitioner<LTS_TYPE> scc_part(l1);
    scc_part.replace_transition_system(preserve_divergence);
    init_l2 = scc_part.get_eq_class(init_l2);
  }
 
  detail::bisim_partitioner_gjkw<LTS_TYPE> bisim_part(l1, branching,
                                                          preserve_divergence);
  return bisim_part.in_same_class(l1.initial_state(), init_l2);
}
 
 
 
 
 
 
/* ************************************************************************* */
/*                                                                           */
/*                       I M P L E M E N T A T I O N S                       */
/*                                                                           */
/* ************************************************************************* */
 
 
 
 
 
// This section contains implementations of functions that refer to details of
// classes defined later, so they could not be defined at the point of
// declaration.
 
namespace bisim_gjkw
{
 
inline const constln_t* state_info_entry::constln() const
{
    return block->constln();
}
 
inline constln_t* state_info_entry::constln()
{
    return block->constln();
}
 
inline B_to_C_descriptor* block_t::FromRed(const constln_t* const SpC)
{
    if (!to_constln.empty() && to_constln.front().to_constln() == SpC)
    {
        return &*to_constln.begin();
    }
    else
    {
                                                                                #ifndef NDEBUG
                                                                                    for (B_to_C_desc_const_iter_t iter = to_constln.begin();
                                                                                                                              to_constln.end() != iter; ++iter)
                                                                                    {
                                                                                        assert(iter->from_block() == this);
                                                                                        assert(iter->to_constln() != SpC);
                                                                                    }
                                                                                #endif
        return nullptr;
    }
}
 
 
inline void block_t::SetFromRed(B_to_C_desc_iter_t const new_fromred)
{                                                                               assert(!to_constln.empty());
    if (to_constln.begin() != new_fromred)
    {
        to_constln.splice(to_constln.begin(), to_constln, new_fromred);
    }                                                                           assert(new_fromred->from_block() == this);
}
 
 
inline bool state_info_entry::surely_has_transition_to(const constln_t* const
                                                                     SpC) const
{                                                                               assert(succ_begin()<=current_constln()); assert(current_constln()<=succ_end());
                                                                                assert(succ_begin() == current_constln() || succ_end() == current_constln() ||
                                                                                        *current_constln()[-1].target->constln() <
                                                                                                                        *current_constln()->target->constln());
                                                                                assert(constln() != SpC);
    // either current_constln()->target or current_constln()[-1].target is in
    // SpC
    if (current_constln() != succ_end() &&
                                   current_constln()->target->constln() == SpC)
    {
        return true;
    }
    return false;
}
 
 
inline bool state_info_entry::surely_has_no_transition_to(
                                              const constln_t* const SpC) const
{                                                                               assert(succ_begin()<=current_constln()); assert(current_constln()<=succ_end());
                                                                                assert(succ_begin() == current_constln() || succ_end() == current_constln() ||
                                                                                        *current_constln()[-1].target->constln() <
                                                                                                                        *current_constln()->target->constln());
                                                                                assert(constln() != SpC);
    // condition:
    // current_constln()->target is in a constellation > SpC and
    // current_constln()[-1].target is in a constellation < SpC.
    if (current_constln() != succ_end() &&
                                 *current_constln()->target->constln() <= *SpC)
    {
        return false;
    }
    if (current_constln() != succ_begin() &&
                              *SpC <= *current_constln()[-1].target->constln())
    {
        return false;
    }
    return true;
}
 
 
} // end namespace bisim_gjkw
} // end namespace detail
} // end namespace lts
} // end namespace mcrl2
 
#endif // ifndef _LIBLTS_BISIM_GJKW_H