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

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
99
100
101

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

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

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

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

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;

269
270
271
272
273
274
bool global_error_flag = false;

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

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


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


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

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

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

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

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

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

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

583
584
#if ENABLE_TIMEOUT
static volatile int alarm_on = 0;
585
586
587
588
589
590
591
592
593
594
595
596
597
598
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.
599
	  kill(-child_pid, SIGTERM);
600
601
602
603
604
605
606
	  // 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.
607
	  kill(-child_pid, SIGKILL);
608
609
610
611
612
	}
    }
  else
    {
      // forward signal
613
      kill(-child_pid, sig);
614
      // cleanup files
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
615
      spot::cleanup_tmpfiles();
616
617
      // and die verbosely
      error(2, 0, "received signal %d", sig);
618
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
    }
}

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

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

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

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

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

    ~printable_result_filename()
    {
      delete val_;
    }

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

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

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

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

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

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

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

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

810
811
812
813
    }

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

827
828
    const std::string&
    formula() const
829
830
831
832
833
834
    {
      // 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;
835
836
      if (!string_ltl_wring.val().empty())
	return string_ltl_wring;
837
838
      if (!string_ltl_lbt.val().empty())
	return string_ltl_lbt;
839
      assert(!"None of the translators need the input formula?");
840
841
842
      return string_ltl_spot;
    }

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

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

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

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

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

882
883
      const char* status_str = 0;

884
      const spot::tgba* res = 0;
885
886
      if (timed_out)
	{
887
888
	  // This is not considered to be a global error.
	  std::cerr << "warning: timeout during execution of command\n";
889
	  ++timeout_count;
890
	  status_str = "timeout";
891
	  problem = false;	// A timeout is not a sign of a bug
892
	  es = -1;
893
894
895
	}
      else if (WIFSIGNALED(es))
	{
896
	  status_str = "signal";
897
	  problem = true;
898
	  es = WTERMSIG(es);
899
	  global_error() << "error: execution terminated by signal "
900
			 << es << ".\n";
901
	  end_error();
902
903
	}
      else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
904
	{
905
906
	  es = WEXITSTATUS(es);
	  status_str = "exit code";
907
	  problem = true;
908
	  global_error() << "error: execution returned exit code "
909
			 << es << ".\n";
910
	  end_error();
911
912
913
	}
      else
	{
914
	  status_str = "ok";
915
	  problem = false;
916
	  es = 0;
917
918
919
	  switch (output.format)
	    {
	    case printable_result_filename::Spin:
920
	      {
921
		spot::neverclaim_parse_error_list pel;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
922
923
		std::string filename = output.val()->name();
		res = spot::neverclaim_parse(filename, pel, &dict);
924
925
		if (!pel.empty())
		  {
926
		    status_str = "parse error";
927
		    problem = true;
928
		    es = -1;
929
930
		    std::ostream& err = global_error();
		    err << "error: failed to parse the produced neverclaim.\n";
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
931
		    spot::format_neverclaim_parse_errors(err, filename, pel);
932
		    end_error();
933
934
935
936
		    delete res;
		    res = 0;
		  }
		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
971
972
973
974
	    case printable_result_filename::Dstar:
	      {
		spot::dstar_parse_error_list pel;
		std::string filename = output.val()->name();
		spot::dstar_aut* aut;
		aut = spot::dstar_parse(filename, pel, &dict);
		if (!pel.empty())
		  {
975
		    status_str = "parse error";
976
		    problem = true;
977
		    es = -1;
978
979
980
981
982
983
984
985
986
		    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();
		    delete aut;
		    res = 0;
		  }
		else
987
		  {
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
		    // 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;

			spot::scc_map m(aut->aut);
			m.build_map();
			st->in_scc = m.scc_count();
		      }
		    // convert it into TGBA for further processing
1016
1017
1018
		    res = dstar_to_tgba(aut);
		    delete aut;
		  }
1019
1020
		break;
	      }
1021
1022
1023
	    case printable_result_filename::None:
	      assert(!"unreachable code");
	    }
1024
	}
1025
1026

      if (want_stats)
