graph.hh

// -*- coding: utf-8 -*-
// Copyright (C) by the Spot authors, see the AUTHORS file for details.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
#pragma once
 
#include <spot/misc/common.hh>
#include <spot/misc/_config.h>
#include <spot/misc/permute.hh>
#include <vector>
#include <type_traits>
#include <tuple>
#include <cassert>
#include <iterator>
#include <algorithm>
#include <map>
#include <iostream>
#ifdef SPOT_ENABLE_PTHREAD
#  include <thread>
#endif // SPOT_ENABLE_PTHREAD
 
 
namespace spot
{
  template <typename State_Data, typename Edge_Data>
  class SPOT_API digraph;
 
  namespace internal
  {
#ifndef SWIG
    template <typename Of, typename ...Args>
    struct first_is_base_of
    {
      static const bool value = false;
    };
 
    template <typename Of, typename Arg1, typename ...Args>
    struct first_is_base_of<Of, Arg1, Args...>
    {
      static const bool value =
        std::is_base_of<Of, typename std::decay<Arg1>::type>::value;
    };
#endif
 
    // The boxed_label class stores Data as an attribute called
    // "label" if boxed is true.  It is an empty class if Data is
    // void, and it simply inherits from Data if boxed is false.
    //
    // The data() method offers an homogeneous access to the Data
    // instance.
    template <typename Data, bool boxed = !std::is_class<Data>::value>
    struct SPOT_API boxed_label
    {
      typedef Data data_t;
      Data label;
 
#ifndef SWIG
      template <typename... Args,
                typename = typename std::enable_if<
                  !first_is_base_of<boxed_label, Args...>::value>::type>
        boxed_label(Args&&... args)
        noexcept(std::is_nothrow_constructible<Data, Args...>::value)
        : label{std::forward<Args>(args)...}
      {
      }
#endif
 
      // if Data is a POD type, G++ 4.8.2 wants default values for all
      // label fields unless we define this default constructor here.
      explicit boxed_label()
        noexcept(std::is_nothrow_constructible<Data>::value)
      {
      }
 
      Data& data()
      {
        return label;
      }
 
      const Data& data() const
      {
        return label;
      }
 
      bool operator<(const boxed_label& other) const
      {
        return label < other.label;
      }
    };
 
    template <>
    struct SPOT_API boxed_label<void, true>: public std::tuple<>
    {
      typedef std::tuple<> data_t;
      std::tuple<>& data()
      {
        return *this;
      }
 
      const std::tuple<>& data() const
      {
        return *this;
      }
 
    };
 
    template <typename Data>
    struct SPOT_API boxed_label<Data, false>: public Data
    {
      typedef Data data_t;
 
#ifndef SWIG
      template <typename... Args,
                typename = typename std::enable_if<
                  !first_is_base_of<boxed_label, Args...>::value>::type>
        boxed_label(Args&&... args)
        noexcept(std::is_nothrow_constructible<Data, Args...>::value)
        : Data{std::forward<Args>(args)...}
      {
      }
#endif
 
      // if Data is a POD type, G++ 4.8.2 wants default values for all
      // label fields unless we define this default constructor here.
      explicit boxed_label()
        noexcept(std::is_nothrow_constructible<Data>::value)
      {
      }
 
      Data& data()
      {
        return *this;
      }
 
      const Data& data() const
      {
        return *this;
      }
    };
 
    // State storage for digraphs
 
    // We have two implementations, one with attached State_Data, and
    // one without.
 
    template <typename Edge, typename State_Data>
    struct SPOT_API distate_storage final: public State_Data
    {
      Edge succ = 0; // First outgoing edge (used when iterating)
      Edge succ_tail = 0;        // Last outgoing edge (used for
                                // appending new edges)
#ifndef SWIG
      template <typename... Args,
                typename = typename std::enable_if<
                  !first_is_base_of<distate_storage, Args...>::value>::type>
      distate_storage(Args&&... args)
        noexcept(std::is_nothrow_constructible<State_Data, Args...>::value)
        : State_Data{std::forward<Args>(args)...}
      {
      }
#endif
    };
 
    // Edge storage
 
    // Again two implementation: one with label, and one without.
 
    template <typename StateIn,
              typename StateOut, typename Edge, typename Edge_Data>
    struct SPOT_API edge_storage final: public Edge_Data
    {
      typedef Edge edge;
 
      StateOut dst;                // destination
      Edge next_succ;        // next outgoing edge with same
                                // source, or 0
      StateIn src;                // source
 
