// Copyright (C) 2004, 2005  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.

#include <cassert>
#include <cstdlib>
#include <iostream>
#include <iomanip>
#include <sstream>
#include <fstream>
#include <string>
#include <utility>
#include <set>
#include <string>
#include "ltlparse/public.hh"
#include "ltlvisit/apcollect.hh"
#include "ltlvisit/destroy.hh"
#include "ltlvisit/randomltl.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/length.hh"
#include "ltlvisit/reduce.hh"
#include "tgbaalgos/randomgraph.hh"
#include "tgbaalgos/save.hh"
#include "tgbaalgos/stats.hh"
#include "ltlenv/defaultenv.hh"
#include "ltlast/atomic_prop.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaparse/public.hh"
#include "misc/random.hh"
#include "tgba/tgbatba.hh"
#include "tgba/tgbaproduct.hh"
#include "misc/timer.hh"

#include "tgbaalgos/ltl2tgba_fm.hh"

#include "tgbaalgos/emptiness.hh"
#include "tgbaalgos/emptiness_stats.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gv04.hh"
#include "tgbaalgos/magic.hh"
#include "tgbaalgos/reducerun.hh"
#include "tgbaalgos/se05.hh"
#include "tgbaalgos/tau03.hh"
#include "tgbaalgos/tau03opt.hh"
#include "tgbaalgos/replayrun.hh"


spot::emptiness_check*
couvreur99_cons(const spot::tgba* a)
{
  return new spot::couvreur99_check(a);
}

spot::emptiness_check*
couvreur99_shy_cons(const spot::tgba* a)
{
  return new spot::couvreur99_check_shy(a);
}

spot::emptiness_check*
couvreur99_shy_minus_cons(const spot::tgba* a)
{
  return new spot::couvreur99_check_shy(a, false);
}

spot::emptiness_check*
bsh_ms_cons(const spot::tgba* a)
{
  return spot::bit_state_hashing_magic_search(a, 4096);
}

spot::emptiness_check*
bsh_se05_cons(const spot::tgba* a)
{
  return spot::bit_state_hashing_se05_search(a, 4096);
}

struct ec_algo
{
  const char* name;
  spot::emptiness_check* (*construct)(const spot::tgba*);
  unsigned int min_acc;
  unsigned int max_acc;
  bool safe;
};

ec_algo ec_algos[] =
  {
    { "Cou99",      couvreur99_cons,                 0, -1U, true },
    { "Cou99_shy-", couvreur99_shy_minus_cons,       0, -1U, true },
    { "Cou99_shy",  couvreur99_shy_cons,             0, -1U, true },
    { "CVWY90",     spot::explicit_magic_search,     0,   1, true },
    { "CVWY90_bsh", bsh_ms_cons,                     0,   1, false },
    { "GV04",       spot::explicit_gv04_check,       0,   1, true },
    { "SE05",       spot::explicit_se05_search,      0,   1, true },
    { "SE05_bsh",   bsh_se05_cons,                   0,   1, false },
    { "Tau03",      spot::explicit_tau03_search,     1, -1U, true },
    { "Tau03_opt",  spot::explicit_tau03_opt_search, 0, -1U, true },
  };

spot::emptiness_check*
cons_emptiness_check(int num, const spot::tgba* a,
		     const spot::tgba* degen, unsigned int n_acc)
{
  if (n_acc < ec_algos[num].min_acc || n_acc > ec_algos[num].max_acc)
    a = degen;
  if (a)
    return ec_algos[num].construct(a);
  return 0;
}

void
syntax(char* prog)
{
  std::cerr << "Usage: "<< prog << " [OPTIONS...] PROPS..." << std::endl
	    << std::endl
	    << "Options:" << std::endl
	    << "  -0      suppress default output, just generate the graph"
	    << " in memory" << std::endl
	    << "  -1    produce minimal output dedicated to the paper"
	    << "  -a N F  number of acceptance conditions and probability that"
	    << " one is true" << std::endl
	    << "            [0 0.0]" << std::endl
	    << "  -d F    density of the graph [0.2]" << std::endl
	    << "  -dp     dump priorities, do not generate any formula"
	    << std::endl
	    << "  -D      degeneralize TGBA for emptiness-check algorithms that"
	    << " would" << std::endl
	    << "            otherwise be skipped (implies -e)" << std::endl
	    << "  -e N    compare result of all "
	    << "emptiness checks on N randomly generated graphs" << std::endl
	    << "  -f N    the size of the formula [15]" << std::endl
	    << "  -F N    number of formulae to generate [0]" << std::endl
	    << "  -g      output in dot format" << std::endl
	    << "  -i FILE do not generate formulae, read them from FILE"
            << std::endl
	    << "  -l N    simplify formulae using all available reductions"
	    << " and reject those" << std::endl
	    << "            strictly smaller than N" << std::endl
	    << "  -m      try to reduce runs, in a second pass (implies -r)"
	    << std::endl
	    << "  -n N    number of nodes of the graph [20]" << std::endl
	    << "  -O ALGO run Only ALGO" << std::endl
	    << "  -p S    priorities to use" << std::endl
	    << "  -r      compute and replay acceptance runs (implies -e)"
	    << std::endl
	    << "  -R N    repeat each emptiness-check and accepting run "
	    << "computation N times" << std::endl
	    << "  -s N    seed for the random number generator" << std::endl
	    << "  -t F    probability of the atomic propositions to be true"
	    << " [0.5]" << std::endl
	    << "  -u      generate unique formulae"
	    << std::endl
	    << "  -z      display statistics about computed accepting runs"
	    << std::endl
	    << "  -Z      like -z, but print extra statistics after the run"
	    << " of each algorithm" << std::endl
	    << "Where:" << std::endl
	    << "  F      are floats between 0.0 and 1.0 inclusive" << std::endl
	    << "  E      are floating values" << std::endl
	    << "  S      are `KEY=E, KEY=E, ...' strings" << std::endl
	    << "  N      are positive integers" << std::endl
	    << "  PROPS  are the atomic properties to use on transitions"
	    << std::endl
	    << "Use -dp to see the list of KEYs." << std::endl;
  exit(2);
}

