randtgba.cc 31.9 KB
Newer Older
1
// -*- coding: utf-8 -*-
2 3
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire
// de Recherche et Développement de l'Epita (LRDE).
4
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris
5 6
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
7 8 9 10 11
//
// 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
12
// the Free Software Foundation; either version 3 of the License, or
13 14 15 16 17 18 19 20
// (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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
22

23
#include <cassert>
24 25
#include <cstdlib>
#include <iostream>
26
#include <iomanip>
27
#include <sstream>
28 29
#include <fstream>
#include <string>
30
#include <utility>
31
#include <set>
32
#include <vector>
33
#include "tl/parse.hh"
34 35 36 37 38
#include "tl/apcollect.hh"
#include "tl/randomltl.hh"
#include "tl/print.hh"
#include "tl/length.hh"
#include "tl/simplify.hh"
39 40 41
#include "twaalgos/randomgraph.hh"
#include "twaalgos/hoa.hh"
#include "twaalgos/stats.hh"
42
#include "tl/defaultenv.hh"
43
#include "twaalgos/dot.hh"
44
#include "misc/random.hh"
45
#include "misc/optionmap.hh"
46 47
#include "twaalgos/degen.hh"
#include "twaalgos/product.hh"
48
#include "misc/timer.hh"
49

50
#include "twaalgos/ltl2tgba_fm.hh"
51

52 53 54 55
#include "twaalgos/emptiness.hh"
#include "twaalgos/emptiness_stats.hh"
#include "twaalgos/reducerun.hh"
#include "twaalgos/replayrun.hh"
56

57 58
struct ec_algo
{
59
  std::string name;
60
  spot::emptiness_check_instantiator_ptr inst;
61
};
62

63 64 65 66 67 68 69 70 71 72 73 74 75 76
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",
77
  "Tau03_opt(condstack)",
78 79
  "Tau03_opt(condstack ordering)",
  "Tau03_opt(condstack ordering !weights)",
80
  nullptr
81 82 83
};

std::vector<ec_algo> ec_algos;
84

85
static spot::emptiness_check_ptr
86 87
cons_emptiness_check(int num, spot::const_twa_graph_ptr a,
		     const spot::const_twa_graph_ptr& degen,
88
		     unsigned int n_acc)
89
{
90
  auto inst = ec_algos[num].inst;
91 92
  if (n_acc < inst->min_acceptance_conditions()
      || n_acc > inst->max_acceptance_conditions())
93 94
    a = degen;
  if (a)
95
    return inst->instantiate(a);
96
  return nullptr;
97 98
}

99
static void
100 101 102 103
syntax(char* prog)
{
  std::cerr << "Usage: "<< prog << " [OPTIONS...] PROPS..." << std::endl
	    << std::endl
104
	    << "General Options:" << std::endl
105 106
	    << "  -0      suppress default output, just generate the graph"
	    << " in memory" << std::endl
107 108 109 110 111 112 113
	    << "  -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
114
	    << std::endl
115
	    << "Graph Generation Options:" << std::endl
116
	    << "  -a N F  number of acceptance conditions and probability that"
117 118
	    << " one is true" << std::endl
	    << "            [0 0.0]" << std::endl
119
	    << "  -d F    density of the graph [0.2]" << std::endl
120 121 122
	    << "  -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
123
	    << "  -det    generate a deterministic and complete graph [false]"
124 125
	    << std::endl
	    << "LTL Formula Generation Options:" << std::endl
126 127
	    << "  -dp     dump priorities, do not generate any formula"
	    << std::endl
128
	    << "  -f N    size of the formula [15]" << std::endl
129
	    << "  -F N    number of formulae to generate [0]" << std::endl
130 131 132
	    << "  -l N    simplify formulae using all available reductions"
	    << " and reject those" << std::endl
	    << "            strictly smaller than N" << std::endl
133
	    << "  -i FILE do not generate formulae, read them from FILE"
134
	    << std::endl
135
	    << "  -p S    priorities to use" << std::endl
136
	    << "  -S N    skip N formulae before starting to use them"
137
	    << std::endl
138 139
	    << "            (useful to replay a specific seed when -u is used)"
	    << std::endl
140
	    << "  -u      generate unique formulae" << std::endl
141
	    << std::endl
142
	    << "Emptiness-Check Options:" << std::endl
143
	    << "  -A FILE use all algorithms listed in FILE" << std::endl
144 145 146 147 148
	    << "  -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
149 150
	    << "  -H      halt on the first statistic difference in algorithms"
	    << std::endl
151 152
	    << "  -m      try to reduce runs, in a second pass (implies -r)"
            << std::endl
153 154
	    << "  -R N    repeat each emptiness-check and accepting run "
	    << "computation N times" << std::endl
155
	    << "  -r      compute and replay accepting runs (implies -e)"
156
	    << std::endl
157 158
	    << "  ar:MODE select the mode MODE for accepting runs computation "
            << "(implies -r)" << std::endl
159
	    << std::endl
160 161
	    << "Where:" << std::endl
	    << "  F      are floats between 0.0 and 1.0 inclusive" << std::endl
162 163
	    << "  E      are floating values" << std::endl
	    << "  S      are `KEY=E, KEY=E, ...' strings" << std::endl
164 165
	    << "  N      are positive integers" << std::endl
	    << "  PROPS  are the atomic properties to use on transitions"
166
	    << std::endl
167 168 169 170 171
	    << "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;
172 173 174
  exit(2);
}

