ltlcross.cc 30 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

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

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


#define OPT_STATES 1
#define OPT_DENSITY 2
80
81
#define OPT_JSON 3
#define OPT_CSV 4
82
#define OPT_DUPS 5
83
#define OPT_NOCHECKS 6
84
#define OPT_STOP_ERR 7
85
86
87
88
89
90
91

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

const struct argp_child children[] =
  {
    { &finput_argp, 0, 0, 1 },
139
    { &misc_argp, 0, 0, -1 },
140
141
142
143
144
    { 0, 0, 0, 0 }
  };

unsigned states = 200;
float density = 0.1;
145
unsigned timeout = 0;
146
147
148
const char* json_output = 0;
const char* csv_output = 0;
bool want_stats = false;
149
bool allow_dups = false;
150
bool no_checks = false;
151
bool stop_on_error = false;
152

153
std::vector<char*> translators;
154
155
156
157
158
159
160
161
bool global_error_flag = false;

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

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

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

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

237
238
239
240
241
242
243
244
245
246
247
// 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();
}

248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
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;
298
299
    case 'T':
      timeout = to_pos_int(arg);
300
301
302
303
#if !ENABLE_TIMEOUT
      std::cerr << "warning: setting a timeout is not supported "
		<< "on your platform" << std::endl;
#endif
304
      break;
305
306
307
308
    case OPT_CSV:
      want_stats = true;
      csv_output = arg ? arg : "-";
      break;
309
310
311
    case OPT_DENSITY:
      density = to_probability(arg);
      break;
312
313
314
    case OPT_DUPS:
      allow_dups = true;
      break;
315
316
317
318
    case OPT_JSON:
      want_stats = true;
      json_output = arg ? arg : "-";
      break;
319
320
321
    case OPT_NOCHECKS:
      no_checks = true;
      break;
322
323
324
    case OPT_STATES:
      states = to_pos_int(arg);
      break;
325
326
327
    case OPT_STOP_ERR:
      stop_on_error = true;
      break;
328
329
330
331
332
333
334
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

static int
335
create_tmpfile(char c, unsigned int n, std::string& name)
336
337
{
  char tmpname[30];
338
  snprintf(tmpname, sizeof tmpname, "lck-%c%u-XXXXXX", c, n);
339
340
341
342
343
344
345
  int fd = mkstemp(tmpname);
  if (fd == -1)
    error(2, errno, "failed to create a temporary file");
  name = tmpname;
  return fd;
}

346
347

static volatile bool timed_out = false;
348
unsigned timeout_count = 0;
349

350
351
#if ENABLE_TIMEOUT
static volatile int alarm_on = 0;
352
353
354
355
356
357
358
359
360
361
362
363
364
365
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.
366
	  kill(-child_pid, SIGTERM);
367
368
369
370
371
372
373
	  // 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.
374
	  kill(-child_pid, SIGKILL);
375
376
377
378
379
	}
    }
  else
    {
      // forward signal
380
      kill(-child_pid, sig);
381
382
      // cleanup files
      cleanup();
383
384
      // and die verbosely
      error(2, 0, "received signal %d", sig);
385
386
387
388
389
390
391
392
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
    }
}

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'");
419
420
      // never reached
      return -1;
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
    }
  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;
}
438
439
440
441
#else // !ENABLE_TIMEOUT
#define exec_with_timeout(cmd) system(cmd)
#define setup_sig_handler() while (0);
#endif // !ENABLE_TIMEOUT
442

443
namespace
444
{
445
446
447
  struct quoted_string: public spot::printable_value<std::string>
  {
    using spot::printable_value<std::string>::operator=;
448

449
450
451
452
453
454
455
456
    void
    print(std::ostream& os, const char* pos) const
    {
      os << '\'';
      this->spot::printable_value<std::string>::print(os, pos);
      os << '\'';
    }
  };
457

458
459
460
461
462
  struct printable_result_filename: public spot::printable_value<std::string>
  {
    unsigned translator_num;
    enum output_format { None, Spin, Lbtt };
    mutable output_format format;
463

464
465
466
467
468
469
    void reset(unsigned n)
    {
      val_.clear();
      translator_num = n;
      format = None;
    }
470

471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
    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_ << '\'';
    }
  };
486

