ltlcross.cc 45.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
3
// Développement de l'Epita (LRDE).
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
//
// 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 "common_sys.hh"

#include <string>
#include <iostream>
#include <sstream>
26
#include <fstream>
27
28
29
#include <cstdlib>
#include <cstdio>
#include <argp.h>
30
31
32
#include <signal.h>
#include <unistd.h>
#include <sys/wait.h>
33
#include "error.h"
34
#include "argmatch.h"
35
36
37

#include "common_setup.hh"
#include "common_cout.hh"
38
#include "common_conv.hh"
39
#include "common_finput.hh"
40
#include "dstarparse/public.hh"
41
#include "hoaparse/public.hh"
42
43
44
45
#include "ltlast/unop.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/apcollect.hh"
#include "ltlvisit/lbt.hh"
46
#include "ltlvisit/mutation.hh"
47
#include "ltlvisit/relabel.hh"
48
#include "tgbaalgos/lbtt.hh"
49
#include "tgbaalgos/product.hh"
50
51
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/randomgraph.hh"
52
#include "tgbaalgos/sccinfo.hh"
53
#include "tgbaalgos/isweakscc.hh"
54
55
#include "tgbaalgos/reducerun.hh"
#include "tgbaalgos/word.hh"
56
#include "tgbaalgos/dtgbacomp.hh"
57
#include "misc/formater.hh"
58
59
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/isdet.hh"
60
#include "misc/escape.hh"
61
#include "misc/hash.hh"
62
#include "misc/random.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
63
#include "misc/tmpfile.hh"
64
#include "misc/timer.hh"
65

66
67
68
69
70
71
72
73
// Disable handling of timeout on systems that miss kill() or alarm().
// For instance MinGW.
#if HAVE_KILL && HAVE_ALARM
# define ENABLE_TIMEOUT 1
#else
# define ENABLE_TIMEOUT 0
#endif

74
75
const char argp_program_doc[] ="\
Call several LTL/PSL translators and cross-compare their output to detect \
76
bugs, or to gather statistics.  The list of formulas to use should be \
77
supplied on standard input, or using the -f or -F options.\v\
78
79
80
81
Exit status:\n\
  0  everything went fine (timeouts are OK too)\n\
  1  some translator failed to output something we understand, or failed\n\
     sanity checks (statistics were output nonetheless)\n\
82
  2  ltlcross aborted on error\n\
83
";
84
85
86
87


#define OPT_STATES 1
#define OPT_DENSITY 2
88
89
#define OPT_JSON 3
#define OPT_CSV 4
90
#define OPT_DUPS 5
91
#define OPT_NOCHECKS 6
92
#define OPT_STOP_ERR 7
93
#define OPT_SEED 8
94
#define OPT_PRODUCTS 9
95
#define OPT_COLOR 10
96
#define OPT_NOCOMP 11
97
#define OPT_OMIT 12
98
#define OPT_BOGUS 13
99
#define OPT_VERBOSE 14
100
#define OPT_GRIND 15
101
102
103
104

