text: // -*- coding: utf-8 -*-
  // Copyright (C) 2013-2015, 2017-2019 Laboratoire de Recherche et
  // Développement de l'Epita.
  //
  // 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 <deque>
  #include <map>
  #include <spot/twaalgos/complement.hh>
  #include <spot/twaalgos/dualize.hh>
  #include <spot/twaalgos/isdet.hh>
  #include <spot/twaalgos/alternation.hh>
  #include <spot/twaalgos/postproc.hh>
  #include <spot/twaalgos/strength.hh>
  #include <spot/twaalgos/sccinfo.hh>
  
  namespace spot
  {
    twa_graph_ptr
    dtwa_complement(const const_twa_graph_ptr& aut)
    {
      if (!is_deterministic(aut))
        throw
          std::runtime_error("dtwa_complement() requires a deterministic input");
  
      return dualize(aut);
    }
  
    namespace
    {
      enum ncsb
        {
          ncsb_n = 0,       // non deterministic
          ncsb_c = 2,       // needs check
          ncsb_cb = 3,      // needs check AND in breakpoint
          ncsb_s = 4,       // safe
          ncsb_m = 1,       // missing
        };
  
      typedef std::vector<ncsb> mstate;
      typedef std::vector<std::pair<unsigned, ncsb>> small_mstate;
  
      struct small_mstate_hash
      {
        size_t
        operator()(small_mstate s) const noexcept
        {
          size_t hash = 0;
          for (const auto& p: s)
            {
              hash = wang32_hash(hash ^ ((p.first<<2) | p.second));
            }
          return hash;
        }
      };
  
      class ncsb_complementation
      {
      private:
        // The source automaton.
        const const_twa_graph_ptr aut_;
  
        // SCCs information of the source automaton.
        scc_info si_;
  
        // Number of states in the input automaton.
        unsigned nb_states_;
  
        // The complement being built.
        twa_graph_ptr res_;
  
        // Association between NCSB states and state numbers of the
        // complement.
        std::unordered_map<small_mstate, unsigned, small_mstate_hash> ncsb2n_;
  
        // States to process.
        std::deque<std::pair<mstate, unsigned>> todo_;
  
        // Support for each state of the source automaton.
        std::vector<bdd> support_;
  
        // Propositions compatible with all transitions of a state.
        std::vector<bdd> compat_;
  
        // Whether a SCC is deterministic or not
        std::vector<bool> is_deter_;
  
        // Whether a state only has accepting transitions
        std::vector<bool> is_accepting_;
  
        // State names for graphviz display
        std::vector<std::string>* names_;
  
        // Show NCSB states in state name to help debug
        bool show_names_;
  
        std::string
        get_name(const small_mstate& ms)
        {
          std::string res = "{";
  
          bool first_state = true;
          for (const auto& p: ms)
            if (p.second == ncsb_n)
              {
                if (!first_state)
                  res += ",";
                first_state = false;
                res += std::to_string(p.first);
              }
  
          res += "},{";
  
          first_state = true;
          for (const auto& p: ms)
            if (p.second & ncsb_c)
              {
                if (!first_state)
                  res += ",";
                first_state = false;
                res += std::to_string(p.first);
              }
  
          res += "},{";
  
          first_state = true;
          for (const auto& p: ms)
            if (p.second == ncsb_s)
              {
                if (!first_state)
                  res += ",";
                first_state = false;
                res += std::to_string(p.first);
              }
  
          res += "},{";
  
          first_state = true;
          for (const auto& p: ms)
            if (p.second == ncsb_cb)
              {
                if (!first_state)
                  res += ",";
                first_state = false;
                res += std::to_string(p.first);
              }
  
          return res + "}";
        }
  
        small_mstate
        to_small_mstate(const mstate& ms)
        {
          unsigned count = 0;
          for (unsigned i = 0; i < nb_states_; ++i)
            count+= (ms[i] != ncsb_m);
          small_mstate small;
          small.reserve(count);
          for (unsigned i = 0; i < nb_states_; ++i)
            if (ms[i] != ncsb_m)
              small.emplace_back(i, ms[i]);
          return small;
        }
  
        // From a NCSB state, looks for a duplicate in the map before
        // creating a new state if needed.
        unsigned
        new_state(mstate&& s)
        {
          auto p = ncsb2n_.emplace(to_small_mstate(s), 0);
          if (p.second) // This is a new state
            {
              p.first->second = res_->new_state();
              if (show_names_)
                names_->push_back(get_name(p.first->first));
              todo_.emplace_back(std::move(s), p.first->second);
            }
          return p.first->second;
        }
  
        void
        ncsb_successors(mstate&& ms, unsigned origin, bdd letter)
        {
          std::vector<mstate> succs;
          succs.emplace_back(nb_states_, ncsb_m);
  
          // Handle S states.
          //
          // Treated first because we can escape early if the letter
          // leads to an accepting transition for a Safe state.
          for (unsigned i = 0; i < nb_states_; ++i)
            {
              if (ms[i] != ncsb_s)
                continue;
  
              for (const auto& t: aut_->out(i))
                {
                  if (!bdd_implies(letter, t.cond))
                    continue;
                  if (t.acc || is_accepting_[t.dst])
                    // Exit early; transition is forbidden for safe
                    // state.
                    return;
  
                  succs[0][t.dst] = ncsb_s;
  
                  // No need to look for other compatible transitions
                  // for this state; it's in the deterministic part of
                  // the automaton
                  break;
                }
            }
  
          // Handle C states.
          for (unsigned i = 0; i < nb_states_; ++i)
            {
              if (!(ms[i] & ncsb_c))
                continue;
  
              bool has_succ = false;
              for (const auto& t: aut_->out(i))
                {
                  if (!bdd_implies(letter, t.cond))
                    continue;
  
                  has_succ = true;
  
                  // state can become safe, if transition is accepting
                  // and destination isn't an accepting state
                  if (t.acc)
                    {
                      // double all the current possible states
                      unsigned length = succs.size();
                      for (unsigned j = 0; j < length; ++j)
                        {
                          if (succs[j][t.dst] == ncsb_m)
                            {
                              if (!is_accepting_[t.dst])
                                {
                                  succs.push_back(succs[j]);
                                  succs.back()[t.dst] = ncsb_s;
                                }
                              succs[j][t.dst] = ncsb_c;
                            }
                        }
                    }
                  else       // state stays in check
                    {
                      auto it = succs.begin();
                      while (it != succs.end())
                        {
                          // remove state if it should stay in s
                          if ((*it)[t.dst] == ncsb_s)
                            {
                              std::iter_swap(it, succs.end() - 1);
                              succs.pop_back();
                              continue;
                            }
                          (*it)[t.dst] = ncsb_c;
                          ++it;
                        }
                    }
                  // No need to look for other compatible transitions
                  // for this state; it's in the deterministic part of
                  // the automaton
                  break;
                }
              if (!has_succ && !is_accepting_[i])
                return;
            }
  
          // Handle N states.
          for (unsigned i = 0; i < nb_states_; ++i)
            {
              if (ms[i] != ncsb_n)
                continue;
              for (const auto& t: aut_->out(i))
                {
                  if (!bdd_implies(letter, t.cond))
                    continue;
  
                  if (is_deter_[si_.scc_of(t.dst)])
                    {
                      // double all the current possible states
                      unsigned length = succs.size();
                      for (unsigned j = 0; j < length; ++j)
                        {
                          if (succs[j][t.dst] == ncsb_m)
                            {
                              // Can become safe if the destination is
                              // not an accepting state.
                              if (!is_accepting_[t.dst])
                                {
                                  succs.push_back(succs[j]);
                                  succs.back()[t.dst] = ncsb_s;
                                }
                              succs[j][t.dst] = ncsb_c;
                            }
                        }
                    }
                  else
                    for (auto& succ: succs)
                      succ[t.dst] = ncsb_n;
                }
            }
  
          // Revisit B states to see if they still exist in successors.
          // This is done at the end because we need to know all of the
          // states present in C before this stage
          bool b_empty = true;
          for (unsigned i = 0; i < nb_states_; ++i)
            {
              if (ms[i] != ncsb_cb)
                continue;
  
              // The original B set wasn't empty
              b_empty = false;
  
              for (const auto& t: aut_->out(i))
                {
                  if (!bdd_implies(letter, t.cond))
                    continue;
  
                  for (auto& succ: succs)
                    {
                      if (succ[t.dst] == ncsb_c)
                        succ[t.dst] = ncsb_cb;
                    }
  
                  // No need to look for other compatible transitions
                  // for this state; it's in the deterministic part of
                  // the automaton
                  break;
                }
            }
  
          // If B was empty, then set every c_not_b to cb in successors
          if (b_empty)
            for (auto& succ: succs)
              for (unsigned i = 0; i < succ.size(); ++i)
                if (succ[i] == ncsb_c)
                  succ[i] = ncsb_cb;
  
          // create the automaton states
          for (auto& succ: succs)
            {
              bool b_empty = true;
              for (const auto& state: succ)
                if (state == ncsb_cb)
                  {
                    b_empty = false;
                    break;
                  }
              if (b_empty) // becomes accepting
                {
                  for (unsigned i = 0; i < succ.size(); ++i)
                    if (succ[i] == ncsb_c)
                      succ[i] = ncsb_cb;
                  unsigned dst = new_state(std::move(succ));
                  res_->new_edge(origin, dst, letter, {0});
                }
              else
                {
                  unsigned dst = new_state(std::move(succ));
                  res_->new_edge(origin, dst, letter);
                }
            }
        }
  
      public:
        ncsb_complementation(const const_twa_graph_ptr& aut, bool show_names)
          : aut_(aut),
            si_(aut),
            nb_states_(aut->num_states()),
            support_(nb_states_),
            compat_(nb_states_),
            is_accepting_(nb_states_),
            show_names_(show_names)
        {
          res_ = make_twa_graph(aut->get_dict());
          res_->copy_ap_of(aut);
          res_->set_buchi();
  
          // Generate bdd supports and compatible options for each state.
          // Also check if all its transitions are accepting.
          for (unsigned i = 0; i < nb_states_; ++i)
            {
              bdd res_support = bddtrue;
              bdd res_compat = bddfalse;
              bool accepting = true;
              bool has_transitions = false;
              for (const auto& out: aut->out(i))
                {
                  has_transitions = true;
                  res_support &= bdd_support(out.cond);
                  res_compat |= out.cond;
                  if (!out.acc)
                    accepting = false;
                }
              support_[i] = res_support;
              compat_[i] = res_compat;
              is_accepting_[i] = accepting && has_transitions;
            }
  
  
  
          // Compute which SCCs are part of the deterministic set.
          is_deter_ = semidet_sccs(si_);
  
          if (show_names_)
            {
              names_ = new std::vector<std::string>();
              res_->set_named_prop("state-names", names_);
            }
  
          // Because we only handle one initial state, we assume it
          // belongs to the N set. (otherwise the automaton would be
          // deterministic)
          unsigned init_state = aut->get_init_state_number();
          mstate new_init_state(nb_states_, ncsb_m);
          new_init_state[init_state] = ncsb_n;
          res_->set_init_state(new_state(std::move(new_init_state)));
        }
  
        twa_graph_ptr
        run()
        {
          // Main stuff happens here
  
          while (!todo_.empty())
            {
              auto top = todo_.front();
              todo_.pop_front();
  
              mstate ms = top.first;
  
              // Compute support of all available states.
              bdd msupport = bddtrue;
              bdd n_s_compat = bddfalse;
              bdd c_compat = bddtrue;
              bool c_empty = true;
              for (unsigned i = 0; i < nb_states_; ++i)
                if (ms[i] != ncsb_m)
                  {
                    msupport &= support_[i];
                    if (ms[i] == ncsb_n || ms[i] == ncsb_s || is_accepting_[i])
                      n_s_compat |= compat_[i];
                    else
                      {
                        c_empty = false;
                        c_compat &= compat_[i];
                      }
                  }
  
              bdd all;
              if (!c_empty)
                all = c_compat;
              else
                {
                  all = n_s_compat;
                  if (all != bddtrue)
                    {
                      mstate empty_state(nb_states_, ncsb_m);
                      res_->new_edge(top.second,
                                     new_state(std::move(empty_state)),
                                     !all,
                                     {0});
                    }
                }
              while (all != bddfalse)
                {
                  bdd one = bdd_satoneset(all, msupport, bddfalse);
                  all -= one;
  
                  // Compute all new states available from the generated
                  // letter.
                  ncsb_successors(std::move(ms), top.second, one);
                }
            }
  
          res_->merge_edges();
          return res_;
        }
      };
  
    }
  
    twa_graph_ptr
    complement_semidet(const const_twa_graph_ptr& aut, bool show_names)
    {
      if (!is_semi_deterministic(aut))
        throw std::runtime_error
          ("complement_semidet() requires a semi-deterministic input");
  
      auto ncsb = ncsb_complementation(aut, show_names);
      return ncsb.run();
    }
  
    twa_graph_ptr
    complement(const const_twa_graph_ptr& aut, const output_aborter* aborter)
    {
      if (!aut->is_existential() || is_universal(aut))
        return dualize(aut);
      if (is_very_weak_automaton(aut))
        return remove_alternation(dualize(aut), aborter);
      // Determinize
      spot::option_map m;
      if (aborter)
        {
          m.set("det-max-states", aborter->max_states());
          m.set("det-max-edges", aborter->max_edges());
        }
      if (aut->num_states() > 32)
        {
          m.set("ba-simul", 0);
          m.set("simul", 0);
        }
      spot::postprocessor p(&m);
      p.set_type(spot::postprocessor::Generic);
      p.set_pref(spot::postprocessor::Deterministic);
      p.set_level(spot::postprocessor::Low);
      auto det = p.run(std::const_pointer_cast<twa_graph>(aut));
      if (!det || !is_universal(det))
        return nullptr;
      return dualize(det);
    }
  }
  