// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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.

#ifndef SSP
#include "gspn.hh"
#define MIN_ARG 3
#else
#include "ssp.hh"
#define MIN_ARG 4
#include "tgba/tgbaexplicit.hh"
#include "tgbaparse/public.hh"
#endif
#include "ltlparse/public.hh"
#include "ltlvisit/destroy.hh"
#include "tgba/tgbatba.hh"
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/ltl2tgba_lacim.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/magic.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"


void
syntax(char* prog)
{
  std::cerr << "Usage: "<< prog
#ifndef SSP
	    << " [OPTIONS...] model formula props..."   << std::endl
#else
	    << " [OPTIONS...] model formula automata props..."   << std::endl
#endif
	    << std::endl
	    << "  -c  compute an example" << std::endl
	    << "      (instead of just checking for emptiness)" << std::endl
	    << std::endl
#ifndef SSP
            << "  -d DEAD" << std::endl
            << "      use DEAD as property for marking dead states"
	    << " (by default DEAD=true)" << std::endl
#endif

	    << "  -e  use Couvreur's emptiness-check (default)" << std::endl
	    << "  -e2 use Couvreur's emptiness-check's shy variant" << std::endl
#ifdef SSP
	    << "  -e3 use semi-d. incl. Couvreur's emptiness-check"
	    << std::endl
	    << "  -e4 use semi-d. incl. Couvreur's emptiness-check's "
	    << "shy variant"
	    << std::endl
	    << "  -e5 use d. incl. Couvreur's emptiness-check's shy variant"
	    << std::endl
#endif
	    << "  -m  degeneralize and perform a magic-search" << std::endl
	    << std::endl
            << "  -l  use Couvreur's LaCIM algorithm for translation (default)"
	    << std::endl
            << "  -f  use Couvreur's FM algorithm for translation" << std::endl
	    << "  -P  do not project example on model" << std::endl;
  exit(2);
}