int
to_int(const char* s)
{
  char* endptr;
  int res = strtol(s, &endptr, 10);
  if (*endptr)
    {
      std::cerr << "Failed to parse `" << s << "' as an integer." << std::endl;
      exit(1);
    }
  return res;
}

float
to_float(const char* s)
{
  char* endptr;
  // Do not use strtof(), it does not exist on Solaris 9.
  float res = strtod(s, &endptr);
  if (*endptr)
    {
      std::cerr << "Failed to parse `" << s << "' as a float." << std::endl;
      exit(1);
    }
  return res;
}

struct ec_stat
{
  int max_tgba_states;
  int tot_tgba_states;
  int min_states;
  int max_states;
  int tot_states;
  int min_transitions;
  int max_transitions;
  int tot_transitions;
  int min_max_depth;
  int max_max_depth;
  int tot_max_depth;
  int n;

  ec_stat()
    : n(0)
  {
  }

  void
  count(const spot::ec_statistics* ec)
  {
    int s = ec->states();
    int t = ec->transitions();
    int m = ec->max_depth();

    if (n++)
      {
	min_states = std::min(min_states, s);
	max_states = std::max(max_states, s);
	tot_states += s;
	min_transitions = std::min(min_transitions, t);
	max_transitions = std::max(max_transitions, t);
	tot_transitions += t;
	min_max_depth = std::min(min_max_depth, m);
	max_max_depth = std::max(max_max_depth, m);
	tot_max_depth += m;
      }
    else
      {
	min_states = max_states = tot_states = s;
	min_transitions = max_transitions = tot_transitions = t;
	min_max_depth = max_max_depth = tot_max_depth = m;
      }
  }
};

struct ec_ratio_stat
{
  float min_states;
  float max_states;
  float tot_states;
  float min_transitions;
  float max_transitions;
  float tot_transitions;
  float min_depth;
  float max_depth;
  float tot_depth;
  int n;

  ec_ratio_stat()
    : n(0)
  {
  }

  void
  count(const spot::ec_statistics* ec, const spot::tgba* a)
  {
    spot::tgba_statistics a_size = spot::stats_reachable(a);
    float ms = ec->states() / static_cast<float>(a_size.states);
    float mt = ec->transitions() / static_cast<float>(a_size.transitions);
    float mm = ec->max_depth() / static_cast<float>(a_size.states);

    if (n++)
      {
        min_states = std::min(min_states, ms);
        max_states = std::max(max_states, ms);
        tot_states += ms;
        min_transitions = std::min(min_transitions, mt);
        max_transitions = std::max(max_transitions, mt);
        tot_transitions += mt;
        min_depth = std::min(min_depth, mm);
        max_depth = std::max(max_depth, mm);
        tot_depth += mm;
      }
    else
      {
        min_states = max_states = tot_states = ms;
        min_transitions = max_transitions = tot_transitions = mt;
        min_depth = max_depth = tot_depth = mm;
      }
  }
};

struct acss_stat
{
  int min_states;
  int max_states;
  int tot_states;
  int n;

  acss_stat()
    : n(0)
  {
  }

  void
  count(const spot::acss_statistics* acss)
  {
    int s = acss->acss_states();
    if (n++)
      {
	min_states = std::min(min_states, s);
	max_states = std::max(max_states, s);
	tot_states += s;
      }
    else
      {
	min_states = max_states = tot_states = s;
      }
  }
};

struct acss_ratio_stat
{
  float min_states;
  float max_states;
  float tot_states;
  int n;

  acss_ratio_stat()
    : n(0)
  {
  }

  void
  count(const spot::acss_statistics* acss, const spot::tgba* a)
  {
    spot::tgba_statistics a_size = spot::stats_reachable(a);
    float ms = acss->acss_states() / static_cast<float>(a_size.states);
    if (n++)
      {
        min_states = std::min(min_states, ms);
        max_states = std::max(max_states, ms);
        tot_states += ms;
      }
    else
      {
        min_states = max_states = tot_states = ms;
      }
  }
};

struct ars_stat
{
  int min_prefix_states;
  int max_prefix_states;
  int tot_prefix_states;
  int min_cycle_states;
  int max_cycle_states;
  int tot_cycle_states;
  int n;

  ars_stat()
    : n(0)
  {
  }

  void
  count(const spot::ars_statistics* acss)
  {
    int p = acss->ars_prefix_states();
    int c = acss->ars_cycle_states();
    if (n++)
      {
	min_prefix_states = std::min(min_prefix_states, p);
	max_prefix_states = std::max(max_prefix_states, p);
	tot_prefix_states += p;
	min_cycle_states = std::min(min_cycle_states, c);
	max_cycle_states = std::max(max_cycle_states, c);
	tot_cycle_states += c;
      }
    else
      {
	min_prefix_states = max_prefix_states = tot_prefix_states = p;
	min_cycle_states = max_cycle_states = tot_cycle_states = c;
      }
  }
};

struct ars_ratio_stat
{
  float min_prefix_states;
  float max_prefix_states;
  float tot_prefix_states;
  float min_cycle_states;
  float max_cycle_states;
  float tot_cycle_states;
  int n;

  ars_ratio_stat()
    : n(0)
  {
  }

  void
  count(const spot::ars_statistics* acss, const spot::tgba* a)
  {
    spot::tgba_statistics a_size = spot::stats_reachable(a);
    float mp = acss->ars_prefix_states() / static_cast<float>(a_size.states);
    float mc = acss->ars_cycle_states() / static_cast<float>(a_size.states);
    if (n++)
      {
	min_prefix_states = std::min(min_prefix_states, mp);
	max_prefix_states = std::max(max_prefix_states, mp);
	tot_prefix_states += mp;
	min_cycle_states = std::min(min_cycle_states, mc);
	max_cycle_states = std::max(max_cycle_states, mc);
	tot_cycle_states += mc;
      }
    else
      {
	min_prefix_states = max_prefix_states = tot_prefix_states = mp;
	min_cycle_states = max_cycle_states = tot_cycle_states = mc;
      }
  }
};

