ltlcross.cc 46.2 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 "gethrxtime.h"
35
#include "argmatch.h"
36
37
38
39
40

#include "common_setup.hh"
#include "common_cout.hh"
#include "common_finput.hh"
#include "neverparse/public.hh"
41
#include "dstarparse/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
50
51
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/randomgraph.hh"
52
#include "tgbaalgos/sccinfo.hh"
53
54
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/dotty.hh"
55
#include "tgbaalgos/isweakscc.hh"
56
57
#include "tgbaalgos/reducerun.hh"
#include "tgbaalgos/word.hh"
58
#include "tgbaalgos/dtgbacomp.hh"
59
#include "misc/formater.hh"
60
61
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/isdet.hh"
62
#include "misc/escape.hh"
63
#include "misc/hash.hh"
64
#include "misc/random.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
65
#include "misc/tmpfile.hh"
66

67
68
69
70
71
72
73
74
// 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

75
76
const char argp_program_doc[] ="\
Call several LTL/PSL translators and cross-compare their output to detect \
77
bugs, or to gather statistics.  The list of formulas to use should be \
78
supplied on standard input, or using the -f or -F options.\v\
79
80
81
82
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\
83
  2  ltlcross aborted on error\n\
84
";
85
86
87
88


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

static const argp_option options[] =
  {
    /**************************************************/
106
    { 0, 0, 0, 0, "Specifying translators to call:", 2 },
107
    { "translator", 't', "COMMANDFMT", 0,
108
      "register one translator to call", 0 },
109
    { "timeout", 'T', "NUMBER", 0, "kill translators after NUMBER seconds", 0 },
110
111
112
113
    /**************************************************/
    { 0, 0, 0, 0,
      "COMMANDFMT should specify input and output arguments using the "
      "following character sequences:", 3 },
114
115
116
117
118
    { "%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 },
119
120
121
    { "%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 },
122
123
124
    { 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 "
125
126
127
128
      "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 },
129
    /**************************************************/
130
    { 0, 0, 0, 0, "ltlcross behavior:", 4 },
131
132
133
134
135
    { "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 },
136
137
    { "no-complement", OPT_NOCOMP, 0, 0,
      "do not complement deterministic automata to perform extra checks", 0 },
138
139
140
    { "stop-on-error", OPT_STOP_ERR, 0, 0,
      "stop on first execution error or failure to pass"
      " sanity checks (timeouts are OK)", 0 },
141
142
    /**************************************************/
    { 0, 0, 0, 0, "State-space generation:", 5 },
143
144
145
146
147
    { "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 },
148
149
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0 by default)", 0 },
150
151
152
    { "products", OPT_PRODUCTS, "[+]INT", 0,
      "number of products to perform (1 by default), statistics will be "
      "averaged unless the number is prefixed with '+'", 0 },
153
    /**************************************************/
154
    { 0, 0, 0, 0, "Statistics output:", 6 },
155
156
157
158
    { "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 },
159
160
    { "omit-missing", OPT_OMIT, 0, 0,
      "do not output statistics for timeouts or failed translations", 0 },
161
    /**************************************************/
162
    { 0, 0, 0, 0, "Miscellaneous options:", -1 },
163
164
165
166
    { "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 },
167
168
169
    { "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 },
170
171
    { "save-bogus", OPT_BOGUS, "FILENAME", 0,
      "save formulas for which problems were detected in FILENAME", 0 },
172
173
    { "verbose", OPT_VERBOSE, 0, 0,
      "print what is being done, for debugging", 0 },
174
175
176
177
178
179
    { 0, 0, 0, 0, 0, 0 }
  };

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

184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
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";
202
const char* bright_blue = "\033[01;34m";
203
const char* bright_yellow = "\033[01;33m";
204
205
const char* reset_color = "\033[m";

206
207
unsigned states = 200;
float density = 0.1;
208
unsigned timeout = 0;
209
210
211
const char* json_output = 0;
const char* csv_output = 0;
bool want_stats = false;
212
bool allow_dups = false;
213
bool no_checks = false;
214
bool no_complement = false;
215
bool stop_on_error = false;
216
int seed = 0;
217
unsigned products = 1;
218
bool products_avg = true;
219
bool opt_omit = false;
220
bool has_sr = false; // Has Streett or Rabin automata to process.
221
222
const char* bogus_output_filename = 0;
std::ofstream* bogus_output = 0;
223
std::ofstream* grind_output = 0;
224
bool verbose = false;
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
279

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;

280
281
282
283
284
285
bool global_error_flag = false;

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

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


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


308
309
struct statistics
{
310
311
  statistics()
    : ok(false),
312
      has_in(false),
313
314
315
      status_str(0),
      status_code(0),
      time(0),
316
317
318
319
320
321
      in_type(0),
      in_states(0),
      in_edges(0),
      in_transitions(0),
      in_acc(0),
      in_scc(0),
322
      states(0),
323
      edges(0),
324
325
326
327
328
329
330
331
332
333
334
      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),
335
      strong_aut(false)
336
337
338
  {
  }

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

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

  void
400
  to_csv(std::ostream& os, bool show_exit, bool show_sr, const char* na = "")
401
  {
402
    if (show_exit)
403
404
405
      os << '"' << status_str << "\"," << status_code << ',';
    os << time << ',';
    if (ok)
406
      {
407
408
409
410
411
412
413
414
415
416
	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 << ',';
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
453
	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);
	  }
      }
454
    else
455
456
      {
	size_t m = products_avg ? 1U : products;
457
458
459
	m *= 3;
	m += 13 + show_sr * 6;
	os << na;
460
	for (size_t i = 0; i < m; ++i)
461
	  os << ',' << na;
462
      }
463
464
465
466
467
468
469
470
  }
};

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

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

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

602
603
#if ENABLE_TIMEOUT
static volatile int alarm_on = 0;
604
605
606
607
608
609
610
611
612
613
614
615
616
617
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.
618
	  kill(-child_pid, SIGTERM);
619
620
621
622
623
624
625
	  // 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.
626
	  kill(-child_pid, SIGKILL);
627
628
629
630
631
	}
    }
  else
    {
      // forward signal
632
      kill(-child_pid, sig);
633
      // cleanup files
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
634
      spot::cleanup_tmpfiles();
635
636
      // and die verbosely
      error(2, 0, "received signal %d", sig);
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
670
    }
}

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

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

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

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

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

    ~printable_result_filename()
    {
      delete val_;
    }

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

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

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
752
      if (val_)
753
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)
	    error(2, 0, "you may not mix %%D, %%N, and %%T specifiers: %s",
758
		  translators[translator_num].spec);
