// Author(s): Wieger Wesselink
// Copyright: see the accompanying file COPYING or copy at
// https://svn.win.tue.nl/trac/MCRL2/browser/trunk/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)
//
/// \file mcrl2/pbes/detail/stategraph_graph.h
/// \brief add your file description here.

#ifndef MCRL2_PBES_DETAIL_STATEGRAPH_GRAPH_H
#define MCRL2_PBES_DETAIL_STATEGRAPH_GRAPH_H

#include <algorithm>
#include <sstream>
#include "mcrl2/data/detail/print_utility.h"
#include "mcrl2/data/detail/sorted_sequence_algorithm.h"
#include "mcrl2/pbes/detail/stategraph_pbes.h"
#include "mcrl2/pbes/detail/stategraph_utility.h"
#include "mcrl2/utilities/detail/container_utility.h"

namespace mcrl2 {

namespace pbes_system {

namespace detail {

// Vertex in the graph of LCFP parameters
class LCFP_vertex
{
  protected:
    core::identifier_string m_name;
    std::size_t m_index;
    data::variable m_variable;

  public:
    LCFP_vertex(const core::identifier_string& name, std::size_t index = data::undefined_index(), const data::variable& variable = data::undefined_variable())
      : m_name(name), m_index(index), m_variable(variable)
    {}

    const core::identifier_string& name() const
    {
      return m_name;
    }

    std::size_t index() const
    {
      return m_index;
    }

    const data::variable& variable() const
    {
      return m_variable;
    }

    bool has_variable() const
    {
      return m_index != data::undefined_index();
    }
};

inline
std::ostream& operator<<(std::ostream& out, const LCFP_vertex& u)
{
  return out << '(' << u.name() << ", " << u.index() << ", " << data::pp(u.variable()) << ')';
}

// Vertex in the graph of GCFP parameters
class GCFP_vertex: public LCFP_vertex
{
  protected:
    std::set<GCFP_vertex*> m_neighbors;

  public:
    GCFP_vertex(const core::identifier_string& name, std::size_t index, const data::variable& variable)
      : LCFP_vertex(name, index, variable)
    {}

    const std::set<GCFP_vertex*>& neighbors() const
    {
      return m_neighbors;
    }

    std::set<GCFP_vertex*>& neighbors()
    {
      return m_neighbors;
    }
};

class GCFP_graph;
std::ostream& operator<<(std::ostream& out, const GCFP_graph& G);

class GCFP_graph
{
  protected:
    std::vector<GCFP_vertex> m_vertices;

  public:
    typedef std::vector<GCFP_vertex> vertex_iterator;

    const std::vector<GCFP_vertex>& vertices() const
    {
      return m_vertices;
    }

    const GCFP_vertex& vertex(std::size_t i) const
    {
      return m_vertices[i];
    }

    void add_vertex(const GCFP_vertex& u)
    {
      m_vertices.push_back(u);
    }

    GCFP_vertex& find_vertex(const core::identifier_string& X, std::size_t n)
    {
      for (auto i = m_vertices.begin(); i != m_vertices.end(); ++i)
      {
        if (i->name() == X && i->index() == n)
        {
          return *i;
        }
      }
      std::ostringstream out;
      out << "vertex (" << X << ", " << n << ") not found in GCFP graph";
      throw mcrl2::runtime_error(out.str());
    }

    std::size_t index(const GCFP_vertex& u) const
    {
      return &u - &(m_vertices.front());
    }
};

inline
std::ostream& operator<<(std::ostream& out, const GCFP_graph& G)
{
  auto const& V = G.vertices();
  for (auto i = V.begin(); i != V.end(); ++i)
  {
    out << *i << std::endl;
  }
  return out;
}

// This class is used to add labeled edges to a vertex
template <typename Vertex>
class add_edges
{
  protected:
    mutable std::map<const Vertex*, std::set<std::size_t> > m_outgoing_edges;
    mutable std::map<const Vertex*, std::set<std::size_t> > m_incoming_edges;
    // the mapped values are the edge labels; note that there can be multiple edges with different labels

  public:
    const std::map<const Vertex*, std::set<std::size_t> >& outgoing_edges() const
    {
      return m_outgoing_edges;
    }

    const std::map<const Vertex*, std::set<std::size_t> >& incoming_edges() const
    {
      return m_incoming_edges;
    }

    void insert_outgoing_edge(const Vertex* u, std::size_t label) const
    {
      m_outgoing_edges[u].insert(label);
    }

