ltlcross.cc 31.6 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2012, 2013 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
36
37
38
39
40
41
42
43

#include "common_setup.hh"
#include "common_cout.hh"
#include "common_finput.hh"
#include "neverparse/public.hh"
#include "ltlast/unop.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/apcollect.hh"
#include "ltlvisit/lbt.hh"
44
#include "ltlvisit/relabel.hh"
45
#include "tgbaalgos/lbtt.hh"
46
47
48
49
50
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/randomgraph.hh"
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/dotty.hh"
51
#include "tgbaalgos/isweakscc.hh"
52
#include "misc/formater.hh"
53
54
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/isdet.hh"
55
#include "misc/escape.hh"
56
#include "misc/hash.hh"
57
#include "misc/random.hh"
58

59
60
61
62
63
64
65
66
// 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

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


#define OPT_STATES 1
#define OPT_DENSITY 2
81
82
#define OPT_JSON 3
#define OPT_CSV 4
83
#define OPT_DUPS 5
84
#define OPT_NOCHECKS 6
85
#define OPT_STOP_ERR 7
86
#define OPT_SEED 8
87
#define OPT_PRODUCTS 9
88
89
90
91
92
93
94

static const argp_option options[] =
  {
    /**************************************************/
    { 0, 0, 0, 0, "Specifying translator to call:", 2 },
    { "translator", 't', "COMMANDFMT", 0,
      "register one translators to call", 0 },
95
    { "timeout", 'T', "NUMBER", 0, "kill translators after NUMBER seconds", 0 },
96
97
98
99
    /**************************************************/
    { 0, 0, 0, 0,
      "COMMANDFMT should specify input and output arguments using the "
      "following character sequences:", 3 },
100
101
102
103
104
    { "%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 },
105
106
    { "%N,%T", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the output automaton as a Never claim, or in LBTT's format", 0 },
107
108
109
110
    { 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 "
      "relabeled automatically.", 0 },
111
    /**************************************************/
112
    { 0, 0, 0, 0, "ltlcross behavior:", 4 },
113
114
115
116
117
    { "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 },
118
119
120
    { "stop-on-error", OPT_STOP_ERR, 0, 0,
      "stop on first execution error or failure to pass"
      " sanity checks (timeouts are OK)", 0 },
121
122
    /**************************************************/
    { 0, 0, 0, 0, "State-space generation:", 5 },
123
124
125
126
127
    { "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 },
128
129
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0 by default)", 0 },
130
131
132
    { "products", OPT_PRODUCTS, "INT", 0,
      "number of product to perform (1 by default), statistics will be "
      "averaged", 0 },
133
    /**************************************************/
134
    { 0, 0, 0, 0, "Statistics output:", 6 },
135
136
137
138
139
    { "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 },
    /**************************************************/
140
141
142
143
144
145
146
    { 0, 0, 0, 0, "Miscellaneous options:", -1 },
    { 0, 0, 0, 0, 0, 0 }
  };

const struct argp_child children[] =
  {
    { &finput_argp, 0, 0, 1 },
147
    { &misc_argp, 0, 0, -1 },
148
149
150
151
152
    { 0, 0, 0, 0 }
  };

unsigned states = 200;
float density = 0.1;
153
unsigned timeout = 0;
154
155
156
const char* json_output = 0;
const char* csv_output = 0;
bool want_stats = false;
157
bool allow_dups = false;
158
bool no_checks = false;
159
bool stop_on_error = false;
160
int seed = 0;
161
unsigned products = 1;
162

163
std::vector<char*> translators;
164
165
166
167
168
169
170
171
bool global_error_flag = false;

static std::ostream&
global_error()
{
  global_error_flag = true;
  return std::cerr;
}
172

173
174
struct statistics
{
175
176
177
178
179
180
181
182
183
184
  statistics()
    : ok(false),
      // Initialize these, because they accumulate values from several
      // products.
      product_states(0),
      product_transitions(0),
      product_scc(0)
  {
  }

185
186
187
188
189
190
  bool ok;
  unsigned states;
  unsigned edges;
  unsigned transitions;
  unsigned acc;
  unsigned scc;
191
192
193
194
  unsigned nonacc_scc;
  unsigned terminal_scc;
  unsigned weak_scc;
  unsigned strong_scc;
195
196
  unsigned nondetstates;
  bool nondeterministic;
197
198
199
  bool terminal_aut;
  bool weak_aut;
  bool strong_aut;
200
  double time;
201
202
203
  double product_states;
  double product_transitions;
  double product_scc;
204
205
206
207

  static void
  fields(std::ostream& os)
  {
208
209
210
211
212
    os << (" \"states\","
	   " \"edges\","
	   " \"transitions\","
	   " \"acc\","
	   " \"scc\","
213
214
215
216
217
218
219
220
221
	   " \"nonacc_scc\","
	   " \"terminal_scc\","
	   " \"weak_scc\","
	   " \"strong_scc\","
	   " \"nondet_states\","
	   " \"nondet_aut\","
	   " \"terminal_aut\","
	   " \"weak_aut\","
	   " \"strong_aut\","
222
223
224
225
	   " \"time\","
	   " \"product_states\","
	   " \"product_transitions\","
	   " \"product_scc\"");
226
227
228
229
230
231
232
233
234
235
  }

  void
  to_csv(std::ostream& os)
  {
    os << states << ", "
       << edges << ", "
       << transitions << ", "
       << acc << ", "
       << scc << ", "
236
237
238
239
       << nonacc_scc << ", "
       << terminal_scc << ", "
       << weak_scc << ", "
       << strong_scc << ", "
240
241
       << nondetstates << ", "
       << nondeterministic << ", "
242
243
244
       << terminal_aut << ", "
       << weak_aut << ", "
       << strong_aut << ", "
245
       << time << ", "
246
247
248
249
250
251
252
253
254
255
256
       << product_states << ", "
       << product_transitions << ", "
       << product_scc;
  }
};

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

257
258
259
260
261
262
263
264
265
266
267
// Cleanup temporary files.
std::list<std::string> toclean;
void
cleanup()
{
  for (std::list<std::string>::const_iterator i = toclean.begin();
       i != toclean.end(); ++i)
    unlink(i->c_str());
  toclean.clear();
}

268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
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;
318
319
    case 'T':
      timeout = to_pos_int(arg);
320
321
322
323
#if !ENABLE_TIMEOUT
      std::cerr << "warning: setting a timeout is not supported "
		<< "on your platform" << std::endl;
#endif
324
      break;
325
326
327
328
    case OPT_CSV:
      want_stats = true;
      csv_output = arg ? arg : "-";
      break;
329
330
331
    case OPT_DENSITY:
      density = to_probability(arg);
      break;
332
333
334
    case OPT_DUPS:
      allow_dups = true;
      break;
335
336
337
338
    case OPT_JSON:
      want_stats = true;
      json_output = arg ? arg : "-";
      break;
339
340
341
    case OPT_PRODUCTS:
      products = to_pos_int(arg);
      break;
342
343
344
    case OPT_NOCHECKS:
      no_checks = true;
      break;
345
346
347
    case OPT_SEED:
      seed = to_pos_int(arg);
      break;
348
349
350
    case OPT_STATES:
      states = to_pos_int(arg);
      break;
351
352
353
    case OPT_STOP_ERR:
      stop_on_error = true;
      break;
354
355
356
357
358
359
360
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

static int
361
create_tmpfile(char c, unsigned int n, std::string& name)
362
363
{
  char tmpname[30];
364
  snprintf(tmpname, sizeof tmpname, "lck-%c%u-XXXXXX", c, n);
365
366
367
368
369
370
371
  int fd = mkstemp(tmpname);
  if (fd == -1)
    error(2, errno, "failed to create a temporary file");
  name = tmpname;
  return fd;
}

372
373

static volatile bool timed_out = false;
374
unsigned timeout_count = 0;
375

376
377
#if ENABLE_TIMEOUT
static volatile int alarm_on = 0;
378
379
380
381
382
383
384
385
386
387
388
389
390
391
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.
392
	  kill(-child_pid, SIGTERM);
393
394
395
396
397
398
399
	  // 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.
400
	  kill(-child_pid, SIGKILL);
401
402
403
404
405
	}
    }
  else
    {
      // forward signal
406
      kill(-child_pid, sig);
407
408
      // cleanup files
      cleanup();
409
410
      // and die verbosely
      error(2, 0, "received signal %d", sig);
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
444
    }
}

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'");
445
446
      // never reached
      return -1;
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
    }
  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;
}
464
465
466
467
#else // !ENABLE_TIMEOUT
#define exec_with_timeout(cmd) system(cmd)
#define setup_sig_handler() while (0);
#endif // !ENABLE_TIMEOUT
468