759
760
761
762
763
764
765
766
	}
      else
	{
	  char prefix[30];
	  snprintf(prefix, sizeof prefix, "lcr-o%u-", translator_num);
	  const_cast<printable_result_filename*>(this)->val_
	    = spot::create_tmpfile(prefix);
	}
767
768
769
      os << '\'' << val_ << '\'';
    }
  };
770

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

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

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

	  // Remember the %-sequences used by all translators.
826
	  prime(t.cmd);
827
	}
828

829
830
831
832
    }

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

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

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

883
    spot::const_tgba_ptr
884
885
    translate(unsigned int translator_num, char l, statistics_formula* fstats,
	      bool& problem)
886
887
888
889
    {
      output.reset(translator_num);

      std::ostringstream command;
890
      format(command, translators[translator_num].cmd);
891

892
      assert(output.format != printable_result_filename::None);
893

894
895
896
      std::string cmd = command.str();
      std::cerr << "Running [" << l << translator_num << "]: "
		<< cmd << std::endl;
897
      xtime_t before = gethrxtime();
898
      int es = exec_with_timeout(cmd.c_str());
899
      xtime_t after = gethrxtime();
900

901
902
      const char* status_str = 0;

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

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

1029
			st->in_scc = spot::scc_info(aut->aut).scc_count();
1030
1031
		      }
		    // convert it into TGBA for further processing
1032
1033
		    if (verbose)
		      std::cerr << "info: converting " << type << " to TGBA\n";
1034
1035
		    res = dstar_to_tgba(aut);
		  }
1036
1037
		break;
	      }
1038
	    case printable_result_filename::None:
1039
	      SPOT_UNREACHABLE();
1040
	    }
1041
	}
1042
1043

      if (want_stats)
1044
1045
	{
	  statistics* st = &(*fstats)[translator_num];
1046
1047
1048
1049
1050
1051
1052
	  st->status_str = status_str;
	  st->status_code = es;
	  double prec = XTIME_PRECISION;
	  st->time = (after - before) / prec;

	  // Compute statistics.
	  if (res)
1053
	    {
1054
1055
	      if (verbose)
		std::cerr << "info: getting statistics\n";
1056
1057
1058
1059
1060
	      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;
1061
	      st->acc = res->acc().num_sets();
1062
1063
1064
	      spot::scc_map m(res);
	      m.build_map();
	      unsigned c = m.scc_count();
1065
	      st->scc = c;
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
	      st->nondetstates = spot::count_nondet_states(res);
	      st->nondeterministic = st->nondetstates != 0;
	      for (unsigned n = 0; n < c; ++n)
		{
		  if (!m.accepting(n))
		    ++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;
1083
	      else
1084
		st->terminal_aut = true;
1085
	    }
1086
	}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1087
      output.cleanup();
1088
      return res;
1089
    }
1090
  };
1091

1092
  static bool
1093
1094
  check_empty_prod(const spot::const_tgba_ptr& aut_i,
		   const spot::const_tgba_ptr& aut_j,
1095
		   size_t i, size_t j, bool icomp, bool jcomp)
1096
  {
1097
    auto prod = spot::product(aut_i, aut_j);
1098
    auto res = spot::couvreur99(prod)->check();
1099

1100
1101
1102
1103
1104
1105
    if (verbose)
      {
	std::cerr << "info: check_empty ";
	if (icomp)
	  std::cerr << "Comp(N" << i << ')';
	else
1106
	  std::cerr << 'P' << i;
1107
1108
1109
1110
1111
1112
1113
	if (jcomp)
	  std::cerr << "*Comp(P" << j << ')';
	else
	  std::cerr << "*N" << j;
	std::cerr << '\n';
      }

1114
1115
    if (res)
      {
1116
1117
1118
	std::ostream& err = global_error();
	err << "error: ";
	if (icomp)
1119
	  err << "Comp(N" << i << ')';
1120
	else
1121
	  err << 'P' << i;
1122
	if (jcomp)
1123
	  err << "*Comp(P" << j << ')';
1124
1125
1126
	else
	  err << "*N" << j;
	err << " is nonempty";
1127

1128
	auto run = res->accepting_run();
1129
1130
	if (run)
	  {
1131
	    run = reduce_run(prod, run);
1132
1133
	    std::cerr << "; both automata accept the infinite word\n"
		      << "       ";
1134
	    spot::tgba_word w(run);
1135
	    w.simplify();
1136
	    w.print(example(), prod->get_dict()) << '\n';
1137
1138
1139
	  }
	else
	  {
1140
	    std::cerr << '\n';
1141
1142
1143
	  }
	end_error();
      }
1144
    return !!res;
1145
1146
  }

1147
  static bool
1148
  cross_check(const std::vector<spot::scc_map*>& maps, char l, unsigned p)
1149
1150
  {
    size_t m = maps.size();
Alexandre Duret-Lutz's avatar