ltlcross.cc 47 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
// 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
38
39

#include "common_setup.hh"
#include "common_cout.hh"
#include "common_finput.hh"
#include "neverparse/public.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", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the output automaton as a Never claim, in LBTT's or in LTL2DSTAR's "
      "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
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
static int
to_int(const char* s)
{
  char* endptr;
  int res = strtol(s, &endptr, 10);
  if (*endptr)
    error(2, 0, "failed to parse '%s' as an integer.", s);
  return res;
}

static int
to_pos_int(const char* s)
{
  int res = to_int(s);
  if (res < 0)
    error(2, 0, "%d is not positive", res);
  return res;
}

static float
to_float(const char* s)
{
  char* endptr;
  // Do not use strtof(), it does not exist on Solaris 9.
  float res = strtod(s, &endptr);
  if (*endptr)
    error(2, 0, "failed to parse '%s' as a float.", s);
  return res;
}

static float
to_probability(const char* s)
{
  float res = to_float(s);
  if (res < 0.0 || res > 1.0)
    error(2, 0, "%f is not between 0 and 1.", res);
  return res;
}


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;
520
521
    case 'T':
      timeout = to_pos_int(arg);
522
523
524
525
#if !ENABLE_TIMEOUT
      std::cerr << "warning: setting a timeout is not supported "
		<< "on your platform" << std::endl;
#endif
526
      break;
527
528
529
530
531
532
533
534
    case OPT_BOGUS:
      {
	bogus_output = new std::ofstream(arg);
	if (!*bogus_output)
	  error(2, errno, "cannot open '%s'", arg);
	bogus_output_filename = arg;
	break;
      }
535
536
537
538
539
540
541
542
    case OPT_COLOR:
      {
	if (arg)
	  color_opt = XARGMATCH("--color", arg, color_args, color_types);
	else
	  color_opt = color_always;
	break;
      }
543
544
545
546
    case OPT_CSV:
      want_stats = true;
      csv_output = arg ? arg : "-";
      break;
547
548
549
    case OPT_DENSITY:
      density = to_probability(arg);
      break;
550
551
552
    case OPT_DUPS:
      allow_dups = true;
      break;
553
554
555
556
557
    case OPT_GRIND:
      grind_output = new std::ofstream(arg);
      if (!*grind_output)
	error(2, errno, "cannot open '%s'", arg);
      break;
558
559
560
561
    case OPT_JSON:
      want_stats = true;
      json_output = arg ? arg : "-";
      break;
562
    case OPT_PRODUCTS:
563
564
565
566
567
      if (*arg == '+')
	{
	  products_avg = false;
	  ++arg;
	}
568
569
      products = to_pos_int(arg);
      break;
570
571
    case OPT_NOCHECKS:
      no_checks = true;
572
573
574
575
      no_complement = true;
      break;
    case OPT_NOCOMP:
      no_complement = true;
576
      break;
577
578
579
    case OPT_OMIT:
      opt_omit = true;
      break;
580
581
582
    case OPT_SEED:
      seed = to_pos_int(arg);
      break;
583
584
585
    case OPT_STATES:
      states = to_pos_int(arg);
      break;
586
587
588
    case OPT_STOP_ERR:
      stop_on_error = true;
      break;
589
590
591
    case OPT_VERBOSE:
      verbose = true;
      break;
592
593
594
595
596
597
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

598
static volatile bool timed_out = false;
599
unsigned timeout_count = 0;
600

601
602
#if ENABLE_TIMEOUT
static volatile int alarm_on = 0;
603
604
605
606
607
608
609
610
611
612
613
614
615
616
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.
617
	  kill(-child_pid, SIGTERM);
618
619
620
621
622
623
624
	  // 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.
625
	  kill(-child_pid, SIGKILL);
626
627
628
629
630
	}
    }
  else
    {
      // forward signal
631
      kill(-child_pid, sig);
632
      // cleanup files
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
633
      spot::cleanup_tmpfiles();
634
635
      // and die verbosely
      error(2, 0, "received signal %d", sig);
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
    }
}

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'");
670
671
      // never reached
      return -1;
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
    }
  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;
}
689
690
691
692
#else // !ENABLE_TIMEOUT
#define exec_with_timeout(cmd) system(cmd)
#define setup_sig_handler() while (0);
#endif // !ENABLE_TIMEOUT
693