      explicit edge_storage()
        noexcept(std::is_nothrow_constructible<Edge_Data>::value)
        : Edge_Data{}
      {
      }
 
#ifndef SWIG
      template <typename... Args>
      edge_storage(StateOut dst, Edge next_succ,
                    StateIn src, Args&&... args)
        noexcept(std::is_nothrow_constructible<Edge_Data, Args...>::value
                 && std::is_nothrow_constructible<StateOut, StateOut>::value
                 && std::is_nothrow_constructible<Edge, Edge>::value)
        : Edge_Data{std::forward<Args>(args)...},
        dst(dst), next_succ(next_succ), src(src)
      {
      }
#endif
 
      bool operator<(const edge_storage& other) const
      {
        if (src < other.src)
          return true;
        if (src > other.src)
          return false;
        // This might be costly if the destination is a vector
        if (dst < other.dst)
          return true;
        if (dst > other.dst)
          return false;
        return this->data() < other.data();
      }
 
      bool operator==(const edge_storage& other) const
      {
        return src == other.src &&
          dst == other.dst &&
          this->data() == other.data();
      }
    };
 
    // Edge iterator
 
    // This holds a graph and a edge number that is the start of
    // a list, and it iterates over all the edge_storage_t elements
    // of that list.
 
    template <typename Graph>
    class SPOT_API edge_iterator
    {
    public:
      typedef typename std::conditional<std::is_const<Graph>::value,
                                        const typename Graph::edge_storage_t,
                                        typename Graph::edge_storage_t>::type
        value_type;
      typedef value_type& reference;
      typedef value_type* pointer;
      typedef std::ptrdiff_t difference_type;
      typedef std::forward_iterator_tag iterator_category;
 
      typedef typename Graph::edge edge;
 
      edge_iterator() noexcept
        : g_(nullptr), t_(0)
      {
      }
 
      edge_iterator(Graph* g, edge t) noexcept
        : g_(g), t_(t)
      {
      }
 
      bool operator==(edge_iterator o) const
      {
        return t_ == o.t_;
      }
 
      bool operator!=(edge_iterator o) const
      {
        return t_ != o.t_;
      }
 
      reference operator*() const
      {
        return g_->edge_storage(t_);
      }
 
      pointer      operator->() const
      {
        return &g_->edge_storage(t_);
      }
 
      edge_iterator operator++()
      {
        t_ = operator*().next_succ;
        return *this;
      }
 
      edge_iterator operator++(int)
      {
        edge_iterator ti = *this;
        t_ = operator*().next_succ;
        return ti;
      }
 
      operator bool() const
      {
        return t_;
      }
 
      edge trans() const
      {
        return t_;
      }
 
    protected:
      Graph* g_;
      edge t_;
    };
 
    template <typename Graph>
    class SPOT_API killer_edge_iterator: public edge_iterator<Graph>
    {
      typedef edge_iterator<Graph> super;
    public:
      typedef typename Graph::state_storage_t state_storage_t;
      typedef typename Graph::edge edge;
 
      killer_edge_iterator(Graph* g, edge t, state_storage_t& src) noexcept
        : super(g, t), src_(src), prev_(0)
      {
      }
 
      killer_edge_iterator operator++()
      {
        prev_ = this->t_;
        this->t_ = this->operator*().next_succ;
        return *this;
      }
 
      killer_edge_iterator operator++(int)
      {
        killer_edge_iterator ti = *this;
        ++*this;
        return ti;
      }
 
      // Erase the current edge and advance the iterator.
      void erase()
      {
        edge next = this->operator*().next_succ;
 
        // Update source state and previous edges
        if (prev_)
          {
            this->g_->edge_storage(prev_).next_succ = next;
          }
        else
          {
            if (src_.succ == this->t_)
              src_.succ = next;
          }
        if (src_.succ_tail == this->t_)
          {
            src_.succ_tail = prev_;
            SPOT_ASSERT(next == 0);
          }
 
        // Erased edges have themselves as next_succ.
        this->operator*().next_succ = this->t_;
 
        // Advance iterator to next edge.
        this->t_ = next;
 
        ++this->g_->killed_edge_;
      }
 
    protected:
      state_storage_t& src_;
      edge prev_;
    };
 
 
    // State OUT
 
    // Fake container listing the outgoing edges of a state.
 
    template <typename Graph>
    class SPOT_API state_out
    {
    public:
      typedef typename Graph::edge edge;
      state_out(Graph* g, edge t) noexcept
        : g_(g), t_(t)
      {
      }
 