175

176
static int
177 178 179 180 181 182 183 184 185 186 187 188
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;
}

189
static int
190 191 192 193 194 195 196 197 198 199 200 201
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;
}

202
static int
203 204 205 206 207 208 209 210 211 212 213 214
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;
}

215
static float
216 217 218
to_float(const char* s)
{
  char* endptr;
219 220
  // Do not use strtof(), it does not exist on Solaris 9.
  float res = strtod(s, &endptr);
221 222 223 224 225 226 227 228
  if (*endptr)
    {
      std::cerr << "Failed to parse `" << s << "' as a float." << std::endl;
      exit(1);
    }
  return res;
}

229
static float
230 231 232 233 234 235 236 237 238 239 240 241
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;
}

242 243 244 245 246 247 248 249 250
// Convertors using for statistics:

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

251
spot::twa_statistics prod_stats;
252

253
static float
254 255 256 257
prod_conv(const char* name, unsigned x)
{
  float y = static_cast<float>(x);
  if (!strcmp(name, "transitions"))
258
    return y / prod_stats.edges * 100.0;
259 260 261 262
  return y / prod_stats.states * 100.0;
}

template <typename T, T (*convertor)(const char*, unsigned) = id<T> >
263
struct stat_collector
264
{
265 266
  struct one_stat
  {
267 268 269
    T min;
    T max;
    T tot;
270
    unsigned n;
271

272 273 274 275 276 277
    one_stat()
      : n(0)
    {
    }

    void
278
    count(T val)
279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298
    {
      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()
299
  {
300
    return stats.empty();
301 302 303
  }

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

313 314
  std::ostream&
  display(std::ostream& os,
315
	  const alg_1stat_map& m, const std::string& title,
316
	  bool total = true) const
317
  {
318
    std::ios::fmtflags old = os.flags();
319
    os << std::setw(25) << "" << " | "
320
       << std::setw(30) << std::left << title << std::right << '|' << std::endl
321
       << std::setw(25) << "algorithm"
322 323
       << " |   min   < mean  < max | total |  n"
       << std::endl
324
       << std::setw(64) << std::setfill('-') << "" << std::setfill(' ')
325
       << std::endl;
326 327 328 329
    os << std::right << std::fixed << std::setprecision(1);
    for (typename alg_1stat_map::const_iterator i = m.begin();
	 i != m.end(); ++i)
      {
330
	os << std::setw(25) << i->first << " |"
331
	   << std::setw(6) << i->second.min
332
	   << ' '
333 334
	   << std::setw(8)
	   << static_cast<float>(i->second.tot) / i->second.n
335
	   << ' '
336 337 338 339 340 341 342 343 344 345
	   << 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;
      }
346
    os << std::setw(64) << std::setfill('-') << "" << std::setfill(' ')
347
       << std::endl;
348
    os << std::setiosflags(old);
349 350 351 352
    return os;
  }

  std::ostream&
353
  display(std::ostream& os, bool total = true) const
354
  {
355
    typename stats_alg_map::const_iterator i;
356
    for (i = stats.begin(); i != stats.end(); ++i)
357
      display(os, i->second, i->first, total);
358
    return os;
359
  }
360 361


362 363
};

364
struct ar_stat
365 366 367 368 369 370 371 372 373 374 375
{
  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;

376
  ar_stat()
377 378 379 380 381
    : n(0)
  {
  }

  void
382
  count(const spot::const_twa_run_ptr& run)
383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405
  {
    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;
      }
  }
};

406 407
stat_collector<unsigned> sc_ec;
stat_collector<unsigned> sc_arc;
408

409
typedef stat_collector<float, prod_conv> ec_ratio_stat_type;
410 411 412
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;
413

414
ec_ratio_stat_type arc_ratio_stats;
415

416 417 418 419
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.

420

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

428
  std::cout << std::setw(25) << ""
429 430
            << " |         prefix        |         cycle         |"
            << std::endl
431
            << std::setw(25) << "algorithm"
432 433 434 435 436
            << " |   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();
437
	   i != ar_stats.end(); ++i)
