// -*- coding: utf-8 -*-
// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// 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/>.

#include "config.h"
#include <spot/twaalgos/sccinfo.hh>
#include <stack>
#include <algorithm>
#include <queue>
#include <spot/twa/bddprint.hh>
#include <spot/twaalgos/mask.hh>
#include <spot/twaalgos/genem.hh>
#include <spot/misc/escape.hh>


namespace spot
{
  void scc_info::report_need_track_states()
  {
    throw std::runtime_error
      ("scc_info was not run with option TRACK_STATES");
  }

  void scc_info::report_need_track_succs()
  {
    throw std::runtime_error
      ("scc_info was not run with option TRACK_SUCCS");
  }

  void scc_info::report_incompatible_stop_on_acc()
  {
    throw std::runtime_error
      ("scc_info was run with option STOP_ON_ACC");
  }

  namespace
  {
    struct scc
    {
    public:
      scc(int index, acc_cond::mark_t in_acc):
        in_acc(in_acc), index(index)
      {
      }

      acc_cond::mark_t in_acc; // Acceptance sets on the incoming transition
      acc_cond::mark_t acc = {}; // union of all acceptance marks in the SCC
      // intersection of all marks in the SCC
      acc_cond::mark_t common = acc_cond::mark_t::all();
      int index;                     // Index of the SCC
      bool trivial = true;           // Whether the SCC has no cycle
      bool accepting = false;        // Necessarily accepting
    };
  }