694
namespace
695
{
696
697
698
  struct quoted_string: public spot::printable_value<std::string>
  {
    using spot::printable_value<std::string>::operator=;
699

700
701
702
703
704
705
706
707
    void
    print(std::ostream& os, const char* pos) const
    {
      os << '\'';
      this->spot::printable_value<std::string>::print(os, pos);
      os << '\'';
    }
  };
708

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
709
710
  struct printable_result_filename:
    public spot::printable_value<spot::temporary_file*>
711
712
  {
    unsigned translator_num;
713
    enum output_format { None, Spin, Lbtt, Dstar, Hoa };
714
    mutable output_format format;
715

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
716
717
718
719
720
721
722
723
724
725
    printable_result_filename()
    {
      val_ = 0;
    }

    ~printable_result_filename()
    {
      delete val_;
    }

726
727
728
729
730
    void reset(unsigned n)
    {
      translator_num = n;
      format = None;
    }
731

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
732
733
734
735
736
737
    void cleanup()
    {
      delete val_;
      val_ = 0;
    }

738
739
740
    void
    print(std::ostream& os, const char* pos) const
    {
741
      output_format old_format = format;
742
743
      if (*pos == 'N')
	format = Spin;
744
      else if (*pos == 'T')
745
	format = Lbtt;
746
747
      else if (*pos == 'D')
	format = Dstar;
748
749
      else if (*pos == 'H')
	format = Hoa;
750
      else
751
	SPOT_UNREACHABLE();
752

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
753
      if (val_)
754
755
756
757
	{
	  // It's OK to use a specified multiple time, but it's not OK
	  // to mix the formats.
	  if (format != old_format)
758
759
	    error(2, 0,
		  "you may not mix %%D, %%H, %%N, and %%T specifiers: %s",
760
		  translators[translator_num].spec);
761
762
763
764
765
766
767
768
	}
      else
	{
	  char prefix[30];
	  snprintf(prefix, sizeof prefix, "lcr-o%u-", translator_num);
	  const_cast<printable_result_filename*>(this)->val_
	    = spot::create_tmpfile(prefix);
	}
769
770
771
      os << '\'' << val_ << '\'';
    }
  };
772

773
774
775
  class translator_runner: protected spot::formater
  {
  private:
776
    spot::bdd_dict_ptr dict;
777
778
779
780
    // Round-specific variables
    quoted_string string_ltl_spot;
    quoted_string string_ltl_spin;
    quoted_string string_ltl_lbt;
781
    quoted_string string_ltl_wring;
782
783
784
    quoted_string filename_ltl_spot;
    quoted_string filename_ltl_spin;
    quoted_string filename_ltl_lbt;
785
    quoted_string filename_ltl_wring;
786
787
788
    // Run-specific variables
    printable_result_filename output;
  public:
789
790
    using spot::formater::has;

791
    translator_runner(spot::bdd_dict_ptr dict)
792
      : dict(dict)
793
794
795
796
    {
      declare('f', &string_ltl_spot);
      declare('s', &string_ltl_spin);
      declare('l', &string_ltl_lbt);
797
      declare('w', &string_ltl_wring);
798
799
800
      declare('F', &filename_ltl_spot);
      declare('S', &filename_ltl_spin);
      declare('L', &filename_ltl_lbt);
801
      declare('W', &filename_ltl_wring);
802
      declare('D', &output);
803
      declare('H', &output);
804
805
806
807
808
809
      declare('N', &output);
      declare('T', &output);

      size_t s = translators.size();
      assert(s);
      for (size_t n = 0; n < s; ++n)
810
811
812
	{
	  // Check that each translator uses at least one input and
	  // one output.
813
	  std::vector<bool> has(256);
814
815
	  const translator_spec& t = translators[n];
	  scan(t.cmd, has);
816
817
818
819
	  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 "
820
		  "to pass the formula.", t.spec);
821
	  bool has_d = has['D'];
822
	  if (!(has_d || has['N'] || has['T'] || has['H']))
823
	    error(2, 0, "no output %%-sequence in '%s'.\n      Use one of "
824
		  "%%D,%%H,%%N,%%T to indicate where the automaton is saved.",
825
		  t.spec);
826
	  has_sr |= has_d;
827
828

	  // Remember the %-sequences used by all translators.
829
	  prime(t.cmd);
830
	}
831

832
833
834
835
    }

    void
    string_to_tmp(std::string& str, unsigned n, std::string& tmpname)
836
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
837
838
839
840
841
      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();
842
843
844
845
      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
846
      tmpfile->close();
847
848
    }