438
    std::cout << std::setw(25) << i->first << " |"
439
              << std::setw(6) << i->second.min_prefix
440
              << ' '
441 442
              << std::setw(8)
              << static_cast<float>(i->second.tot_prefix) / i->second.n
443
              << ' '
444 445 446
              << std::setw(6) << i->second.max_prefix
              << " |"
              << std::setw(6) << i->second.min_cycle
447
              << ' '
448 449
              << std::setw(8)
              << static_cast<float>(i->second.tot_cycle) / i->second.n
450
              << ' '
451 452 453 454 455 456
              << 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
457
            << std::setw(25) << ""
458 459
            << " |          runs         |         total         |"
            << std::endl <<
460
	std::setw(25) << "algorithm"
461 462 463 464 465
            << " |   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();
466
	   i != ar_stats.end(); ++i)
467
    std::cout << std::setw(25) << i->first << " |"
468 469
              << std::setw(6)
              << i->second.min_run
470
              << ' '
471 472 473
              << std::setw(8)
              << static_cast<float>(i->second.tot_prefix
                                    + i->second.tot_cycle) / i->second.n
474
              << ' '
475 476 477 478
              << std::setw(6)
              << i->second.max_run
              << " |"
              << std::setw(6) << i->second.tot_prefix
479
              << ' '
480
              << std::setw(6) << i->second.tot_cycle
481
              << ' '
482 483 484 485
              << std::setw(8) << i->second.tot_prefix + i->second.tot_cycle
              << " |"
              << std::setw(4) << i->second.n
              << std::endl;
486
  std::cout << std::setiosflags(old);
487 488
}

489
static spot::formula
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
490
generate_formula(const spot::random_ltl& rl,
491
		 spot::tl_simplifier& simp,
492
		 int opt_f, int opt_s,
493 494 495 496 497 498 499 500
                 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++);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
501
      spot::formula f;
502 503 504 505 506 507
      int max_tries_l = 1000;
      while (max_tries_l--)
        {
          f = rl.generate(opt_f);
          if (opt_l)
            {
508
              f = simp.simplify(f);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
509
              if (spot::length(f) < opt_l)
510
		continue;
511 512 513
            }
          else
            {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
514
              assert(spot::length(f) <= opt_f);
515 516 517 518 519 520 521 522
            }
          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;
523
          return nullptr;
524
        }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
525
      std::string txt = spot::str_psl(f);
526
      if (!opt_u || unique.insert(txt).second)
527
	return f;
528 529 530 531
    }
  assert(opt_u);
  std::cerr << "Failed to generate another unique formula."
            << std::endl;
532
  return nullptr;
533 534
}

