// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015 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 "compsusp.hh"
#include "sccfilter.hh"
#include "sccinfo.hh"
#include "twa/twagraph.hh"
#include "ltl2tgba_fm.hh"
#include "minimize.hh"
#include "simulation.hh"
#include "safety.hh"
#include "tl/print.hh"
#include <queue>
#include <sstream>
#include "tl/environment.hh"

namespace spot
{
  namespace
  {
    typedef std::map<ltl::formula, bdd> formula_bdd_map;
    typedef std::vector<ltl::formula> vec;

    // Rewrite the suspendable subformulae "s" of an LTL formula in
    // the form Gg where "g" is an atomic proposition representing
    // "s".  At the same time, populate maps that associate "s" to "g"
    // and vice-versa.
    class ltl_suspender_visitor final
    {
    public:
      typedef std::map<ltl::formula, ltl::formula> fmap_t;
      ltl_suspender_visitor(fmap_t& g2s, fmap_t& a2o, bool oblig)
	: g2s_(g2s), a2o_(a2o), oblig_(oblig)
      {
      }

      ltl::formula
      visit(ltl::formula f)
      {
	switch (ltl::op op = f.kind())
	  {
	  case ltl::op::Or:
	  case ltl::op::And:
	    {
	      vec res;
	      vec oblig;
	      vec susp;
	      unsigned mos = f.size();
	      for (unsigned i = 0; i < mos; ++i)
		{
		  ltl::formula c = f[i];
		  if (c.is_boolean())
		    res.push_back(c);
		  else if (oblig_ && c.is_syntactic_obligation())
		    oblig.push_back(c);
		  else if (c.is_eventual() && c.is_universal())
		    susp.push_back(c);
		  else
		    res.push_back(recurse(c));
		}
	      if (!oblig.empty())
		{
		  res.push_back(recurse(ltl::formula::multop(op, oblig)));
		}
	      if (!susp.empty())
		{
		  ltl::formula o = ltl::formula::multop(op, susp);
		  // Rewrite 'o' as 'G"o"'
		  ltl::formula g = recurse(o);
		  if (op == ltl::op::And)
		    {
		      res.push_back(g);
		    }
		  else
		    {
		      // res || susp -> (res && G![susp]) || G[susp])
		      auto r = ltl::formula::multop(op, res);
		      auto gn = ltl::formula::G(ltl::formula::Not(g[0]));
		      return ltl::formula::Or({ltl::formula::And({r, gn}), g});
		    }
		}
	      return ltl::formula::multop(op, res);
	    }
	    break;
	  default:
	    return f.map([this](ltl::formula f)
			 {
			   return this->recurse(f);
			 });
	  }
      }

      ltl::formula
      recurse(ltl::formula f)
      {
	ltl::formula res;
	if (f.is_boolean())
	  return f;
	if (oblig_ && f.is_syntactic_obligation())
	  {
	    fmap_t::const_iterator i = assoc_.find(f);
	    if (i != assoc_.end())
	      return i->second;

	    std::ostringstream s;
	    print_psl(s << "〈", f) << "〉";
	    res = ltl::formula::ap(s.str());
	    a2o_[res] = f;
	    assoc_[f] = res;
	    return res;
	  }
	if (f.is_eventual() && f.is_universal())
	  {
	    fmap_t::const_iterator i = assoc_.find(f);
	    if (i != assoc_.end())
	      return ltl::formula::G(i->second);

	    std::ostringstream s;
	    print_psl(s << '[', f) << "]$";
	    res = ltl::formula::ap(s.str());
	    g2s_[res] = f;
	    assoc_[f] = res;
	    return ltl::formula::G(res);
	  }
	return visit(f);
      }

    private:
      fmap_t& g2s_;
      fmap_t assoc_;		// This one is only needed by the visitor.
      fmap_t& a2o_;
      bool oblig_;
    };


    typedef std::pair<const state*, const state*> state_pair;

    typedef std::map<state_pair, unsigned> pair_map;
    typedef std::deque<state_pair> pair_queue;

