// -*- coding: utf-8 -*-
// Copyright (C) 2012 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 2 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 Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

#include "common_sys.hh"

#include <cstdlib>
#include <vector>
#include <string>
#include <iostream>
#include <fstream>
#include <argp.h>
#include <cstring>
#include "progname.h"
#include "error.h"

#include "common_output.hh"
#include "common_cout.hh"
#include "common_r.hh"

#include "misc/_config.h"
#include "misc/hash.hh"
#include "ltlparse/public.hh"
#include "ltlvisit/simplify.hh"
#include "ltlvisit/length.hh"
#include "ltlvisit/relabel.hh"
#include "ltlvisit/wmunabbrev.hh"
#include "ltlast/unop.hh"
#include "ltlast/multop.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/minimize.hh"
#include "tgbaalgos/safety.hh"

const char* argp_program_version = "\
ltlfilter (" SPOT_PACKAGE_STRING ")\n\
\n\
Copyright (C) 2012  Laboratoire de Recherche et Développement de l'Epita.\n\
This is free software; see the source for copying conditions.  There is NO\n\
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE,\n\
to the extent permitted by law.";

const char* argp_program_bug_address = "<" SPOT_PACKAGE_BUGREPORT ">";

const char argp_program_doc[] ="\
Read a list of formulas and output them back after some optional processing.\v\
Exit status:\n\
  0  if some formulas were output (skipped syntax errors do not count)\n\
  1  if no formula were output (no match)\n\
  2  if any error has been reported";

#define OPT_SKIP_ERRORS 2
#define OPT_DROP_ERRORS 3
#define OPT_NNF 4
#define OPT_LTL 5
#define OPT_PSL 6
#define OPT_NOX 7
#define OPT_BOOLEAN 8
#define OPT_EVENTUAL 9
#define OPT_UNIVERSAL 10
#define OPT_SYNTACTIC_SAFETY 11
#define OPT_SYNTACTIC_GUARANTEE 12
#define OPT_SYNTACTIC_OBLIGATION 13
#define OPT_SYNTACTIC_RECURRENCE 14
#define OPT_SYNTACTIC_PERSISTENCE 15
#define OPT_SAFETY 16
#define OPT_GUARANTEE 17
#define OPT_OBLIGATION 18
#define OPT_SIZE_MIN 19
#define OPT_SIZE_MAX 20
#define OPT_BSIZE_MIN 21
#define OPT_BSIZE_MAX 22
#define OPT_IMPLIED_BY 23
#define OPT_IMPLY 24
#define OPT_EQUIVALENT_TO 25
#define OPT_LBT 26
#define OPT_RELABEL 27
#define OPT_REMOVE_WM 28