      edge_iterator<Graph> begin() const
      {
        return {g_, t_};
      }
 
      edge_iterator<Graph> end() const
      {
        return {};
      }
 
      void recycle(edge t)
      {
        t_ = t;
      }
 
    protected:
      Graph* g_;
      edge t_;
    };
 
    // all_trans
 
    template <typename Graph>
    class SPOT_API all_edge_iterator
    {
    public:
      typedef typename std::conditional<std::is_const<Graph>::value,
                                        const typename Graph::edge_storage_t,
                                        typename Graph::edge_storage_t>::type
        value_type;
      typedef value_type& reference;
      typedef value_type* pointer;
      typedef std::ptrdiff_t difference_type;
      typedef std::forward_iterator_tag iterator_category;
 
    protected:
      typedef typename std::conditional<std::is_const<Graph>::value,
                                        const typename Graph::edge_vector_t,
                                        typename Graph::edge_vector_t>::type
        tv_t;
 
      unsigned t_;
      tv_t& tv_;
 
      void skip_()
      {
        unsigned s = tv_.size();
        do
          ++t_;
        while (t_ < s && tv_[t_].next_succ == t_);
      }
 
    public:
      all_edge_iterator(unsigned pos, tv_t& tv) noexcept
        : t_(pos), tv_(tv)
      {
        skip_();
      }
 
      all_edge_iterator(tv_t& tv) noexcept
        : t_(tv.size()), tv_(tv)
      {
      }
 
      all_edge_iterator& operator++()
      {
        skip_();
        return *this;
      }
 
      all_edge_iterator operator++(int)
      {
        all_edge_iterator old = *this;
        ++*this;
        return old;
      }
 
      bool operator==(all_edge_iterator o) const
      {
        return t_ == o.t_;
      }
 
      bool operator!=(all_edge_iterator o) const
      {
        return t_ != o.t_;
      }
 
      reference operator*() const
      {
        return tv_[t_];
      }
 
      pointer operator->() const
      {
        return &tv_[t_];
      }
    };
 
 
    template <typename Graph>
    class SPOT_API all_trans
    {
    public:
      typedef typename std::conditional<std::is_const<Graph>::value,
                                        const typename Graph::edge_vector_t,
                                        typename Graph::edge_vector_t>::type
        tv_t;
      typedef all_edge_iterator<Graph> iter_t;
    private:
      tv_t& tv_;
    public:
 
      all_trans(tv_t& tv) noexcept
        : tv_(tv)
      {
      }
 
      iter_t begin() const
      {
        return {0, tv_};
      }
 
      iter_t end() const
      {
        return {tv_};
      }
    };
 
    class SPOT_API const_universal_dests
    {
    private:
      const unsigned* begin_;
      const unsigned* end_;
      unsigned tmp_;
    public:
      const_universal_dests(const unsigned* begin, const unsigned* end) noexcept
        : begin_(begin), end_(end)
      {
      }
 
      const_universal_dests(unsigned state) noexcept
        : begin_(&tmp_), end_(&tmp_ + 1), tmp_(state)
      {
      }
 
      const unsigned* begin() const
      {
        return begin_;
      }
 
      const unsigned* end() const
      {
        return end_;
      }
    };
 
    template<class G>
    class univ_dest_mapper
    {
      std::map<std::vector<unsigned>, unsigned> uniq_;
      G& g_;
    public:
 
      univ_dest_mapper(G& graph)
        : g_(graph)
      {
      }
 
      template<class I>
      unsigned new_univ_dests(I begin, I end)
      {
        std::vector<unsigned> tmp(begin, end);
        std::sort(tmp.begin(), tmp.end());
        tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
        auto p = uniq_.emplace(tmp, 0);
        if (p.second)
          p.first->second = g_.new_univ_dests(tmp.begin(), tmp.end());
        return p.first->second;
      }
 
      unsigned new_univ_dests(std::vector<unsigned>&& tmp)
      {
        std::sort(tmp.begin(), tmp.end());
        tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
        auto p = uniq_.emplace(tmp, 0);
        if (p.second)
          p.first->second = g_.new_univ_dests(tmp.begin(), tmp.end());
        return p.first->second;
      }
    };
 
  } // namespace internal
 
 
  template <typename State_Data, typename Edge_Data>
  class digraph
  {
    friend class internal::edge_iterator<digraph>;
    friend class internal::edge_iterator<const digraph>;
    friend class internal::killer_edge_iterator<digraph>;
 