1027
1028
	{
	  statistics* st = &(*fstats)[translator_num];
1029
1030
1031
1032
1033
1034
1035
	  st->status_str = status_str;
	  st->status_code = es;
	  double prec = XTIME_PRECISION;
	  st->time = (after - before) / prec;

	  // Compute statistics.
	  if (res)
1036
	    {
1037
1038
1039
1040
1041
1042
1043
1044
1045
	      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();
1046
	      st->scc = c;
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
	      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;
1064
	      else
1065
		st->terminal_aut = true;
1066
	    }
1067
	}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1068
      output.cleanup();
1069
      return res;
1070
    }
1071
  };
1072

1073
  static bool
1074
  check_empty_prod(const spot::tgba* aut_i, const spot::tgba* aut_j,
1075
		   size_t i, size_t j, bool icomp, bool jcomp)
1076
  {
1077
1078
    spot::tgba_product* prod = new spot::tgba_product(aut_i, aut_j);
    spot::emptiness_check* ec = spot::couvreur99(prod);
1079
    spot::emptiness_check_result* res = ec->check();
1080
1081
1082

    if (res)
      {
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
	std::ostream& err = global_error();
	err << "error: ";
	if (icomp)
	  err << "Comp(N" << i << ")";
	else
	  err << "P" << i;
	if (jcomp)
	  err << "*Comp(P" << j << ")";
	else
	  err << "*N" << j;
	err << " is nonempty";
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112

	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();
	    w.print(example(), prod->get_dict()) << "\n";
	    delete runmin;
	  }
	else
	  {
	    std::cerr << "\n";
	  }
	end_error();
      }
1113
1114
    delete res;
    delete ec;
1115
    delete prod;
1116
    return res;
1117
1118
  }

1119
  static bool
1120
  cross_check(const std::vector<spot::scc_map*>& maps, char l, unsigned p)
1121
1122
  {
    size_t m = maps.size();
1123

1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
    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)
1142
      {
1143
1144
	std::ostream& err = global_error();
	err << "error: {";
1145
1146
1147
1148
1149
1150
1151
	bool first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && res[i])
	    {
	      if (first)
		first = false;
	      else
1152
		err << ',';
1153
	      err << l << i;
1154
	    }
1155
	err << "} disagree with {";
1156
1157
1158
1159
1160
1161
1162
	first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && !res[i])
	    {
	      if (first)
		first = false;
	      else
1163
		err << ',';
1164
	      err << l << i;
1165
	    }
1166
1167
	err << "} when evaluating ";
	if (products > 1)
1168
	  err << "state-space #" << p << "/" << products << "\n";
1169
	else
1170
	  err << "the state-space\n";
1171
	end_error();
1172
	return true;
1173
      }
1174
    return false;
1175
  }
1176

1177
  typedef std::set<spot::state*, spot::state_ptr_less_than> state_set;
1178

1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
  // Collect all the states of SSPACE that appear in the accepting SCCs
  // of PROD.
  static void
  states_in_acc(const spot::scc_map* m, const spot::tgba* sspace,
		state_set& s)
  {
    const spot::tgba* aut = m->get_aut();
    unsigned c = m->scc_count();
    for (unsigned n = 0; n < c; ++n)
      if (m->accepting(n))
	{
	  const std::list<const spot::state*>& l = m->states_of(n);
	  for (std::list<const spot::state*>::const_iterator i = l.begin();
	       i != l.end(); ++i)
	    {
	      spot::state* x = aut->project_state(*i, sspace);
	      if (!s.insert(x).second)
		x->destroy();
	    }
	}
  }
1200

1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
  static bool
  consistency_check(const spot::scc_map* pos, const spot::scc_map* neg,
		    const spot::tgba* sspace)
  {
    // the states of SSPACE should appear in the accepting SCC of at
    // least one of POS or NEG.  Maybe both.
    state_set s;
    states_in_acc(pos, sspace, s);
    states_in_acc(neg, sspace, s);
    bool res = s.size() == states;
    state_set::iterator it;
1212
    for (it = s.begin(); it != s.end(); ++it)
1213
1214
1215
      (*it)->destroy();
    return res;
  }
1216

1217
1218
1219
1220
1221
  typedef
  Sgi::hash_set<const spot::ltl::formula*,
		const spot::ptr_hash<const spot::ltl::formula> > fset_t;