ltlcross.cc 43.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/relabel.hh"
47
#include "tgbaalgos/lbtt.hh"
48
49
50
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/randomgraph.hh"
51
#include "tgbaalgos/sccinfo.hh"
52
53
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/dotty.hh"
54
#include "tgbaalgos/isweakscc.hh"
55
56
#include "tgbaalgos/reducerun.hh"
#include "tgbaalgos/word.hh"
57
#include "tgbaalgos/dtgbacomp.hh"
58
#include "misc/formater.hh"
59
60
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/isdet.hh"
61
#include "misc/escape.hh"
62
#include "misc/hash.hh"
63
#include "misc/random.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
64
#include "misc/tmpfile.hh"
65

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

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


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

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

const struct argp_child children[] =
  {
    { &finput_argp, 0, 0, 1 },
172
    { &misc_argp, 0, 0, -1 },
173
174
175
    { 0, 0, 0, 0 }
  };

176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
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";
194
const char* bright_blue = "\033[01;34m";
195
const char* bright_yellow = "\033[01;33m";
196
197
const char* reset_color = "\033[m";

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

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;

270
271
272
273
274
275
bool global_error_flag = false;

static std::ostream&
global_error()
{
  global_error_flag = true;
276
277
  if (color_opt)
    std::cerr << bright_red;
278
279
  return std::cerr;
}
280

281
282
283
284
285
286
287
288
289
static std::ostream&
example()
{
  if (color_opt)
    std::cerr << bright_yellow;
  return std::cerr;
}


290
291
292
293
294
295
296
297
static void
end_error()
{
  if (color_opt)
    std::cerr << reset_color;
}


298
299
struct statistics
{
300
301
  statistics()
    : ok(false),
302
      has_in(false),
303
304
305
      status_str(0),
      status_code(0),
      time(0),
306
307
308
309
310
311
      in_type(0),
      in_states(0),
      in_edges(0),
      in_transitions(0),
      in_acc(0),
      in_scc(0),
312
      states(0),
313
      edges(0),
314
315
316
317
318
319
320
321
322
323
324
      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),
325
      strong_aut(false)
326
327
328
  {
  }

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

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

  void
390
  to_csv(std::ostream& os, bool show_exit, bool show_sr, const char* na = "")
391
  {
392
    if (show_exit)
393
394
395
      os << '"' << status_str << "\"," << status_code << ',';
    os << time << ',';
    if (ok)
396
      {
397
398
399
400
401
402
403
404
405
406
	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 << ',';
407
408
409
410
411
412
413
414
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
	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);
	  }
      }
444
    else
445
446
      {
	size_t m = products_avg ? 1U : products;
447
448
449
	m *= 3;
	m += 13 + show_sr * 6;
	os << na;
450
	for (size_t i = 0; i < m; ++i)
451
	  os << ',' << na;
452
      }
453
454
455
456
457
458
459
460
  }
};

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

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

581
static volatile bool timed_out = false;
582
unsigned timeout_count = 0;
583

584
585
#if ENABLE_TIMEOUT
static volatile int alarm_on = 0;
586
587
588
589
590
591
592
593
594
595
596
597
598
599
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.
600
	  kill(-child_pid, SIGTERM);
601
602
603
604
605
606
607
	  // 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.
608
	  kill(-child_pid, SIGKILL);
609
610
611
612
613
	}
    }
  else
    {
      // forward signal
614
      kill(-child_pid, sig);
615
      // cleanup files
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
616
      spot::cleanup_tmpfiles();
617
618
      // and die verbosely
      error(2, 0, "received signal %d", sig);
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
    }
}

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'");
653
654
      // never reached
      return -1;
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
    }
  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;
}
672
673
674
675
#else // !ENABLE_TIMEOUT
#define exec_with_timeout(cmd) system(cmd)
#define setup_sig_handler() while (0);
#endif // !ENABLE_TIMEOUT
676

