ltlcross.cc 30.3 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
88
89
90
91
92
93

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

const struct argp_child children[] =
  {
    { &finput_argp, 0, 0, 1 },
143
    { &misc_argp, 0, 0, -1 },
144
145
146
147
148
    { 0, 0, 0, 0 }
  };

unsigned states = 200;
float density = 0.1;
149
unsigned timeout = 0;
150
151
152
const char* json_output = 0;
const char* csv_output = 0;
bool want_stats = false;
153
bool allow_dups = false;
154
bool no_checks = false;
155
bool stop_on_error = false;
156
int seed = 0;
157

158
std::vector<char*> translators;
159
160
161
162
163
164
165
166
bool global_error_flag = false;

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

168
169
170
171
172
173
174
175
struct statistics
{
  bool ok;
  unsigned states;
  unsigned edges;
  unsigned transitions;
  unsigned acc;
  unsigned scc;
176
177
178
179
  unsigned nonacc_scc;
  unsigned terminal_scc;
  unsigned weak_scc;
  unsigned strong_scc;
180
181
  unsigned nondetstates;
  bool nondeterministic;
182
183
184
  bool terminal_aut;
  bool weak_aut;
  bool strong_aut;
185
  double time;
186
187
188
189
190
191
192
  unsigned product_states;
  unsigned product_transitions;
  unsigned product_scc;

  static void
  fields(std::ostream& os)
  {
193
194
195
196
197
    os << (" \"states\","
	   " \"edges\","
	   " \"transitions\","
	   " \"acc\","
	   " \"scc\","
198
199
200
201
202
203
204
205
206
	   " \"nonacc_scc\","
	   " \"terminal_scc\","
	   " \"weak_scc\","
	   " \"strong_scc\","
	   " \"nondet_states\","
	   " \"nondet_aut\","
	   " \"terminal_aut\","
	   " \"weak_aut\","
	   " \"strong_aut\","
207
208
209
210
	   " \"time\","
	   " \"product_states\","
	   " \"product_transitions\","
	   " \"product_scc\"");
211
212
213
214
215
216
217
218
219
220
  }

  void
  to_csv(std::ostream& os)
  {
    os << states << ", "
       << edges << ", "
       << transitions << ", "
       << acc << ", "
       << scc << ", "
221
222
223
224
       << nonacc_scc << ", "
       << terminal_scc << ", "
       << weak_scc << ", "
       << strong_scc << ", "
225
226
       << nondetstates << ", "
       << nondeterministic << ", "
227
228
229
       << terminal_aut << ", "
       << weak_aut << ", "
       << strong_aut << ", "
230
       << time << ", "
231
232
233
234
235
236
237
238
239
240
241
       << 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;

242
243
244
245
246
247
248
249
250
251
252
// 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();
}

253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
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
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;
303
304
    case 'T':
      timeout = to_pos_int(arg);
305
306
307
308
#if !ENABLE_TIMEOUT
      std::cerr << "warning: setting a timeout is not supported "
		<< "on your platform" << std::endl;
#endif
309
      break;
310
311
312
313
    case OPT_CSV:
      want_stats = true;
      csv_output = arg ? arg : "-";
      break;
314
315
316
    case OPT_DENSITY:
      density = to_probability(arg);
      break;
317
318
319
    case OPT_DUPS:
      allow_dups = true;
      break;
320
321
322
323
    case OPT_JSON:
      want_stats = true;
      json_output = arg ? arg : "-";
      break;
324
325
326
    case OPT_NOCHECKS:
      no_checks = true;
      break;
327
328
329
    case OPT_SEED:
      seed = to_pos_int(arg);
      break;
330
331
332
    case OPT_STATES:
      states = to_pos_int(arg);
      break;
333
334
335
    case OPT_STOP_ERR:
      stop_on_error = true;
      break;
336
337
338
339
340
341
342
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

static int
343
create_tmpfile(char c, unsigned int n, std::string& name)
344
345
{
  char tmpname[30];
346
  snprintf(tmpname, sizeof tmpname, "lck-%c%u-XXXXXX", c, n);
347
348
349
350
351
352
353
  int fd = mkstemp(tmpname);
  if (fd == -1)
    error(2, errno, "failed to create a temporary file");
  name = tmpname;
  return fd;
}

354
355

static volatile bool timed_out = false;
356
unsigned timeout_count = 0;
357

358
359
#if ENABLE_TIMEOUT
static volatile int alarm_on = 0;
360
361
362
363
364
365
366
367
368
369
370
371
372
373
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.
374
	  kill(-child_pid, SIGTERM);
375
376
377
378
379
380
381
	  // 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.
382
	  kill(-child_pid, SIGKILL);
383
384
385
386
387
	}
    }
  else
    {
      // forward signal
388
      kill(-child_pid, sig);
389
390
      // cleanup files
      cleanup();
391
392
      // and die verbosely
      error(2, 0, "received signal %d", sig);
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
    }
}

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'");
427
428
      // never reached
      return -1;
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
    }
  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;
}
446
447
448
449
#else // !ENABLE_TIMEOUT
#define exec_with_timeout(cmd) system(cmd)
#define setup_sig_handler() while (0);
#endif // !ENABLE_TIMEOUT
450