487
488
489
  class translator_runner: protected spot::formater
  {
  private:
490
    spot::bdd_dict& dict;
491
492
493
494
    // Round-specific variables
    quoted_string string_ltl_spot;
    quoted_string string_ltl_spin;
    quoted_string string_ltl_lbt;
495
    quoted_string string_ltl_wring;
496
497
498
    quoted_string filename_ltl_spot;
    quoted_string filename_ltl_spin;
    quoted_string filename_ltl_lbt;
499
    quoted_string filename_ltl_wring;
500
501
502
    // Run-specific variables
    printable_result_filename output;
  public:
503
504
    using spot::formater::has;

505
506
    translator_runner(spot::bdd_dict& dict)
      : dict(dict)
507
508
509
510
    {
      declare('f', &string_ltl_spot);
      declare('s', &string_ltl_spin);
      declare('l', &string_ltl_lbt);
511
      declare('w', &string_ltl_wring);
512
513
514
      declare('F', &filename_ltl_spot);
      declare('S', &filename_ltl_spin);
      declare('L', &filename_ltl_lbt);
515
      declare('W', &filename_ltl_wring);
516
517
518
      declare('N', &output);
      declare('T', &output);

519
      std::vector<bool> has(256);
520
521
522
      size_t s = translators.size();
      assert(s);
      for (size_t n = 0; n < s; ++n)
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
	{
	  // 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]);
	}
541

542
543
544
545
    }

    void
    string_to_tmp(std::string& str, unsigned n, std::string& tmpname)
546
    {
547
      int fd = create_tmpfile('i', n, tmpname);
548
549
550
551
552
553
      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());
554
555
556
      toclean.push_back(tmpname);
    }

557
558
    const std::string&
    formula() const
559
560
561
562
563
564
    {
      // 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;
565
566
      if (!string_ltl_wring.val().empty())
	return string_ltl_wring;
567
568
      if (!string_ltl_lbt.val().empty())
	return string_ltl_lbt;
569
      assert(!"None of the translators need the input formula?");
570
571
572
      return string_ltl_spot;
    }

573
574
    void
    round_formula(const spot::ltl::formula* f, unsigned serial)
575
576
577
578
579
580
581
    {
      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);
582
583
      if (has('w') || has('W'))
	string_ltl_wring = spot::ltl::to_wring_string(f);
584
585
586
587
588
589
      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);
590
591
      if (has('W'))
	string_to_tmp(string_ltl_wring, serial, filename_ltl_wring);
592
593
    }

594
595
    const spot::tgba*
    translate(unsigned int translator_num, char l, statistics_formula* fstats)
596
597
598
599
600
601
    {
      output.reset(translator_num);

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

603
      assert(output.format != printable_result_filename::None);
604

605
606
607
      std::string cmd = command.str();
      std::cerr << "Running [" << l << translator_num << "]: "
		<< cmd << std::endl;
608
      xtime_t before = gethrxtime();
609
      int es = exec_with_timeout(cmd.c_str());
610
      xtime_t after = gethrxtime();
611
612

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

711
712
713
714
715
716
717
718
719
720
721
722
723
724
  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();
725

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

772
  typedef std::set<spot::state*, spot::state_ptr_less_than> state_set;
773

774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
  // 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();
	    }
	}
  }
795

796
797
798
799
800
801
802
803
804
805
806
  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;
807
    for (it = s.begin(); it != s.end(); ++it)
808
809
810
      (*it)->destroy();
    return res;
  }
811

812
813
814
815
816
  typedef
  Sgi::hash_set<const spot::ltl::formula*,
		const spot::ptr_hash<const spot::ltl::formula> > fset_t;


817
818
  class processor: public job_processor
  {
819
    spot::bdd_dict dict;
820
    translator_runner runner;
821
    fset_t unique_set;
822
  public:
823
824
825
826
827
    processor()
      : runner(dict)
    {
    }

828
829
830
831
832
833
834
    ~processor()
    {
      fset_t::iterator i = unique_set.begin();
      while (i != unique_set.end())
	(*i++)->destroy();
    }

835
836
837
838
839
840
    int
    process_formula(const spot::ltl::formula* f,
		    const char* filename = 0, int linenum = 0)
    {
      (void) filename;
      (void) linenum;
841
      static unsigned round = 0;
842

843
844
845
846
847
848
849
850
851
852
      // 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;
	}

853
854
      // ---------- Positive Formula ----------

855
      runner.round_formula(f, round);
856

857
858
859
      // Call formula() before printing anything else, in case it
      // complains.
      std::string fstr = runner.formula();
860
861
862
863
864
865
      if (filename)
	std::cerr << filename << ":";
      if (linenum)
	std::cerr << linenum << ":";
      if (filename || linenum)
	std::cerr << " ";
866
      std::cerr << fstr << "\n";
867

868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
      // 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();
893
      vstats.resize(n + (no_checks ? 1 : 2));
894
      statistics_formula* pstats = &vstats[n];
895
      statistics_formula* nstats = 0;
896
      pstats->resize(m);
897
898
      formulas.push_back(fstr);

899
      for (size_t n = 0; n < m; ++n)
900
901
902
	pos[n] = runner.translate(n, 'P', pstats);

      // ---------- Negative Formula ----------
903

904
905
906
      // The negative formula is only needed when checks are
      // activated.
      if (!no_checks)
907
	{
908
909
	  nstats = &vstats[n + 1];
	  nstats->resize(m);
910

911
912
	  const spot::ltl::formula* nf =
	    spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone());
913

914
915
916
917
918
919
920
921
922
	  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;
	    }