469
namespace
470
{
471
472
473
  struct quoted_string: public spot::printable_value<std::string>
  {
    using spot::printable_value<std::string>::operator=;
474

475
476
477
478
479
480
481
482
    void
    print(std::ostream& os, const char* pos) const
    {
      os << '\'';
      this->spot::printable_value<std::string>::print(os, pos);
      os << '\'';
    }
  };
483

484
485
486
487
488
  struct printable_result_filename: public spot::printable_value<std::string>
  {
    unsigned translator_num;
    enum output_format { None, Spin, Lbtt };
    mutable output_format format;
489

490
491
492
493
494
495
    void reset(unsigned n)
    {
      val_.clear();
      translator_num = n;
      format = None;
    }
496

497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
    void
    print(std::ostream& os, const char* pos) const
    {
      if (*pos == 'N')
	format = Spin;
      else
	format = Lbtt;
      if (!val_.empty())
	error(2, 0, "you may have only one %%N or %%T specifier: %s",
	      translators[translator_num]);
      close(create_tmpfile('o', translator_num,
			   const_cast<std::string&>(val_)));
      os << '\'' << val_ << '\'';
    }
  };
512

513
514
515
  class translator_runner: protected spot::formater
  {
  private:
516
    spot::bdd_dict& dict;
517
518
519
520
    // Round-specific variables
    quoted_string string_ltl_spot;
    quoted_string string_ltl_spin;
    quoted_string string_ltl_lbt;
521
    quoted_string string_ltl_wring;
522
523
524
    quoted_string filename_ltl_spot;
    quoted_string filename_ltl_spin;
    quoted_string filename_ltl_lbt;
525
    quoted_string filename_ltl_wring;
526
527
528
    // Run-specific variables
    printable_result_filename output;
  public:
529
530
    using spot::formater::has;

531
532
    translator_runner(spot::bdd_dict& dict)
      : dict(dict)
533
534
535
536
    {
      declare('f', &string_ltl_spot);
      declare('s', &string_ltl_spin);
      declare('l', &string_ltl_lbt);
537
      declare('w', &string_ltl_wring);
538
539
540
      declare('F', &filename_ltl_spot);
      declare('S', &filename_ltl_spin);
      declare('L', &filename_ltl_lbt);
541
      declare('W', &filename_ltl_wring);
542
543
544
      declare('N', &output);
      declare('T', &output);

545
      std::vector<bool> has(256);
546
547
548
      size_t s = translators.size();
      assert(s);
      for (size_t n = 0; n < s; ++n)
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
	{
	  // Check that each translator uses at least one input and
	  // one output.
	  has.clear();
	  scan(translators[n], has);
	  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 "
		  "to pass the formula.", translators[n]);
	  if (!(has['N'] || has['T']))
	    error(2, 0, "no output %%-sequence in '%s'.\n      Use "
		  "one of %%N,%%T to indicate where the automaton is saved.",
		  translators[n]);

	  // Remember the %-sequences used by all translators.
	  prime(translators[n]);
	}
567

568
569
570
571
    }

    void
    string_to_tmp(std::string& str, unsigned n, std::string& tmpname)
572
    {
573
      int fd = create_tmpfile('i', n, tmpname);
574
575
576
577
578
579
      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());
      if (close(fd))
	error(2, errno, "failed to close %s", tmpname.c_str());
580
581
582
      toclean.push_back(tmpname);
    }