  scc_info::scc_info(const_twa_graph_ptr aut,
                     unsigned initial_state,
                     edge_filter filter,
                     void* filter_data,
                     scc_info_options options)
    : aut_(aut), initial_state_(initial_state),
      filter_(filter), filter_data_(filter_data),
      options_(options)
  {
    unsigned n = aut->num_states();

    if (initial_state != -1U && n <= initial_state)
      throw std::runtime_error
        ("scc_info: supplied initial state does not exist");

    sccof_.resize(n, -1U);

    if (!!(options & scc_info_options::TRACK_STATES_IF_FIN_USED)
        && aut->acc().uses_fin_acceptance())
      options_ = options = options | scc_info_options::TRACK_STATES;

    std::vector<unsigned> live;
    live.reserve(n);
    std::deque<scc> root_;        // Stack of SCC roots.
    std::vector<int> h_(n, 0);
    // Map of visited states.  Values > 0 designate maximal SCC.
    // Values < 0 number states that are part of incomplete SCCs being
    // completed.  0 denotes non-visited states.

    int num_ = 0;               // Number of visited nodes, negated.

    struct stack_item {
      unsigned src;
      unsigned out_edge;
      unsigned univ_pos;
    };
    // DFS stack.  Holds (STATE, TRANS, UNIV_POS) pairs where TRANS is
    // the current outgoing transition of STATE, and UNIV_POS is used
    // when the transition is universal to iterate over all possible
    // destinations.
    std::stack<stack_item> todo_;
    auto& gr = aut->get_graph();

    std::deque<unsigned> init_states;
    std::vector<bool> init_seen(n, false);
    auto push_init = [&](unsigned s)
      {
        if (h_[s] != 0 || init_seen[s])
          return;
        init_seen[s] = true;
        init_states.push_back(s);
      };

    bool track_states = !!(options & scc_info_options::TRACK_STATES);
    bool track_succs = !!(options & scc_info_options::TRACK_SUCCS);
    auto backtrack = [&](unsigned curr)
      {
        if (root_.back().index == h_[curr])
          {
            unsigned num = node_.size();
            acc_cond::mark_t acc = root_.back().acc;
            acc_cond::mark_t common = root_.back().common;
            bool triv = root_.back().trivial;
            node_.emplace_back(acc, common, triv);

            auto& succ = node_.back().succ_;
            unsigned np1 = num + 1;
            auto s = live.rbegin();
            do
              {
                sccof_[*s] = num;
                h_[*s] = np1;

                // Gather all successor SCCs
                if (track_succs)
                  for (auto& t: aut->out(*s))
                    for (unsigned d: aut->univ_dests(t))
                      {
                        unsigned n = sccof_[d];
                        if (n == num || n == -1U)
                          continue;
                        // If edges are cut, we are not able to
                        // maintain proper successor information.
                        if (filter_)
                          switch (filter_(t, d, filter_data_))
                            {
                            case edge_filter_choice::keep:
                              break;
                            case edge_filter_choice::ignore:
                            case edge_filter_choice::cut:
                              continue;
                            }
                        succ.emplace_back(n);
                      }
              }
            while (*s++ != curr);

            if (track_states)
              {
                auto& nbs = node_.back().states_;
                nbs.insert(nbs.end(), s.base(), live.end());
              }

            node_.back().one_state_ = curr;
            live.erase(s.base(), live.end());

            if (track_succs)
              {
                std::sort(succ.begin(), succ.end());
                succ.erase(std::unique(succ.begin(), succ.end()), succ.end());
              }

            bool accept = !triv && root_.back().accepting;
            node_.back().accepting_ = accept;
            if (accept)
              one_acc_scc_ = num;
            bool reject = triv ||
              aut->acc().maybe_accepting(acc, common).is_false();
            node_.back().rejecting_ = reject;
            root_.pop_back();
          }
      };

    // Setup depth-first search from the initial state.  But we may
    // have a conjunction of initial state in alternating automata.
    if (initial_state_ == -1U)
      initial_state_ = aut->get_init_state_number();
    for (unsigned init: aut->univ_dests(initial_state_))
      push_init(init);

    while (!init_states.empty())
      {
        unsigned init = init_states.front();
        init_states.pop_front();
        int spi = h_[init];
        if (spi > 0)
          continue;
        assert(spi == 0);
        h_[init] = --num_;
        root_.emplace_back(num_, acc_cond::mark_t({}));
        todo_.emplace(stack_item{init, gr.state_storage(init).succ, 0});
        live.emplace_back(init);

        while (!todo_.empty())
          {
            // We are looking at the next successor in SUCC.
            unsigned tr_succ = todo_.top().out_edge;

            // If there is no more successor, backtrack.
            if (!tr_succ)
              {
                // We have explored all successors of state CURR.
                unsigned curr = todo_.top().src;

                // Backtrack TODO_.
                todo_.pop();

                // When backtracking the root of an SCC, we must also
                // remove that SCC from the ARC/ROOT stacks.  We must
                // discard from H all reachable states from this SCC.
                assert(!root_.empty());
                backtrack(curr);
                continue;
              }

            // We have a successor to look at.
            // Fetch the values we are interested in...
            auto& e = gr.edge_storage(tr_succ);

            unsigned dest = e.dst;
            if ((int) dest < 0)
              {
                // Iterate over all destinations of a universal edge.
                if (todo_.top().univ_pos == 0)
                  todo_.top().univ_pos = ~dest + 1;
                const auto& v = gr.dests_vector();
                dest = v[todo_.top().univ_pos];
                // Last universal destination?
                if (~e.dst + v[~e.dst] == todo_.top().univ_pos)
                  {
                    todo_.top().out_edge = e.next_succ;
                    todo_.top().univ_pos = 0;
                  }
                else
                  {
                    ++todo_.top().univ_pos;
                  }
              }
            else
              {
                todo_.top().out_edge = e.next_succ;
              }

            // Do we really want to look at this
            if (filter_)
              switch (filter_(e, dest, filter_data_))
                {
                case edge_filter_choice::keep:
                  break;
                case edge_filter_choice::ignore:
                  continue;
                case edge_filter_choice::cut:
                  push_init(e.dst);
                  continue;
                }

            acc_cond::mark_t acc = e.acc;

            // Are we going to a new state?
            int spi = h_[dest];
            if (spi == 0)
              {
                // Yes.  Number it, stack it, and register its successors
                // for later processing.
                h_[dest] = --num_;
                root_.emplace_back(num_, acc);
                todo_.emplace(stack_item{dest, gr.state_storage(dest).succ, 0});
                live.emplace_back(dest);
                continue;
              }

            // We already know the state.

            // Have we reached a maximal SCC?
            if (spi > 0)
              continue;

            // Now this is the most interesting case.  We have reached a
            // state S1 which is already part of a non-dead SCC.  Any such
            // non-dead SCC has necessarily been crossed by our path to
            // this state: there is a state S2 in our path which belongs
            // to this SCC too.  We are going to merge all states between
            // this S1 and S2 into this SCC..
            //
            // This merge is easy to do because the order of the SCC in
            // ROOT is descending: we just have to merge all SCCs from the
            // top of ROOT that have an index lesser than the one of
            // the SCC of S2 (called the "threshold").
            int threshold = spi;
            bool is_accepting = false;
            // If this is a self-loop, check its acceptance alone.
            if (dest == e.src)
              is_accepting = aut->acc().accepting(acc);

            acc_cond::mark_t common = acc;
            assert(!root_.empty());
            while (threshold > root_.back().index)
              {
                acc |= root_.back().acc;
                acc_cond::mark_t in_acc = root_.back().in_acc;
                acc |= in_acc;
                common &= root_.back().common;
                common &= in_acc;
                is_accepting |= root_.back().accepting;
                root_.pop_back();
                assert(!root_.empty());
              }

            // Note that we do not always have
            //  threshold == root_.back().index
            // after this loop, the SCC whose index is threshold might have
            // been merged with a higher SCC.

            root_.back().acc |= acc;
            root_.back().common &= common;
            root_.back().accepting |= is_accepting
              || aut->acc().accepting(root_.back().acc);
            // This SCC is no longer trivial.
            root_.back().trivial = false;

            if (root_.back().accepting
                && !!(options & scc_info_options::STOP_ON_ACC))
              {
                while (!todo_.empty())
                  {
                    unsigned curr = todo_.top().src;
                    todo_.pop();
                    backtrack(curr);
                  }
                return;
              }
          }
      }
    if (track_succs && !(options & scc_info_options::STOP_ON_ACC))
      determine_usefulness();
  }

