randtgba.cc

// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire
// de Recherche et Développement de l'Epita (LRDE).
// 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 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 <cassert>
#include <cstdlib>
#include <iostream>
#include <iomanip>
#include <sstream>
#include <fstream>
#include <string>
#include <utility>
#include <set>
#include <vector>
#include "tl/parse.hh"
#include "tl/apcollect.hh"
#include "tl/randomltl.hh"
#include "tl/print.hh"
#include "tl/length.hh"
#include "tl/simplify.hh"
#include "twaalgos/randomgraph.hh"
#include "twaalgos/hoa.hh"
#include "twaalgos/stats.hh"
#include "tl/defaultenv.hh"
#include "twaalgos/dot.hh"
#include "misc/random.hh"
#include "misc/optionmap.hh"
#include "twaalgos/degen.hh"
#include "twaalgos/product.hh"
#include "misc/timer.hh"

#include "twaalgos/ltl2tgba_fm.hh"

#include "twaalgos/emptiness.hh"
#include "twaalgos/emptiness_stats.hh"
#include "twaalgos/reducerun.hh"
#include "twaalgos/replayrun.hh"

struct ec_algo
{
  std::string name;
  spot::emptiness_check_instantiator_ptr inst;
};

const char* default_algos[] = {
  "Cou99(!poprem)",
  "Cou99(!poprem shy !group)",
  "Cou99(!poprem shy group)",
  "Cou99(poprem)",
  "Cou99(poprem shy !group)",
  "Cou99(poprem shy group)",
  "CVWY90",
  "CVWY90(bsh=4K)",
  "GV04",
  "SE05",
  "SE05(bsh=4K)",
  "Tau03",
  "Tau03_opt",
  "Tau03_opt(condstack)",
  "Tau03_opt(condstack ordering)",
  "Tau03_opt(condstack ordering !weights)",
  nullptr
};

std::vector<ec_algo> ec_algos;

static spot::emptiness_check_ptr
cons_emptiness_check(int num, spot::const_twa_graph_ptr a,
		     const spot::const_twa_graph_ptr& degen,
		     unsigned int n_acc)
{
  auto inst = ec_algos[num].inst;
  if (n_acc < inst->min_acceptance_conditions()
      || n_acc > inst->max_acceptance_conditions())
    a = degen;
  if (a)
    return inst->instantiate(a);
  return nullptr;
}

static void
syntax(char* prog)
{
  std::cerr << "Usage: "<< prog << " [OPTIONS...] PROPS..." << std::endl
	    << std::endl
	    << "General Options:" << std::endl
	    << "  -0      suppress default output, just generate the graph"
	    << " in memory" << std::endl
	    << "  -1      produce minimal output (for our paper)" << std::endl
	    << "  -g      output graph in dot format" << std::endl
	    << "  -s N    seed for the random number generator" << std::endl
	    << "  -z      display statistics about emptiness-check algorithms"
	    << std::endl
	    << "  -Z      like -z, but print extra statistics after the run"
	    << " of each algorithm" << std::endl
	    << std::endl
	    << "Graph Generation Options:" << std::endl
	    << "  -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
	    << "  -n N    number of nodes of the graph [20]" << std::endl
	    << "  -t F    probability of the atomic propositions to be true"
	    << " [0.5]" << std::endl
	    << "  -det    generate a deterministic and complete graph [false]"
	    << std::endl
	    << "LTL Formula Generation Options:" << std::endl
	    << "  -dp     dump priorities, do not generate any formula"
	    << std::endl
	    << "  -f N    size of the formula [15]" << std::endl
	    << "  -F N    number of formulae to generate [0]" << std::endl
	    << "  -l N    simplify formulae using all available reductions"
	    << " and reject those" << std::endl
	    << "            strictly smaller than N" << std::endl
	    << "  -i FILE do not generate formulae, read them from FILE"
	    << std::endl
	    << "  -p S    priorities to use" << std::endl
	    << "  -S N    skip N formulae before starting to use them"
	    << std::endl
	    << "            (useful to replay a specific seed when -u is used)"
	    << std::endl
	    << "  -u      generate unique formulae" << std::endl
	    << std::endl
	    << "Emptiness-Check Options:" << std::endl
	    << "  -A FILE use all algorithms listed in FILE" << 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
	    << "  -H      halt on the first statistic difference in algorithms"
	    << std::endl
	    << "  -m      try to reduce runs, in a second pass (implies -r)"
            << std::endl
	    << "  -R N    repeat each emptiness-check and accepting run "
	    << "computation N times" << std::endl
	    << "  -r      compute and replay accepting runs (implies -e)"
	    << std::endl
	    << "  ar:MODE select the mode MODE for accepting runs computation "
            << "(implies -r)" << std::endl
	    << 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
	    << std::endl
	    << "When -F or -i is used, a random graph a synchronized with"
	    << " each formula." << std::endl << "If -e N is additionally used"
	    << " N random graphs are generated for each formula." << std::endl;
  exit(2);
}