static const argp_option options[] =
  {
    /**************************************************/
    { 0, 0, 0, 0, "Input options:", 1 },
    { "formula", 'f', "STRING", 0, "process the formula STRING", 0 },
    { "file", 'F', "FILENAME", 0,
      "process each line of FILENAME as a formula", 0 },
    { "lbt-input", OPT_LBT, 0, 0,
      "read all formulas using LBT's prefix syntax", 0 },
    { 0, 0, 0, 0, "Error handling:", 2 },
    { "skip-errors", OPT_SKIP_ERRORS, 0, 0,
      "output erroneous lines as-is without processing", 0 },
    { "drop-errors", OPT_DROP_ERRORS, 0, 0,
      "discard erroneous lines (default)", 0 },
    { "quiet", 'q', 0, 0, "do not report syntax errors", 0 },
    /**************************************************/
    { 0, 0, 0, 0, "Transformation options:", 3 },
    { "negate", 'n', 0, 0, "negate each formula", 0 },
    { "nnf", OPT_NNF, 0, 0, "rewrite formulas in negative normal form", 0 },
    { "relabel", OPT_RELABEL, "abc|pnn", OPTION_ARG_OPTIONAL,
      "relabel all atomic propositions, alphabetically unless " \
      "specified otherwise", 0 },
    { "remove-wm", OPT_REMOVE_WM, 0, 0,
      "rewrite operators W and M using U and R", 0 },
    DECLARE_OPT_R,
    LEVEL_DOC(4),
    /**************************************************/
    { 0, 0, 0, 0,
      "Filtering options (matching is done after transformation):", 5 },
    { "ltl", OPT_LTL, 0, 0, "match LTL formulas", 0 },
    { "psl", OPT_PSL, 0, 0, "match PSL formulas", 0 },
    { "nox", OPT_NOX, 0, 0, "match X-free formulas", 0 },
    { "boolean", OPT_BOOLEAN, 0, 0, "match Boolean formulas", 0 },
    { "eventual", OPT_EVENTUAL, 0, 0, "match pure eventualities", 0 },
    { "universal", OPT_UNIVERSAL, 0, 0, "match purely universal formulas", 0 },
    { "syntactic-safety", OPT_SYNTACTIC_SAFETY, 0, 0,
      "match syntactic-safety formulas", 0 },
    { "syntactic-guarantee", OPT_SYNTACTIC_GUARANTEE, 0, 0,
      "match syntactic-guarantee formulas", 0 },
    { "syntactic-obligation", OPT_SYNTACTIC_OBLIGATION, 0, 0,
      "match syntactic-obligation formulas", 0 },
    { "syntactic-recurrence", OPT_SYNTACTIC_RECURRENCE, 0, 0,
      "match syntactic-recurrence formulas", 0 },
    { "syntactic-persistence", OPT_SYNTACTIC_PERSISTENCE, 0, 0,
      "match syntactic-persistence formulas", 0 },
    { "safety", OPT_SAFETY, 0, 0,
      "match safety formulas (even pathological)", 0 },
    { "guarantee", OPT_GUARANTEE, 0, 0,
      "match guarantee formulas (even pathological)", 0 },
    { "obligation", OPT_OBLIGATION, 0, 0,
      "match obligation formulas (even pathological)", 0 },
    { "size-max", OPT_SIZE_MAX, "INT", 0,
      "match formulas with size <= INT", 0 },
    { "size-min", OPT_SIZE_MIN, "INT", 0,
      "match formulas with size >= INT", 0 },
    { "bsize-max", OPT_BSIZE_MAX, "INT", 0,
      "match formulas with Boolean size <= INT", 0 },
    { "bsize-min", OPT_BSIZE_MIN, "INT", 0,
      "match formulas with Boolean size >= INT", 0 },
    { "implied-by", OPT_IMPLIED_BY, "FORMULA", 0,
      "match formulas implied by FORMULA", 0 },
    { "imply", OPT_IMPLY, "FORMULA", 0,
      "match formulas implying FORMULA", 0 },
    { "equivalent-to", OPT_EQUIVALENT_TO, "FORMULA", 0,
      "match formulas equivalent to FORMULA", 0 },
    { "invert-match", 'v', 0, 0, "select non-matching formulas", 0},
    { "unique", 'u', 0, 0,
      "drop formulas that have already been output (not affected by -v)", 0 },
    /**************************************************/
    { 0, 0, 0, 0, "Output options:", -20 },
    { 0, 0, 0, 0, "Miscellaneous options:", -1 },
    { 0, 0, 0, 0, 0, 0 }
  };

const struct argp_child children[] =
  {
    { &output_argp, 0, 0, -20 },
    { 0, 0, 0, 0 }
  };

struct job
{
  const char* str;
  bool file_p;	// true if str is a filename, false if it is a formula

  job(const char* str, bool file_p)
    : str(str), file_p(file_p)
  {
  }
};

typedef std::vector<job> jobs_t;
static jobs_t jobs;

static bool one_match = false;

enum error_style_t { drop_errors, skip_errors };
static error_style_t error_style = drop_errors;
static bool lbt = false;
static bool quiet = false;
static bool nnf = false;
static bool negate = false;
static bool unique = false;
static bool psl = false;
static bool ltl = false;
static bool nox = false;
static bool invert = false;
static bool boolean = false;
static bool universal = false;
static bool eventual = false;
static bool syntactic_safety = false;
static bool syntactic_guarantee = false;
static bool syntactic_obligation = false;
static bool syntactic_recurrence = false;
static bool syntactic_persistence = false;
static bool safety = false;
static bool guarantee = false;
static bool obligation = false;
static int size_min = -1;
static int size_max = -1;
static int bsize_min = -1;
static int bsize_max = -1;
static bool relabeling = false;
static spot::ltl::relabeling_style style = spot::ltl::Abc;
static bool remove_wm = false;

static const spot::ltl::formula* implied_by = 0;
static const spot::ltl::formula* imply = 0;
static const spot::ltl::formula* equivalent_to = 0;

static int
to_int(const char* s)
{
  char* endptr;
  int res = strtol(s, &endptr, 10);
  if (*endptr)
    error(2, 0, "failed to parse '%s' as an integer.", s);
  return res;
}


static const spot::ltl::formula*
parse_formula_arg(const std::string& input)
{
  spot::ltl::parse_error_list pel;
  const spot::ltl::formula* f = spot::ltl::parse(input, pel);
  if (spot::ltl::format_parse_errors(std::cerr, input, pel))
    error(2, 0, "parse error when parsing an argument");
  return f;
}