    void insert_incoming_edge(const Vertex* u, std::size_t label) const
    {
      m_incoming_edges[u].insert(label);
    }

    std::string print_outgoing_edges() const
    {
      std::ostringstream out;
      for (auto i = m_outgoing_edges.begin(); i != m_outgoing_edges.end(); ++i)
      {
        if (i != m_outgoing_edges.begin())
        {
          out << "; ";
        }
        out << *i->first << " (labels = " << core::detail::print_set(i->second) << ")";
      }
      return out.str();
    }

    void remove_edges()
    {
      m_outgoing_edges.clear();
      m_incoming_edges.clear();
    }
};

// Vertex in a local control flow graph.
class local_control_flow_graph_vertex: public LCFP_vertex, public add_edges<local_control_flow_graph_vertex>
{
  protected:
    typedef add_edges<local_control_flow_graph_vertex> super;

    data::data_expression m_value;
    mutable std::set<data::variable> m_marking; // used in the reset variables procedure

    // (i, l) is mapped to FV(rewr(e[l], [d_X[n] := z])) intersect {d | (X, d) in B},
    // where Y(e) = PVI(phi_X, i), d_X[n] = variable(), z = value(), and B is the belongs relation
    // corresponding to the graph of this vertex
    mutable std::map<std::pair<std::size_t, data::variable>, std::set<data::variable> > m_marking_update;

  public:
    using super::incoming_edges;
    using super::outgoing_edges;
    using super::print_outgoing_edges;
    using super::insert_outgoing_edge;
    using super::insert_incoming_edge;
    using super::remove_edges;

    local_control_flow_graph_vertex(const core::identifier_string& name, std::size_t index, const data::variable& variable, const data::data_expression& value)
      : LCFP_vertex(name, index, variable), m_value(value)
    {}

    local_control_flow_graph_vertex(const core::identifier_string& name, const data::data_expression& value)
      : LCFP_vertex(name), m_value(value)
    {}

    const data::data_expression& value() const
    {
      return m_value;
    }

    const std::set<data::variable>& marking() const
    {
      return m_marking;
    }

    void set_marking(const std::set<data::variable>& marking) const
    {
      m_marking = marking;
    }

    void extend_marking(const std::set<data::variable>& marking) const
    {
      m_marking.insert(marking.begin(), marking.end());
    }

    bool operator==(const local_control_flow_graph_vertex& other) const
    {
      return m_name == other.m_name && m_index == other.m_index && m_value == other.m_value;
    }

    std::string print_marking() const
    {
      std::ostringstream out;
      out << "vertex " << *this << " marking = " << core::detail::print_set(m_marking);
      return out.str();
    }

    void set_marking_update(std::size_t i, const data::variable& d, const std::set<data::variable>& V) const
    {
      std::pair<std::size_t, data::variable> p(i, d);
      m_marking_update[p] = V;
    }

    const std::map<std::pair<std::size_t, data::variable>, std::set<data::variable> >& marking_update() const
    {
      return m_marking_update;
    }
};

inline
std::ostream& operator<<(std::ostream& out, const local_control_flow_graph_vertex& u)
{
  if (u.index() == data::undefined_index())
  {
    return out << '(' << u.name() << ", ?, ?=?)";
    assert(u.value() == data::undefined_data_expression());
  }
  return out << '(' << u.name() << ", " << u.index() << ", " << data::pp(u.variable()) << "=" << data::pp(u.value()) << ')';
}

inline
bool operator<(const local_control_flow_graph_vertex& u, const local_control_flow_graph_vertex& v)
{
  if (u.name() != v.name())
  {
    return u.name() < v.name();
  }
  if (u.index() != v.index())
  {
    return u.index() < v.index();
  }
  return u.value() < v.value();
}

template <typename Vertex>
struct control_flow_graph
{
  std::set<Vertex> vertices;

  // an index for the vertices in the control flow graph with a given name
  std::map<core::identifier_string, std::set<const Vertex*> > m_graph_index;

  const Vertex& find_vertex(const Vertex& u) const
  {
    auto i = vertices.find(u);
    if (i == vertices.end())
    {
      std::cout << "could not find vertex " << u << " in the graph\n" << *this << std::endl;
      throw mcrl2::runtime_error("control_flow_graph::find_vertex: vertex not found!");
    }
    return *i;
  }