583
584
    const std::string&
    formula() const
585
586
587
588
589
590
    {
      // 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;
591
592
      if (!string_ltl_wring.val().empty())
	return string_ltl_wring;
593
594
      if (!string_ltl_lbt.val().empty())
	return string_ltl_lbt;
595
      assert(!"None of the translators need the input formula?");
596
597
598
      return string_ltl_spot;
    }

599
600
    void
    round_formula(const spot::ltl::formula* f, unsigned serial)
601
602
603
604
605
606
607
    {
      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);
608
609
      if (has('w') || has('W'))
	string_ltl_wring = spot::ltl::to_wring_string(f);
610
611
612
613
614
615
      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);
616
617
      if (has('W'))
	string_to_tmp(string_ltl_wring, serial, filename_ltl_wring);
618
619
    }

620
621
    const spot::tgba*
    translate(unsigned int translator_num, char l, statistics_formula* fstats)
622
623
624
625
626
627
    {
      output.reset(translator_num);

      std::ostringstream command;
      format(command, translators[translator_num]);
      toclean.push_back(output.val());
628

629
      assert(output.format != printable_result_filename::None);
630

631
632
633
      std::string cmd = command.str();
      std::cerr << "Running [" << l << translator_num << "]: "
		<< cmd << std::endl;
634
      xtime_t before = gethrxtime();
635
      int es = exec_with_timeout(cmd.c_str());
636
      xtime_t after = gethrxtime();
637
638

      const spot::tgba* res = 0;
639
640
      if (timed_out)
	{
641
642
	  // This is not considered to be a global error.
	  std::cerr << "warning: timeout during execution of command\n";
643
	  ++timeout_count;
644
645
646
	}
      else if (WIFSIGNALED(es))
	{
647
648
	  global_error() << "error: execution terminated by signal "
			 << WTERMSIG(es) << ".\n";
649
650
	}
      else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
651
	{
652
653
	  global_error() << "error: execution returned exit code "
			 << WEXITSTATUS(es) << ".\n";
654
655
656
657
658
659
	}
      else
	{
	  switch (output.format)
	    {
	    case printable_result_filename::Spin:
660
	      {
661
662
663
664
		spot::neverclaim_parse_error_list pel;
		res = spot::neverclaim_parse(output, pel, &dict);
		if (!pel.empty())
		  {
665
666
667
		    std::ostream& err = global_error();
		    err << "error: failed to parse the produced neverclaim.\n";
		    spot::format_neverclaim_parse_errors(err, output, pel);
668
669
670
671
		    delete res;
		    res = 0;
		  }
		break;
672
	      }
673
	    case printable_result_filename::Lbtt:
674
	      {
675
		std::string error;
676
		std::ifstream f(output.val().c_str());
677
678
		if (!f)
		  {
679
680
681
		    global_error() << "Cannot open " << output.val()
				   << std::endl;
		    global_error_flag = true;
682
683
684
		  }
		else
		  {
685
		    res = spot::lbtt_parse(f, error, &dict);
686
		    if (!res)
687
		      global_error() << ("error: failed to parse output in "
688
689
					 "LBTT format: ")
				     << error << std::endl;
690
691
		  }
		break;
692
	      }
693
694
695
	    case printable_result_filename::None:
	      assert(!"unreachable code");
	    }
696
	}
697
      // Compute statistics.
698
      if (res && want_stats)
699
700
701
702
703
704
705
706
707
708
	{
	  statistics* st = &(*fstats)[translator_num];
	  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();
709
	  unsigned c = m.scc_count();
710
711
712
	  st->scc = m.scc_count();
	  st->nondetstates = spot::count_nondet_states(res);
	  st->nondeterministic = st->nondetstates != 0;
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
	  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;
	  else
	    st->terminal_aut = true;
730
731
          double prec = XTIME_PRECISION;
	  st->time = (after - before) / prec;
732
	}
733
      return res;
734
    }