  public:
    typedef internal::edge_iterator<digraph> iterator;
    typedef internal::edge_iterator<const digraph> const_iterator;
 
    // Extra data to store on each state or edge.
    typedef State_Data state_data_t;
    typedef Edge_Data edge_data_t;
 
    // State and edges are identified by their indices in some
    // vector.
    typedef unsigned state;
    typedef unsigned edge;
 
    typedef internal::distate_storage<edge,
                                      internal::boxed_label<State_Data>>
      state_storage_t;
    typedef internal::edge_storage<state, state, edge,
                                   internal::boxed_label<Edge_Data>>
      edge_storage_t;
    typedef std::vector<state_storage_t> state_vector;
    typedef std::vector<edge_storage_t> edge_vector_t;
 
    // A sequence of universal destination groups of the form:
    //   (n state_1 state_2 ... state_n)*
    typedef std::vector<unsigned> dests_vector_t;
 
  protected:
    state_vector states_;
    edge_vector_t edges_;
    dests_vector_t dests_;      // Only used by alternating automata.
    // Number of erased edges.
    unsigned killed_edge_;
  public:
    digraph(unsigned max_states = 10, unsigned max_trans = 0)
      : killed_edge_(0)
    {
      states_.reserve(max_states);
      if (max_trans == 0)
        max_trans = max_states * 2;
      edges_.reserve(max_trans + 1);
      // Edge number 0 is not used, because we use this index
      // to mark the absence of a edge.
      edges_.resize(1);
      // This causes edge 0 to be considered as dead.
      edges_[0].next_succ = 0;
    }
 
    unsigned num_states() const
    {
      return states_.size();
    }
 
    unsigned num_edges() const
    {
      return edges_.size() - killed_edge_ - 1;
    }
 
    bool is_existential() const
    {
      return dests_.empty();
    }
 
    template <typename... Args>
    state new_state(Args&&... args)
    {
      state s = states_.size();
      states_.emplace_back(std::forward<Args>(args)...);
      return s;
    }
 
    template <typename... Args>
    state new_states(unsigned n, Args&&... args)
    {
      state s = states_.size();
      states_.reserve(s + n);
      while (n--)
        states_.emplace_back(std::forward<Args>(args)...);
      return s;
    }
 
    state_storage_t&
    state_storage(state s)
    {
      return states_[s];
    }
 
    const state_storage_t&
    state_storage(state s) const
    {
      return states_[s];
    }
 
    typename state_storage_t::data_t&
    state_data(state s)
    {
      return states_[s].data();
    }
 
    const typename state_storage_t::data_t&
    state_data(state s) const
    {
      return states_[s].data();
    }
 
    edge_storage_t&
    edge_storage(edge s)
    {
      return edges_[s];
    }
 
    const edge_storage_t&
    edge_storage(edge s) const
    {
      return edges_[s];
    }
 
    typename edge_storage_t::data_t&
    edge_data(edge s)
    {
      return edges_[s].data();
    }
 
    const typename edge_storage_t::data_t&
    edge_data(edge s) const
    {
      return edges_[s].data();
    }
 
    template <typename... Args>
    edge
    new_edge(state src, state dst, Args&&... args)
    {
      edge t = edges_.size();
      edges_.emplace_back(dst, 0, src, std::forward<Args>(args)...);
 
      edge st = states_[src].succ_tail;
      SPOT_ASSERT(st < t || !st);
      if (!st)
        states_[src].succ = t;
      else
        edges_[st].next_succ = t;
      states_[src].succ_tail = t;
      return t;
    }
 
    template <typename I>
    state
    new_univ_dests(I dst_begin, I dst_end)
    {
      unsigned sz = std::distance(dst_begin, dst_end);
      if (sz == 1)
        return *dst_begin;
      SPOT_ASSERT(sz > 1);
      unsigned d = dests_.size();
      if (!dests_.empty()
          && &*dst_begin >= &dests_.front()
          && &*dst_begin <= &dests_.back()
          && (dests_.capacity() - dests_.size()) < (sz + 1))
        {
          // If dst_begin...dst_end points into dests_ and dests_ risk
          // being reallocated, we have to save the destination
          // states before we lose them.
          std::vector<unsigned> tmp(dst_begin, dst_end);
          dests_.emplace_back(sz);
          dests_.insert(dests_.end(), tmp.begin(), tmp.end());
        }
      else
        {
          dests_.emplace_back(sz);
          dests_.insert(dests_.end(), dst_begin, dst_end);
        }
      return ~d;
    }
 