451
namespace
452
{
453
454
455
  struct quoted_string: public spot::printable_value<std::string>
  {
    using spot::printable_value<std::string>::operator=;
456

457
458
459
460
461
462
463
464
    void
    print(std::ostream& os, const char* pos) const
    {
      os << '\'';
      this->spot::printable_value<std::string>::print(os, pos);
      os << '\'';
    }
  };
465

466
467
468
469
470
  struct printable_result_filename: public spot::printable_value<std::string>
  {
    unsigned translator_num;
    enum output_format { None, Spin, Lbtt };
    mutable output_format format;
471

472
473
474
475
476
477
    void reset(unsigned n)
    {
      val_.clear();
      translator_num = n;
      format = None;
    }
478

479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
    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_ << '\'';
    }
  };
494

495
496
497
  class translator_runner: protected spot::formater
  {
  private:
498
    spot::bdd_dict& dict;
499
500
501
502
    // Round-specific variables
    quoted_string string_ltl_spot;
    quoted_string string_ltl_spin;
    quoted_string string_ltl_lbt;
503
    quoted_string string_ltl_wring;
504
505
506
    quoted_string filename_ltl_spot;
    quoted_string filename_ltl_spin;
    quoted_string filename_ltl_lbt;
507
    quoted_string filename_ltl_wring;
508
509
510
    // Run-specific variables
    printable_result_filename output;
  public:
511
512
    using spot::formater::has;

513
514
    translator_runner(spot::bdd_dict& dict)
      : dict(dict)
515
516
517
518
    {
      declare('f', &string_ltl_spot);
      declare('s', &string_ltl_spin);
      declare('l', &string_ltl_lbt);
519
      declare('w', &string_ltl_wring);
520
521
522
      declare('F', &filename_ltl_spot);
      declare('S', &filename_ltl_spin);
      declare('L', &filename_ltl_lbt);
523
      declare('W', &filename_ltl_wring);
524
525
526
      declare('N', &output);
      declare('T', &output);

527
      std::vector<bool> has(256);
528
529
530
      size_t s = translators.size();
      assert(s);
      for (size_t n = 0; n < s; ++n)
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
	{
	  // 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]);
	}
549

550
551
552
553
    }

    void
    string_to_tmp(std::string& str, unsigned n, std::string& tmpname)
554
    {
555
      int fd = create_tmpfile('i', n, tmpname);
556
557
558
559
560
561
      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());
562
563
564
      toclean.push_back(tmpname);
    }

565
566
    const std::string&
    formula() const
567
568
569
570
571
572
    {
      // 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;
573
574
      if (!string_ltl_wring.val().empty())
	return string_ltl_wring;
575
576
      if (!string_ltl_lbt.val().empty())
	return string_ltl_lbt;
577
      assert(!"None of the translators need the input formula?");
578
579
580
      return string_ltl_spot;
    }

581
582
    void
    round_formula(const spot::ltl::formula* f, unsigned serial)
583
584
585
586
587
588
589
    {
      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);
590
591
      if (has('w') || has('W'))
	string_ltl_wring = spot::ltl::to_wring_string(f);
592
593
594
595
596
597
      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);
598
599
      if (has('W'))
	string_to_tmp(string_ltl_wring, serial, filename_ltl_wring);
600
601
    }

602
603
    const spot::tgba*
    translate(unsigned int translator_num, char l, statistics_formula* fstats)