735
  };
736

737
738
739
740
741
742
743
744
745
746
747
  static bool
  is_empty(const spot::tgba* aut)
  {
    spot::emptiness_check* ec = spot::couvreur99(aut);
    spot::emptiness_check_result* res = ec->check();
    delete res;
    delete ec;
    return !res;
  }

  static void
748
  cross_check(const std::vector<spot::scc_map*>& maps, char l, unsigned p)
749
750
  {
    size_t m = maps.size();
751

752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
    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)
770
      {
771
772
	std::ostream& err = global_error();
	err << "error: {";
773
774
775
776
777
778
779
	bool first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && res[i])
	    {
	      if (first)
		first = false;
	      else
780
781
		err << ",";
	      err << l << i;
782
	    }
783
	err << "} disagree with {";
784
785
786
787
788
789
790
	first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && !res[i])
	    {
	      if (first)
		first = false;
	      else
791
792
		err << ",";
	      err << l << i;
793
	    }
794
795
796
797
798
	err << "} when evaluating ";
	if (products > 1)
	  err << "state-space #" << p << "/" << products;
	else
	  err << "the state-space";
799
      }
800
  }
801

802
  typedef std::set<spot::state*, spot::state_ptr_less_than> state_set;
803

804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
  // 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();
	    }
	}
  }