923

924
925
	  runner.round_formula(nf, round);
	  formulas.push_back(runner.formula());
926

927
928
929
930
	  for (size_t n = 0; n < m; ++n)
	    neg[n] = runner.translate(n, 'N', nstats);
	  nf->destroy();
	}
931

932
      f->destroy();
933
      cleanup();
934
      ++round;
935

936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
      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;
	}
959
960

      // build products with a random state-space.
961
      spot::ltl::atomic_prop_set* ap = spot::ltl::atomic_prop_collect(f);
962
      spot::tgba* statespace = spot::random_graph(states, density, ap, &dict);
963
      delete ap;
964
965
966
967
968
969
970
971
972
973
974
975
976

      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;
977
978

	    // Statistics
979
980
981
982
983
984
985
	    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;
	      }
986
	  }
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
      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;
		}
	    }
1006

1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
      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";
	}
1020
1021
1022

      // Cleanup.

1023
1024
      if (!no_checks)
	for (size_t n = 0; n < m; ++n)
1025
1026
1027
	{
	  delete neg_map[n];
	  delete neg_prod[n];
1028
	  delete neg[n];
1029
1030
1031
	}
      for (size_t n = 0; n < m; ++n)
	{
1032
1033
	  delete pos_map[n];
	  delete pos_prod[n];
1034
1035
	  delete pos[n];
	}
1036
      delete statespace;
1037
      std::cerr << std::endl;
1038
1039
1040

      // Shall we stop processing formulas now?
      abort_run = global_error_flag && stop_on_error;
1041
1042
1043
1044
1045
      return 0;
    }
  };
}

1046
static void
1047
print_stats_csv(const char* filename)
1048
{
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
  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();
1063
  unsigned rounds = vstats.size();
1064
  assert(rounds == formulas.size());
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
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

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

1100
  unsigned ntrans = translators.size();
1101
  unsigned rounds = vstats.size();
1102
  assert(rounds == formulas.size());
1103

Elie Abi Saad's avatar
Elie Abi Saad committed
1104
  *out << "{\n  \"tool\": [\n    \"";
1105
  spot::escape_str(*out, translators[0]);
1106
  for (unsigned t = 1; t < ntrans; ++t)
1107
1108
1109
1110
    {
      *out << "\",\n    \"";
      spot::escape_str(*out, translators[t]);
    }
Elie Abi Saad's avatar
Elie Abi Saad committed
1111
  *out << "\"\n  ],\n  \"formula\": [\n    \"";
1112
  spot::escape_str(*out, formulas[0]);
1113
  for (unsigned r = 1; r < rounds; ++r)
1114
1115
1116
1117
    {
      *out << "\",\n    \"";
      spot::escape_str(*out, formulas[r]);
    }
Elie Abi Saad's avatar
Elie Abi Saad committed
1118
  *out << ("\"\n  ],\n  \"fields\":  [\n  \"formula\", \"tool\",");
1119
  statistics::fields(*out);
Elie Abi Saad's avatar
Elie Abi Saad committed
1120
1121
  *out << "\n  ],\n  \"inputs\":  [ 0, 1 ],";
  *out << "\n  \"results\": [";
1122
1123
1124
1125
1126
1127
  bool notfirst = false;
  for (unsigned r = 0; r < rounds; ++r)
    for (unsigned t = 0; t < ntrans; ++t)
      if (vstats[r][t].ok)
	{
	  if (notfirst)
1128
	    *out << ",";
1129
	  notfirst = true;
1130
1131
1132
	  *out << "\n    [ " << r << ", " << t << ", ";
	  vstats[r][t].to_csv(*out);
	  *out << " ]";
1133
	}
1134
1135
1136
  *out << "\n  ]\n}\n";

  delete outfile;
1137
}
1138
1139
1140
1141
1142
1143
1144
1145
1146

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

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

1147
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
1148
1149
1150
1151
1152
1153
1154
1155
1156
    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);

1157
1158
  setup_sig_handler();

1159
1160
1161
  processor p;
  if (p.run())
    return 2;
1162

1163
1164
1165
1166
1167
1168
1169
  if (formulas.empty())
    {
      error(2, 0, "no formula to translate");
    }
  else
    {
      if (global_error_flag)
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
	{
	  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;
1189
1190
1191
1192
1193
1194
1195
    }

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

1196
  return global_error_flag;
1197
}