604
605
606
607
608
609
    {
      output.reset(translator_num);

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

611
      assert(output.format != printable_result_filename::None);
612

613
614
615
      std::string cmd = command.str();
      std::cerr << "Running [" << l << translator_num << "]: "
		<< cmd << std::endl;
616
      xtime_t before = gethrxtime();
617
      int es = exec_with_timeout(cmd.c_str());
618
      xtime_t after = gethrxtime();
619
620

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

719
720
721
722
723
724
725
726
727
728
729
730
731
732
  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
  cross_check(const std::vector<spot::scc_map*>& maps, char l)
  {
    size_t m = maps.size();
733

734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
    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)
752
      {
753
754
	std::ostream& err = global_error();
	err << "error: {";
755
756
757
758
759
760
761
	bool first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && res[i])
	    {
	      if (first)
		first = false;
	      else
762
763
		err << ",";
	      err << l << i;
764
	    }
765
	err << "} disagree with {";
766
767
768
769
770
771
772
	first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && !res[i])
	    {
	      if (first)
		first = false;
	      else
773
774
		err << ",";
	      err << l << i;
775
	    }
776
	err << "} when evaluating the state-space\n";
777
      }
778
  }
779

780
  typedef std::set<spot::state*, spot::state_ptr_less_than> state_set;
781

782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
  // 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();
	    }
	}
  }
803

804
805
806
807
808
809
810
811
812
813
814
  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;
815
    for (it = s.begin(); it != s.end(); ++it)
816
817
818
      (*it)->destroy();
    return res;
  }
819

820
821
822
823
824
  typedef
  Sgi::hash_set<const spot::ltl::formula*,
		const spot::ptr_hash<const spot::ltl::formula> > fset_t;


825
826
  class processor: public job_processor
  {
827
    spot::bdd_dict dict;
828
    translator_runner runner;
829
    fset_t unique_set;
830
  public:
831
832
833
834
835
    processor()
      : runner(dict)
    {
    }

836
837
838
839
840
841
842
    ~processor()
    {
      fset_t::iterator i = unique_set.begin();
      while (i != unique_set.end())
	(*i++)->destroy();
    }

843
844
845
846
847
848
    int
    process_formula(const spot::ltl::formula* f,
		    const char* filename = 0, int linenum = 0)
    {
      (void) filename;
      (void) linenum;
849
      static unsigned round = 0;
850

851
852
853
854
855
856
857
858
859
860
      // 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;
	}

861
862
      // ---------- Positive Formula ----------

863
      runner.round_formula(f, round);
864

865
866
867
      // Call formula() before printing anything else, in case it
      // complains.
      std::string fstr = runner.formula();
868
869
870
871
872
873
      if (filename)
	std::cerr << filename << ":";
      if (linenum)
	std::cerr << linenum << ":";
      if (filename || linenum)
	std::cerr << " ";
874
      std::cerr << fstr << "\n";
875

876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
      // 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();
901
      vstats.resize(n + (no_checks ? 1 : 2));
902
      statistics_formula* pstats = &vstats[n];
903
      statistics_formula* nstats = 0;
904
      pstats->resize(m);
905
906
      formulas.push_back(fstr);

907
      for (size_t n = 0; n < m; ++n)
908
909
910
	pos[n] = runner.translate(n, 'P', pstats);

      // ---------- Negative Formula ----------
911

912
913
914
      // The negative formula is only needed when checks are
      // activated.
      if (!no_checks)
915
	{
916
917
	  nstats = &vstats[n + 1];
	  nstats->resize(m);
918

919
920
	  const spot::ltl::formula* nf =
	    spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone());
921

922
923
924
925
926
927
928
929
930
	  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;
	    }
931

932
933
	  runner.round_formula(nf, round);
	  formulas.push_back(runner.formula());
934

935
936
937
938
	  for (size_t n = 0; n < m; ++n)
	    neg[n] = runner.translate(n, 'N', nstats);
	  nf->destroy();
	}
939

940
      f->destroy();
941
      cleanup();
942
      ++round;
943

944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
      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;
	}
967
968

      // build products with a random state-space.
969
      spot::ltl::atomic_prop_set* ap = spot::ltl::atomic_prop_collect(f);
970
      spot::srand(seed);