825

826
827
828
829
830
831
832
833
834
835
836
  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;
837
    for (it = s.begin(); it != s.end(); ++it)
838
839
840
      (*it)->destroy();
    return res;
  }
841

842
843
844
845
846
  typedef
  Sgi::hash_set<const spot::ltl::formula*,
		const spot::ptr_hash<const spot::ltl::formula> > fset_t;


847
848
  class processor: public job_processor
  {
849
    spot::bdd_dict dict;
850
    translator_runner runner;
851
    fset_t unique_set;
852
  public:
853
854
855
856
857
    processor()
      : runner(dict)
    {
    }

858
859
860
861
862
863
864
    ~processor()
    {
      fset_t::iterator i = unique_set.begin();
      while (i != unique_set.end())
	(*i++)->destroy();
    }

865
866
867
868
869
870
    int
    process_formula(const spot::ltl::formula* f,
		    const char* filename = 0, int linenum = 0)
    {
      (void) filename;
      (void) linenum;
871
      static unsigned round = 0;
872

873
874
875
876
877
878
879
880
881
882
      // If we need LBT atomic proposition in any of the input or
      // output, relabel the formula.
      if (!f->has_lbt_atomic_props() &&
	  (runner.has('l') || runner.has('L') || runner.has('T')))
	{
	  const spot::ltl::formula* g = spot::ltl::relabel(f, spot::ltl::Pnn);
	  f->destroy();
	  f = g;
	}

883
884
      // ---------- Positive Formula ----------

885
      runner.round_formula(f, round);
886

887
888
889
      // Call formula() before printing anything else, in case it
      // complains.
      std::string fstr = runner.formula();
890
891
892
893
894
895
      if (filename)
	std::cerr << filename << ":";
      if (linenum)
	std::cerr << linenum << ":";
      if (filename || linenum)
	std::cerr << " ";
896
      std::cerr << fstr << "\n";
897

898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
      // Make sure we do not translate the same formula twice.
      if (!allow_dups)
	{
	  if (unique_set.insert(f).second)
	    {
	      f->clone();
	    }
	  else
	    {
	      std::cerr
		<< ("warning: This formula or its negation has already"
		    " been checked.\n         Use --allow-dups if it "
		    "should not be ignored.\n")
		<< std::endl;
	      f->destroy();
	      return 0;
	    }
	}

      size_t m = translators.size();
      std::vector<const spot::tgba*> pos(m);
      std::vector<const spot::tgba*> neg(m);

      unsigned n = vstats.size();
922
      vstats.resize(n + (no_checks ? 1 : 2));
923
      statistics_formula* pstats = &vstats[n];
924
      statistics_formula* nstats = 0;
925
      pstats->resize(m);
926
927
      formulas.push_back(fstr);

928
      for (size_t n = 0; n < m; ++n)
929
930
931
	pos[n] = runner.translate(n, 'P', pstats);

      // ---------- Negative Formula ----------
932

933
934
935
      // The negative formula is only needed when checks are
      // activated.
      if (!no_checks)
936
	{
937
938
	  nstats = &vstats[n + 1];
	  nstats->resize(m);
939

940
941
	  const spot::ltl::formula* nf =
	    spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone());
942

943
944
945
946
947
948
949
950
951
	  if (!allow_dups)
	    {
	      bool res = unique_set.insert(nf->clone()).second;
	      // It is not possible to discover that nf has already been
	      // translated, otherwise that would mean that f had been
	      // translated too and we would have caught it before.
	      assert(res);
	      (void) res;
	    }
952

953
954
	  runner.round_formula(nf, round);
	  formulas.push_back(runner.formula());
955

956
957
958
959
	  for (size_t n = 0; n < m; ++n)
	    neg[n] = runner.translate(n, 'N', nstats);
	  nf->destroy();
	}
960

961
      f->destroy();
962
      cleanup();
963
      ++round;
964

965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
      if (!no_checks)
	{
	  std::cerr << "Performing sanity checks and gathering statistics..."
		    << std::endl;

	  // intersection test
	  for (size_t i = 0; i < m; ++i)
	    if (pos[i])
	      for (size_t j = 0; j < m; ++j)
		if (neg[j])
		  {
		    spot::tgba_product* prod =
		      new spot::tgba_product(pos[i], neg[j]);
		    if (!is_empty(prod))
		      global_error() << "error: P" << i << "*N" << j
				     << " is nonempty\n";
		    delete prod;
		  }
	}
      else
	{
	  std::cerr << "Gathering statistics..." << std::endl;
	}
988

989
      spot::ltl::atomic_prop_set* ap = spot::ltl::atomic_prop_collect(f);
990

991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
      for (unsigned p = 0; p < products; ++p)
	{
	  // build a random state-space.
	  spot::srand(seed);
	  spot::tgba* statespace = spot::random_graph(states, density,
						      ap, &dict);

	  // Products of the state space with the positive automata.
	  std::vector<spot::tgba*> pos_prod(m);
	  // Products of the state space with the negative automata.
	  std::vector<spot::tgba*> neg_prod(m);
	  // Associated SCC maps.
	  std::vector<spot::scc_map*> pos_map(m);
	  std::vector<spot::scc_map*> neg_map(m);
	  for (size_t i = 0; i < m; ++i)
	    if (pos[i])
1007
	      {
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
		spot::tgba* p = new spot::tgba_product(pos[i], statespace);
		pos_prod[i] = p;
		spot::scc_map* sm = new spot::scc_map(p);
		sm->build_map();
		pos_map[i] = sm;

		// Statistics
		if (want_stats)
		  {
		    (*pstats)[i].product_scc += sm->scc_count();
		    spot::tgba_statistics s = spot::stats_reachable(p);
		    (*pstats)[i].product_states += s.states;
		    (*pstats)[i].product_transitions += s.transitions;
		  }
1022
	      }
1023

1024
1025
1026
1027

	  if (!no_checks)
	    for (size_t i = 0; i < m; ++i)
	      if (neg[i])
1028
		{
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
		  spot::tgba* p = new spot::tgba_product(neg[i], statespace);
		  neg_prod[i] = p;
		  spot::scc_map* sm = new spot::scc_map(p);
		  sm->build_map();
		  neg_map[i] = sm;

		  // Statistics
		  if (want_stats)
		    {
		      (*nstats)[i].product_scc += sm->scc_count();
		      spot::tgba_statistics s = spot::stats_reachable(p);
		      (*nstats)[i].product_states += s.states;
		      (*nstats)[i].product_transitions += s.transitions;
		    }
1043
		}
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063

	  if (!no_checks)
	    {
	      // cross-comparison test
	      cross_check(pos_map, 'P', p);
	      cross_check(neg_map, 'N', p);

	      // consistency check
	      for (size_t i = 0; i < m; ++i)
		if (pos_map[i] && neg_map[i] &&
		    !(consistency_check(pos_map[i], neg_map[i], statespace)))
		  {
		    global_error() << "error: inconsistency between P" << i
				   << " and N" << i;
		    if (products > 1)
		      global_error() << " for state-space #" << p
				     << "/" << products << "\n";
		    else
		      global_error() << "\n";
		  }
1064
	    }
1065

1066
	  // Cleanup.
1067

1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
	  if (!no_checks)
	    for (size_t i = 0; i < m; ++i)
	      {
		delete neg_map[i];
		delete neg_prod[i];
		if (want_stats)
		  {
		    (*nstats)[i].product_scc /= products;
		    (*nstats)[i].product_states /= products;
		    (*nstats)[i].product_transitions /= products;
		  }
	      }
1080
	  for (size_t i = 0; i < m; ++i)
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
	    {
	      delete pos_map[i];
	      delete pos_prod[i];
	      if (want_stats)
		{
		  (*pstats)[i].product_scc /= products;
		  (*pstats)[i].product_states /= products;
		  (*pstats)[i].product_transitions /= products;
		}
	    }
	  delete statespace;
	  ++seed;
1093
	}
1094
1095
      std::cerr << std::endl;
      delete ap;
1096

1097
      if (!no_checks)
1098
1099
1100
1101
	for (size_t i = 0; i < m; ++i)
	  delete neg[i];
      for (size_t i = 0; i < m; ++i)
	delete pos[i];
1102
1103
1104

      // Shall we stop processing formulas now?
      abort_run = global_error_flag && stop_on_error;
1105
1106
1107
1108
1109
      return 0;
    }
  };
}