static int
parse_opt(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case 'f':
      jobs.push_back(job(arg, false));
      break;
    case 'F':
      jobs.push_back(job(arg, true));
      break;
    case 'n':
      negate = true;
      break;
    case 'q':
      quiet = true;
      break;
    case OPT_R:
      parse_r(arg);
      break;
    case 'u':
      unique = true;
      break;
    case 'v':
      invert = true;
      break;
    case ARGP_KEY_ARG:
      // FIXME: use stat() to distinguish filename from string?
      jobs.push_back(job(arg, true));
      break;
    case OPT_BOOLEAN:
      boolean = true;
      break;
    case OPT_BSIZE_MIN:
      bsize_min = to_int(arg);
      break;
    case OPT_BSIZE_MAX:
      bsize_max = to_int(arg);
      break;
    case OPT_DROP_ERRORS:
      error_style = drop_errors;
      break;
    case OPT_EQUIVALENT_TO:
      {
	if (equivalent_to)
	  error(2, 0, "only one --equivalent-to option can be given");
	equivalent_to = parse_formula_arg(arg);
	break;
      }
    case OPT_GUARANTEE:
      guarantee = obligation = true;
      break;
    case OPT_IMPLIED_BY:
      {
	const spot::ltl::formula* i = parse_formula_arg(arg);
	// a→c∧b→c ≡ (a∨b)→c
	implied_by =
	  spot::ltl::multop::instance(spot::ltl::multop::Or, implied_by, i);
	break;
      }
    case OPT_IMPLY:
      {
	// a→b∧a→c ≡ a→(b∧c)
	const spot::ltl::formula* i = parse_formula_arg(arg);
	imply =
	  spot::ltl::multop::instance(spot::ltl::multop::And, imply, i);
	break;
      }
    case OPT_LBT:
      lbt = true;
    case OPT_LTL:
      ltl = true;
      break;
    case OPT_NNF:
      nnf = true;
      break;
    case OPT_NOX:
      nox = true;
      break;
    case OPT_OBLIGATION:
      obligation = true;
      break;
    case OPT_PSL:
      psl = true;
      break;
    case OPT_RELABEL:
      relabeling = true;
      if (!arg || !strncasecmp(arg, "abc", 6))
	style = spot::ltl::Abc;
      else if (!strncasecmp(arg, "pnn", 4))
	style = spot::ltl::Pnn;
      else
	error(2, 0, "invalid argument for --relabel: '%s'", arg);
      break;
    case OPT_REMOVE_WM:
      remove_wm = true;
      break;
    case OPT_SAFETY:
      safety = obligation = true;
      break;
    case OPT_SIZE_MIN:
      size_min = to_int(arg);
      break;
    case OPT_SIZE_MAX:
      size_max = to_int(arg);
      break;
    case OPT_SKIP_ERRORS:
      error_style = skip_errors;
      break;
    case OPT_SYNTACTIC_SAFETY:
      syntactic_safety = true;
      break;
    case OPT_SYNTACTIC_GUARANTEE:
      syntactic_guarantee = true;
      break;
    case OPT_SYNTACTIC_OBLIGATION:
      syntactic_obligation = true;
      break;
    case OPT_SYNTACTIC_RECURRENCE:
      syntactic_recurrence = true;
      break;
    case OPT_SYNTACTIC_PERSISTENCE:
      syntactic_persistence = true;
      break;
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

typedef Sgi::hash_set<const spot::ltl::formula*,
		      const spot::ptr_hash<const spot::ltl::formula> > fset_t;

namespace
{
  class ltl_processor
  {
  public:
    spot::ltl::ltl_simplifier& simpl;
    fset_t unique_set;

    ltl_processor(spot::ltl::ltl_simplifier& simpl)
    : simpl(simpl)
    {
    }

    int
    process_formula(const std::string& input,
		    const char* filename = 0, int linenum = 0)
    {
      spot::ltl::parse_error_list pel;
      const spot::ltl::formula* f;
      if (lbt)
	f = spot::ltl::parse_lbt(input, pel);
      else
	f = spot::ltl::parse(input, pel);

      if (!f || pel.size() > 0)
	  {
	    if (!quiet)
	      {
		if (filename)
		  error_at_line(0, 0, filename, linenum, "parse error:");
		spot::ltl::format_parse_errors(std::cerr, input, pel);
	      }

	    if (f)
	      f->destroy();

	    if (error_style == skip_errors)
	      std::cout << input << std::endl;
	    else
	      assert(error_style == drop_errors);
	    check_cout();
	    return !quiet;
	  }

      if (negate)
	f = spot::ltl::unop::instance(spot::ltl::unop::Not, f);

      if (simplification_level)
	{
	  const spot::ltl::formula* res = simpl.simplify(f);
	  f->destroy();
	  f = res;
	}

      if (nnf)
	{
	  const spot::ltl::formula* res = simpl.negative_normal_form(f);
	  f->destroy();
	  f = res;
	}

      if (relabeling)
	{
	  const spot::ltl::formula* res = spot::ltl::relabel(f, style);
	  f->destroy();
	  f = res;
	}

      if (remove_wm)
	{
	  const spot::ltl::formula* res = spot::ltl::unabbreviate_wm(f);
	  f->destroy();
	  f = res;
	}

      bool matched = true;

      matched &= !ltl || f->is_ltl_formula();
      matched &= !psl || f->is_psl_formula();
      matched &= !nox || f->is_X_free();
      matched &= !boolean || f->is_boolean();
      matched &= !universal || f->is_universal();
      matched &= !eventual || f->is_eventual();
      matched &= !syntactic_safety || f->is_syntactic_safety();
      matched &= !syntactic_guarantee || f->is_syntactic_guarantee();
      matched &= !syntactic_obligation || f->is_syntactic_obligation();
      matched &= !syntactic_recurrence || f->is_syntactic_recurrence();
      matched &= !syntactic_persistence || f->is_syntactic_persistence();

      if (matched && (size_min > 0 || size_max >= 0))
	{
	  int l = spot::ltl::length(f);
	  matched &= (size_min <= 0) || (l >= size_min);
	  matched &= (size_max < 0) || (l <= size_max);
	}

      if (matched && (bsize_min > 0 || bsize_max >= 0))
	{
	  int l = spot::ltl::length_boolone(f);
	  matched &= (bsize_min <= 0) || (l >= bsize_min);
	  matched &= (bsize_max < 0) || (l <= bsize_max);
	}

      matched &= !implied_by || simpl.implication(implied_by, f);
      matched &= !imply || simpl.implication(f, imply);
      matched &= !equivalent_to || simpl.are_equivalent(f, equivalent_to);

      // Match obligations and subclasses using WDBA minimization.
      // Because this is costly, we compute it later, so that we don't
      // have to compute it on formulas that have been discarded for
      // other reasons.
      if (matched && obligation)
	{
	  spot::tgba* aut = ltl_to_tgba_fm(f, simpl.get_dict());
	  spot::tgba* min = minimize_obligation(aut, f);
	  assert(min);
	  if (aut == min)
	    {
	      // Not an obligation
	      matched = false;
	    }
	  else
	    {
	      matched &= !guarantee || is_guarantee_automaton(min);
	      matched &= !safety || is_safety_mwdba(min);
	      delete min;
	    }
	  delete aut;
	}

      matched ^= invert;

      if (unique)
	{
	  if (unique_set.insert(f).second)
	    f->clone();
	  else
	    matched = false;
	}

      if (matched)
	{
	  one_match = true;
	  output_formula(f, filename, linenum);
	}
      f->destroy();
      return 0;
    }

    int
    process_stream(std::istream& is, const char* filename)
    {
      int error = 0;
      int linenum = 0;
      std::string line;
      while (std::getline(is, line))
	error |= process_formula(line, filename, ++linenum);
      return error;
    }

    int
    process_file(const char* filename)
    {
      // Special case for stdin.
      if (filename[0] == '-' && filename[1] == 0)
	return process_stream(std::cin, filename);

      errno = 0;
      std::ifstream input(filename);
      if (!input)
	error(2, errno, "cannot open '%s'", filename);
      return process_stream(input, filename);
    }
  };
}

static int
run_jobs()
{
  spot::ltl::ltl_simplifier simpl(simplifier_options());
  ltl_processor processor(simpl);

  int nerror = 0;
  jobs_t::const_iterator i;
  for (i = jobs.begin(); i != jobs.end(); ++i)
    {
      if (!i->file_p)
	nerror |= processor.process_formula(i->str);
      else
	nerror |= processor.process_file(i->str);
    }
  if (nerror)
    return 2;
  return one_match ? 0 : 1;
}

int
main(int argc, char** argv)
{
  set_program_name(argv[0]);
  // Simplify the program name, because argp() uses it to report errors
  // and display help text.
  argv[0] = const_cast<char*>(program_name);

  const argp ap = { options, parse_opt, "[FILENAME...]",
		    argp_program_doc, children, 0, 0 };

  if (int err = argp_parse(&ap, argc, argv, 0, 0, 0))
    exit(err);

  if (jobs.empty())
    jobs.push_back(job("-", 1));

  return run_jobs();
}