677
namespace
678
{
679
680
681
  struct quoted_string: public spot::printable_value<std::string>
  {
    using spot::printable_value<std::string>::operator=;
682

683
684
685
686
687
688
689
690
    void
    print(std::ostream& os, const char* pos) const
    {
      os << '\'';
      this->spot::printable_value<std::string>::print(os, pos);
      os << '\'';
    }
  };
691

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
692
693
  struct printable_result_filename:
    public spot::printable_value<spot::temporary_file*>
694
695
  {
    unsigned translator_num;
696
    enum output_format { None, Spin, Lbtt, Dstar };
697
    mutable output_format format;
698

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
699
700
701
702
703
704
705
706
707
708
    printable_result_filename()
    {
      val_ = 0;
    }

    ~printable_result_filename()
    {
      delete val_;
    }

709
710
711
712
713
    void reset(unsigned n)
    {
      translator_num = n;
      format = None;
    }
714

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
715
716
717
718
719
720
    void cleanup()
    {
      delete val_;
      val_ = 0;
    }

721
722
723
    void
    print(std::ostream& os, const char* pos) const
    {
724
      output_format old_format = format;
725
726
      if (*pos == 'N')
	format = Spin;
727
      else if (*pos == 'T')
728
	format = Lbtt;
729
730
731
      else if (*pos == 'D')
	format = Dstar;
      else
732
	SPOT_UNREACHABLE();
733

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
734
      if (val_)
735
736
737
738
739
	{
	  // 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",
740
		  translators[translator_num].spec);
741
742
743
744
745
746
747
748
	}
      else
	{
	  char prefix[30];
	  snprintf(prefix, sizeof prefix, "lcr-o%u-", translator_num);
	  const_cast<printable_result_filename*>(this)->val_
	    = spot::create_tmpfile(prefix);
	}
749
750
751
      os << '\'' << val_ << '\'';
    }
  };
752

753
754
755
  class translator_runner: protected spot::formater
  {
  private:
756
    spot::bdd_dict_ptr dict;
757
758
759
760
    // Round-specific variables
    quoted_string string_ltl_spot;
    quoted_string string_ltl_spin;
    quoted_string string_ltl_lbt;
761
    quoted_string string_ltl_wring;
762
763
764
    quoted_string filename_ltl_spot;
    quoted_string filename_ltl_spin;
    quoted_string filename_ltl_lbt;
765
    quoted_string filename_ltl_wring;
766
767
768
    // Run-specific variables
    printable_result_filename output;
  public:
769
770
    using spot::formater::has;

771
    translator_runner(spot::bdd_dict_ptr dict)
772
      : dict(dict)
773
774
775
776
    {
      declare('f', &string_ltl_spot);
      declare('s', &string_ltl_spin);
      declare('l', &string_ltl_lbt);
777
      declare('w', &string_ltl_wring);
778
779
780
      declare('F', &filename_ltl_spot);
      declare('S', &filename_ltl_spin);
      declare('L', &filename_ltl_lbt);
781
      declare('W', &filename_ltl_wring);
782
      declare('D', &output);
783
784
785
786
787
788
      declare('N', &output);
      declare('T', &output);

      size_t s = translators.size();
      assert(s);
      for (size_t n = 0; n < s; ++n)
789
790
791
	{
	  // Check that each translator uses at least one input and
	  // one output.
792
	  std::vector<bool> has(256);
793
794
	  const translator_spec& t = translators[n];
	  scan(t.cmd, has);
795
796
797
798
	  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 "
799
		  "to pass the formula.", t.spec);
800
801
	  bool has_d = has['D'];
	  if (!(has_d || has['N'] || has['T']))
802
803
	    error(2, 0, "no output %%-sequence in '%s'.\n      Use one of "
		  "%%D,%%N,%%T to indicate where the automaton is saved.",
804
		  t.spec);
805
	  has_sr |= has_d;
806
807

	  // Remember the %-sequences used by all translators.
808
	  prime(t.cmd);
809
	}
810

811
812
813
814
    }

    void
    string_to_tmp(std::string& str, unsigned n, std::string& tmpname)
815
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
816
817
818
819
820
      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();
821
822
823
824
      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
825
      tmpfile->close();
826
827
    }

828
829
    const std::string&
    formula() const
830
831
832
833
834
835
    {
      // 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;
836
837
      if (!string_ltl_wring.val().empty())
	return string_ltl_wring;
838
839
      if (!string_ltl_lbt.val().empty())
	return string_ltl_lbt;
840
      SPOT_UNREACHABLE();
841
842
843
      return string_ltl_spot;
    }

844
845
    void
    round_formula(const spot::ltl::formula* f, unsigned serial)
846
847
848
849
850
851
852
    {
      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);
853
854
      if (has('w') || has('W'))
	string_ltl_wring = spot::ltl::to_wring_string(f);
855
856
857
858
859
860
      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);
861
862
      if (has('W'))
	string_to_tmp(string_ltl_wring, serial, filename_ltl_wring);
863
864
    }

865
    spot::const_tgba_ptr
866
867
    translate(unsigned int translator_num, char l, statistics_formula* fstats,
	      bool& problem)