  void compute_index()
  {
    m_graph_index.clear();

    // create an index for the vertices in the control flow graph with a given name
    for (auto i = vertices.begin(); i != vertices.end(); ++i)
    {
      const Vertex& u = *i;
      m_graph_index[u.name()].insert(&u);
    }
  }

  std::set<const Vertex*> index(const core::identifier_string& X) const
  {
    auto i = m_graph_index.find(X);
    if (i == m_graph_index.end())
    {
      return std::set<const Vertex*>();
    }
    else
    {
      return i->second;
    }
  }

  bool has_vertex(const core::identifier_string& X, std::size_t p) const
  {
    for (auto i = vertices.begin(); i != vertices.end(); ++i)
    {
      if (i->name() == X && i->index() == p)
      {
        return true;
      }
    }
    return false;
  }

  /// \brief Default constructor
  control_flow_graph()
  {}

  /// \brief Copy constructor N.B. The implementation is rather inefficient!
  control_flow_graph(const control_flow_graph<Vertex>& other)
  {
    // copy the vertices, but not the neighbors
    for (auto i = other.vertices.begin(); i != other.vertices.end(); ++i)
    {
      auto u = *i;
      u.remove_edges();
      vertices.insert(u);
    }

    // reconstruct the incoming and outgoing edges
    for (auto i = other.vertices.begin(); i != other.vertices.end(); ++i)
    {
      const Vertex& u = find_vertex(*i);
      auto const& outgoing_edges = i->outgoing_edges();
      for (auto j = outgoing_edges.begin(); j != outgoing_edges.end(); ++j)
      {
        const Vertex& v = find_vertex(*(j->first));
        std::set<std::size_t> labels = j->second;
        for (auto k = labels.begin(); k != labels.end(); ++k)
        {
          u.insert_outgoing_edge(&v, *k);
          v.insert_incoming_edge(&u, *k);
        }
      }
    }
    compute_index();
  }

  // throws a runtime_error if an error is found in the internal representation
  void self_check() const
  {
    // check if all targets of outgoing edges are part of the graph
    for (auto i = vertices.begin(); i != vertices.end(); ++i)
    {
      auto const& outgoing_edges = i->outgoing_edges();
      for (auto j = outgoing_edges.begin(); j != outgoing_edges.end(); ++j)
      {
        const Vertex& v = *(j->first);
        find_vertex(v);
      }

      auto const& incoming_edges = i->incoming_edges();
      for (auto j = incoming_edges.begin(); j != incoming_edges.end(); ++j)
      {
        const Vertex& v = *(j->first);
        find_vertex(v);
      }
    }

    // check if no two vertices (X, i, v) and (X, i', v') are in the graph with i != i'
    std::map<core::identifier_string, std::set<std::size_t> > m;
    for (auto i = vertices.begin(); i != vertices.end(); ++i)
    {
      auto& m_i = m[i->name()];
      m_i.insert(i->index());
      if (m_i.size() > 1)
      {
        auto const& X = i->name();
        std::ostringstream out;
        out << "Illegal state in control flow graph::vertices";
        for (auto k = m_i.begin(); k != m_i.end(); ++k)
        {
          out <<  " (" << X << ", " << *k << ")";
        }
        out << " encountered";
        throw mcrl2::runtime_error(out.str());
      }
    }
  }

  std::pair<typename std::set<Vertex>::iterator, bool> insert(const Vertex& u)
  {
    auto result = vertices.insert(u);
    // self_check();
    return result;
  }

  const Vertex& insert_vertex(const Vertex& v_)
  {
    auto j = std::find(vertices.begin(), vertices.end(), v_);
    if (j == vertices.end())
    {
      mCRL2log(log::debug1, "stategraph") << " add vertex v = " << v_ << std::endl;
      auto k = vertices.insert(v_);
      j = k.first;
    }
    return *j;
  }

  void insert_edge(const Vertex& u,
                   std::size_t i,
                   const Vertex& v
                  )
  {
    // add edge (u, v)
    auto q = u.outgoing_edges().find(&v);
    if (u.outgoing_edges().find(&v) == u.outgoing_edges().end() || q->second.find(i) == q->second.end())
    {
      mCRL2log(log::debug1, "stategraph") << " add edge " << u << " -> " << v << std::endl;
      u.insert_outgoing_edge(&v, i);
      v.insert_incoming_edge(&u, i);
    }
    else
    {
      mCRL2log(log::debug1, "stategraph") << " edge already exists!" << std::endl;
    }
  }