    template <typename I, typename... Args>
    edge
    new_univ_edge(state src, I dst_begin, I dst_end, Args&&... args)
    {
      return new_edge(src, new_univ_dests(dst_begin, dst_end),
                      std::forward<Args>(args)...);
    }
 
    template <typename... Args>
    edge
    new_univ_edge(state src, const std::initializer_list<state>& dsts,
                  Args&&... args)
    {
      return new_univ_edge(src, dsts.begin(), dsts.end(),
                           std::forward<Args>(args)...);
    }
 
    internal::const_universal_dests univ_dests(state src) const
    {
      if ((int)src < 0)
        {
          unsigned pos = ~src;
          const unsigned* d = dests_.data();
          d += pos;
          unsigned num = *d;
          return { d + 1, d + num + 1 };
        }
      else
        {
          return src;
        }
    }
 
    internal::const_universal_dests univ_dests(const edge_storage_t& e) const
    {
      return univ_dests(e.dst);
    }
 
    state index_of_state(const state_storage_t& ss) const
    {
      SPOT_ASSERT(!states_.empty());
      return &ss - &states_.front();
    }
 
    edge index_of_edge(const edge_storage_t& tt) const
    {
      SPOT_ASSERT(!edges_.empty());
      return &tt - &edges_.front();
    }
 
    internal::state_out<digraph>
    out(state src)
    {
      return {this, states_[src].succ};
    }
 
    internal::state_out<digraph>
    out(state_storage_t& src)
    {
      return out(index_of_state(src));
    }
 
    internal::state_out<const digraph>
    out(state src) const
    {
      return {this, states_[src].succ};
    }
 
    internal::state_out<const digraph>
    out(state_storage_t& src) const
    {
      return out(index_of_state(src));
    }
 
    internal::killer_edge_iterator<digraph>
    out_iteraser(state_storage_t& src)
    {
      return {this, src.succ, src};
    }
 
    internal::killer_edge_iterator<digraph>
    out_iteraser(state src)
    {
      return out_iteraser(state_storage(src));
    }
 
    const state_vector& states() const
    {
      return states_;
    }
 
    state_vector& states()
    {
      return states_;
    }
 
    internal::all_trans<const digraph> edges() const
    {
      return edges_;
    }
 
    internal::all_trans<digraph> edges()
    {
      return edges_;
    }
 
    const edge_vector_t& edge_vector() const
    {
      return edges_;
    }
 
    edge_vector_t& edge_vector()
    {
      return edges_;
    }
 
    bool is_valid_edge(edge t) const
    {
      // Erased edges have their next_succ pointing to
      // themselves.
      return (t < edges_.size() &&
              edges_[t].next_succ != t);
    }
 
    bool is_dead_edge(unsigned t) const
    {
      return edges_[t].next_succ == t;
    }
 
    bool is_dead_edge(const edge_storage_t& t) const
    {
      return t.next_succ == index_of_edge(t);
    }
 
    const dests_vector_t& dests_vector() const
    {
      return dests_;
    }
 
    dests_vector_t& dests_vector()
    {
      return dests_;
    }
 
    void dump_storage(std::ostream& o) const
    {
      unsigned tend = edges_.size();
      for (unsigned t = 1; t < tend; ++t)
        {
          o << 't' << t << ": (s"
            << edges_[t].src << ", ";
          int d = edges_[t].dst;
          if (d < 0)
            o << 'd' << ~d;
          else
            o << 's' << d;
          o << ") t" << edges_[t].next_succ << '\n';
        }
      unsigned send = states_.size();
      for (unsigned s = 0; s < send; ++s)
        {
          o << 's' << s << ": t"
            << states_[s].succ << " t"
            << states_[s].succ_tail << '\n';
        }
      unsigned dend = dests_.size();
      unsigned size = 0;
      for (unsigned s = 0; s < dend; ++s)
        {
          o << 'd' << s << ": ";
          if (size == 0)
            {
              o << '#';
              size = dests_[s];
            }
          else
            {
              o << 's';
              --size;
            }
          o << dests_[s] << '\n';
        }
    }
 