535 536 537
int
main(int argc, char** argv)
{
538
  bool opt_paper = false;
539 540
  bool opt_dp = false;
  int opt_f = 15;
541
  int opt_F = 0;
542 543 544
  char* opt_p = nullptr;
  char* opt_i = nullptr;
  std::istream *formula_file = nullptr;
545 546
  int opt_l = 0;
  bool opt_u = false;
547
  int opt_S = 0;
548

549 550 551 552 553
  int opt_n_acc = 0;
  float opt_a = 0.0;
  float opt_d = 0.2;
  int opt_n = 20;
  float opt_t = 0.5;
554
  bool opt_det = false;
555

556
  bool opt_0 = false;
557 558 559
  bool opt_z = false;
  bool opt_Z = false;

560 561
  int opt_R = 0;

562
  bool opt_dot = false;
563 564
  int opt_ec = 0;
  int opt_ec_seed = 0;
565
  bool opt_reduce = false;
566
  bool opt_replay = false;
567
  bool opt_degen = false;
568 569
  int argn = 0;

570 571
  int exit_code = 0;

572 573
  bool stop_on_first_difference = false;

574 575
  spot::twa_graph_ptr formula = nullptr;
  spot::twa_graph_ptr product = nullptr;
576

577 578
  spot::option_map options;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
579 580
  auto& env = spot::default_environment::instance();
  spot::atomic_prop_set* ap = new spot::atomic_prop_set;
581
  auto dict = spot::make_bdd_dict();
582

583 584
  spot::tl_simplifier_options simpopt(true, true, true, true, true);
  spot::tl_simplifier simp(simpopt);
585

586 587 588 589 590
  if (argc <= 1)
    syntax(argv[0]);

  while (++argn < argc)
    {
591 592 593 594
      if (!strcmp(argv[argn], "-0"))
	{
	  opt_0 = true;
	}
595 596 597
      else if (!strcmp(argv[argn], "-1"))
	{
	  opt_paper = true;
598
	  opt_z = true;
599
	}
600
      else if (!strcmp(argv[argn], "-a"))
601 602 603
	{
	  if (argc < argn + 3)
	    syntax(argv[0]);
604 605
	  opt_n_acc = to_int_nonneg(argv[++argn], "-a");
	  opt_a = to_float_nonneg(argv[++argn], "-a");
606
	}
607 608 609 610
      else if (!strcmp(argv[argn], "-A"))
        {
          if (argc < argn + 2)
            syntax(argv[0]);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
611 612
	  if (!opt_ec)
	    opt_ec = 1;
613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635
	  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;
636
	      ec_algo a = { input, nullptr };
637 638 639 640 641 642
	      ec_algos.push_back(a);
	    }

	  if (in != &std::cin)
	    delete in;
        }
643 644 645 646 647 648 649 650
      else if (!strncmp(argv[argn], "ar:", 3))
        {
          if (options.parse_options(argv[argn]))
            {
              std::cerr << "Failed to parse " << argv[argn] << std::endl;
              exit(2);
            }
        }
651 652
      else if (!strcmp(argv[argn], "-d"))
	{
653
	  if (argc < argn + 2)
654
	    syntax(argv[0]);
655
	  opt_d = to_float_nonneg(argv[++argn], "-d");
656
	}
657 658 659 660 661 662
      else if (!strcmp(argv[argn], "-D"))
	{
	  opt_degen = true;
	  if (!opt_ec)
	    opt_ec = 1;
	}
663 664 665 666
      else if (!strcmp(argv[argn], "-det"))
	{
	  opt_det = true;
	}
667 668 669 670
      else if (!strcmp(argv[argn], "-e"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
671
	  opt_ec = to_int_nonneg(argv[++argn], "-e");
672
	}
673 674 675 676
      else if (!strcmp(argv[argn], "-g"))
	{
	  opt_dot = true;
	}
677
      else if (!strcmp(argv[argn], "-H"))
678
	{
679 680 681
	  if (argc < argn + 1)
	    syntax(argv[0]);
	  stop_on_first_difference = true;
682
	}
683 684 685 686 687 688 689 690
      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);
691
              if (!*formula_file)
692 693 694 695 696 697 698 699 700
                {
                  delete formula_file;
                  std::cerr << "Failed to open " << opt_i << std::endl;
                  exit(2);
                }
            }
          else
            formula_file = &std::cin;
        }
701 702 703 704 705 706 707
      else if (!strcmp(argv[argn], "-m"))
	{
	  opt_reduce = true;
	  opt_replay = true;
	  if (!opt_ec)
	    opt_ec = 1;
	}
708 709
      else if (!strcmp(argv[argn], "-n"))
	{
710
	  if (argc < argn + 2)
711
	    syntax(argv[0]);
712
	  opt_n = to_int_pos(argv[++argn], "-n");
713
	}
714 715 716 717 718 719
      else if (!strcmp(argv[argn], "-r"))
	{
	  opt_replay = true;
	  if (!opt_ec)
	    opt_ec = 1;
	}