struct ar_stat
{
  int min_prefix;
  int max_prefix;
  int tot_prefix;
  int min_cycle;
  int max_cycle;
  int tot_cycle;
  int min_run;
  int max_run;
  int n;

  ar_stat()
    : n(0)
  {
  }

  void
  count(const spot::tgba_run* run)
  {
    int p = run->prefix.size();
    int c = run->cycle.size();
    if (n++)
      {
	min_prefix = std::min(min_prefix, p);
	max_prefix = std::max(max_prefix, p);
	tot_prefix += p;
	min_cycle = std::min(min_cycle, c);
	max_cycle = std::max(max_cycle, c);
	tot_cycle += c;
	min_run = std::min(min_run, c + p);
	max_run = std::max(max_run, c + p);
      }
    else
      {
	min_prefix = max_prefix = tot_prefix = p;
	min_cycle = max_cycle = tot_cycle = c;
	min_run = max_run = c + p;
      }
  }
};

typedef std::map<std::string, ec_stat> ec_stats_type;
ec_stats_type ec_stats;

typedef std::map<std::string, ec_ratio_stat> ec_ratio_stat_type;
ec_ratio_stat_type glob_ec_ratio_stats;
typedef std::map<int, ec_ratio_stat_type > ec_ratio_stats_type;
ec_ratio_stats_type ec_ratio_stats;

typedef std::map<std::string, acss_stat> acss_stats_type;
acss_stats_type acss_stats;

typedef std::map<std::string, acss_ratio_stat> acss_ratio_stats_type;
acss_ratio_stats_type acss_ratio_stats;

typedef std::map<std::string, ars_stat> ars_stats_type;
ars_stats_type ars_stats;

typedef std::map<std::string, ars_ratio_stat> ars_ratio_stats_type;
ars_ratio_stats_type ars_ratio_stats;

typedef std::map<std::string, ar_stat> ar_stats_type;
ar_stats_type ar_stats;		// Statistics about accepting runs.
ar_stats_type mar_stats;        // ... about minimized accepting runs.

void
print_ec_stats(const ec_stats_type& ec_stats, bool opt_paper = false)
{
  std::ios::fmtflags old = std::cout.flags();
  if (!opt_paper)
    {
      std::cout << std::endl;
      std::cout << std::right << std::fixed << std::setprecision(1);

      std::cout << "Statistics about emptiness checkers:" << std::endl;
      std::cout << std::setw(22) << ""
                << " |         states        |      transitions      |"
                << std::endl << std::setw(22) << "algorithm"
                << " |   min   < mean  < max |   min   < mean  < max |   n"
                << std::endl
                << std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
                << std::endl;
      for (ec_stats_type::const_iterator i = ec_stats.begin();
            i != ec_stats.end(); ++i)
        std::cout << std::setw(22) << i->first << " |"
                  << std::setw(6) << i->second.min_states
                  << " "
                  << std::setw(8)
                  << static_cast<float>(i->second.tot_states) / i->second.n
                  << " "
                  << std::setw(6) << i->second.max_states
                  << " |"
                  << std::setw(6) << i->second.min_transitions
                  << " "
                  << std::setw(8)
                  << static_cast<float>(i->second.tot_transitions) / i->second.n
                  << " "
                  << std::setw(6) << i->second.max_transitions
                  << " |"
                  << std::setw(4) << i->second.n
                  << std::endl;
      std::cout << std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
                << std::endl
                << std::setw(22) << ""
                << " |     maximal depth     |"
                << std::endl
                << std::setw(22) << "algorithm"
                << " |   min   < mean  < max |   n"
                << std::endl
                << std::setw(53) << std::setfill('-') << "" << std::setfill(' ')
                << std::endl;
      for (ec_stats_type::const_iterator i = ec_stats.begin();
            i != ec_stats.end(); ++i)
        std::cout << std::setw(22) << i->first << " |"
                  << std::setw(6)
                  << i->second.min_max_depth
                  << " "
                  << std::setw(8)
                  << static_cast<float>(i->second.tot_max_depth) / i->second.n
                  << " "
                  << std::setw(6)
                  << i->second.max_max_depth
                  << " |"
                  << std::setw(4) << i->second.n
                  << std::endl;
    }
  std::cout << std::setiosflags(old);
}

void
print_ar_stats(ar_stats_type& ar_stats, const std::string s,
              bool opt_paper = false)
{
  std::ios::fmtflags old = std::cout.flags();
  if (!opt_paper)
    {
      std::cout << std::endl << s << std::endl;
      std::cout << std::right << std::fixed << std::setprecision(1);

      std::cout << std::setw(22) << ""
                << " |         prefix        |         cycle         |"
                << std::endl
                << std::setw(22) << "algorithm"
                << " |   min   < mean  < max |   min   < mean  < max |   n"
                << std::endl
                << std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
                << std::endl;
      for (ar_stats_type::const_iterator i = ar_stats.begin();
            i != ar_stats.end(); ++i)
        std::cout << std::setw(22) << i->first << " |"
                  << std::setw(6) << i->second.min_prefix
                  << " "
                  << std::setw(8)
                  << static_cast<float>(i->second.tot_prefix) / i->second.n
                  << " "
                  << std::setw(6) << i->second.max_prefix
                  << " |"
                  << std::setw(6) << i->second.min_cycle
                  << " "
                  << std::setw(8)
                  << static_cast<float>(i->second.tot_cycle) / i->second.n
                  << " "
                  << std::setw(6) << i->second.max_cycle
                  << " |"
                  << std::setw(4) << i->second.n
                  << std::endl;
      std::cout << std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
                << std::endl
                << std::setw(22) << ""
                << " |          runs         |         total         |"
                << std::endl <<
                std::setw(22) << "algorithm"
                << " |   min   < mean  < max |  pre.   cyc.     runs |   n"
                << std::endl
                << std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
                << std::endl;
      for (ar_stats_type::const_iterator i = ar_stats.begin();
            i != ar_stats.end(); ++i)
        std::cout << std::setw(22) << i->first << " |"
                  << std::setw(6)
                  << i->second.min_run
                  << " "
                  << std::setw(8)
                  << static_cast<float>(i->second.tot_prefix
                                        + i->second.tot_cycle) / i->second.n
                  << " "
                  << std::setw(6)
                  << i->second.max_run
                  << " |"
                  << std::setw(6) << i->second.tot_prefix
                  << " "
                  << std::setw(6) << i->second.tot_cycle
                  << " "
                  << std::setw(8) << i->second.tot_prefix + i->second.tot_cycle
                  << " |"
                  << std::setw(4) << i->second.n
                  << std::endl;
    }
  std::cout << std::setiosflags(old);
}