    static
    twa_graph_ptr
    susp_prod(const const_twa_ptr& left, ltl::formula f, bdd v)
    {
      bdd_dict_ptr dict = left->get_dict();
      auto right =
	iterated_simulations(scc_filter(ltl_to_tgba_fm(f, dict, true, true),
					false));

      twa_graph_ptr res = make_twa_graph(dict);
      dict->register_all_variables_of(left, res);
      dict->register_all_variables_of(right, res);
      dict->unregister_variable(bdd_var(v), res);

      const acc_cond& la = left->acc();
      const acc_cond& ra = right->acc();
      res->set_generalized_buchi(la.num_sets() + ra.num_sets());

      acc_cond::mark_t radd = ra.all_sets();

      pair_map seen;
      pair_queue todo;

      state_pair p(left->get_init_state(), nullptr);
      state* ris = right->get_init_state();
      p.second = ris;
      unsigned i = res->new_state();
      seen[p] = i;
      todo.push_back(p);
      res->set_init_state(i);

      while (!todo.empty())
	{
	  p = todo.front();
	  todo.pop_front();
	  const state* ls = p.first;
	  const state* rs = p.second;
	  int src = seen[p];

	  for (auto li: left->succ(ls))
	    {
	      state_pair d(li->current_state(), ris);
	      bdd lc = li->current_condition();

	      twa_succ_iterator* ri = nullptr;
	      // Should we reset the right automaton?
	      if ((lc & v) == lc)
		{
		  // No.
		  ri = right->succ_iter(rs);
		  ri->first();
		}
	      // Yes.  Reset the right automaton.
	      else
		{
		  p.second = ris;
		}

	      // This loops over all the right edges
	      // if RI is defined.  Otherwise this just makes
	      // one iteration as if the right automaton was
	      // looping in state 0 with "true".
	      while (!ri || !ri->done())
		{
		  bdd cond = lc;
		  acc_cond::mark_t racc = radd;
		  if (ri)
		    {
		      cond = lc & ri->current_condition();
		      // Skip incompatible edges.
		      if (cond == bddfalse)
			{
			  ri->next();
			  continue;
			}
		      d.second = ri->current_state();
		      racc = ri->current_acceptance_conditions();
		    }

		  int dest;
		  pair_map::const_iterator i = seen.find(d);
		  if (i != seen.end()) // Is this an existing state?
		    {
		      dest = i->second;
		    }
		  else
		    {
		      dest = res->new_state();
		      seen[d] = dest;
		      todo.push_back(d);
		    }

		  acc_cond::mark_t a =
		    res->acc().join(la, li->current_acceptance_conditions(),
				    ra, racc);
		  res->new_edge(src, dest, bdd_exist(cond, v), a);

		  if (ri)
		    ri->next();
		  else
		    break;
		}
	      if (ri)
		right->release_iter(ri);
	    }
	}
      return res;
    }
  }


  twa_graph_ptr
  compsusp(ltl::formula f, const bdd_dict_ptr& dict,
	   bool no_wdba, bool no_simulation,
	   bool early_susp, bool no_susp_product, bool wdba_smaller,
	   bool oblig)
  {
    ltl_suspender_visitor::fmap_t g2s;
    ltl_suspender_visitor::fmap_t a2o;
    ltl_suspender_visitor v(g2s, a2o, oblig);
    ltl::formula g = v.recurse(f);

    // Translate the patched formula, and remove useless SCCs.
    twa_graph_ptr res =
      scc_filter(ltl_to_tgba_fm(g, dict, true, true, false, false,
				nullptr, nullptr),
		 false);

    if (!no_wdba)
      {
	twa_graph_ptr min = minimize_obligation(res, g,
						nullptr, wdba_smaller);
	if (min != res)
	  {
	    res = min;
	    no_simulation = true;
	  }
      }

    if (!no_simulation)
      res = iterated_simulations(res);

    // Create a map of suspended formulae to BDD variables.
    spot::formula_bdd_map susp;
    for (auto& it: g2s)
      {
	auto j = dict->var_map.find(it.first);
	// If no BDD variable of this suspended formula exist in the
	// BDD dict, it means the suspended subformulae was never
	// actually used in the automaton.  Just skip it.  FIXME: It
	// would be better if we had a way to check that the variable
	// is used in this automaton, and not in some automaton
	// (sharing the same dictionary.)
	if (j != dict->var_map.end())
	  susp[it.second] = bdd_ithvar(j->second);
      }

    // Remove suspendable formulae from non-accepting SCCs.
    bdd suspvars = bddtrue;
    for (formula_bdd_map::const_iterator i = susp.begin();
	 i != susp.end(); ++i)
      suspvars &= i->second;

    bdd allaccap = bddtrue; // set of atomic prop used in accepting SCCs.
    {
      scc_info si(res);

      // Restrict suspvars to the set of suspension labels that occur
      // in accepting SCC.
      unsigned sn = si.scc_count();
      for (unsigned n = 0; n < sn; n++)
	if (si.is_accepting_scc(n))
	  allaccap &= si.scc_ap_support(n);

      bdd ignored = bdd_exist(suspvars, allaccap);
      suspvars = bdd_existcomp(suspvars, allaccap);
      res = scc_filter_susp(res, false, suspvars, ignored, early_susp, &si);
    }

    // Do we need to synchronize any suspended formula?
    if (!susp.empty() && !no_susp_product)
      for (formula_bdd_map::const_iterator i = susp.begin();
	   i != susp.end(); ++i)
	if ((allaccap & i->second) == allaccap)
	  res = susp_prod(res, i->first, i->second);

    return res;
  }
}