    enum dump_storage_items {
      DSI_GraphHeader = 1,
      DSI_GraphFooter = 2,
      DSI_StatesHeader = 4,
      DSI_StatesBody = 8,
      DSI_StatesFooter = 16,
      DSI_States = DSI_StatesHeader | DSI_StatesBody | DSI_StatesFooter,
      DSI_EdgesHeader = 32,
      DSI_EdgesBody = 64,
      DSI_EdgesFooter = 128,
      DSI_Edges = DSI_EdgesHeader | DSI_EdgesBody | DSI_EdgesFooter,
      DSI_DestsHeader = 256,
      DSI_DestsBody = 512,
      DSI_DestsFooter = 1024,
      DSI_Dests = DSI_DestsHeader | DSI_DestsBody | DSI_DestsFooter,
      DSI_All =
      DSI_GraphHeader | DSI_States | DSI_Edges | DSI_Dests | DSI_GraphFooter,
    };
 
    void dump_storage_as_dot(std::ostream& o, int dsi = DSI_All) const
    {
      if (dsi & DSI_GraphHeader)
        o << "digraph g { \nnode [shape=plaintext]\n";
      unsigned send = states_.size();
      if (dsi & DSI_StatesHeader)
        {
          o << ("states [label=<\n"
                "<table border='0' cellborder='1' cellspacing='0'>\n"
                "<tr><td sides='b' bgcolor='yellow' port='s'>states</td>\n");
          for (unsigned s = 0; s < send; ++s)
            o << "<td sides='b' bgcolor='yellow' port='s" << s << "'>"
              << s << "</td>\n";
          o << "</tr>\n";
        }
      if (dsi & DSI_StatesBody)
        {
          o << "<tr><td port='ss'>succ</td>\n";
          for (unsigned s = 0; s < send; ++s)
            {
              o << "<td port='ss" << s;
              if (states_[s].succ)
                o << "' bgcolor='cyan";
              o << "'>" << states_[s].succ << "</td>\n";
            }
          o << "</tr><tr><td port='st'>succ_tail</td>\n";
          for (unsigned s = 0; s < send; ++s)
            {
              o << "<td port='st" << s;
              if (states_[s].succ_tail)
                o << "' bgcolor='cyan";
              o << "'>" << states_[s].succ_tail << "</td>\n";
            }
          o << "</tr>\n";
        }
      if (dsi & DSI_StatesFooter)
        o << "</table>>]\n";
      unsigned eend = edges_.size();
      if (dsi & DSI_EdgesHeader)
        {
          o << ("edges [label=<\n"
                "<table border='0' cellborder='1' cellspacing='0'>\n"
                "<tr><td sides='b' bgcolor='cyan' port='e'>edges</td>\n");
          for (unsigned e = 1; e < eend; ++e)
            {
              o << "<td sides='b' bgcolor='"
                << (e != edges_[e].next_succ ? "cyan" : "gray")
                << "' port='e" << e << "'>" << e << "</td>\n";
            }
          o << "</tr>";
        }
      if (dsi & DSI_EdgesBody)
        {
          o << "<tr><td port='ed'>dst</td>\n";
          for (unsigned e = 1; e < eend; ++e)
            {
              o << "<td port='ed" << e;
              int d = edges_[e].dst;
              if (d < 0)
                o << "' bgcolor='pink'>~" << ~d;
              else
                o << "' bgcolor='yellow'>" << d;
              o << "</td>\n";
            }
          o << "</tr><tr><td port='en'>next_succ</td>\n";
          for (unsigned e = 1; e < eend; ++e)
            {
              o << "<td port='en" << e;
              if (edges_[e].next_succ)
                {
                  if (edges_[e].next_succ != e)
                    o << "' bgcolor='cyan";
                  else
                    o << "' bgcolor='gray";
                }
              o << "'>" << edges_[e].next_succ << "</td>\n";
            }
          o << "</tr><tr><td port='es'>src</td>\n";
          for (unsigned e = 1; e < eend; ++e)
            o << "<td port='es" << e << "' bgcolor='yellow'>"
              << edges_[e].src << "</td>\n";
          o << "</tr>\n";
        }
      if (dsi & DSI_EdgesFooter)
        o << "</table>>]\n";
      if (!dests_.empty())
        {
          unsigned dend = dests_.size();
          if (dsi & DSI_DestsHeader)
            {
              o << ("dests [label=<\n"
                    "<table border='0' cellborder='1' cellspacing='0'>\n"
                    "<tr><td sides='b' bgcolor='pink' port='d'>dests</td>\n");
              unsigned d = 0;
              while (d < dend)
                {
                  o << "<td sides='b' bgcolor='pink' port='d"
                    << d << "'>~" << d << "</td>\n";
                  unsigned cnt = dests_[d];
                  d += cnt + 1;
                  while (cnt--)
                    o << "<td sides='b'></td>\n";
                }
              o << "</tr>\n";
            }
          if (dsi & DSI_DestsBody)
            {
              o << "<tr><td port='dd'>#cnt/dst</td>\n";
              unsigned d = 0;
              while (d < dend)
                {
                  unsigned cnt = dests_[d];
                  o << "<td port='d'>#" << cnt << "</td>\n";
                  ++d;
                  while (cnt--)
                    {
                      o << "<td bgcolor='yellow' port='dd"
                        << d << "'>" << dests_[d] << "</td>\n";
                      ++d;
                    }
                }
              o << "</tr>\n";
            }
          if (dsi & DSI_DestsFooter)
            o << "</table>>]\n";
        }
      if (dsi & DSI_GraphFooter)
        o << "}\n";
    }
 
