randtgba.cc 39.2 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire
3
// 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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
#include <spot/tl/parse.hh>
#include <spot/tl/apcollect.hh>
#include <spot/tl/randomltl.hh>
#include <spot/tl/print.hh>
#include <spot/tl/length.hh>
#include <spot/tl/simplify.hh>
#include <spot/twaalgos/randomgraph.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/stats.hh>
#include <spot/tl/defaultenv.hh>
#include <spot/twaalgos/dot.hh>
#include <spot/misc/random.hh>
#include <spot/misc/optionmap.hh>
#include <spot/twaalgos/degen.hh>
#include <spot/twaalgos/product.hh>
#include <spot/misc/timer.hh>
49

50
#include <spot/twaalgos/ltl2tgba_fm.hh>
51

52
53
#include <spot/twaalgos/emptiness.hh>
#include <spot/twaalgos/emptiness_stats.hh>
54

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

61
62
63
64
65
66
67
const char* default_algos[] = {
  "Cou99(!poprem)",
  "Cou99(!poprem shy !group)",
  "Cou99(!poprem shy group)",
  "Cou99(poprem)",
  "Cou99(poprem shy !group)",
  "Cou99(poprem shy group)",
68
69
  "Cou99new",
  "Cou99abs",
70
71
72
73
74
75
76
  "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
cons_emptiness_check(int num, spot::const_twa_graph_ptr a,
87
88
                     const spot::const_twa_graph_ptr& degen,
                     unsigned int n_acc)
89
{
90
  auto inst = ec_algos[num].inst;
91
  if (n_acc < inst->min_sets() || n_acc > inst->max_sets())
92
93
    a = degen;
  if (a)
94
    return inst->instantiate(a);
95
  return nullptr;
96
97
}

98
static void
99
100
101
syntax(char* prog)
{
  std::cerr << "Usage: "<< prog << " [OPTIONS...] PROPS..." << std::endl
102
            << std::endl
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
            << "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 "
157
            << "(implies -r)" << std::endl
158
159
160
161
162
163
164
165
166
167
168
169
170
            << 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;
171
172
173
  exit(2);
}

174

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

188
static int
189
190
191
192
193
194
to_int_pos(const char* s, const char* arg)
{
  int res = to_int(s);
  if (res <= 0)
    {
      std::cerr << "argument of " << arg
195
                << " (" << res << ") must be positive" << std::endl;
196
197
198
199
200
      exit(1);
    }
  return res;
}

201
static int
202
203
204
205
206
207
to_int_nonneg(const char* s, const char* arg)
{
  int res = to_int(s);
  if (res < 0)
    {
      std::cerr << "argument of " << arg
208
                << " (" << res << ") must be nonnegative" << std::endl;
209
210
211
212
213
      exit(1);
    }
  return res;
}

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

228
static float
229
230
231
232
233
234
to_float_nonneg(const char* s, const char* arg)
{
  float res = to_float(s);
  if (res < 0)
    {
      std::cerr << "argument of " << arg
235
                << " (" << res << ") must be nonnegative" << std::endl;
236
237
238
239
240
      exit(1);
    }
  return res;
}

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

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

250
spot::twa_statistics prod_stats;
251

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

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

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

    void
277
    count(T val)
278
279
    {
      if (n++)
280
281
282
283
284
        {
          min = std::min(min, val);
          max = std::max(max, val);
          tot += val;
        }
285
      else
286
287
288
        {
          max = min = tot = val;
        }
289
290
291
292
293
294
295
296
297
    }
  };

  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()
298
  {
299
    return stats.empty();
300
301
302
  }

  void
303
  count(const std::string& algorithm, const spot::unsigned_statistics* s)
304
  {
305
306
307
308
    if (!s)
      return;
    spot::unsigned_statistics::stats_map::const_iterator i;
    for (i = s->stats.begin(); i != s->stats.end(); ++i)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
309
310
311
312
313
      {
        auto u = (s->*i->second)();
        auto t = convertor(i->first, u);
        stats[i->first][algorithm].count(t);
      }
314
  }