void
print_ec_ratio_stats(const std::string& s,
                    const ec_ratio_stat_type& ec_ratio_stats,
                    bool opt_paper = false)
{
  std::ios::fmtflags old = std::cout.flags();
  if (opt_paper)
    {
      std::cout << std::endl;
      std::cout << "Ratios about empt. check (" << s << ")" << std::endl;
      std::cout << std::right << std::fixed << std::setprecision(1);
      for (ec_ratio_stat_type::const_iterator i = ec_ratio_stats.begin();
          i != ec_ratio_stats.end(); ++i)
        std::cout << std::setw(22)  << i->first
                  << " " << std::setw(8)
                  << (i->second.tot_states / i->second.n) * 100.
                  << " " << std::setw(8)
                  << (static_cast<float>(i->second.tot_transitions) /
                                                        i->second.n) * 100.
                  << " " << std::setw(8)
                  << (static_cast<float>(i->second.tot_depth) /
                                                        i->second.n) * 100.
                  << " " << std::setw(4)
                  << i->second.n
                  << std::endl;
    }
  else
    {
      std::cout << std::endl;
      std::cout << std::right << std::fixed << std::setprecision(1);
      std::cout << "Ratios in case of non-emptiness (" << s << ")"
                << std::endl;
      std::cout << "<for all algorithms, the reference size is the one of"
                << " the generalized automaton>" << std::endl;
      std::cout << std::setw(22) << ""
                << " |       % states        |    % transitions      |"
                << std::endl << std::setw(22) << "algorithm"
                << " |   min   < mean  < max |   min   < mean  < max |   n"
                << std::endl
                << std::setw(79) << std::setfill('-') << ""
                << std::setfill(' ') << std::endl;
      for (ec_ratio_stat_type::const_iterator i = ec_ratio_stats.begin();
          i != ec_ratio_stats.end(); ++i)
        std::cout << std::setw(22) << i->first << " |"
                  << std::setw(6) << i->second.min_states * 100.
                  << " "
                  << std::setw(8)
                  << (i->second.tot_states / i->second.n) * 100.
                  << " "
                  << std::setw(6) << i->second.max_states * 100.
                  << " |"
                  << std::setw(6) << i->second.min_transitions * 100.
                  << " "
                  << std::setw(8)
                  << (i->second.tot_transitions / i->second.n) * 100.
                  << " "
                  << std::setw(6) << i->second.max_transitions * 100.
                  << " |"
                  << std::setw(4) << i->second.n
                  << std::endl;
      std::cout << std::setw(79) << std::setfill('-') << ""
                << std::setfill(' ') << std::endl
                << std::setw(22) << ""
                << " |   % maximal depth     |"
                << std::endl
                << std::setw(22) << "algorithm"
                << " |   min   < mean  < max |   n"
                << std::endl
                << std::setw(53) << std::setfill('-') << ""
                << std::setfill(' ') << std::endl;
      for (ec_ratio_stat_type::const_iterator i = ec_ratio_stats.begin();
          i != ec_ratio_stats.end(); ++i)
        std::cout << std::setw(22) << i->first << " |"
                  << std::setw(6)
                  << i->second.min_depth * 100.
                  << " "
                  << std::setw(8)
                  << (i->second.tot_depth / i->second.n) * 100.
                  << " "
                  << std::setw(6)
                  << i->second.max_depth * 100.
                  << " |"
                  << std::setw(4) << i->second.n
                  << std::endl;
    }
  std::cout << std::setiosflags(old);
}

void
print_acss_stats(const acss_stats_type& acss_stats, bool opt_paper = false)
{
  std::ios::fmtflags old = std::cout.flags();
  if (!opt_paper)
    {
      std::cout << std::endl;
      std::cout << std::right << std::fixed << std::setprecision(1);

      std::cout << "Statistics about accepting cycle search space:"
		<< std::endl;
      std::cout << std::setw(22) << ""
		<< " |              states           |"
		<< std::endl << std::setw(22) << "algorithm"
		<< " |   min   < mean  < max | total |  n"
		<< std::endl
		<< std::setw(61) << std::setfill('-') << "" << std::setfill(' ')
		<< std::endl;
      for (acss_stats_type::const_iterator i = acss_stats.begin();
	   i != acss_stats.end(); ++i)
	std::cout << std::setw(22) << i->first << " |"
		  << std::setw(6) << i->second.min_states
		  << " "
		  << std::setw(8)
		  << static_cast<float>(i->second.tot_states) / i->second.n
		  << " "
		  << std::setw(6) << i->second.max_states
		  << " |"
		  << std::setw(6) << i->second.tot_states
		  << " |"
		  << std::setw(4) << i->second.n
		  << std::endl;
    }
  std::cout << std::setiosflags(old);
}