849
850
    const std::string&
    formula() const
851
852
853
854
855
856
    {
      // 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;
857
858
      if (!string_ltl_wring.val().empty())
	return string_ltl_wring;
859
860
      if (!string_ltl_lbt.val().empty())
	return string_ltl_lbt;
861
      SPOT_UNREACHABLE();
862
863
864
      return string_ltl_spot;
    }

865
866
    void
    round_formula(const spot::ltl::formula* f, unsigned serial)
867
868
869
870
871
872
873
    {
      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);
874
875
      if (has('w') || has('W'))
	string_ltl_wring = spot::ltl::to_wring_string(f);
876
877
878
879
880
881
      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);
882
883
      if (has('W'))
	string_to_tmp(string_ltl_wring, serial, filename_ltl_wring);
884
885
    }

886
    spot::const_tgba_digraph_ptr
887
888
    translate(unsigned int translator_num, char l, statistics_formula* fstats,
	      bool& problem)
889
890
891
892
    {
      output.reset(translator_num);

      std::ostringstream command;
893
      format(command, translators[translator_num].cmd);
894

895
      assert(output.format != printable_result_filename::None);
896

897
898
899
      std::string cmd = command.str();
      std::cerr << "Running [" << l << translator_num << "]: "
		<< cmd << std::endl;
900
901
      spot::stopwatch sw;
      sw.start();
902
      int es = exec_with_timeout(cmd.c_str());
903
      double duration = sw.stop();
904

905
906
      const char* status_str = 0;

907
      spot::const_tgba_digraph_ptr res = 0;
908
909
      if (timed_out)
	{
910
911
	  // This is not considered to be a global error.
	  std::cerr << "warning: timeout during execution of command\n";
912
	  ++timeout_count;
913
	  status_str = "timeout";
914
	  problem = false;	// A timeout is not a sign of a bug
915
	  es = -1;
916
917
918
	}
      else if (WIFSIGNALED(es))
	{
919
	  status_str = "signal";
920
	  problem = true;
921
	  es = WTERMSIG(es);
922
	  global_error() << "error: execution terminated by signal "
923
			 << es << ".\n";
924
	  end_error();
925
926
	}
      else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
927
	{
928
929
	  es = WEXITSTATUS(es);
	  status_str = "exit code";
930
	  problem = true;
931
	  global_error() << "error: execution returned exit code "
932
			 << es << ".\n";
933
	  end_error();
934
935
936
	}
      else
	{
937
	  status_str = "ok";
938
	  problem = false;
939
	  es = 0;
940
941
942
	  switch (output.format)
	    {
	    case printable_result_filename::Spin:
943
	      {
944
		spot::neverclaim_parse_error_list pel;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
945
		std::string filename = output.val()->name();
946
		res = spot::neverclaim_parse(filename, pel, dict);
947
948
		if (!pel.empty())
		  {
949
		    status_str = "parse error";
950
		    problem = true;
951
		    es = -1;
952
953
		    std::ostream& err = global_error();
		    err << "error: failed to parse the produced neverclaim.\n";
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
954
		    spot::format_neverclaim_parse_errors(err, filename, pel);
955
		    end_error();
956
		    res = nullptr;
957
958
		  }
		break;
959
	      }
960
	    case printable_result_filename::Lbtt:
961
	      {
962
		std::string error;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
963
		std::ifstream f(output.val()->name());
964
965
		if (!f)
		  {
966
		    status_str = "no output";
967
		    problem = true;
968
		    es = -1;
969
970
		    global_error() << "Cannot open " << output.val()
				   << std::endl;
971
		    end_error();
972
973
974
		  }
		else
		  {
975
		    res = spot::lbtt_parse(f, error, dict);
976
		    if (!res)
977
		      {
978
			status_str = "parse error";
979
			problem = true;
980
			es = -1;
981
982
983
984
985
			global_error() << ("error: failed to parse output in "
					   "LBTT format: ")
				       << error << std::endl;
			end_error();
		      }
986
987
		  }
		break;
988
	      }
989
990
991
992
	    case printable_result_filename::Dstar:
	      {
		spot::dstar_parse_error_list pel;
		std::string filename = output.val()->name();
993
		auto aut = spot::dstar_parse(filename, pel, dict);
994
995
		if (!pel.empty())
		  {
996
		    status_str = "parse error";
997
		    problem = true;
998
		    es = -1;
999
1000
1001
1002
1003
		    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();
1004
		    res = nullptr;
1005
1006
		  }
		else
1007
		  {
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
		    const char* type = 0;
		    switch (aut->type)
		      {
		      case spot::Rabin:
			type = "DRA";
			break;
		      case spot::Streett:
			type = "DSA";
			break;
		      }
		    assert(type);

1020
1021
1022
1023
1024
		    // Gather statistics about the input automaton
		    if (want_stats)
		      {
			statistics* st = &(*fstats)[translator_num];
			st->has_in = true;
1025
			st->in_type = type;
1026
1027
1028
1029
1030
1031
1032
			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;

1033
			st->in_scc = spot::scc_info(aut->aut).scc_count();
1034
1035
		      }
		    // convert it into TGBA for further processing
1036
1037
		    if (verbose)
		      std::cerr << "info: converting " << type << " to TGBA\n";
1038
1039
		    res = dstar_to_tgba(aut);
		  }
1040
1041
		break;
	      }
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
	    case printable_result_filename::Hoa:
	      {
		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();
		    err << "error: failed to parse the produced HOA file.\n";
		    spot::format_hoa_parse_errors(err, filename, pel);
		    end_error();
		    res = nullptr;
		  }
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
		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;
		  }
1068
1069
1070
1071
1072
1073
		else
		  {
		    res = aut->aut;
		  }
		break;
	      }
1074
	    case printable_result_filename::None:
1075
	      SPOT_UNREACHABLE();
1076
	    }