720 721 722 723
      else if (!strcmp(argv[argn], "-R"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
724
	  opt_R = to_int_pos(argv[++argn], "-R");
725
	}
726 727
      else if (!strcmp(argv[argn], "-s"))
	{
728
	  if (argc < argn + 2)
729
	    syntax(argv[0]);
730
	  opt_ec_seed = to_int_nonneg(argv[++argn], "-s");
731
	  spot::srand(opt_ec_seed);
732
	}
733 734 735 736 737 738
      else if (!strcmp(argv[argn], "-S"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_S = to_int_pos(argv[++argn], "-S");
	}
739 740
      else if (!strcmp(argv[argn], "-t"))
	{
741
	  if (argc < argn + 2)
742
	    syntax(argv[0]);
743
	  opt_t = to_float_nonneg(argv[++argn], "-t");
744
	}
745 746 747 748 749 750 751 752
      else if (!strcmp(argv[argn], "-z"))
	{
	  opt_z = true;
	}
      else if (!strcmp(argv[argn], "-Z"))
	{
	  opt_Z = opt_z = true;
	}
753 754 755 756 757 758 759 760
      else if (!strcmp(argv[argn], "-dp"))
	{
	  opt_dp = true;
	}
      else if (!strcmp(argv[argn], "-f"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
761
	  opt_f = to_int_pos(argv[++argn], "-f");
762 763 764 765 766
	}
      else if (!strcmp(argv[argn], "-F"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
767
	  opt_F = to_int_nonneg(argv[++argn], "-F");
768 769 770 771 772 773 774 775 776 777 778
	}
      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]);
779
	  opt_l = to_int_nonneg(argv[++argn], "-l");
780 781 782 783 784
	}
      else if (!strcmp(argv[argn], "-u"))
	{
	  opt_u = true;
	}
785 786
      else
	{
787
	  ap->insert(env.require(argv[argn]));
788 789 790
	}
    }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
791
  spot::random_ltl rl(ap);
792 793 794 795
  const char* tok = rl.parse_options(opt_p);
  if (tok)
    {
      std::cerr << "failed to parse probabilities near `"
796
		<< tok << '\'' << std::endl;
797 798 799 800 801 802
      exit(2);
    }

  if (opt_l > opt_f)
    {
      std::cerr << "-l's argument (" << opt_l << ") should not be larger than "
803
		<< "-f's (" << opt_f << ')' << std::endl;
804 805 806 807 808 809 810 811 812
      exit(2);
    }

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

813 814 815 816 817
  if (ec_algos.empty())
    {
      const char** i = default_algos;
      while (*i)
	{
818
	  ec_algo a = { *(i++), nullptr };
819 820 821 822
	  ec_algos.push_back(a);
	}
    }

823 824
  spot::timer_map tm_ec;
  spot::timer_map tm_ar;
825
  std::set<int> failed_seeds;
826
  int init_opt_ec = opt_ec;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
827
  spot::atomic_prop_set* apf = new spot::atomic_prop_set;
828

829 830
  if (opt_ec)
    {
831
      for (unsigned i = 0; i < ec_algos.size(); ++i)
832 833 834
	{
	  const char* err;
	  ec_algos[i].inst =
835 836
	    spot::make_emptiness_check_instantiator(ec_algos[i].name.c_str(),
						    &err);
837
	  if (!ec_algos[i].inst)
838
	    {
839
	      std::cerr << "Parse error after `" << err << '\'' << std::endl;
840 841 842 843 844 845
	      exit(1);
	    }
	  ec_algos[i].inst->options().set(options);
	}
    }

846 847
  do
    {
848 849
      if (opt_F)
        {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
850
          spot::formula f =
851
	    generate_formula(rl, simp, opt_f, opt_ec_seed, opt_l, opt_u);
852 853 854 855
          if (!f)
            exit(1);
          formula = spot::ltl_to_tgba_fm(f, dict, true);
        }
856 857 858 859 860
      else if (opt_i)
        {
          if (formula_file->good())
            {
              std::string input;
861 862 863 864
              if (std::getline(*formula_file, input, '\n').fail())
		break;
	      else if (input == "")
		break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
865 866 867
              spot::parse_error_list pel;
              auto f = spot::parse_infix_psl(input, pel, env);
              if (spot::format_parse_errors(std::cerr, input, pel))
868 869 870 871
		{
		  exit_code = 1;
		  break;
		}
872
              formula = spot::ltl_to_tgba_fm(f, dict, true);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
873
              auto* tmp = spot::atomic_prop_collect(f);
874 875
              for (auto i: *tmp)
		apf->insert(i);
876 877 878 879 880 881 882 883 884 885
              delete tmp;
            }
          else
            {
              if (formula_file->bad())
                std::cerr << "Failed to read " << opt_i << std::endl;
              break;
            }
        }

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

889
      if (!opt_S)
890
	{
891
	  do
892
	    {
893 894 895
	      if (opt_ec && !opt_paper)
		std::cout << "seed: " << opt_ec_seed << std::endl;
	      spot::srand(opt_ec_seed);
896 897


898
	      spot::twa_graph_ptr a =