static const argp_option options[] =
  {
    /**************************************************/
105
    { 0, 0, 0, 0, "Specifying translators to call:", 2 },
106
    { "translator", 't', "COMMANDFMT", 0,
107
      "register one translator to call", 0 },
108
    { "timeout", 'T', "NUMBER", 0, "kill translators after NUMBER seconds", 0 },
109
110
111
112
    /**************************************************/
    { 0, 0, 0, 0,
      "COMMANDFMT should specify input and output arguments using the "
      "following character sequences:", 3 },
113
114
115
116
117
    { "%f,%s,%l,%w", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the formula as a (quoted) string in Spot, Spin, LBT, or Wring's syntax",
      0 },
    { "%F,%S,%L,%W", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the formula as a file in Spot, Spin, LBT, or Wring's syntax", 0 },
118
119
120
    { "%N,%T,%D,%H", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the automaton is output as a Never claim, or in LBTT's, in LTL2DSTAR's,"
      "or in the HOA format", 0 },
121
122
123
    { 0, 0, 0, 0,
      "If either %l, %L, or %T are used, any input formula that does "
      "not use LBT-style atomic propositions (i.e. p0, p1, ...) will be "
124
125
126
127
      "relabeled automatically.\n"
      "Furthermore, if COMMANDFMT has the form \"{NAME}CMD\", then only CMD "
      "will be passed to the shell, and NAME will be used to name the tool "
      "in the CSV or JSON outputs.", 0 },
128
    /**************************************************/
129
    { 0, 0, 0, 0, "ltlcross behavior:", 4 },
130
131
132
133
134
    { "allow-dups", OPT_DUPS, 0, 0,
      "translate duplicate formulas in input", 0 },
    { "no-checks", OPT_NOCHECKS, 0, 0,
      "do not perform any sanity checks (negated formulas "
      "will not be translated)", 0 },
135
136
    { "no-complement", OPT_NOCOMP, 0, 0,
      "do not complement deterministic automata to perform extra checks", 0 },
137
138
139
    { "stop-on-error", OPT_STOP_ERR, 0, 0,
      "stop on first execution error or failure to pass"
      " sanity checks (timeouts are OK)", 0 },
140
141
    /**************************************************/
    { 0, 0, 0, 0, "State-space generation:", 5 },
142
143
144
145
146
    { "states", OPT_STATES, "INT", 0,
      "number of the states in the state-spaces (200 by default)", 0 },
    { "density", OPT_DENSITY, "FLOAT", 0,
      "probability, between 0.0 and 1.0, to add a transition between "
      "two states (0.1 by default)", 0 },
147
148
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0 by default)", 0 },
149
150
151
    { "products", OPT_PRODUCTS, "[+]INT", 0,
      "number of products to perform (1 by default), statistics will be "
      "averaged unless the number is prefixed with '+'", 0 },
152
    /**************************************************/
153
    { 0, 0, 0, 0, "Statistics output:", 6 },
154
155
156
157
    { "json", OPT_JSON, "FILENAME", OPTION_ARG_OPTIONAL,
      "output statistics as JSON in FILENAME or on standard output", 0 },
    { "csv", OPT_CSV, "FILENAME", OPTION_ARG_OPTIONAL,
      "output statistics as CSV in FILENAME or on standard output", 0 },
158
159
    { "omit-missing", OPT_OMIT, 0, 0,
      "do not output statistics for timeouts or failed translations", 0 },
160
    /**************************************************/
161
    { 0, 0, 0, 0, "Miscellaneous options:", -1 },
162
163
164
165
    { "color", OPT_COLOR, "WHEN", OPTION_ARG_OPTIONAL,
      "colorize output; WHEN can be 'never', 'always' (the default if "
      "--color is used without argument), or "
      "'auto' (the default if --color is not used)", 0 },
166
167
168
    { "grind", OPT_GRIND, "FILENAME", 0,
      "for each formula for which a problem was detected, write a simpler " \
      "formula that fails on the same test in FILENAME", 0 },
169
170
    { "save-bogus", OPT_BOGUS, "FILENAME", 0,
      "save formulas for which problems were detected in FILENAME", 0 },
171
172
    { "verbose", OPT_VERBOSE, 0, 0,
      "print what is being done, for debugging", 0 },
173
174
175
176
177
178
    { 0, 0, 0, 0, 0, 0 }
  };

const struct argp_child children[] =
  {
    { &finput_argp, 0, 0, 1 },
179
    { &misc_argp, 0, 0, -1 },
180
181
182
    { 0, 0, 0, 0 }
  };

183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
enum color_type { color_never, color_always, color_if_tty };

static char const *const color_args[] =
{
  "always", "yes", "force",
  "never", "no", "none",
  "auto", "tty", "if-tty", 0
};
static color_type const color_types[] =
{
  color_always, color_always, color_always,
  color_never, color_never, color_never,
  color_if_tty, color_if_tty, color_if_tty
};
ARGMATCH_VERIFY(color_args, color_types);

color_type color_opt = color_if_tty;
const char* bright_red = "\033[01;31m";
201
const char* bright_blue = "\033[01;34m";
202
const char* bright_yellow = "\033[01;33m";
203
204
const char* reset_color = "\033[m";

205
206
unsigned states = 200;
float density = 0.1;
207
unsigned timeout = 0;
208
209
210
const char* json_output = 0;
const char* csv_output = 0;
bool want_stats = false;
211
bool allow_dups = false;
212
bool no_checks = false;
213
bool no_complement = false;
214
bool stop_on_error = false;
215
int seed = 0;
216
unsigned products = 1;
217
bool products_avg = true;
218
bool opt_omit = false;
219
bool has_sr = false; // Has Streett or Rabin automata to process.
220
221
const char* bogus_output_filename = 0;
std::ofstream* bogus_output = 0;
222
std::ofstream* grind_output = 0;
223
bool verbose = false;
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278

struct translator_spec
{
  // The translator command, as specified on the command-line.
  // If this has the form of
  //    {name}cmd
  // then it is split in two components.
  // Otherwise, spec=cmd=name.
  const char* spec;
  // actual shell command (or spec)
  const char* cmd;
  // name of the translator (or spec)
  const char* name;