868
869
870
871
    {
      output.reset(translator_num);

      std::ostringstream command;
872
      format(command, translators[translator_num].cmd);
873

874
      assert(output.format != printable_result_filename::None);
875

876
877
878
      std::string cmd = command.str();
      std::cerr << "Running [" << l << translator_num << "]: "
		<< cmd << std::endl;
879
      xtime_t before = gethrxtime();
880
      int es = exec_with_timeout(cmd.c_str());
881
      xtime_t after = gethrxtime();
882

883
884
      const char* status_str = 0;

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

			switch (aut->type)
			  {
			  case spot::Rabin:
			    st->in_type = "DRA";
			    break;
			  case spot::Streett:
			    st->in_type = "DSA";
			    break;
			  }

			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;

1009
			st->in_scc = spot::scc_info(aut->aut).scc_count();
1010
1011
		      }
		    // convert it into TGBA for further processing
1012
1013
		    res = dstar_to_tgba(aut);
		  }
1014
1015
		break;
	      }
1016
	    case printable_result_filename::None:
1017
	      SPOT_UNREACHABLE();
1018
	    }
1019
	}
1020
1021

      if (want_stats)
1022
1023
	{
	  statistics* st = &(*fstats)[translator_num];
1024
1025
1026
1027
1028
1029
1030
	  st->status_str = status_str;
	  st->status_code = es;
	  double prec = XTIME_PRECISION;
	  st->time = (after - before) / prec;

	  // Compute statistics.
	  if (res)
1031
	    {
1032
1033
1034
1035
1036
1037
1038
1039
1040
	      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;
	      st->acc = res->number_of_acceptance_conditions();
	      spot::scc_map m(res);
	      m.build_map();
	      unsigned c = m.scc_count();
1041
	      st->scc = c;
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
	      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;
1059
	      else
1060
		st->terminal_aut = true;
1061
	    }
1062
	}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1063
      output.cleanup();
1064
      return res;
1065
    }
1066
  };
1067

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

    if (res)
      {
1079
1080
1081
	std::ostream& err = global_error();
	err << "error: ";
	if (icomp)
1082
	  err << "Comp(N" << i << ')';
1083
	else
1084
	  err << 'P' << i;
1085
	if (jcomp)
1086
	  err << "*Comp(P" << j << ')';
1087
1088
1089
	else
	  err << "*N" << j;
	err << " is nonempty";
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099

	spot::tgba_run* run = res->accepting_run();
	if (run)
	  {
	    const spot::tgba_run* runmin = reduce_run(prod, run);
	    delete run;
	    std::cerr << "; both automata accept the infinite word\n"
		      << "       ";
	    spot::tgba_word w(runmin);
	    w.simplify();
1100
	    w.print(example(), prod->get_dict()) << '\n';
1101
1102
1103
1104
	    delete runmin;
	  }
	else
	  {
1105
	    std::cerr << '\n';
1106
1107
1108
	  }
	end_error();
      }
1109
1110
    delete res;
    delete ec;
1111
    return res;
1112
1113
  }

1114
  static bool
1115
  cross_check(const std::vector<spot::scc_map*>& maps, char l, unsigned p)
1116
1117
  {
    size_t m = maps.size();
1118

1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
    std::vector<bool> res(m);
    unsigned verified = 0;
    unsigned violated = 0;
    for (size_t i = 0; i < m; ++i)
      if (spot::scc_map* m = maps[i])
	{
	  // r == true iff the automaton i is accepting.
	  bool r = false;
	  unsigned c = m->scc_count();
	  for (unsigned j = 0; (j < c) && !r; ++j)
	    r |= m->accepting(j);
	  res[i] = r;
	  if (r)
	    ++verified;
	  else
	    ++violated;
	}
    if (verified != 0 && violated != 0)
1137
      {
1138
1139
	std::ostream& err = global_error();
	err << "error: {";
1140
1141
1142
1143
1144
1145
1146
	bool first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && res[i])
	    {
	      if (first)
		first = false;
	      else
1147
		err << ',';
1148
	      err << l << i;
1149
	    }
1150
	err << "} disagree with {";
1151
1152
1153
1154
1155
1156
1157
	first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && !res[i])
	    {
	      if (first)
		first = false;
	      else
1158
		err << ',';
1159
	      err << l << i;
1160
	    }
1161
1162
	err << "} when evaluating ";
	if (products > 1)
1163
	  err << "state-space #" << p << '/' << products << '\n';
1164
	else
1165
	  err << "the state-space\n";
1166
	end_error();
1167
	return true;
1168
      }
Alexandre Duret-Lutz's avatar