1077
	}
1078
1079

      if (want_stats)
1080
1081
	{
	  statistics* st = &(*fstats)[translator_num];
1082
1083
	  st->status_str = status_str;
	  st->status_code = es;
1084
	  st->time = duration;
1085
1086
1087

	  // Compute statistics.
	  if (res)
1088
	    {
1089
1090
	      if (verbose)
		std::cerr << "info: getting statistics\n";
1091
1092
1093
1094
1095
	      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;
1096
	      st->acc = res->acc().num_sets();
1097
	      spot::scc_info m(res);
1098
	      unsigned c = m.scc_count();
1099
	      st->scc = c;
1100
1101
1102
1103
	      st->nondetstates = spot::count_nondet_states(res);
	      st->nondeterministic = st->nondetstates != 0;
	      for (unsigned n = 0; n < c; ++n)
		{
1104
		  if (!m.is_accepting_scc(n))
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
		    ++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;
1117
	      else
1118
		st->terminal_aut = true;
1119
	    }
1120
	}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1121
      output.cleanup();
1122
      return res;
1123
    }
1124
  };
1125

1126
  static bool
1127
1128
  check_empty_prod(const spot::const_tgba_digraph_ptr& aut_i,
		   const spot::const_tgba_digraph_ptr& aut_j,
1129
		   size_t i, size_t j, bool icomp, bool jcomp)
1130
  {
1131
    auto prod = spot::product(aut_i, aut_j);
1132
    auto res = spot::couvreur99(prod)->check();
1133

1134
1135
1136
1137
1138
1139
    if (verbose)
      {
	std::cerr << "info: check_empty ";
	if (icomp)
	  std::cerr << "Comp(N" << i << ')';
	else
1140
	  std::cerr << 'P' << i;
1141
1142
1143
1144
1145
1146
1147
	if (jcomp)
	  std::cerr << "*Comp(P" << j << ')';
	else
	  std::cerr << "*N" << j;
	std::cerr << '\n';
      }

1148
1149
    if (res)
      {
1150
1151
1152
	std::ostream& err = global_error();
	err << "error: ";
	if (icomp)
1153
	  err << "Comp(N" << i << ')';
1154
	else
1155
	  err << 'P' << i;
1156
	if (jcomp)
1157
	  err << "*Comp(P" << j << ')';