int
main(int argc, char **argv)
  try
    {
      int formula_index = 1;
      enum { Couvreur, Couvreur2, Couvreur3,
	     Couvreur4, Couvreur5, Magic } check = Couvreur;
      enum { Lacim, Fm } trans = Lacim;
      bool compute_counter_example = false;
      bool proj = true;
      std::string dead = "true";

      spot::ltl::declarative_environment env;

      while (formula_index < argc && *argv[formula_index] == '-')
	{
	  if (!strcmp(argv[formula_index], "-c"))
	    {
	      compute_counter_example = true;
	    }
#ifndef SSP
	  else if (!strcmp(argv[formula_index], "-d"))
	    {
	      if (formula_index + 1 >= argc)
		syntax(argv[0]);
	      dead = argv[++formula_index];
	      if (strcasecmp(dead.c_str(), "true")
		  && strcasecmp(dead.c_str(), "false"))
		env.declare(dead);
	    }
#endif
	  else if (!strcmp(argv[formula_index], "-e"))
	    {
	      check = Couvreur;
	    }
	  else if (!strcmp(argv[formula_index], "-e2"))
	    {
	      check = Couvreur2;
	    }
#ifdef SSP
	  else if (!strcmp(argv[formula_index], "-e3"))
	    {
	      check = Couvreur3;
	    }
	  else if (!strcmp(argv[formula_index], "-e4"))
	    {
	      check = Couvreur4;
	    }
	  else if (!strcmp(argv[formula_index], "-e5"))
	    {
	      check = Couvreur5;
	    }
#endif
	  else if (!strcmp(argv[formula_index], "-m"))
	    {
	      check = Magic;
	    }
	  else if (!strcmp(argv[formula_index], "-l"))
	    {
	      trans = Lacim;
	    }
	  else if (!strcmp(argv[formula_index], "-f"))
	    {
	      trans = Fm;
	    }
	  else if (!strcmp(argv[formula_index], "-P"))
	    {
	      proj = 0;
	    }
	  else
	    {
	      syntax(argv[0]);
	    }
	  ++formula_index;
	}
      if (argc < formula_index + MIN_ARG)
	syntax(argv[0]);


      while (argc >= formula_index + MIN_ARG)
	{
	  env.declare(argv[argc - 1]);
	  --argc;
	}

      spot::ltl::parse_error_list pel;
      spot::ltl::formula* f = spot::ltl::parse(argv[formula_index + 1],
					       pel, env);

      if (spot::ltl::format_parse_errors(std::cerr,
					 argv[formula_index + 1], pel))
	exit(2);

      argv[1] = argv[formula_index];
      spot::bdd_dict* dict = new spot::bdd_dict();

#if SSP
      bool inclusion = (check != Couvreur && check != Couvreur2);
      spot::gspn_ssp_interface gspn(2, argv, dict, env, inclusion);

      spot::tgba_parse_error_list pel1;
      spot::tgba_explicit* control = spot::tgba_parse(argv[formula_index + 2],
						      pel1, dict, env);
      if (spot::format_tgba_parse_errors(std::cerr, pel1))
	return 2;
#else
      spot::gspn_interface gspn(2, argv, dict, env, dead);
#endif

      spot::tgba* a_f = 0;
      switch (trans)
	{
	case Fm:
	  a_f = spot::ltl_to_tgba_fm(f, dict);
	  break;
	case Lacim:
	  a_f = spot::ltl_to_tgba_lacim(f, dict);
	  break;
	}
      spot::ltl::destroy(f);

#ifndef SSP
      spot::tgba* model        = gspn.automaton();
      spot::tgba_product* prod = new spot::tgba_product(model, a_f);
#else
      spot::tgba_product* ca = new spot::tgba_product(control, a_f);
      spot::tgba* model      = gspn.automaton(ca);
      spot::tgba* prod = model;
#endif

      switch (check)
	{
	case Couvreur:
	case Couvreur2:
	case Couvreur3:
	case Couvreur4:
	case Couvreur5:
	  {
	    spot::couvreur99_check* ec;

	    switch (check)
	      {
	      case Couvreur:
		ec = new spot::couvreur99_check(prod);
		break;
	      case Couvreur2:
		ec = new spot::couvreur99_check_shy(prod);
		break;
#ifdef SSP
	      case Couvreur3:
		ec = spot::couvreur99_check_ssp_semi(prod);
		break;
	      case Couvreur4:
		ec = spot::couvreur99_check_ssp_shy_semi(prod);
		break;
	      case Couvreur5:
		ec = spot::couvreur99_check_ssp_shy(prod);
		break;
#endif
	      default:
		assert(0);
		// Assign something so that GCC does not complains
		// EC might be used uninitialized if assert is disabled.
		ec = 0;
	      }

	    spot::emptiness_check_result* res = ec->check();
	    const spot::couvreur99_check_status* ecs = ec->result();
	    if (res)
	      {
		if (compute_counter_example)
		  {
		    spot::couvreur99_check_result* ce;
#ifndef SSP
		    ce = new spot::couvreur99_check_result(ecs);
#else
		    switch (check)
		      {
		      case Couvreur:
		      case Couvreur2:
		      case Couvreur5:
			ce = new spot::couvreur99_check_result(ecs);
			break;
		      default:
			ce = spot::counter_example_ssp(ecs);
		      }
#endif
		    spot::tgba_run* run = ce->accepting_run();
		    // FIXME: reimplement the projection
		    spot::print_tgba_run(std::cout, prod, run);
		    ce->print_stats(std::cout);
		    delete run;
		    delete ce;
		  }
		else
		  {
		    std::cout << "non empty" << std::endl;
		    ecs->print_stats(std::cout);
		  }
		delete res;
	      }
	    else
	      {
		std::cout << "empty" << std::endl;
		ecs->print_stats(std::cout);
	      }
	    std::cout << std::endl;
	    delete ec;
	    if (res)
	      exit(1);
	  }
	  break;
	case Magic:
	  {
	    spot::tgba_tba_proxy* d  = new spot::tgba_tba_proxy(prod);
	    spot::magic_search ms(d);

	    spot::emptiness_check_result* res = ms.check();
	    if (res)
	      {
		if (compute_counter_example)
		  {
		    spot::tgba_run* run = res->accepting_run();
		    // FIXME: reimplement the projection
		    spot::print_tgba_run(std::cout, prod, run);
		    delete run;
		  }
		else
		  std::cout << "non-empty" << std::endl;
		delete res;
		exit(1);
	      }
	    else
	      {
		std::cout << "empty" << std::endl;
	      }
	    delete d;
	  }
	}
#ifndef SSP
      delete prod;
      delete model;
#else
      delete model;
      delete control;
#endif
      delete a_f;
      delete dict;
    }
  catch (spot::gspn_exeption e)
    {
      std::cerr << e << std::endl;
      throw;
    }