315

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

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


365
366
};

367
struct ar_stat
368
369
370
371
372
373
374
375
376
377
378
{
  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;

379
  ar_stat()
380
381
382
383
384
    : n(0)
  {
  }

  void
385
  count(const spot::const_twa_run_ptr& run)
386
387
388
389
390
  {
    int p = run->prefix.size();
    int c = run->cycle.size();
    if (n++)
      {
391
392
393
394
395
396
397
398
        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);
399
400
401
      }
    else
      {
402
403
404
        min_prefix = max_prefix = tot_prefix = p;
        min_cycle = max_cycle = tot_cycle = c;
        min_run = max_run = c + p;
405
406
407
408
      }
  }
};

409
410
stat_collector<unsigned> sc_ec;
stat_collector<unsigned> sc_arc;
411

412
typedef stat_collector<float, prod_conv> ec_ratio_stat_type;
413
414
415
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;
416

417
ec_ratio_stat_type arc_ratio_stats;
418

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

423

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

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

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

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

552
553
554
555
556
  int opt_n_acc = 0;
  float opt_a = 0.0;
  float opt_d = 0.2;
  int opt_n = 20;
  float opt_t = 0.5;
557
  bool opt_det = false;
558

559
  bool opt_0 = false;
560
561
562
  bool opt_z = false;
  bool opt_Z = false;

563
564
  int opt_R = 0;

565
  bool opt_dot = false;
566
567
  int opt_ec = 0;
  int opt_ec_seed = 0;
568
  bool opt_reduce = false;
569
  bool opt_replay = false;
570
  bool opt_degen = false;
571
572
  int argn = 0;

573
574
  int exit_code = 0;

575
576
  bool stop_on_first_difference = false;

577
578
  spot::twa_graph_ptr formula = nullptr;
  spot::twa_graph_ptr product = nullptr;
579

580
581
  spot::option_map options;

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

586
587
  spot::tl_simplifier_options simpopt(true, true, true, true, true);
  spot::tl_simplifier simp(simpopt);
588