  translator_spec(const char* spec)
    : spec(spec), cmd(spec), name(spec)
  {
    if (*cmd != '{')
      return;

    // Match the closing '}'
    const char* pos = cmd;
    unsigned count = 1;
    while (*++pos)
      {
	if (*pos == '{')
	  ++count;
	else if (*pos == '}')
	  if (!--count)
	    {
	      name = strndup(cmd + 1, pos - cmd - 1);
	      cmd = pos + 1;
	      while (*cmd == ' ' || *cmd == '\t')
		++cmd;
	      break;
	    }
      }
  }

  translator_spec(const translator_spec& other)
    : spec(other.spec), cmd(other.cmd), name(other.name)
  {
    if (name != spec)
      name = strdup(name);
  }

  ~translator_spec()
  {
    if (name != spec)
      free(const_cast<char*>(name));
  }
};

std::vector<translator_spec> translators;

279
280
281
282
283
284
bool global_error_flag = false;

static std::ostream&
global_error()
{
  global_error_flag = true;
285
286
  if (color_opt)
    std::cerr << bright_red;
287
288
  return std::cerr;
}
289

290
291
292
293
294
295
296
297
298
static std::ostream&
example()
{
  if (color_opt)
    std::cerr << bright_yellow;
  return std::cerr;
}


299
300
301
302
303
304
305
306
static void
end_error()
{
  if (color_opt)
    std::cerr << reset_color;
}


307
308
struct statistics
{
309
310
  statistics()
    : ok(false),
311
      has_in(false),
312
313
314
      status_str(0),
      status_code(0),
      time(0),
315
316
317
318
319
320
      in_type(0),
      in_states(0),
      in_edges(0),
      in_transitions(0),
      in_acc(0),
      in_scc(0),
321
      states(0),
322
      edges(0),
323
324
325
326
327
328
329
330
331
332
333
      transitions(0),
      acc(0),
      scc(0),
      nonacc_scc(0),
      terminal_scc(0),
      weak_scc(0),
      strong_scc(0),
      nondetstates(0),
      nondeterministic(false),
      terminal_aut(false),
      weak_aut(false),
334
      strong_aut(false)
335
336
337
  {
  }

338
339
  // If OK is false, only the status_str, status_code, and time fields
  // should be valid.
340
  bool ok;
341
342
  // has in_* data to display.
  bool has_in;
343
344
345
  const char* status_str;
  int status_code;
  double time;
346
347
348
349
350
351
  const char* in_type;
  unsigned in_states;
  unsigned in_edges;
  unsigned in_transitions;
  unsigned in_acc;
  unsigned in_scc;
352
353
354
355
356
  unsigned states;
  unsigned edges;
  unsigned transitions;
  unsigned acc;
  unsigned scc;
357
358
359
360
  unsigned nonacc_scc;
  unsigned terminal_scc;
  unsigned weak_scc;
  unsigned strong_scc;
361
362
  unsigned nondetstates;
  bool nondeterministic;
363
364
365
  bool terminal_aut;
  bool weak_aut;
  bool strong_aut;
366
367
368
  std::vector<double> product_states;
  std::vector<double> product_transitions;
  std::vector<double> product_scc;
369
370

  static void
371
  fields(std::ostream& os, bool show_exit, bool show_sr)
372
  {
373
    if (show_exit)
374
      os << "\"exit_status\",\"exit_code\",";
375
376
377
378
379
    os << "\"time\",";
    if (show_sr)
      os << ("\"in_type\",\"in_states\",\"in_edges\",\"in_transitions\","
	     "\"in_acc\",\"in_scc\",");
    os << ("\"states\","
380
381
382
383
384
385
386
387
388
389
390
391
	   "\"edges\","
	   "\"transitions\","
	   "\"acc\","
	   "\"scc\","
	   "\"nonacc_scc\","
	   "\"terminal_scc\","
	   "\"weak_scc\","
	   "\"strong_scc\","
	   "\"nondet_states\","
	   "\"nondet_aut\","
	   "\"terminal_aut\","
	   "\"weak_aut\","
392
393
394
395
	   "\"strong_aut\"");
    size_t m = products_avg ? 1U : products;
    for (size_t i = 0; i < m; ++i)
      os << ",\"product_states\",\"product_transitions\",\"product_scc\"";
396
397
398
  }