  void scc_info::determine_usefulness()
  {
    // An SCC is useful if it is not rejecting or it has a successor
    // SCC that is useful.
    unsigned scccount = scc_count();
    for (unsigned i = 0; i < scccount; ++i)
      {
        if (!node_[i].is_rejecting())
          {
            node_[i].useful_ = true;
            continue;
          }
        node_[i].useful_ = false;
        for (unsigned j: node_[i].succ())
          if (node_[j].is_useful())
            {
              node_[i].useful_ = true;
              break;
            }
      }
  }

  std::set<acc_cond::mark_t> scc_info::marks_of(unsigned scc) const
  {
    std::set<acc_cond::mark_t> res;
    for (auto& t: inner_edges_of(scc))
      res.insert(t.acc);
    return res;
  }

  std::vector<std::set<acc_cond::mark_t>> scc_info::marks() const
  {
    unsigned n = aut_->num_states();
    std::vector<std::set<acc_cond::mark_t>> result(scc_count());

    for (unsigned src = 0; src < n; ++src)
      {
        unsigned src_scc = scc_of(src);
        if (src_scc == -1U || is_rejecting_scc(src_scc))
          continue;
        auto& s = result[src_scc];
        for (auto& t: aut_->out(src))
          {
            if (scc_of(t.dst) != src_scc)
              continue;
            s.insert(t.acc);
          }
      }
    return result;
  }

  std::vector<bool> scc_info::weak_sccs() const
  {
    unsigned n = scc_count();
    std::vector<bool> result(scc_count());
    auto acc = marks();
    for (unsigned s = 0; s < n; ++s)
      result[s] = is_rejecting_scc(s) || acc[s].size() == 1;
    return result;
  }

  bdd scc_info::scc_ap_support(unsigned scc) const
  {
    bdd support = bddtrue;
    for (auto& t: edges_of(scc))
      support &= bdd_support(t.cond);
    return support;
  }

  bool scc_info::check_scc_emptiness(unsigned n)
  {
    if (SPOT_UNLIKELY(!aut_->is_existential()))
      throw std::runtime_error("scc_info::check_scc_emptiness() "
                               "does not support alternating automata");
    if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
      report_need_track_states();
    return generic_emptiness_check_for_scc(*this, n);
  }

  void scc_info::determine_unknown_acceptance()
  {
    unsigned s = scc_count();
    bool changed = false;
    // iterate over SCCs in topological order
    do
      {
        --s;
        if (!is_rejecting_scc(s) && !is_accepting_scc(s))
          {
            if (SPOT_UNLIKELY(!aut_->is_existential()))
              throw std::runtime_error(
                  "scc_info::determine_unknown_acceptance() "
                  "does not support alternating automata");
            auto& node = node_[s];
            if (check_scc_emptiness(s))
              node.rejecting_ = true;
            else
              node.accepting_ = true;
            changed = true;
          }
      }
    while (s);
    if (changed && !!(options_ & scc_info_options::TRACK_SUCCS))
      determine_usefulness();
  }

  std::ostream&
  dump_scc_info_dot(std::ostream& out,
                    const_twa_graph_ptr aut, scc_info* sccinfo)
  {
    scc_info* m = sccinfo ? sccinfo : new scc_info(aut);

    out << "digraph G {\n  i [label=\"\", style=invis, height=0]\n";
    int start = m->scc_of(aut->get_init_state_number());
    out << "  i -> " << start << std::endl;

    std::vector<bool> seen(m->scc_count());
    seen[start] = true;

    std::queue<int> q;
    q.push(start);
    while (!q.empty())
      {
        int state = q.front();
        q.pop();

        out << "  " << state << " [shape=box,"
            << (aut->acc().accepting(m->acc_sets_of(state)) ?
                "style=bold," : "")
            << "label=\"" << state;
        {
          size_t n = m->states_of(state).size();
          out << " (" << n << " state";
          if (n > 1)
            out << 's';
          out << ')';
        }
        out << "\"]\n";

        for (unsigned dest: m->succ(state))
          {
            out << "  " << state << " -> " << dest << '\n';
            if (seen[dest])
              continue;
            seen[dest] = true;
            q.push(dest);
          }
      }

    out << "}\n";
    if (!sccinfo)
      delete m;
    return out;
  }