static 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;
}

static int
to_int_pos(const char* s, const char* arg)
{
  int res = to_int(s);
  if (res <= 0)
    {
      std::cerr << "argument of " << arg
		<< " (" << res << ") must be positive" << std::endl;
      exit(1);
    }
  return res;
}

static int
to_int_nonneg(const char* s, const char* arg)
{
  int res = to_int(s);
  if (res < 0)
    {
      std::cerr << "argument of " << arg
		<< " (" << res << ") must be nonnegative" << std::endl;
      exit(1);
    }
  return res;
}

static 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;
}

static float
to_float_nonneg(const char* s, const char* arg)
{
  float res = to_float(s);
  if (res < 0)
    {
      std::cerr << "argument of " << arg
		<< " (" << res << ") must be nonnegative" << std::endl;
      exit(1);
    }
  return res;
}

// Convertors using for statistics:

template <typename T>
T
id(const char*, unsigned x)
{
  return static_cast<T>(x);
}

spot::twa_statistics prod_stats;

static float
prod_conv(const char* name, unsigned x)
{
  float y = static_cast<float>(x);
  if (!strcmp(name, "transitions"))
    return y / prod_stats.edges * 100.0;
  return y / prod_stats.states * 100.0;
}

template <typename T, T (*convertor)(const char*, unsigned) = id<T> >
struct stat_collector
{
  struct one_stat
  {
    T min;
    T max;
    T tot;
    unsigned n;

    one_stat()
      : n(0)
    {
    }

    void
    count(T val)
    {
      if (n++)
	{
	  min = std::min(min, val);
	  max = std::max(max, val);
	  tot += val;
	}
      else
	{
	  max = min = tot = val;
	}
    }
  };

  typedef std::map<std::string, one_stat> alg_1stat_map;
  typedef std::map<std::string, alg_1stat_map> stats_alg_map;
  stats_alg_map stats;

  bool
  empty()
  {
    return stats.empty();
  }

  void
  count(const std::string& algorithm, const spot::unsigned_statistics* s)
  {
    if (!s)
      return;
    spot::unsigned_statistics::stats_map::const_iterator i;
    for (i = s->stats.begin(); i != s->stats.end(); ++i)
      stats[i->first][algorithm].count(convertor(i->first, (s->*i->second)()));
  }

  std::ostream&
  display(std::ostream& os,
	  const alg_1stat_map& m, const std::string& title,
	  bool total = true) const
  {
    std::ios::fmtflags old = os.flags();
    os << std::setw(25) << "" << " | "
       << std::setw(30) << std::left << title << std::right << '|' << std::endl
       << std::setw(25) << "algorithm"
       << " |   min   < mean  < max | total |  n"
       << std::endl
       << std::setw(64) << std::setfill('-') << "" << std::setfill(' ')
       << std::endl;
    os << std::right << std::fixed << std::setprecision(1);
    for (typename alg_1stat_map::const_iterator i = m.begin();
	 i != m.end(); ++i)
      {
	os << std::setw(25) << i->first << " |"
	   << std::setw(6) << i->second.min
	   << ' '
	   << std::setw(8)
	   << static_cast<float>(i->second.tot) / i->second.n
	   << ' '
	   << std::setw(6) << i->second.max
	   << " |";
	if (total)
	  os << std::setw(6) << i->second.tot;
	else
	  os << "      ";
	os << " |"
	   << std::setw(4) << i->second.n
	   << std::endl;
      }
    os << std::setw(64) << std::setfill('-') << "" << std::setfill(' ')
       << std::endl;
    os << std::setiosflags(old);
    return os;
  }