1110
static void
1111
print_stats_csv(const char* filename)
1112
{
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
  std::ofstream* outfile = 0;
  std::ostream* out;
  if (!strncmp(filename, "-", 2))
    {
      out = &std::cout;
    }
  else
    {
      out = outfile = new std::ofstream(filename);
      if (!outfile)
	error(2, errno, "cannot open '%s'", filename);
    }

  unsigned ntrans = translators.size();
1127
  unsigned rounds = vstats.size();
1128
  assert(rounds == formulas.size());
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163

  *out << "\"formula\", \"tool\", ";
  statistics::fields(*out);
  *out << "\n";
  for (unsigned r = 0; r < rounds; ++r)
    for (unsigned t = 0; t < ntrans; ++t)
      if (vstats[r][t].ok)
	{
	  *out << "\"";
	  spot::escape_str(*out, formulas[r]);
	  *out << "\", \"";
	  spot::escape_str(*out, translators[t]);
	  *out << "\", ";
	  vstats[r][t].to_csv(*out);
	  *out << "\n";
	}
  delete outfile;
}

static void
print_stats_json(const char* filename)
{
  std::ofstream* outfile = 0;
  std::ostream* out;
  if (!strncmp(filename, "-", 2))
    {
      out = &std::cout;
    }
  else
    {
      out = outfile = new std::ofstream(filename);
      if (!outfile)
	error(2, errno, "cannot open '%s'", filename);
    }

1164
  unsigned ntrans = translators.size();
1165
  unsigned rounds = vstats.size();
1166
  assert(rounds == formulas.size());
1167

Elie Abi Saad's avatar
Elie Abi Saad committed
1168
  *out << "{\n  \"tool\": [\n    \"";
1169
  spot::escape_str(*out, translators[0]);
1170
  for (unsigned t = 1; t < ntrans; ++t)
1171
1172
1173
1174
    {
      *out << "\",\n    \"";
      spot::escape_str(*out, translators[t]);
    }
Elie Abi Saad's avatar
Elie Abi Saad committed
1175
  *out << "\"\n  ],\n  \"formula\": [\n    \"";
1176
  spot::escape_str(*out, formulas[0]);
1177
  for (unsigned r = 1; r < rounds; ++r)
1178
1179
1180
1181
    {
      *out << "\",\n    \"";
      spot::escape_str(*out, formulas[r]);
    }
Elie Abi Saad's avatar
Elie Abi Saad committed
1182
  *out << ("\"\n  ],\n  \"fields\":  [\n  \"formula\", \"tool\",");
1183
  statistics::fields(*out);
Elie Abi Saad's avatar
Elie Abi Saad committed
1184
1185
  *out << "\n  ],\n  \"inputs\":  [ 0, 1 ],";
  *out << "\n  \"results\": [";
1186
1187
1188
1189
1190
1191
  bool notfirst = false;
  for (unsigned r = 0; r < rounds; ++r)
    for (unsigned t = 0; t < ntrans; ++t)
      if (vstats[r][t].ok)
	{
	  if (notfirst)
1192
	    *out << ",";
1193
	  notfirst = true;
1194
1195
1196
	  *out << "\n    [ " << r << ", " << t << ", ";
	  vstats[r][t].to_csv(*out);
	  *out << " ]";
1197
	}
1198
1199
1200
  *out << "\n  ]\n}\n";

  delete outfile;
1201
}
1202
1203
1204
1205
1206
1207
1208
1209
1210