  void
399
  to_csv(std::ostream& os, bool show_exit, bool show_sr, const char* na = "")
400
  {
401
    if (show_exit)
402
403
404
      os << '"' << status_str << "\"," << status_code << ',';
    os << time << ',';
    if (ok)
405
      {
406
407
408
409
410
411
412
413
414
415
	if (has_in)
	  os << '"' << in_type << "\","
	     << in_states << ','
	     << in_edges << ','
	     << in_transitions << ','
	     << in_acc << ','
	     << in_scc << ',';
	else if (show_sr)
	  os << na << ',' << na << ',' << na << ','
	     << na << ',' << na << ',' << na << ',';
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
	os << states << ','
	   << edges << ','
	   << transitions << ','
	   << acc << ','
	   << scc << ','
	   << nonacc_scc << ','
	   << terminal_scc << ','
	   << weak_scc << ','
	   << strong_scc << ','
	   << nondetstates << ','
	   << nondeterministic << ','
	   << terminal_aut << ','
	   << weak_aut << ','
	   << strong_aut;
	if (!products_avg)
	  {
	    for (size_t i = 0; i < products; ++i)
	      os << ',' << product_states[i]
		 << ',' << product_transitions[i]
		 << ',' << product_scc[i];
	  }
	else
	  {
	    double st = 0.0;
	    double tr = 0.0;
	    double sc = 0.0;
	    for (size_t i = 0; i < products; ++i)
	      {
		st += product_states[i];
		tr += product_transitions[i];
		sc += product_scc[i];
	      }
	    os << ',' << (st / products)
	       << ',' << (tr / products)
	       << ',' << (sc / products);
	  }
      }
453
    else
454
455
      {
	size_t m = products_avg ? 1U : products;
456
457
458
	m *= 3;
	m += 13 + show_sr * 6;
	os << na;
459
	for (size_t i = 0; i < m; ++i)
460
	  os << ',' << na;
461
      }
462
463
464
465
466
467
468
469
  }
};

typedef std::vector<statistics> statistics_formula;
typedef std::vector<statistics_formula> statistics_vector;
statistics_vector vstats;
std::vector<std::string> formulas;