    void remove_dead_edges_()
    {
      if (killed_edge_ == 0)
        return;
      auto i = std::remove_if(edges_.begin() + 1, edges_.end(),
                              [this](const edge_storage_t& t) {
                                return this->is_dead_edge(t);
                              });
      edges_.erase(i, edges_.end());
      killed_edge_ = 0;
    }
 
    template<class Predicate = std::less<edge_storage_t>>
    void sort_edges_(Predicate p = Predicate())
    {
      //std::cerr << "\nbefore\n";
      //dump_storage(std::cerr);
      std::stable_sort(edges_.begin() + 1, edges_.end(), p);
    }
 
    template<class Predicate = std::less<edge_storage_t>>
    void sort_edges_srcfirst_(Predicate p = Predicate(),
                              parallel_policy ppolicy = parallel_policy())
    {
      SPOT_ASSERT(!edges_.empty());
      const unsigned ns = num_states();
      std::vector<unsigned> idx_list(ns+1);
      edge_vector_t new_edges;
      new_edges.reserve(edges_.size());
      new_edges.resize(1);
      // This causes edge 0 to be considered as dead.
      new_edges[0].next_succ = 0;
      // Copy all edges so that they are sorted by src
      for (unsigned s = 0; s < ns; ++s)
        {
          idx_list[s] = new_edges.size();
          for (const auto& e : out(s))
            new_edges.push_back(e);
        }
      idx_list[ns] = new_edges.size();
      // New edge sorted by source
      // If we have few edge or only one threads
      // Benchmark few?
      auto bne = new_edges.begin();
#ifndef SPOT_ENABLE_PTHREAD
      (void) ppolicy;
#else
      unsigned nthreads = ppolicy.nthreads();
      if (nthreads <= 1)
#endif
        {
          for (unsigned s = 0u; s < ns; ++s)
            std::stable_sort(bne + idx_list[s],
                             bne + idx_list[s+1], p);
        }
#ifdef SPOT_ENABLE_PTHREAD
      else
        {
          static std::vector<std::thread> tv;
          SPOT_ASSERT(tv.empty());
          tv.resize(nthreads);
          // FIXME: Due to the way these thread advance into the state
          // vector, they access very close memory location.  It would
          // seems more cache friendly to have threads work on blocks
          // of continuous states.
          for (unsigned id = 0; id < nthreads; ++id)
            tv[id] = std::thread(
              [bne, id, ns, &idx_list, p, nthreads]()
              {
                for (unsigned s = id; s < ns; s += nthreads)
                  std::stable_sort(bne + idx_list[s],
                                   bne + idx_list[s+1], p);
                return;
              });
          for (auto& t : tv)
            t.join();
          tv.clear();
        }
#endif
      std::swap(edges_, new_edges);
      // Like after normal sort_edges, they need to be chained before usage
    }
 
    template<bool Stable = false, class Predicate = std::less<edge_storage_t>>
    void sort_edges_of_(Predicate p = Predicate(),
                        const std::vector<bool>* to_sort_ptr = nullptr)
    {
      SPOT_ASSERT((to_sort_ptr == nullptr)
                  || (to_sort_ptr->size() == num_states()));
      //std::cerr << "\nbefore\n";
      //dump_storage(std::cerr);
      auto pi = [&](unsigned t1, unsigned t2)
          {return p(edges_[t1], edges_[t2]); };
 
      // Sort the outgoing edges of each selected state according
      // to predicate p.  Do that in place.
      std::vector<unsigned> sort_idx_;
      unsigned ns = num_states();
      for (unsigned i = 0; i < ns; ++i)
        {
          if (to_sort_ptr && !(*to_sort_ptr)[i])
            continue;
          unsigned t = states_[i].succ;
          if (t == 0)
            continue;
          sort_idx_.clear();
          do
            {
               sort_idx_.push_back(t);
               t = edges_[t].next_succ;
            } while (t != 0);
          if constexpr (Stable)
            std::stable_sort(sort_idx_.begin(), sort_idx_.end(), pi);
          else
            std::sort(sort_idx_.begin(), sort_idx_.end(), pi);
          // Update the graph
          states_[i].succ = sort_idx_.front();
          states_[i].succ_tail = sort_idx_.back();
          const unsigned n_outs_n1 = sort_idx_.size() - 1;
          for (unsigned k = 0; k < n_outs_n1; ++k)
            edges_[sort_idx_[k]].next_succ = sort_idx_[k+1];
          edges_[sort_idx_.back()].next_succ = 0; // terminal
        }
      // Done
    }
 