void
print_acss_ratio_stats(const acss_ratio_stats_type& acss_ratio_stats,
                      bool opt_paper = false)
{
  std::ios::fmtflags old = std::cout.flags();
  if (opt_paper)
    {
      std::cout << std::endl;
      std::cout << "Ratios about search space" << std::endl;
      std::cout << std::right << std::fixed << std::setprecision(1);
      for (acss_ratio_stats_type::const_iterator i = acss_ratio_stats.begin();
	   i != acss_ratio_stats.end(); ++i)
        std::cout << std::setw(22)  << i->first
                  << " " << std::setw(8)
                  << (i->second.tot_states / i->second.n) * 100.
                  << std::endl;
    }
  else
    {
      std::cout << std::endl;
      std::cout << std::right << std::fixed << std::setprecision(1);

      std::cout << "Ratios about accepting cycle search space:"
		<< std::endl;
      std::cout << std::setw(22) << ""
		<< " |            % states           |"
		<< std::endl << std::setw(22) << "algorithm"
		<< " |   min   < mean  < max | total |  n"
		<< std::endl
		<< std::setw(61) << std::setfill('-') << "" << std::setfill(' ')
		<< std::endl;
      for (acss_ratio_stats_type::const_iterator i = acss_ratio_stats.begin();
	   i != acss_ratio_stats.end(); ++i)
	std::cout << std::setw(22) << i->first << " |"
		  << std::setw(6) << i->second.min_states * 100.
		  << " "
		  << std::setw(8)
		  << (i->second.tot_states / i->second.n) * 100.
		  << " "
		  << std::setw(6) << i->second.max_states * 100.
		  << " |"
		  << std::setw(6) << i->second.tot_states * 100.
		  << " |"
		  << std::setw(4) << i->second.n
		  << std::endl;
    }
  std::cout << std::setiosflags(old);
}

void
print_ars_stats(const ars_stats_type& ars_stats, bool opt_paper = false)
{
  std::ios::fmtflags old = std::cout.flags();
  if (!opt_paper)
    {
      std::cout << std::endl;
      std::cout << std::right << std::fixed << std::setprecision(1);

      std::cout << "Statistics about accepting run computation:"
		<< std::endl;
      std::cout << std::setw(22) << ""
		<< " |(non unique) states for prefix |"
		<< std::endl << std::setw(22) << "algorithm"
		<< " |   min   < mean  < max | total |  n"
		<< std::endl
		<< std::setw(61) << std::setfill('-') << "" << std::setfill(' ')
		<< std::endl;
      for (ars_stats_type::const_iterator i = ars_stats.begin();
	   i != ars_stats.end(); ++i)
	std::cout << std::setw(22) << i->first << " |"
		  << std::setw(6) << i->second.min_prefix_states
		  << " "
		  << std::setw(8)
		  << (static_cast<float>(i->second.tot_prefix_states)
		      / i->second.n)
		  << " "
		  << std::setw(6) << i->second.max_prefix_states
		  << " |"
		  << std::setw(6) << i->second.tot_prefix_states
		  << " |"
		  << std::setw(4) << i->second.n
		  << std::endl;
      std::cout << std::setw(22) << ""
		<< " | (non unique) states for cycle |"
		<< std::endl << std::setw(22) << "algorithm"
		<< " |   min   < mean  < max | total |  n"
		<< std::endl
		<< std::setw(61) << std::setfill('-') << "" << std::setfill(' ')
		<< std::endl;
      for (ars_stats_type::const_iterator i = ars_stats.begin();
	   i != ars_stats.end(); ++i)
	std::cout << std::setw(22) << i->first << " |"
		  << std::setw(6) << i->second.min_cycle_states
		  << " "
		  << std::setw(8)
		  << (static_cast<float>(i->second.tot_cycle_states)
		      / i->second.n)
		  << " "
		  << std::setw(6) << i->second.max_cycle_states
		  << " |"
		  << std::setw(6) << i->second.tot_cycle_states
		  << " |"
		  << std::setw(4) << i->second.n
		  << std::endl;
    }
  std::cout << std::setiosflags(old);
}

void
print_ars_ratio_stats(const ars_ratio_stats_type& ars_ratio_stats,
                     bool opt_paper = false)
{
  std::ios::fmtflags old = std::cout.flags();
  if (opt_paper)
    {
      std::cout << std::endl;
      std::cout << "Ratios about acc. run computation" << std::endl;
      std::cout << std::right << std::fixed << std::setprecision(1);
      for (ars_ratio_stats_type::const_iterator i = ars_ratio_stats.begin();
	   i != ars_ratio_stats.end(); ++i)
        std::cout << std::setw(22)  << i->first
	          << " " << std::setw(8)
		  << (i->second.tot_cycle_states / i->second.n) * 100.
                  << std::endl;
    }
  else
    {
      std::cout << std::endl;
      std::cout << std::right << std::fixed << std::setprecision(1);

      std::cout << "Ratios about accepting run computation:"
		<< std::endl;
      std::cout << std::setw(22) << ""
		<< " |%(non unique) states for prefix|"
		<< std::endl << std::setw(22) << "algorithm"
		<< " |   min   < mean  < max | total |  n"
		<< std::endl
		<< std::setw(61) << std::setfill('-') << "" << std::setfill(' ')
		<< std::endl;
      for (ars_ratio_stats_type::const_iterator i = ars_ratio_stats.begin();
	   i != ars_ratio_stats.end(); ++i)
	std::cout << std::setw(22) << i->first << " |"
		  << std::setw(6) << i->second.min_prefix_states * 100.
		  << " " << std::setw(8)
		  << (i->second.tot_prefix_states / i->second.n) * 100.
		  << " " << std::setw(6)
                  << i->second.max_prefix_states * 100.
		  << " |"
		  << std::setw(6) << i->second.tot_prefix_states * 100.
		  << " |"
		  << std::setw(4) << i->second.n
		  << std::endl;
      std::cout << std::setw(22) << ""
		<< " |% (non unique) states for cycle|"
		<< std::endl << std::setw(22) << "algorithm"
		<< " |   min   < mean  < max | total |  n"
		<< std::endl
		<< std::setw(61) << std::setfill('-') << "" << std::setfill(' ')
		<< std::endl;
      for (ars_ratio_stats_type::const_iterator i = ars_ratio_stats.begin();
	   i != ars_ratio_stats.end(); ++i)
	std::cout << std::setw(22) << i->first << " |"
		  << std::setw(6) << i->second.min_cycle_states * 100.
		  << " "
		  << std::setw(8)
		  << (i->second.tot_cycle_states / i->second.n) * 100.
		  << " "
		  << std::setw(6) << i->second.max_cycle_states * 100.
		  << " |"
		  << std::setw(6) << i->second.tot_cycle_states * 100.
		  << " |"
		  << std::setw(4) << i->second.n
		  << std::endl;
    }
  std::cout << std::setiosflags(old);
}