971
      spot::tgba* statespace = spot::random_graph(states, density, ap, &dict);
972
      delete ap;
973
974
975
976
977
978
979
980
981
982
983
984
985

      std::vector<spot::tgba*> pos_prod(m);
      std::vector<spot::tgba*> neg_prod(m);
      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])
	  {
	    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;
986
987

	    // Statistics
988
989
990
991
992
993
994
	    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;
	      }
995
	  }
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
      if (!no_checks)
	for (size_t i = 0; i < m; ++i)
	  if (neg[i])
	    {
	      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;
		}
	    }
1015

1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
      if (!no_checks)
	{
	  // cross-comparison test
	  cross_check(pos_map, 'P');
	  cross_check(neg_map, 'N');

	  // 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 << "\n";
	}
1029
1030
1031

      // Cleanup.

1032
1033
      if (!no_checks)
	for (size_t n = 0; n < m; ++n)
1034
1035
1036
	{
	  delete neg_map[n];
	  delete neg_prod[n];
1037
	  delete neg[n];
1038
1039
1040
	}
      for (size_t n = 0; n < m; ++n)
	{
1041
1042
	  delete pos_map[n];
	  delete pos_prod[n];
1043
1044
	  delete pos[n];
	}
1045
      delete statespace;
1046
      ++seed;
1047
      std::cerr << std::endl;
1048
1049
1050

      // Shall we stop processing formulas now?
      abort_run = global_error_flag && stop_on_error;
1051
1052
1053
1054
1055
      return 0;
    }
  };
}

1056
static void
1057
print_stats_csv(const char* filename)
1058
{
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
  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();
1073
  unsigned rounds = vstats.size();
1074
  assert(rounds == formulas.size());
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109

  *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);
    }

1110
  unsigned ntrans = translators.size();
1111
  unsigned rounds = vstats.size();
1112
  assert(rounds == formulas.size());
1113

Elie Abi Saad's avatar
Elie Abi Saad committed
1114
  *out << "{\n  \"tool\": [\n    \"";
1115
  spot::escape_str(*out, translators[0]);
1116
  for (unsigned t = 1; t < ntrans; ++t)
1117
1118
1119
1120
    {
      *out << "\",\n    \"";
      spot::escape_str(*out, translators[t]);
    }
Elie Abi Saad's avatar
Elie Abi Saad committed
1121
  *out << "\"\n  ],\n  \"formula\": [\n    \"";
1122
  spot::escape_str(*out, formulas[0]);
1123
  for (unsigned r = 1; r < rounds; ++r)
1124
1125
1126
1127
    {
      *out << "\",\n    \"";
      spot::escape_str(*out, formulas[r]);
    }
Elie Abi Saad's avatar
Elie Abi Saad committed
1128
  *out << ("\"\n  ],\n  \"fields\":  [\n  \"formula\", \"tool\",");
1129
  statistics::fields(*out);
Elie Abi Saad's avatar
Elie Abi Saad committed
1130
1131
  *out << "\n  ],\n  \"inputs\":  [ 0, 1 ],";
  *out << "\n  \"results\": [";
1132
1133
1134
1135
1136
1137
  bool notfirst = false;
  for (unsigned r = 0; r < rounds; ++r)
    for (unsigned t = 0; t < ntrans; ++t)
      if (vstats[r][t].ok)
	{
	  if (notfirst)
1138
	    *out << ",";
1139
	  notfirst = true;
1140
1141
1142
	  *out << "\n    [ " << r << ", " << t << ", ";
	  vstats[r][t].to_csv(*out);
	  *out << " ]";
1143
	}
1144
1145
1146
  *out << "\n  ]\n}\n";

  delete outfile;
1147
}
1148
1149
1150
1151
1152
1153
1154
1155
1156

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

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

1157
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
1158
1159
1160
1161
1162
1163
1164
1165
1166
    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);

1167
1168
  setup_sig_handler();

1169
1170
1171
  processor p;
  if (p.run())
    return 2;
1172

1173
1174
1175
1176
1177
1178
1179
  if (formulas.empty())
    {
      error(2, 0, "no formula to translate");
    }
  else
    {
      if (global_error_flag)
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
	{
	  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;
1199
1200
1201
1202
1203
1204
1205
    }

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

1206
  return global_error_flag;
1207
}