470
471
472
473
474
475
476
477
478
479
static int
parse_opt(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case 't':
    case ARGP_KEY_ARG:
      translators.push_back(arg);
      break;
480
481
    case 'T':
      timeout = to_pos_int(arg);
482
483
484
485
#if !ENABLE_TIMEOUT
      std::cerr << "warning: setting a timeout is not supported "
		<< "on your platform" << std::endl;
#endif
486
      break;
487
488
489
490
491
492
493
494
    case OPT_BOGUS:
      {
	bogus_output = new std::ofstream(arg);
	if (!*bogus_output)
	  error(2, errno, "cannot open '%s'", arg);
	bogus_output_filename = arg;
	break;
      }
495
496
497
498
499
500
501
502
    case OPT_COLOR:
      {
	if (arg)
	  color_opt = XARGMATCH("--color", arg, color_args, color_types);
	else
	  color_opt = color_always;
	break;
      }
503
504
505
506
    case OPT_CSV:
      want_stats = true;
      csv_output = arg ? arg : "-";
      break;
507
508
509
    case OPT_DENSITY:
      density = to_probability(arg);
      break;
510
511
512
    case OPT_DUPS:
      allow_dups = true;
      break;
513
514
515
516
517
    case OPT_GRIND:
      grind_output = new std::ofstream(arg);
      if (!*grind_output)
	error(2, errno, "cannot open '%s'", arg);
      break;
518
519
520
521
    case OPT_JSON:
      want_stats = true;
      json_output = arg ? arg : "-";
      break;
522
    case OPT_PRODUCTS:
523
524
525
526
527
      if (*arg == '+')
	{
	  products_avg = false;
	  ++arg;
	}
528
529
      products = to_pos_int(arg);
      break;
530
531
    case OPT_NOCHECKS:
      no_checks = true;
532
533
534
535
      no_complement = true;
      break;
    case OPT_NOCOMP:
      no_complement = true;
536
      break;
537
538
539
    case OPT_OMIT:
      opt_omit = true;
      break;
540
541
542
    case OPT_SEED:
      seed = to_pos_int(arg);
      break;
543
544
545
    case OPT_STATES:
      states = to_pos_int(arg);
      break;
546
547
548
    case OPT_STOP_ERR:
      stop_on_error = true;
      break;
549
550
551
    case OPT_VERBOSE:
      verbose = true;
      break;
552
553
554
555
556
557
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

558
static volatile bool timed_out = false;
559
unsigned timeout_count = 0;
560

561
562
#if ENABLE_TIMEOUT
static volatile int alarm_on = 0;
563
564
565
566
567
568
569
570
571
572
573
574
575
576
static int child_pid = -1;

static void
sig_handler(int sig)
{
  if (child_pid == 0)
    error(2, 0, "child received signal %d before starting", sig);

  if (sig == SIGALRM && alarm_on)
    {
      timed_out = true;
      if (--alarm_on)
	{
	  // Send SIGTERM to children.
577
	  kill(-child_pid, SIGTERM);
578
579
580
581
582
583
584
	  // Try again later if it didn't work.  (alarm() will be reset
	  // if it did work and the call to wait() returns)
	  alarm(2);
	}
      else
	{
	  // After a few gentle tries, really kill that child.
585
	  kill(-child_pid, SIGKILL);
586
587
588
589
590
	}
    }
  else
    {
      // forward signal
591
      kill(-child_pid, sig);
592
      // cleanup files
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
593
      spot::cleanup_tmpfiles();
594
595
      // and die verbosely
      error(2, 0, "received signal %d", sig);
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
    }
}

static void
setup_sig_handler()
{
  struct sigaction sa;
  sa.sa_handler = sig_handler;
  sigemptyset(&sa.sa_mask);
  sa.sa_flags = SA_RESTART; // So that wait() doesn't get aborted by SIGALRM.
  sigaction(SIGALRM, &sa, 0);
  // Catch termination signals, so we can kill the subprocess.
  sigaction(SIGHUP, &sa, 0);
  sigaction(SIGINT, &sa, 0);
  sigaction(SIGQUIT, &sa, 0);
  sigaction(SIGTERM, &sa, 0);
}

static int
exec_with_timeout(const char* cmd)
{
  int status;

  timed_out = false;

  child_pid = fork();
  if (child_pid == -1)
    error(2, errno, "failed to fork()");

  if (child_pid == 0)
    {
      setpgid(0, 0);
      execlp("sh", "sh", "-c", cmd, (char*)0);
      error(2, errno, "failed to run 'sh'");
630
631
      // never reached
      return -1;
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
    }
  else
    {
      alarm(timeout);
      // Upon SIGALRM, the child will receive up to 3
      // signals: SIGTERM, SIGTERM, SIGKILL.
      alarm_on = 3;
      int w = waitpid(child_pid, &status, 0);
      alarm_on = 0;

      if (w == -1)
	error(2, errno, "error during wait()");

      alarm(0);
    }
  return status;
}
649
650
651
652
#else // !ENABLE_TIMEOUT
#define exec_with_timeout(cmd) system(cmd)
#define setup_sig_handler() while (0);
#endif // !ENABLE_TIMEOUT
653

654
namespace
655
{
656
657
658
  struct quoted_string: public spot::printable_value<std::string>
  {
    using spot::printable_value<std::string>::operator=;
659

660
661
662
663
664
665
666
667
    void
    print(std::ostream& os, const char* pos) const
    {
      os << '\'';
      this->spot::printable_value<std::string>::print(os, pos);
      os << '\'';
    }
  };
668

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
669
670
  struct printable_result_filename:
    public spot::printable_value<spot::temporary_file*>
671
672
  {
    unsigned translator_num;
673
    enum output_format { None, Lbtt, Dstar, Hoa };
674
    mutable output_format format;
675

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
676
677
678
679
680
681
682
683
684
685
    printable_result_filename()
    {
      val_ = 0;
    }

    ~printable_result_filename()
    {
      delete val_;
    }

686
687
688
689
690
    void reset(unsigned n)
    {
      translator_num = n;
      format = None;
    }
691

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
692
693
694
695
696
697
    void cleanup()
    {
      delete val_;
      val_ = 0;
    }

698
699
700
    void
    print(std::ostream& os, const char* pos) const
    {
701
      output_format old_format = format;
702
      if (*pos == 'N')
703
	format = Hoa;		// The HOA parse also reads neverclaims
704
      else if (*pos == 'T')
705
	format = Lbtt;
706
707
      else if (*pos == 'D')
	format = Dstar;
708
709
      else if (*pos == 'H')
	format = Hoa;
710
      else
711
	SPOT_UNREACHABLE();
712

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
713
      if (val_)
714
715
716
717
	{
	  // It's OK to use a specified multiple time, but it's not OK
	  // to mix the formats.
	  if (format != old_format)
718
719
	    error(2, 0,
		  "you may not mix %%D, %%H, %%N, and %%T specifiers: %s",
720
		  translators[translator_num].spec);
721
722
723
724
725
726
727
728
	}
      else
	{
	  char prefix[30];
	  snprintf(prefix, sizeof prefix, "lcr-o%u-", translator_num);
	  const_cast<printable_result_filename*>(this)->val_
	    = spot::create_tmpfile(prefix);
	}
729
730
731
      os << '\'' << val_ << '\'';
    }
  };
732

733
734
735
  class translator_runner: protected spot::formater
  {
  private:
736
    spot::bdd_dict_ptr dict;
737
738
739
740
    // Round-specific variables
    quoted_string string_ltl_spot;
    quoted_string string_ltl_spin;
    quoted_string string_ltl_lbt;
741
    quoted_string string_ltl_wring;
742
743
744
    quoted_string filename_ltl_spot;
    quoted_string filename_ltl_spin;
    quoted_string filename_ltl_lbt;
745
    quoted_string filename_ltl_wring;
746
747
748
    // Run-specific variables
    printable_result_filename output;
  public:
749
750
    using spot::formater::has;

751
    translator_runner(spot::bdd_dict_ptr dict)
752
      : dict(dict)
753
754
755
756
    {
      declare('f', &string_ltl_spot);
      declare('s', &string_ltl_spin);
      declare('l', &string_ltl_lbt);
757
      declare('w', &string_ltl_wring);
758
759
760
      declare('F', &filename_ltl_spot);
      declare('S', &filename_ltl_spin);
      declare('L', &filename_ltl_lbt);
761
      declare('W', &filename_ltl_wring);
762
      declare('D', &output);
763
      declare('H', &output);
764
765
766
767
768
769
      declare('N', &output);
      declare('T', &output);

      size_t s = translators.size();
      assert(s);
      for (size_t n = 0; n < s; ++n)
770
771
772
	{
	  // Check that each translator uses at least one input and
	  // one output.
773
	  std::vector<bool> has(256);
774
775
	  const translator_spec& t = translators[n];
	  scan(t.cmd, has);
776
777
778
779
	  if (!(has['f'] || has['s'] || has['l'] || has['w']
		|| has['F'] || has['S'] || has['L'] || has['W']))
	    error(2, 0, "no input %%-sequence in '%s'.\n       Use "
		  "one of %%f,%%s,%%l,%%w,%%F,%%S,%%L,%%W to indicate how "
780
		  "to pass the formula.", t.spec);
781
	  bool has_d = has['D'];
782
	  if (!(has_d || has['N'] || has['T'] || has['H']))
783
	    error(2, 0, "no output %%-sequence in '%s'.\n      Use one of "
784
		  "%%D,%%H,%%N,%%T to indicate where the automaton is saved.",
785
		  t.spec);
786
	  has_sr |= has_d;
787
788

	  // Remember the %-sequences used by all translators.
789
	  prime(t.cmd);
790
	}
791

792
793
794
795
    }

    void
    string_to_tmp(std::string& str, unsigned n, std::string& tmpname)
796
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
797
798
799
800
801
      char prefix[30];
      snprintf(prefix, sizeof prefix, "lcr-i%u-", n);
      spot::open_temporary_file* tmpfile = spot::create_open_tmpfile(prefix);
      tmpname = tmpfile->name();
      int fd = tmpfile->fd();
802
803
804
805
      ssize_t s = str.size();
      if (write(fd, str.c_str(), s) != s
	  || write(fd, "\n", 1) != 1)
	error(2, errno, "failed to write into %s", tmpname.c_str());
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
806
      tmpfile->close();
807
808
    }

809
810
    const std::string&
    formula() const
811
812
813
814
815
816
    {
      // Pick the most readable format we have...
      if (!string_ltl_spot.val().empty())
	return string_ltl_spot;
      if (!string_ltl_spin.val().empty())
	return string_ltl_spin;
817
818
      if (!string_ltl_wring.val().empty())
	return string_ltl_wring;
819
820
      if (!string_ltl_lbt.val().empty())
	return string_ltl_lbt;
821
      SPOT_UNREACHABLE();
822
823
824
      return string_ltl_spot;
    }

825
826
    void
    round_formula(const spot::ltl::formula* f, unsigned serial)
827
828
829
830
831
832
833
    {
      if (has('f') || has('F'))
	string_ltl_spot = spot::ltl::to_string(f, true);
      if (has('s') || has('S'))
	string_ltl_spin = spot::ltl::to_spin_string(f, true);
      if (has('l') || has('L'))
	string_ltl_lbt = spot::ltl::to_lbt_string(f);
834
835
      if (has('w') || has('W'))
	string_ltl_wring = spot::ltl::to_wring_string(f);
836
837
838
839
840
841
      if (has('F'))
	string_to_tmp(string_ltl_spot, serial, filename_ltl_spot);
      if (has('S'))
	string_to_tmp(string_ltl_spin, serial, filename_ltl_spin);
      if (has('L'))
	string_to_tmp(string_ltl_lbt, serial, filename_ltl_lbt);
842
843
      if (has('W'))
	string_to_tmp(string_ltl_wring, serial, filename_ltl_wring);
844
845
    }

846
    spot::const_tgba_digraph_ptr
847
848
    translate(unsigned int translator_num, char l, statistics_formula* fstats,
	      bool& problem)
849
850
851
852
    {
      output.reset(translator_num);

      std::ostringstream command;
853
      format(command, translators[translator_num].cmd);
854

855
      assert(output.format != printable_result_filename::None);
856

857
858
859
      std::string cmd = command.str();
      std::cerr << "Running [" << l << translator_num << "]: "
		<< cmd << std::endl;
860
861
      spot::stopwatch sw;
      sw.start();
862
      int es = exec_with_timeout(cmd.c_str());
863
      double duration = sw.stop();
864

865
866
      const char* status_str = 0;

867
      spot::const_tgba_digraph_ptr res = 0;
868
869
      if (timed_out)
	{
870
871
	  // This is not considered to be a global error.
	  std::cerr << "warning: timeout during execution of command\n";
872
	  ++timeout_count;
873
	  status_str = "timeout";
874
	  problem = false;	// A timeout is not a sign of a bug
875
	  es = -1;
876
877
878
	}
      else if (WIFSIGNALED(es))
	{
879
	  status_str = "signal";
880
	  problem = true;
881
	  es = WTERMSIG(es);
882
	  global_error() << "error: execution terminated by signal "
883
			 << es << ".\n";
884
	  end_error();
885
886
	}
      else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
887
	{
888
889
	  es = WEXITSTATUS(es);
	  status_str = "exit code";
890
	  problem = true;
891
	  global_error() << "error: execution returned exit code "
892
			 << es << ".\n";
893
	  end_error();
894
895
896
	}
      else
	{
897
	  status_str = "ok";
898
	  problem = false;
899
	  es = 0;
900
901
902
	  switch (output.format)
	    {
	    case printable_result_filename::Lbtt:
903
	      {
904
		std::string error;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
905
		std::ifstream f(output.val()->name());
906
907
		if (!f)
		  {
908
		    status_str = "no output";
909
		    problem = true;
910
		    es = -1;
911
912
		    global_error() << "Cannot open " << output.val()
				   << std::endl;
913
		    end_error();
914
915
916
		  }
		else
		  {
917
		    res = spot::lbtt_parse(f, error, dict);
918
		    if (!res)
919
		      {
920
			status_str = "parse error";
921
			problem = true;
922
			es = -1;
923
924
925
926
927
			global_error() << ("error: failed to parse output in "
					   "LBTT format: ")
				       << error << std::endl;
			end_error();
		      }
928
929
		  }
		break;
930
	      }
931
932
933
934
	    case printable_result_filename::Dstar:
	      {
		spot::dstar_parse_error_list pel;
		std::string filename = output.val()->name();
935
		auto aut = spot::dstar_parse(filename, pel, dict);
936
937
		if (!pel.empty())
		  {
938
		    status_str = "parse error";
939
		    problem = true;
940
		    es = -1;
941
942
943
944
945
		    std::ostream& err = global_error();
		    err << "error: failed to parse the produced DSTAR"
		      " output.\n";
		    spot::format_dstar_parse_errors(err, filename, pel);
		    end_error();
946
		    res = nullptr;
947
948
		  }
		else
949
		  {
950
951
952
953
954
955
956
957
958
959
960
961
		    const char* type = 0;
		    switch (aut->type)
		      {
		      case spot::Rabin:
			type = "DRA";
			break;
		      case spot::Streett:
			type = "DSA";
			break;
		      }
		    assert(type);

962
963
964
965
966
		    // Gather statistics about the input automaton
		    if (want_stats)
		      {
			statistics* st = &(*fstats)[translator_num];
			st->has_in = true;
967
			st->in_type = type;
968
969
970
971
972
973
974
			spot::tgba_sub_statistics s =
			  sub_stats_reachable(aut->aut);
			st->in_states= s.states;
			st->in_edges = s.transitions;
			st->in_transitions = s.sub_transitions;
			st->in_acc = aut->accpair_count;

975
			st->in_scc = spot::scc_info(aut->aut).scc_count();
976
977
		      }
		    // convert it into TGBA for further processing
978
979
		    if (verbose)
		      std::cerr << "info: converting " << type << " to TGBA\n";
980
981
		    res = dstar_to_tgba(aut);
		  }
982
983
		break;
	      }
984
	    case printable_result_filename::Hoa: // Will also read neverclaims
985
986
987
988
989
990
991
992
993
994
	      {
		spot::hoa_parse_error_list pel;
		std::string filename = output.val()->name();
		auto aut = spot::hoa_parse(filename, pel, dict);
		if (!pel.empty())
		  {
		    status_str = "parse error";
		    problem = true;
		    es = -1;
		    std::ostream& err = global_error();
995
		    err << "error: failed to parse the produced automaton.\n";
996
997
998
999
		    spot::format_hoa_parse_errors(err, filename, pel);
		    end_error();
		    res = nullptr;
		  }
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
		else if (aut->aborted)
		  {
		    status_str = "aborted";
		    problem = true;
		    es = -1;
		    std::ostream& err = global_error();
		    err << "error: aborted HOA file.\n";
		    end_error();
		    res = nullptr;
		  }
1010
1011
1012
1013
1014
1015
		else
		  {
		    res = aut->aut;
		  }
		break;
	      }
1016
	    case printable_result_filename::None:
1017
	      SPOT_UNREACHABLE();
1018
	    }
1019
	}
1020
1021

      if (want_stats)
1022
1023
	{
	  statistics* st = &(*fstats)[translator_num];
1024
1025
	  st->status_str = status_str;
	  st->status_code = es;
1026
	  st->time = duration;
1027
1028
1029

	  // Compute statistics.
	  if (res)
1030
	    {
1031
1032
	      if (verbose)
		std::cerr << "info: getting statistics\n";
1033
1034
1035
1036
1037
	      st->ok = true;
	      spot::tgba_sub_statistics s = sub_stats_reachable(res);
	      st->states = s.states;
	      st->edges = s.transitions;
	      st->transitions = s.sub_transitions;
1038
	      st->acc = res->acc().num_sets();
1039
	      spot::scc_info m(res);
1040
	      unsigned c = m.scc_count();
1041
	      st->scc = c;
1042
1043
1044
1045
	      st->nondetstates = spot::count_nondet_states(res);
	      st->nondeterministic = st->nondetstates != 0;
	      for (unsigned n = 0; n < c; ++n)
		{
1046
		  if (!m.is_accepting_scc(n))
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
		    ++st->nonacc_scc;
		  else if (is_terminal_scc(m, n))
		    ++st->terminal_scc;
		  else if (is_weak_scc(m, n))
		    ++st->weak_scc;
		  else
		    ++st->strong_scc;
		}
	      if (st->strong_scc)
		st->strong_aut = true;
	      else if (st->weak_scc)
		st->weak_aut = true;
1059
	      else
1060
		st->terminal_aut = true;
1061
	    }
1062
	}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1063
      output.cleanup();
1064
      return res;
1065
    }
1066
  };
1067

1068
  static bool
1069
1070
  check_empty_prod(const spot::const_tgba_digraph_ptr& aut_i,
		   const spot::const_tgba_digraph_ptr& aut_j,
1071
		   size_t i, size_t j, bool icomp, bool jcomp)
1072
  {
1073
    auto prod = spot::product(aut_i, aut_j);
1074
    auto res = spot::couvreur99(prod)->check();
1075

1076
1077
1078
1079
1080
1081
    if (verbose)
      {
	std::cerr << "info: check_empty ";
	if (icomp)
	  std::cerr << "Comp(N" << i << ')';
	else
1082
	  std::cerr << 'P' << i;
1083
1084
1085
1086
1087
1088
1089
	if (jcomp)
	  std::cerr << "*Comp(P" << j << ')';
	else
	  std::cerr << "*N" << j;
	std::cerr << '\n';
      }

1090
1091
    if (res)
      {
1092
1093
1094
	std::ostream& err = global_error();
	err << "error: ";
	if (icomp)
1095
	  err << "Comp(N" << i << ')';
1096
	else
1097
	  err << 'P' << i;
1098
	if (jcomp)
1099
	  err << "*Comp(P" << j << ')';
1100
1101
1102
	else
	  err << "*N" << j;
	err << " is nonempty";
1103

1104
	auto run = res->accepting_run();
1105
1106
	if (run)
	  {
1107
	    run = reduce_run(prod, run);
1108
1109
	    std::cerr << "; both automata accept the infinite word\n"
		      << "       ";
1110
	    spot::tgba_word w(run);
1111
	    w.simplify();
1112
	    w.print(example(), prod->get_dict()) << '\n';
1113
1114
1115
	  }
	else
	  {
1116
	    std::cerr << '\n';
1117
1118
1119
	  }
	end_error();
      }
1120
    return !!res;
1121
1122
  }

1123
  static bool
1124
  cross_check(const std::vector<spot::scc_info*>& maps, char l, unsigned p)