  std::ostream&
  display(std::ostream& os, bool total = true) const
  {
    typename stats_alg_map::const_iterator i;
    for (i = stats.begin(); i != stats.end(); ++i)
      display(os, i->second, i->first, total);
    return os;
  }


};

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::const_twa_run_ptr& 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;
      }
  }
};

stat_collector<unsigned> sc_ec;
stat_collector<unsigned> sc_arc;

typedef stat_collector<float, prod_conv> 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;

ec_ratio_stat_type arc_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.


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

  std::cout << std::setw(25) << ""
            << " |         prefix        |         cycle         |"
            << std::endl
            << std::setw(25) << "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(25) << 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(25) << ""
            << " |          runs         |         total         |"
            << std::endl <<
	std::setw(25) << "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(25) << 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);
}

static spot::formula
generate_formula(const spot::random_ltl& rl,
		 spot::tl_simplifier& simp,
		 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::formula f;
      int max_tries_l = 1000;
      while (max_tries_l--)
        {
          f = rl.generate(opt_f);
          if (opt_l)
            {
              f = simp.simplify(f);
              if (spot::length(f) < opt_l)
		continue;
            }
          else
            {
              assert(spot::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 nullptr;
        }
      std::string txt = spot::str_psl(f);
      if (!opt_u || unique.insert(txt).second)
	return f;
    }
  assert(opt_u);
  std::cerr << "Failed to generate another unique formula."
            << std::endl;
  return nullptr;
}

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 = nullptr;
  char* opt_i = nullptr;
  std::istream *formula_file = nullptr;
  int opt_l = 0;
  bool opt_u = false;
  int opt_S = 0;

  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_det = false;

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

  int opt_R = 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;

  bool stop_on_first_difference = false;

  spot::twa_graph_ptr formula = nullptr;
  spot::twa_graph_ptr product = nullptr;

  spot::option_map options;

  auto& env = spot::default_environment::instance();
  spot::atomic_prop_set* ap = new spot::atomic_prop_set;
  auto dict = spot::make_bdd_dict();

  spot::tl_simplifier_options simpopt(true, true, true, true, true);
  spot::tl_simplifier simp(simpopt);

  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;
	  opt_z = true;
	}
      else if (!strcmp(argv[argn], "-a"))
	{
	  if (argc < argn + 3)
	    syntax(argv[0]);
	  opt_n_acc = to_int_nonneg(argv[++argn], "-a");
	  opt_a = to_float_nonneg(argv[++argn], "-a");
	}
      else if (!strcmp(argv[argn], "-A"))
        {
          if (argc < argn + 2)
            syntax(argv[0]);
	  if (!opt_ec)
	    opt_ec = 1;
	  std::istream* in;
          if (strcmp(argv[++argn], "-"))
            {
              in = new std::ifstream(argv[argn]);
              if (!*in)
                {
                  delete in;
                  std::cerr << "Failed to open " << argv[argn] << std::endl;
                  exit(2);
                }
            }
          else
	    {
	      in = &std::cin;
	    }

          while (in->good())
            {
              std::string input;
              if (std::getline(*in, input, '\n').fail())
		break;
	      else if (input == "")
		break;
	      ec_algo a = { input, nullptr };
	      ec_algos.push_back(a);
	    }

	  if (in != &std::cin)
	    delete in;
        }
      else if (!strncmp(argv[argn], "ar:", 3))
        {
          if (options.parse_options(argv[argn]))
            {
              std::cerr << "Failed to parse " << argv[argn] << std::endl;
              exit(2);
            }
        }
      else if (!strcmp(argv[argn], "-d"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_d = to_float_nonneg(argv[++argn], "-d");
	}
      else if (!strcmp(argv[argn], "-D"))
	{
	  opt_degen = true;
	  if (!opt_ec)
	    opt_ec = 1;
	}
      else if (!strcmp(argv[argn], "-det"))
	{
	  opt_det = true;
	}
      else if (!strcmp(argv[argn], "-e"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_ec = to_int_nonneg(argv[++argn], "-e");
	}
      else if (!strcmp(argv[argn], "-g"))
	{
	  opt_dot = true;
	}
      else if (!strcmp(argv[argn], "-H"))
	{
	  if (argc < argn + 1)
	    syntax(argv[0]);
	  stop_on_first_difference = true;
	}
      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], "-m"))
	{
	  opt_reduce = true;
	  opt_replay = true;
	  if (!opt_ec)
	    opt_ec = 1;
	}
      else if (!strcmp(argv[argn], "-n"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_n = to_int_pos(argv[++argn], "-n");
	}
      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_pos(argv[++argn], "-R");
	}
      else if (!strcmp(argv[argn], "-s"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_ec_seed = to_int_nonneg(argv[++argn], "-s");
	  spot::srand(opt_ec_seed);
	}
      else if (!strcmp(argv[argn], "-S"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_S = to_int_pos(argv[++argn], "-S");
	}
      else if (!strcmp(argv[argn], "-t"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_t = to_float_nonneg(argv[++argn], "-t");
	}
      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_pos(argv[++argn], "-f");
	}
      else if (!strcmp(argv[argn], "-F"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_F = to_int_nonneg(argv[++argn], "-F");
	}
      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_nonneg(argv[++argn], "-l");
	}
      else if (!strcmp(argv[argn], "-u"))
	{
	  opt_u = true;
	}
      else
	{
	  ap->insert(env.require(argv[argn]));
	}
    }

  spot::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);
    }

  if (ec_algos.empty())
    {
      const char** i = default_algos;
      while (*i)
	{
	  ec_algo a = { *(i++), nullptr };
	  ec_algos.push_back(a);
	}
    }

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

  if (opt_ec)
    {
      for (unsigned i = 0; i < ec_algos.size(); ++i)
	{
	  const char* err;
	  ec_algos[i].inst =
	    spot::make_emptiness_check_instantiator(ec_algos[i].name.c_str(),
						    &err);
	  if (!ec_algos[i].inst)
	    {
	      std::cerr << "Parse error after `" << err << '\'' << std::endl;
	      exit(1);
	    }
	  ec_algos[i].inst->options().set(options);
	}
    }

  do
    {
      if (opt_F)
        {
          spot::formula f =
	    generate_formula(rl, simp, opt_f, opt_ec_seed, opt_l, opt_u);
          if (!f)
            exit(1);
          formula = spot::ltl_to_tgba_fm(f, dict, true);
        }
      else if (opt_i)
        {
          if (formula_file->good())
            {
              std::string input;
              if (std::getline(*formula_file, input, '\n').fail())
		break;
	      else if (input == "")
		break;
              spot::parse_error_list pel;
              auto f = spot::parse_infix_psl(input, pel, env);
              if (spot::format_parse_errors(std::cerr, input, pel))
		{
		  exit_code = 1;
		  break;
		}
              formula = spot::ltl_to_tgba_fm(f, dict, true);
              auto* tmp = spot::atomic_prop_collect(f);
              for (auto i: *tmp)
		apf->insert(i);
              delete tmp;
            }
          else
            {
              if (formula_file->bad())
                std::cerr << "Failed to read " << opt_i << std::endl;
              break;
            }
        }

      for (auto i: *ap)
	apf->insert(i);

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


	      spot::twa_graph_ptr a =