int
main(int argc, char** argv)
{
  setup(argv);

  const argp ap = { options, parse_opt, "[COMMANDFMT...]",
		    argp_program_doc, children, 0, 0 };

1211
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
1212
1213
1214
1215
1216
1217
1218
1219
1220
    exit(err);

  if (jobs.empty())
    jobs.push_back(job("-", 1));

  if (translators.empty())
    error(2, 0, "No translator to run?  Run '%s --help' for usage.",
	  program_name);

1221
1222
  setup_sig_handler();

1223
1224
1225
  processor p;
  if (p.run())
    return 2;
1226

1227
1228
1229
1230
1231
1232
1233
  if (formulas.empty())
    {
      error(2, 0, "no formula to translate");
    }
  else
    {
      if (global_error_flag)
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
	{
	  std::cerr
	    << ("error: some error was detected during the above runs,\n"
		"       please search for 'error:' messages in the above "
		"trace.")
	    << std::endl;
	  if (timeout_count == 1)
	    std::cerr << "Additionally, 1 timeout occurred." << std::endl;
	  else if (timeout_count > 1)
	    std::cerr << "Additionally, "
		      << timeout_count << " timeouts occurred." << std::endl;
	}
      else if (timeout_count == 0)
	std::cerr << "No problem detected." << std::endl;
      else if (timeout_count == 1)
	std::cerr << "1 timeout, but no other problem detected." << std::endl;
      else
	std::cerr << timeout_count
		  << " timeouts, but no other problem detected." << std::endl;
1253
1254
1255
1256
1257
1258
1259
    }

  if (json_output)
    print_stats_json(json_output);
  if (csv_output)
    print_stats_csv(csv_output);

1260
  return global_error_flag;
1261
}