589
590
591
592
593
  if (argc <= 1)
    syntax(argv[0]);

  while (++argn < argc)
    {
594
      if (!strcmp(argv[argn], "-0"))
595
596
597
        {
          opt_0 = true;
        }
598
      else if (!strcmp(argv[argn], "-1"))
599
600
601
602
        {
          opt_paper = true;
          opt_z = true;
        }
603
      else if (!strcmp(argv[argn], "-a"))
604
605
606
607
608
609
        {
          if (argc < argn + 3)
            syntax(argv[0]);
          opt_n_acc = to_int_nonneg(argv[++argn], "-a");
          opt_a = to_float_nonneg(argv[++argn], "-a");
        }
610
611
612
613
      else if (!strcmp(argv[argn], "-A"))
        {
          if (argc < argn + 2)
            syntax(argv[0]);
614
615
616
          if (!opt_ec)
            opt_ec = 1;
          std::istream* in;
617
618
619
620
621
622
623
624
625
626
627
          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
628
629
630
            {
              in = &std::cin;
            }
631
632
633
634
635

          while (in->good())
            {
              std::string input;
              if (std::getline(*in, input, '\n').fail())
636
637
638
639
640
641
642
643
644
                break;
              else if (input == "")
                break;
              ec_algo a = { input, nullptr };
              ec_algos.push_back(a);
            }

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

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

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

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

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

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

832
833
  if (opt_ec)
    {
834
      for (unsigned i = 0; i < ec_algos.size(); ++i)
835
836
837
838
839
840
841
842
843
844
845
846
        {
          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);
        }
847
848
    }

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

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

891
      if (!opt_S)
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
        {
          do
            {
              if (opt_ec && !opt_paper)
                std::cout << "seed: " << opt_ec_seed << std::endl;
              spot::srand(opt_ec_seed);


              spot::twa_graph_ptr a =
                spot::random_graph(opt_n, opt_d, apf, dict,
                                   opt_n_acc, opt_a, opt_t, opt_det);
              if (formula)
                a = spot::product(formula, a);

              int real_n_acc = a->acc().num_sets();

              if (opt_dot)
                {
                  print_dot(std::cout, a);
                }
              if (!opt_ec)
                {
                  if (!opt_0 && !opt_dot)
                    print_hoa(std::cout, a, nullptr);
                }
              else
                {
                  spot::twa_graph_ptr degen = nullptr;
                  if (opt_degen && real_n_acc > 1)
                    degen = degeneralize_tba(a);

                  int n_alg = ec_algos.size();
                  int n_ec = 0;
                  int n_empty = 0;
                  int n_non_empty = 0;
                  int n_maybe_empty = 0;
                  spot::unsigned_statistics_copy ostats_ec, ostats_arc;

                  for (int i = 0; i < n_alg; ++i)
                    {
                      auto ec = cons_emptiness_check(i, a, degen, real_n_acc);
                      if (!ec)
                        continue;
                      ++n_ec;
                      const std::string algo = ec_algos[i].name;
                      if (!opt_paper)
                        {
                          std::cout.width(32);
                          std::cout << algo << ": ";
                        }
                      tm_ec.start(algo);
                      spot::emptiness_check_result_ptr res;
                      for (int count = opt_R;;)
                        {
                          res = ec->check();
                          if (count-- <= 0)
                            break;
                          ec = cons_emptiness_check(i, a, degen, real_n_acc);
                        }
                      tm_ec.stop(algo);
                      auto ecs = ec->statistics();
                      if (opt_z && res)
                        {
                          // Notice that ratios are computed w.r.t. the
                          // generalized automaton a.
                          prod_stats = spot::stats_reachable(a);
                        }
                      else
                        {
                          // To trigger a division by 0 if used erroneously.
                          prod_stats.states = 0;
                          prod_stats.edges = 0;
                        }

                      if (opt_z && ecs)
                        {
                          sc_ec.count(algo, ecs);
                          if (res)
                            {
                              ec_ratio_stats[real_n_acc].count(algo, ecs);
                              glob_ec_ratio_stats.count(algo, ecs);
                            }
                        }

                      if (stop_on_first_difference && ecs)
                        if (!ostats_ec.seteq(*ecs))
                          {
                            std::cout << "DIFFERING STATS for emptiness check,"
                                      << " halting... ";
                            opt_ec = n_alg = opt_F = 0;
                          }

                      if (res)
                        {
                          if (!opt_paper)
                            std::cout << "acc. run";
                          ++n_non_empty;
                          if (opt_replay)
                            {
                              spot::twa_run_ptr run;
                              tm_ar.start(algo);
                              for (int count = opt_R;;)
                                {
                                  run = res->accepting_run();
                                  if (count-- <= 0 || !run)
                                    break;
                                }
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
                              if (!run)
                                tm_ar.cancel(algo);
                              else
                                tm_ar.stop(algo);

                              const spot::unsigned_statistics* s
                                = res->statistics();
                              if (opt_z)
                                {
                                  // Count only the last run (the
                                  // other way would be to divide
                                  // the stats by opt_R).
                                  sc_arc.count(algo, s);
                                  arc_ratio_stats.count(algo, s);
                                }
                              if (stop_on_first_difference && s)
                                if (!ostats_arc.seteq(*s))
                                  {
                                    std::cout << "DIFFERING STATS for "
                                              << "accepting runs,"
                                              << " halting... ";
                                    opt_ec = n_alg = opt_F = 0;
                                  }
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
                              if (!run)
                                {
                                  if (!opt_paper)
                                    std::cout << " exists, not computed";
                                }
                              else
                                {
                                  std::ostringstream s;
                                  if (!run->replay(s))
                                    {
                                      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)
                                    {
                                      auto redrun = run->reduce();
                                      if (!redrun->replay(s))
                                        {
                                          if (!opt_paper)
                                            std::cout
                                              << ", but could not replay "
                                              << "its minimization (ERROR!)";
                                          failed_seeds.insert(opt_ec_seed);
                                        }
                                      else
                                        {
                                          if (!opt_paper)
                                            std::cout << ", reduced";
                                          if (opt_z)
                                            mar_stats[algo].count(redrun);
                                        }
                                      if (opt_z && !opt_paper)
                                        {
                                          std::cout << " ["
                                                    << redrun->prefix.size()
                                                    << '+'
                                                    << redrun->cycle.size()
                                                    << ']';
                                        }
                                    }
                                }
                            }
                          if (!opt_paper)
                            std::cout << std::endl;
                        }
                      else
                        {
                          if (ec->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);
                    }

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

              if (opt_ec)
                {
                  --opt_ec;
                  ++opt_ec_seed;
                }
            }
          while (opt_ec);
        }
1122
      else
1123
1124
1125
1126
        {
          --opt_S;
          opt_ec_seed += init_opt_ec;
        }
1127
1128
1129
1130

      if (opt_F)
        --opt_F;
      opt_ec = init_opt_ec;
1131
      apf->clear();
1132
    }
1133
  while (opt_F || opt_i);
1134

1135
  if (!opt_paper && opt_z)
1136
1137
    {
      if (!sc_ec.empty())
1138
1139
1140
1141
1142
1143
        {
          std::cout << std::endl
                    << "Statistics about emptiness checks:"
                    << std::endl;
          sc_ec.display(std::cout);
        }
1144
      if (!sc_arc.empty())
1145
1146
1147
1148
1149
1150
        {
          std::cout << std::endl
                    << "Statistics about accepting run computations:"
                    << std::endl;
          sc_arc.display(std::cout);
        }
1151
      if (!glob_ec_ratio_stats.empty())
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
        {
          std::cout << std::endl
                    << "Emptiness check ratios for non-empty automata:"
                    << std::endl << "all tests"
                    << std::endl;
          glob_ec_ratio_stats.display(std::cout, false);
          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::cout << "tests with " << i->first
                          << " acceptance conditions"
                          << std::endl;
                i->second.display(std::cout, false);
              }
        }
1168
      if (!ar_stats.empty())
1169
        print_ar_stats(ar_stats, "Statistics about accepting runs:");
1170
      if (!mar_stats.empty())
1171
        print_ar_stats(mar_stats, "Statistics about reduced accepting runs:");
1172
      if (!arc_ratio_stats.empty())
1173
1174
1175
1176
1177
        {
          std::cout << std::endl
                    << "Accepting run ratios:" << std::endl;
          arc_ratio_stats.display(std::cout, false);
        }
1178
      if (!tm_ec.empty())
1179
1180
1181
1182
1183
        {
          std::cout << std::endl
                    << "emptiness checks cumulated timings:" << std::endl;
          tm_ec.print(std::cout);
        }
1184
      if (!tm_ar.empty())
1185
1186
1187
1188
1189
        {
          std::cout << std::endl
                    << "accepting runs cumulated timings:" << std::endl;
          tm_ar.print(std::cout);
        }
1190
    }
1191
1192
1193
1194
1195
1196
1197
  else if (opt_paper)
    {
      std::cout << "Emptiness check ratios" << std::endl;
      std::cout << std::right << std::fixed << std::setprecision(1);
      ec_ratio_stat_type::stats_alg_map& stats = glob_ec_ratio_stats.stats;
      typedef ec_ratio_stat_type::alg_1stat_map::const_iterator ec_iter;

1198
      for (unsigned ai = 0; ai < ec_algos.size(); ++ai)
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
        {
          const std::string algo = ec_algos[ai].name;

          int n = -1;

          std::cout << std::setw(25)  << algo << ' ' << std::setw(8);

          ec_iter i = stats["states"].find(algo);
          if (i != stats["states"].end())
            {
              std::cout << i->second.tot / i->second.n;
              n = i->second.n;
            }
          else
            std::cout << "";
          std::cout << ' ' << std::setw(8);

          i = stats["transitions"].find(algo);
          if (i != stats["transitions"].end())
            {
              std::cout << i->second.tot / i->second.n;
              n = i->second.n;
            }
          else
            std::cout << "";