spot::ltl::formula*
generate_formula(const spot::ltl::random_ltl& rl, int opt_f, int opt_s,
                 int opt_l = 0, bool opt_u = false)
{
  static std::set<std::string> unique;

  int max_tries_u = 1000;
  while (max_tries_u--)
    {
      spot::srand(opt_s++);
      spot::ltl::formula* f;
      int max_tries_l = 1000;
      while (max_tries_l--)
        {
          f = rl.generate(opt_f);
          if (opt_l)
            {
              spot::ltl::formula* g = reduce(f);
              spot::ltl::destroy(f);
              if (spot::ltl::length(g) < opt_l)
                {
                  spot::ltl::destroy(g);
                  continue;
                }
              f = g;
            }
          else
            {
              assert(spot::ltl::length(f) <= opt_f);
            }
          break;
        }
      if (max_tries_l < 0)
        {
          assert(opt_l);
          std::cerr << "Failed to generate non-reducible formula "
                    << "of size " << opt_l << " or more." << std::endl;
          return 0;
        }
      std::string txt = spot::ltl::to_string(f);
      if (!opt_u || unique.insert(txt).second)
        {
          return f;
        }
      spot::ltl::destroy(f);
    }
  assert(opt_u);
  std::cerr << "Failed to generate another unique formula."
            << std::endl;
  return 0;
}

