ltlcross.cc 46.5 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

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

65
66
67
68
69
70
71
72
// 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

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


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

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

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

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

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

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;

278
279
280
281
282
283
bool global_error_flag = false;

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

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


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


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

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

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

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

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

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

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

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

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

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

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

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

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

    ~printable_result_filename()
    {
      delete val_;
    }

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

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

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

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

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

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

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

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

831
832
833
834
    }

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

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

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

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

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

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

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

904
905
      const char* status_str = 0;

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

1001
1002
1003
1004
1005
		    // Gather statistics about the input automaton
		    if (want_stats)
		      {
			statistics* st = &(*fstats)[translator_num];
			st->has_in = true;
1006
			st->in_type = type;
1007
1008
1009
1010
1011
1012
1013
			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;

1014
			st->in_scc = spot::scc_info(aut->aut).scc_count();
1015
1016
		      }
		    // convert it into TGBA for further processing
1017
1018
		    if (verbose)
		      std::cerr << "info: converting " << type << " to TGBA\n";
1019
1020
		    res = dstar_to_tgba(aut);
		  }
1021
1022
		break;
	      }
1023
	    case printable_result_filename::Hoa: // Will also read neverclaims
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
	      {
		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();
1034
		    err << "error: failed to parse the produced automaton.\n";
1035
1036
1037
1038
		    spot::format_hoa_parse_errors(err, filename, pel);
		    end_error();
		    res = nullptr;
		  }
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
		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;
		  }
1049
1050
1051
1052
1053
1054
		else
		  {
		    res = aut->aut;
		  }
		break;
	      }
1055
	    case printable_result_filename::None:
1056
	      SPOT_UNREACHABLE();
1057
	    }
1058
	}
1059
1060

      if (want_stats)
1061
1062
	{
	  statistics* st = &(*fstats)[translator_num];
1063
1064
	  st->status_str = status_str;
	  st->status_code = es;
1065
	  st->time = duration;
1066
1067
1068

	  // Compute statistics.
	  if (res)
1069
	    {
1070
1071
	      if (verbose)
		std::cerr << "info: getting statistics\n";
1072
1073
1074
1075
1076
	      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;
1077
	      st->acc = res->acc().num_sets();
1078
	      spot::scc_info m(res);
1079
	      unsigned c = m.scc_count();
1080
	      st->scc = c;
1081
1082
1083
1084
	      st->nondetstates = spot::count_nondet_states(res);
	      st->nondeterministic = st->nondetstates != 0;
	      for (unsigned n = 0; n < c; ++n)
		{
1085
		  if (!m.is_accepting_scc(n))
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
		    ++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;
1098
	      else
1099
		st->terminal_aut = true;
1100
	    }
1101
	}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1102
      output.cleanup();
1103
      return res;
1104
    }
1105
  };
1106

1107
  static bool
1108
1109
  check_empty_prod(const spot::const_tgba_digraph_ptr& aut_i,
		   const spot::const_tgba_digraph_ptr& aut_j,
1110
		   size_t i, size_t j, bool icomp, bool jcomp)
1111
  {
1112
    auto prod = spot::product(aut_i, aut_j);
1113
    auto res = spot::couvreur99(prod)->check();
1114

1115
1116
1117
1118
1119
1120
    if (verbose)
      {
	std::cerr << "info: check_empty ";
	if (icomp)
	  std::cerr << "Comp(N" << i << ')';
	else
1121
	  std::cerr << 'P' << i;
1122
1123
1124
1125
1126
1127
1128
	if (jcomp)
	  std::cerr << "*Comp(P" << j << ')';
	else
	  std::cerr << "*N" << j;
	std::cerr << '\n';
      }

1129
1130
    if (res)
      {
1131
1132
1133
	std::ostream& err = global_error();
	err << "error: ";
	if (icomp)
1134
	  err << "Comp(N" << i << ')';
1135
	else
1136
	  err << 'P' << i;
1137
	if (jcomp)
1138
	  err << "*Comp(P" << j << ')';
1139
1140
1141
	else
	  err << "*N" << j;
	err << " is nonempty";
1142

1143
	auto run = res->accepting_run();
1144
1145
	if (run)
	  {
1146
	    run = reduce_run(prod, run);
1147
1148
	    std::cerr << "; both automata accept the infinite word\n"
		      << "       ";
1149
	    spot::tgba_word w(run);
1150
	    w.simplify();
1151
	    w.print(example(), prod->get_dict()) << '\n';
1152
1153
1154
	  }
	else
	  {
1155
	    std::cerr << '\n';
1156
1157
1158
	  }
	end_error</