ltlcross.cc 46.1 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
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", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the output automaton as a Never claim, in LBTT's or in LTL2DSTAR's "
      "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, Spin, Lbtt, Dstar };
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
742
      if (*pos == 'N')
	format = Spin;
743
      else if (*pos == 'T')
744
	format = Lbtt;
745
746
747
      else if (*pos == 'D')
	format = Dstar;
      else
748
	SPOT_UNREACHABLE();
749

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
750
      if (val_)
751
752
753
754
755
	{
	  // 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",
756
		  translators[translator_num].spec);
757
758
759
760
761
762
763
764
	}
      else
	{
	  char prefix[30];
	  snprintf(prefix, sizeof prefix, "lcr-o%u-", translator_num);
	  const_cast<printable_result_filename*>(this)->val_
	    = spot::create_tmpfile(prefix);
	}
765
766
767
      os << '\'' << val_ << '\'';
    }
  };
768

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

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

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

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

827
828
829
830
    }

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

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

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

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

      std::ostringstream command;
888
      format(command, translators[translator_num].cmd);
889

890
      assert(output.format != printable_result_filename::None);
891

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

900
901
      const char* status_str = 0;

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

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

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

      if (want_stats)
1043
1044
	{
	  statistics* st = &(*fstats)[translator_num];
1045
1046
	  st->status_str = status_str;
	  st->status_code = es;
1047
	  st->time = duration;
1048
1049
1050

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

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

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

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

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