int
main(int argc, char** argv)
{
  bool opt_paper = false;
  bool opt_dp = false;
  int opt_f = 15;
  int opt_F = 0;
  char* opt_p = 0;
  char* opt_i = 0;
  std::istream *formula_file = 0;
  int opt_l = 0;
  bool opt_u = false;

  int opt_n_acc = 0;
  float opt_a = 0.0;
  float opt_d = 0.2;
  int opt_n = 20;
  float opt_t = 0.5;

  bool opt_0 = false;
  bool opt_z = false;
  bool opt_Z = false;

  int opt_R = 0;

  const char* opt_O = 0;

  bool opt_dot = false;
  int opt_ec = 0;
  int opt_ec_seed = 0;
  bool opt_reduce = false;
  bool opt_replay = false;
  bool opt_degen = false;
  int argn = 0;

  int exit_code = 0;

  spot::tgba* formula = 0;
  spot::tgba* product = 0;

  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set;
  spot::bdd_dict* dict = new spot::bdd_dict();

  if (argc <= 1)
    syntax(argv[0]);

  while (++argn < argc)
    {
      if (!strcmp(argv[argn], "-0"))
	{
	  opt_0 = true;
	}
      else if (!strcmp(argv[argn], "-1"))
	{
	  opt_paper = true;
	}
      else if (!strcmp(argv[argn], "-a"))
	{
	  if (argc < argn + 3)
	    syntax(argv[0]);
	  opt_n_acc = to_int(argv[++argn]);
	  opt_a = to_float(argv[++argn]);
	}
      else if (!strcmp(argv[argn], "-d"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_d = to_float(argv[++argn]);
	}
      else if (!strcmp(argv[argn], "-D"))
	{
	  opt_degen = true;
	  if (!opt_ec)
	    opt_ec = 1;
	}
      else if (!strcmp(argv[argn], "-e"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_ec = to_int(argv[++argn]);
	}
      else if (!strcmp(argv[argn], "-g"))
	{
	  opt_dot = true;
	}
      else if (!strcmp(argv[argn], "-m"))
	{
	  opt_reduce = true;
	  opt_replay = true;
	  if (!opt_ec)
	    opt_ec = 1;
	}
      else if (!strcmp(argv[argn], "-i"))
        {
          if (argc < argn + 2)
            syntax(argv[0]);
          opt_i = argv[++argn];
          if (strcmp(opt_i, "-"))
            {
              formula_file = new std::ifstream(opt_i);
              if (!(*formula_file))
                {
                  delete formula_file;
                  std::cerr << "Failed to open " << opt_i << std::endl;
                  exit(2);
                }
            }
          else
            formula_file = &std::cin;
        }
      else if (!strcmp(argv[argn], "-n"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_n = to_int(argv[++argn]);
	}
      else if (!strcmp(argv[argn], "-O"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_O = argv[++argn];
	  int s = sizeof(ec_algos) / sizeof(*ec_algos);
	  int i;
	  for (i = 0; i < s; ++i)
	    if (!strcmp(opt_O, ec_algos[i].name))
	      break;
	  if (i == s)
	    {
	      std::cerr << "Unknown algorithm.  Available algorithms are:"
			<< std::endl;
	      for (i = 0; i < s; ++i)
		std::cerr << "  " << ec_algos[i].name << std::endl;
	      exit(1);
	    }
	}
      else if (!strcmp(argv[argn], "-r"))
	{
	  opt_replay = true;
	  if (!opt_ec)
	    opt_ec = 1;
	}
      else if (!strcmp(argv[argn], "-R"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_R = to_int(argv[++argn]);
	}
      else if (!strcmp(argv[argn], "-s"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_ec_seed = to_int(argv[++argn]);
	  spot::srand(opt_ec_seed);
	}
      else if (!strcmp(argv[argn], "-t"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_t = to_float(argv[++argn]);
	}
      else if (!strcmp(argv[argn], "-z"))
	{
	  opt_z = true;
	}
      else if (!strcmp(argv[argn], "-Z"))
	{
	  opt_Z = opt_z = true;
	}
      else if (!strcmp(argv[argn], "-dp"))
	{
	  opt_dp = true;
	}
      else if (!strcmp(argv[argn], "-f"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_f = to_int(argv[++argn]);
	}
      else if (!strcmp(argv[argn], "-F"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_F = to_int(argv[++argn]);
	}
      else if (!strcmp(argv[argn], "-p"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_p = argv[++argn];
	}
      else if (!strcmp(argv[argn], "-l"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_l = to_int(argv[++argn]);
	}
      else if (!strcmp(argv[argn], "-u"))
	{
	  opt_u = true;
	}
      else
	{
	  ap->insert(static_cast<spot::ltl::atomic_prop*>
		     (env.require(argv[argn])));
	}
    }

  spot::ltl::random_ltl rl(ap);
  const char* tok = rl.parse_options(opt_p);
  if (tok)
    {
      std::cerr << "failed to parse probabilities near `"
		<< tok << "'" << std::endl;
      exit(2);
    }

  if (opt_l > opt_f)
    {
      std::cerr << "-l's argument (" << opt_l << ") should not be larger than "
		<< "-f's (" << opt_f << ")" << std::endl;
      exit(2);
    }

  if (opt_dp)
    {
      rl.dump_priorities(std::cout);
      exit(0);
    }

  spot::timer_map tm_ec;
  spot::timer_map tm_ar;
  std::set<int> failed_seeds;
  int init_opt_ec = opt_ec;
  spot::ltl::atomic_prop_set* apf = new spot::ltl::atomic_prop_set;

  do
    {
      if (opt_F)
        {
          spot::ltl::formula* f = generate_formula(rl, opt_f, opt_ec_seed,
                                                  opt_l, opt_u);
          if (!f)
            exit(1);
          formula = spot::ltl_to_tgba_fm(f, dict, true);
          spot::ltl::destroy(f);
        }
      else if (opt_i)
        {
          if (formula_file->good())
            {
              std::string input;
              std::getline(*formula_file, input, '\n');
              spot::ltl::parse_error_list pel;
              spot::ltl::formula* f = spot::ltl::parse(input, pel, env);
              if (spot::ltl::format_parse_errors(std::cerr, input, pel))
                break;
              formula = spot::ltl_to_tgba_fm(f, dict, true);
              spot::ltl::atomic_prop_set* tmp =
                                            spot::ltl::atomic_prop_collect(f);
              for (spot::ltl::atomic_prop_set::iterator i = tmp->begin();
                                                        i != tmp->end(); ++i)
                  apf->insert(
                            dynamic_cast<spot::ltl::atomic_prop*>((*i)->ref()));
              spot::ltl::destroy(f);
              delete tmp;
            }
          else
            {
              if (formula_file->bad())
                std::cerr << "Failed to read " << opt_i << std::endl;
              break;
            }
        }

     for (spot::ltl::atomic_prop_set::iterator i = ap->begin();
                                                         i != ap->end(); ++i)
         apf->insert(dynamic_cast<spot::ltl::atomic_prop*>((*i)->ref()));

      do
        {
          if (opt_ec)
            {
              if (!opt_paper)
                std::cout << "seed: " << opt_ec_seed << std::endl;
              spot::srand(opt_ec_seed);
            }

          spot::tgba* a;
          spot::tgba* r = a = spot::random_graph(opt_n, opt_d, apf, dict,
                                                opt_n_acc, opt_a, opt_t, &env);

          if (formula)
            a = product = new spot::tgba_product(formula, a);

          int real_n_acc = a->number_of_acceptance_conditions();

          if (!opt_ec)
            {
              if (opt_dot)
                dotty_reachable(std::cout, a);
              else if (!opt_0)
                tgba_save_reachable(std::cout, a);
            }
          else
            {
              spot::tgba* degen = 0;
              if (opt_degen && real_n_acc > 1)
                degen = new spot::tgba_tba_proxy(a);

              int n_alg = sizeof(ec_algos) / sizeof(*ec_algos);
              int n_ec = 0;
              int n_empty = 0;
              int n_non_empty = 0;
              int n_maybe_empty = 0;

              for (int i = 0; i < n_alg; ++i)
                {
                  spot::emptiness_check* ec;
                  spot::emptiness_check_result* res;
                  if (opt_O && strcmp(opt_O, ec_algos[i].name))
                    continue;
                  ec = cons_emptiness_check(i, a, degen, real_n_acc);
                  if (!ec)
                    continue;
                  ++n_ec;
                  std::string algo = ec_algos[i].name;
                  if (!opt_paper)
                    {
                      std::cout.width(32);
                      std::cout << algo << ": ";
                    }
                  tm_ec.start(algo);
                  for (int count = opt_R;;)
                    {
                      res = ec->check();
                      if (count-- <= 0)
                        break;
                      delete res;
                      delete ec;
                      ec = cons_emptiness_check(i, a, degen, real_n_acc);
                    }
                  tm_ec.stop(algo);
                  const spot::ec_statistics* ecs =
                    dynamic_cast<const spot::ec_statistics*>(ec);
                  if (opt_z && ecs)
                    {
                      ec_stats[algo].count(ecs);
                      if (res)
                        {
                          // Notice that ratios are computed w.r.t. the
                          // generalized automaton a.
                          ec_ratio_stats[real_n_acc][algo].count(ecs, a);
                          glob_ec_ratio_stats[algo].count(ecs, a);
                        }
                    }
                  if (res)
                    {
                      if (!opt_paper)
                        std::cout << "acc. run";
                      ++n_non_empty;
                      const spot::acss_statistics* acss =
                        dynamic_cast<const spot::acss_statistics*>(res);
                      if (opt_z && acss)
                        {
                          acss_stats[algo].count(acss);
                          acss_ratio_stats[algo].count(acss, a);
                        }
                      if (opt_replay)
                        {
                          spot::tgba_run* run;

                          const spot::ars_statistics* ars =
                            dynamic_cast<const spot::ars_statistics*>(res);

                          tm_ar.start(algo);
                          for (int count = opt_R;;)
                            {
                              run = res->accepting_run();
                              if (opt_z && ars)
                                {
                                  // Count only the first run (the other way
                                  // would be to divide the stats by opt_R).
                                  ars_stats[algo].count(ars);
                                  ars_ratio_stats[algo].count(ars, a);
                                  ars = 0;
                                }
                              if (count-- <= 0 || !run)
                                break;
                              delete run;
                            }
                          if (!run)
                            {
                              tm_ar.cancel(algo);
                              if (!opt_paper)
                                std::cout << " exists, not computed";
                            }
                          else
                            {
                              tm_ar.stop(algo);
                              std::ostringstream s;
                              if (!spot::replay_tgba_run(s, res->automaton(),
                                                        run))
                                {
                                  if (!opt_paper)
                                    std::cout << ", but could not replay it "
                                              << "(ERROR!)";
                                  failed_seeds.insert(opt_ec_seed);
                                }
                              else
                                {
                                  if (!opt_paper)
                                    std::cout << ", computed";
                                  if (opt_z)
                                    ar_stats[algo].count(run);
                                }
                              if (opt_z && !opt_paper)
                                std::cout << " [" << run->prefix.size()
                                          << "+" << run->cycle.size()
                                          << "]";

                              if (opt_reduce)
                                {
                                  spot::tgba_run* redrun =
                                    spot::reduce_run(res->automaton(), run);
                                  if (!spot::replay_tgba_run(s,
                                                    res->automaton(), redrun))
                                    {
                                      if (!opt_paper)
                                        std::cout << ", but could not replay "
                                                 << "its minimization (ERROR!)";
                                      failed_seeds.insert(opt_ec_seed);
                                    }
                                  else
                                    {
                                      std::cout << ", reduced";
                                      if (opt_z)
                                        mar_stats[algo].count(redrun);
                                    }
                                  if (opt_z && !opt_paper)
                                    {
                                      std::cout << " [" << redrun->prefix.size()
                                                << "+" << redrun->cycle.size()
                                                << "]";
                                    }
                                  delete redrun;
                                }
                              delete run;
                            }
                        }
                      if (!opt_paper)
                        std::cout << std::endl;
                      delete res;
                    }
                  else
                    {
                      if (ec_algos[i].safe)
                        {
                          if (!opt_paper)
                            std::cout << "empty language" << std::endl;
                          ++n_empty;
                        }
                      else
                        {
                          if (!opt_paper)
                            std::cout << "maybe empty language" << std::endl;
                          ++n_maybe_empty;
                        }

                    }

                  if (opt_Z && !opt_paper)
                    ec->print_stats(std::cout);
                  delete ec;
                }

              assert(n_empty + n_non_empty + n_maybe_empty == n_ec);

              if ((n_empty == 0 && (n_non_empty + n_maybe_empty) != n_ec)
                  || (n_empty != 0 && n_non_empty != 0))
                {
                  std::cout << "ERROR: not all algorithms agree" << std::endl;
                  failed_seeds.insert(opt_ec_seed);
                }

              delete degen;
            }

          delete product;
          delete r;

          if (opt_ec)
            {
              --opt_ec;
              ++opt_ec_seed;
            }
        }
      while (opt_ec);

      delete formula;
      if (opt_F)
        --opt_F;
      opt_ec = init_opt_ec;
      for (spot::ltl::atomic_prop_set::iterator i = apf->begin();
          i != apf->end(); ++i)
        spot::ltl::destroy(*i);
      apf->clear();
    }
  while (opt_F || opt_i);

  if (!ec_stats.empty())
    print_ec_stats(ec_stats, opt_paper);

  if (!glob_ec_ratio_stats.empty())
    {
      print_ec_ratio_stats("all tests", glob_ec_ratio_stats, opt_paper);
      if (ec_ratio_stats.size() > 1)
        for (ec_ratio_stats_type::const_iterator i = ec_ratio_stats.begin();
            i != ec_ratio_stats.end(); ++i)
          {
            std::ostringstream s;
            s << "tests with " << i->first << " acceptance conditions";
            print_ec_ratio_stats(s.str(), i->second, opt_paper);
          }
    }

  if (!acss_stats.empty())
    print_acss_stats(acss_stats, opt_paper);

  if (!acss_ratio_stats.empty())
    print_acss_ratio_stats(acss_ratio_stats, opt_paper);

  if (!ars_stats.empty())
    print_ars_stats(ars_stats, opt_paper);

  if (!ars_ratio_stats.empty())
      print_ars_ratio_stats(ars_ratio_stats, opt_paper);

  if (!ar_stats.empty())
    print_ar_stats(ar_stats, "Statistics about accepting runs:", opt_paper);

  if (!mar_stats.empty())
    print_ar_stats(mar_stats, "Statistics about reduced accepting runs:",
                    opt_paper);

  if (!opt_paper && opt_z)
    {
      if (!tm_ec.empty())
	{
	  std::cout << std::endl
		    << "emptiness checks cumulated timings:" << std::endl;
	  tm_ec.print(std::cout);
	}
      if (!tm_ar.empty())
	{
	  std::cout << std::endl
		    << "accepting runs cumulated timings:" << std::endl;
	  tm_ar.print(std::cout);
	}
    }

  if (!failed_seeds.empty())
    {
      exit_code = 1;
      std::cout << "The check failed for the following seeds:";
      for (std::set<int>::const_iterator i = failed_seeds.begin();
	   i != failed_seeds.end(); ++i)
	std::cout << " " << *i;
      std::cout << std::endl;
    }

  for (spot::ltl::atomic_prop_set::iterator i = ap->begin();
       i != ap->end(); ++i)
    spot::ltl::destroy(*i);

  if (opt_i && strcmp(opt_i, "-"))
    {
      dynamic_cast<std::ifstream*>(formula_file)->close();
      delete formula_file;
    }
  delete ap;
  delete apf;
  delete dict;
  return exit_code;
}