  std::vector<twa_graph_ptr>
  scc_info::split_on_sets(unsigned scc, acc_cond::mark_t sets,
                          bool preserve_names) const
  {
    if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
      report_need_track_states();
    std::vector<twa_graph_ptr> res;

    std::vector<bool> seen(aut_->num_states(), false);
    std::vector<bool> cur(aut_->num_states(), false);

    for (unsigned init: states_of(scc))
      {
        if (seen[init])
          continue;
        cur.assign(aut_->num_states(), false);

        auto copy = make_twa_graph(aut_->get_dict());
        copy->copy_ap_of(aut_);
        copy->copy_acceptance_of(aut_);
        copy->prop_state_acc(aut_->prop_state_acc());
        transform_accessible(aut_, copy, [&](unsigned src,
                                             bdd& cond,
                                             acc_cond::mark_t& m,
                                             unsigned dst)
                             {
                               cur[src] = seen[src] = true;
                               if (scc_of(dst) != scc
                                   || (m & sets)
                                   || (seen[dst] && !cur[dst]))
                                 {
                                   cond = bddfalse;
                                   return;
                                 }
                             },
                             init);
        if (copy->num_edges())
          {
            if (preserve_names)
              copy->copy_state_names_from(aut_);
            res.push_back(copy);
          }
      }
    return res;
  }

  void
  scc_info::states_on_acc_cycle_of_rec(unsigned scc,
                                       acc_cond::mark_t all_fin,
                                       acc_cond::mark_t all_inf,
                                       unsigned nb_pairs,
                                       std::vector<acc_cond::rs_pair>& pairs,
                                       std::vector<unsigned>& res,
                                       std::vector<unsigned>& old) const
  {
    if (is_useful_scc(scc) && !is_rejecting_scc(scc))
      {
        acc_cond::mark_t all_acc = acc_sets_of(scc);
        acc_cond::mark_t fin = all_fin & all_acc;
        acc_cond::mark_t inf = all_inf & all_acc;

        // Get all Fin acceptance set that appears in the SCC and does not have
        // their corresponding Inf appearing in the SCC.
        acc_cond::mark_t m = {};
        if (fin)
          for (unsigned p = 0; p < nb_pairs; ++p)
            if (fin & pairs[p].fin && !(inf & pairs[p].inf))
              m |= pairs[p].fin;

        if (m)
          for (const twa_graph_ptr& aut : split_on_sets(scc, m))
            {
              auto orig_sts = aut->get_named_prop
                <std::vector<unsigned>>("original-states");

              // Update mapping of state numbers between the current automaton
              // and the starting one.
              for (unsigned i = 0; i < orig_sts->size(); ++i)
                (*orig_sts)[i] = old[(*orig_sts)[i]];

              scc_info si_tmp(aut, scc_info_options::TRACK_STATES
                                   | scc_info_options::TRACK_SUCCS);
              unsigned scccount_tmp = si_tmp.scc_count();
              for (unsigned scc_tmp = 0; scc_tmp < scccount_tmp; ++scc_tmp)
                si_tmp.states_on_acc_cycle_of_rec(scc_tmp, all_fin, all_inf,
                                                  nb_pairs, pairs, res,
                                                  *orig_sts);
            }

        else  // Accepting cycle found.
          for (unsigned s : states_of(scc))
            res.push_back(old[s]);
      }
  }

  std::vector<unsigned>
  scc_info::states_on_acc_cycle_of(unsigned scc) const
  {
    std::vector<acc_cond::rs_pair> pairs;
    if (!aut_->acc().is_streett_like(pairs))
      throw std::runtime_error("states_on_acc_cycle_of only works with "
                               "Streett-like acceptance condition");
    unsigned nb_pairs = pairs.size();

    std::vector<unsigned> res;
    if (is_useful_scc(scc) && !is_rejecting_scc(scc))
      {
        std::vector<unsigned> old;
        unsigned nb_states = aut_->num_states();
        for (unsigned i = 0; i < nb_states; ++i)
          old.push_back(i);

        acc_cond::mark_t all_fin = {};
        acc_cond::mark_t all_inf = {};
        std::tie(all_inf, all_fin) = aut_->get_acceptance().used_inf_fin_sets();

        states_on_acc_cycle_of_rec(scc, all_fin, all_inf, nb_pairs, pairs, res,
                                   old);
      }

    return res;
  }
}