  // Returns true if there is an edge X(e) -- label --> Y(f) in the graph, for some e, f, Y.
  bool has_label(const core::identifier_string& X, std::size_t label) const
  {
    for (auto i = vertices.begin(); i != vertices.end(); ++i)
    {
      if (i->name() != X)
      {
        continue;
      }
      auto const& outgoing_edges = i->outgoing_edges();
      for (auto j = outgoing_edges.begin(); j != outgoing_edges.end(); ++j)
      {
        if (j->second.find(label) != j->second.end())
        {
          return true;
        }
      }
    }
    return false;
  }

  typename std::set<Vertex>::const_iterator begin() const
  {
    return vertices.begin();
  }

  typename std::set<Vertex>::const_iterator end() const
  {
    return vertices.end();
  }
};

template <typename Vertex>
std::ostream& operator<<(std::ostream& out, const control_flow_graph<Vertex>& G)
{
  for (auto i = G.vertices.begin(); i != G.vertices.end(); ++i)
  {
    out << *i << " outgoing_edges: " << i->print_outgoing_edges() << std::endl;
  }
  return out;
}

struct local_control_flow_graph: public control_flow_graph<local_control_flow_graph_vertex>
{
  typedef control_flow_graph<local_control_flow_graph_vertex> super;

  using super::find_vertex;
  using super::has_label;
  using super::insert_edge;
  using super::insert_vertex;

  /// \brief Default constructor
  local_control_flow_graph()
  {}

  /// \brief Copy constructor N.B. The implementation is rather inefficient!
  local_control_flow_graph(const local_control_flow_graph& other)
    : super(other)
  {}

  // Inserts an edge between the vertex u and the vertex v = (Y, k1, e1).
  void insert_edge(std::set<const local_control_flow_graph_vertex*>& todo,
                   const stategraph_pbes& p,
                   const local_control_flow_graph_vertex& u,
                   const core::identifier_string& Y,
                   std::size_t k1,
                   const data::data_expression& e1,
                   std::size_t edge_label
                  )
  {
    mCRL2log(log::debug1, "stategraph") << " insert_edge" << std::endl;
    const stategraph_equation& eq_Y = *find_equation(p, Y);
    const data::variable& d1 = (k1 == data::undefined_index() ? data::undefined_variable() : eq_Y.parameters()[k1]);

    std::size_t size = vertices.size();
    const local_control_flow_graph_vertex& v = insert_vertex(local_control_flow_graph_vertex(Y, k1, d1, e1));
    if (vertices.size() != size)
    {
      todo.insert(&v);
    }

    mCRL2log(log::debug1, "stategraph") << " u.outgoing_edges() = " << u.print_outgoing_edges() << std::endl;
    insert_edge(u, edge_label, v);
    // self_check();
  }

  std::string print_marking() const
  {
    std::ostringstream out;
    for (auto i = vertices.begin(); i != vertices.end(); ++i)
    {
      out << i->print_marking() << std::endl;
    }
    return out.str();
  }

  // finds the vertex with given name and index
  const local_control_flow_graph_vertex& find_vertex(const core::identifier_string& X, std::size_t p) const
  {
    for (auto i = vertices.begin(); i != vertices.end(); ++i)
    {
      if (i->name() == X && i->index() == p)
      {
        return *i;
      }
    }
    throw mcrl2::runtime_error("stategraph_global_graph::find_vertex: vertex not found!");
  }

  // finds the vertex with given name
  const local_control_flow_graph_vertex& find_vertex(const core::identifier_string& X) const
  {
    for (auto i = vertices.begin(); i != vertices.end(); ++i)
    {
      if (i->name() == X)
      {
        return *i;
      }
    }
    throw mcrl2::runtime_error("stategraph_global_graph::find_vertex: vertex not found!");
  }
};

class global_control_flow_graph_vertex;
std::ostream& operator<<(std::ostream& out, const global_control_flow_graph_vertex&);

// Vertex in the global control flow graph.
class global_control_flow_graph_vertex: public add_edges<global_control_flow_graph_vertex>
{
  protected:
    typedef add_edges<global_control_flow_graph_vertex> super;
    core::identifier_string m_name;
    data::data_expression_list m_values;
    mutable std::set<data::variable> m_sig;
    mutable std::set<data::variable> m_marking;    // used in the reset variables procedure
    mutable std::vector<bool> m_marked_parameters; // will be set after computing the marking