    void chain_edges_()
    {
      state last_src = -1U;
      edge tend = edges_.size();
      for (edge t = 1; t < tend; ++t)
        {
          state src = edges_[t].src;
          if (src != last_src)
            {
              states_[src].succ = t;
              if (last_src != -1U)
                {
                  states_[last_src].succ_tail = t - 1;
                  edges_[t - 1].next_succ = 0;
                }
              while (++last_src != src)
                {
                  states_[last_src].succ = 0;
                  states_[last_src].succ_tail = 0;
                }
            }
          else
            {
              edges_[t - 1].next_succ = t;
            }
        }
      if (last_src != -1U)
        {
          states_[last_src].succ_tail = tend - 1;
          edges_[tend - 1].next_succ = 0;
        }
      unsigned send = states_.size();
      while (++last_src != send)
        {
          states_[last_src].succ = 0;
          states_[last_src].succ_tail = 0;
        }
      //std::cerr << "\nafter\n";
      //dump_storage(std::cerr);
    }
 
    void rename_states_(const std::vector<unsigned>& newst)
    {
      SPOT_ASSERT(newst.size() == states_.size());
      unsigned tend = edges_.size();
      for (unsigned t = 1; t < tend; t++)
        {
          edges_[t].dst = newst[edges_[t].dst];
          edges_[t].src = newst[edges_[t].src];
        }
    }
 
    void defrag_states(const std::vector<unsigned>& newst, unsigned used_states)
    {
      SPOT_ASSERT(newst.size() >= states_.size());
      SPOT_ASSERT(used_states > 0);
 
      //std::cerr << "\nbefore defrag\n";
      //dump_storage(std::cerr);
 
      // Permute all states in states_, as indicated by newst.
      // This will put erased states after used_states.
      permute_vector(states_, newst);
      unsigned send = states_.size();
      for (state s = used_states; s < send; ++s)
        {
          // This is an erased state.  Mark all its edges as
          // dead (i.e., t.next_succ should point to t for each of
          // them).
          auto t = states_[s].succ;
          while (t)
            std::swap(t, edges_[t].next_succ);
        }
      states_.resize(used_states);
 
      // Shift all edges in edges_.  The algorithm is
      // similar to remove_if, but it also keeps the correspondence
      // between the old and new index as newidx[old] = new.
      //
      // If you change anything to this logic, you might want to
      // double check twa_graph::defrag_states where we need to
      // predict the new edges indices in order to update
      // highlight-edges.
      unsigned tend = edges_.size();
      std::vector<edge> newidx(tend);
      unsigned dest = 1;
      for (edge t = 1; t < tend; ++t)
        {
          if (is_dead_edge(t))
            continue;
          if (t != dest)
            edges_[dest] = std::move(edges_[t]);
          newidx[t] = dest;
          ++dest;
        }
      edges_.resize(dest);
      killed_edge_ = 0;
 
      // Adjust next_succ and dst pointers in all edges.
      for (edge t = 1; t < dest; ++t)
        {
          auto& tr = edges_[t];
          tr.src = newst[tr.src];
          tr.dst = newst[tr.dst];
          tr.next_succ = newidx[tr.next_succ];
        }
 
      // Adjust succ and succ_tails pointers in all states.
      for (auto& s: states_)
        {
          s.succ = newidx[s.succ];
          s.succ_tail = newidx[s.succ_tail];
        }
 
      //std::cerr << "\nafter defrag\n";
      //dump_storage(std::cerr);
    }
 
    // prototype was changed in Spot 2.10
    SPOT_DEPRECATED("use reference version of this method")
    void defrag_states(std::vector<unsigned>&& newst, unsigned used_states)
    {
      return defrag_states(newst, used_states);
    }
  };
}