  public:
    using super::incoming_edges;
    using super::outgoing_edges;
    using super::print_outgoing_edges;
    using super::insert_outgoing_edge;
    using super::insert_incoming_edge;
    using super::remove_edges;

    global_control_flow_graph_vertex(const core::identifier_string& name, const data::data_expression_list& values)
      : m_name(name), m_values(values)
    {}

    const core::identifier_string& name() const
    {
      return m_name;
    }

    const data::data_expression_list& values() const
    {
      return m_values;
    }

    void set_marking(const std::set<data::variable>& marking) const
    {
      m_marking = marking;
    }

    void extend_marking(const std::set<data::variable>& marking) const
    {
      m_marking.insert(marking.begin(), marking.end());
    }

    void set_significant_variables(const std::set<data::variable>& sig) const
    {
      m_sig = sig;
    }

    bool operator==(const global_control_flow_graph_vertex& other) const
    {
      return m_name == other.m_name && m_values == other.m_values;
    }

    std::string print() const
    {
      return print_outgoing_edges();
      // std::ostringstream out;
      // out << pbes_system::pp(X);
      // out << " edges:";
      // for (auto i = outgoing_edges.begin(); i != outgoing_edges.end(); ++i)
      // {
      //   out << " " << pbes_system::pp(i->target->X);
      // }
      // out << " sig: " << core::detail::print_set(sig);
      // return out.str();
    }

    // also print the parameters
    std::string print(const data::variable_list& d_X) const
    {
      return print_outgoing_edges();
      // std::ostringstream out;
      // out << core::pp(X.name());
      // out << "(";
      // out << data::pp(data::make_assignment_list(d_X, X.parameters()));
      // out << ")";
      // out << " edges:";
      // for (auto i = outgoing_edges.begin(); i != outgoing_edges.end(); ++i)
      // {
      //   out << " " << i->print();
      // }
      // out << " sig: " << core::detail::print_set(sig);
      // return out.str();
    }

    std::set<std::size_t> marking_variable_indices(const stategraph_pbes& p) const
    {
      std::set<std::size_t> result;
      for (auto i = marking().begin(); i != marking().end(); ++i)
      {
        // TODO: make this code more efficient
        const stategraph_equation& eqn = *find_equation(p, m_name);
        const std::vector<data::variable>& d = eqn.parameters();
        for (auto j = d.begin(); j != d.end(); ++j)
        {
          if (*i == *j)
          {
            result.insert(j - d.begin());
            break;
          }
        }
      }
      return result;
    }

    // returns true if the i-th parameter of X is marked
    bool is_marked_parameter(std::size_t i) const
    {
      return m_marked_parameters[i];
    }

    void add_marked_parameter(bool b) const
    {
      m_marked_parameters.push_back(b);
    }

    std::string print_marking() const
    {
      std::ostringstream out;
      out << "vertex " << *this << " = " << core::detail::print_set(m_marking);
      return out.str();
    }

    const std::set<data::variable>& sig() const
    {
      return m_sig;
    }

    const std::set<data::variable>& marking() const
    {
      return m_marking;
    }

    const std::vector<bool>& marked_parameters() const
    {
      return m_marked_parameters;
    }
};

inline
bool operator<(const global_control_flow_graph_vertex& x, const global_control_flow_graph_vertex& y)
{
  return x.name() < y.name() || (x.name() == y.name() && x.values() < y.values());
}

std::ostream& operator<<(std::ostream& out, const global_control_flow_graph_vertex& u)
{
  return out << u.name() << core::detail::print_container(u.values(), "(", ")", "", false, false);
}

struct global_control_flow_graph: public control_flow_graph<global_control_flow_graph_vertex>
{
  typedef control_flow_graph<global_control_flow_graph_vertex> super;
  typedef global_control_flow_graph_vertex vertex_type;

  /// \brief Default constructor
  global_control_flow_graph()
  {}

  /// \brief Copy constructor N.B. The implementation is rather inefficient!
  global_control_flow_graph(const global_control_flow_graph& other)
    : super(other)
  {}

  std::string print_marking() const
  {
    std::ostringstream out;
    for (auto i = vertices.begin(); i != vertices.end(); ++i)
    {
      out << i->print_marking() << std::endl;
    }
    return out.str();
  }
};

} // namespace detail

} // namespace pbes_system

} // namespace mcrl2

#endif // MCRL2_PBES_DETAIL_STATEGRAPH_GRAPH_H
