ltlcheck.cc 27.4 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
//
// 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 "misc/formater.hh"
52
53
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/isdet.hh"
54
#include "misc/escape.hh"
55
#include "misc/hash.hh"
56

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

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


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

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

const struct argp_child children[] =
  {
    { &finput_argp, 0, 0, 1 },
134
    { &misc_argp, 0, 0, -1 },
135
136
137
138
139
    { 0, 0, 0, 0 }
  };

unsigned states = 200;
float density = 0.1;
140
unsigned timeout = 0;
141
142
143
const char* json_output = 0;
const char* csv_output = 0;
bool want_stats = false;
144
bool allow_dups = false;
145
bool no_checks = false;
146

147
std::vector<char*> translators;
148
149
150
151
152
153
154
155
bool global_error_flag = false;

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

157
158
159
160
161
162
163
164
165
166
struct statistics
{
  bool ok;
  unsigned states;
  unsigned edges;
  unsigned transitions;
  unsigned acc;
  unsigned scc;
  unsigned nondetstates;
  bool nondeterministic;
167
  double time;
168
169
170
171
172
173
174
  unsigned product_states;
  unsigned product_transitions;
  unsigned product_scc;

  static void
  fields(std::ostream& os)
  {
175
176
177
178
179
180
181
182
183
184
185
    os << (" \"states\","
	   " \"edges\","
	   " \"transitions\","
	   " \"acc\","
	   " \"scc\","
	   " \"nondetstates\","
	   " \"nondeterministic\","
	   " \"time\","
	   " \"product_states\","
	   " \"product_transitions\","
	   " \"product_scc\"");
186
187
188
189
190
191
192
193
194
195
196
197
  }

  void
  to_csv(std::ostream& os)
  {
    os << states << ", "
       << edges << ", "
       << transitions << ", "
       << acc << ", "
       << scc << ", "
       << nondetstates << ", "
       << nondeterministic << ", "
198
       << time << ", "
199
200
201
202
203
204
205
206
207
208
209
       << 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;

210
211
212
213
214
215
216
217
218
219
220
// 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();
}

221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
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;
271
272
    case 'T':
      timeout = to_pos_int(arg);
273
274
275
276
#if !ENABLE_TIMEOUT
      std::cerr << "warning: setting a timeout is not supported "
		<< "on your platform" << std::endl;
#endif
277
      break;
278
279
280
281
    case OPT_CSV:
      want_stats = true;
      csv_output = arg ? arg : "-";
      break;
282
283
284
    case OPT_DENSITY:
      density = to_probability(arg);
      break;
285
286
287
    case OPT_DUPS:
      allow_dups = true;
      break;
288
289
290
291
    case OPT_JSON:
      want_stats = true;
      json_output = arg ? arg : "-";
      break;
292
293
294
    case OPT_NOCHECKS:
      no_checks = true;
      break;
295
296
297
298
299
300
301
302
303
304
    case OPT_STATES:
      states = to_pos_int(arg);
      break;
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

static int
305
create_tmpfile(char c, unsigned int n, std::string& name)
306
307
{
  char tmpname[30];
308
  snprintf(tmpname, sizeof tmpname, "lck-%c%u-XXXXXX", c, n);
309
310
311
312
313
314
315
  int fd = mkstemp(tmpname);
  if (fd == -1)
    error(2, errno, "failed to create a temporary file");
  name = tmpname;
  return fd;
}

316
317

static volatile bool timed_out = false;
318

319
320
#if ENABLE_TIMEOUT
static volatile int alarm_on = 0;
321
322
323
324
325
326
327
328
329
330
331
332
333
334
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.
335
	  kill(-child_pid, SIGTERM);
336
337
338
339
340
341
342
	  // 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.
343
	  kill(-child_pid, SIGKILL);
344
345
346
347
348
	}
    }
  else
    {
      // forward signal
349
      kill(-child_pid, sig);
350
351
      // cleanup files
      cleanup();
352
353
      // and die verbosely
      error(2, 0, "received signal %d", sig);
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
    }
}

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'");
    }
  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;
}
405
406
407
408
#else // !ENABLE_TIMEOUT
#define exec_with_timeout(cmd) system(cmd)
#define setup_sig_handler() while (0);
#endif // !ENABLE_TIMEOUT
409

410
namespace
411
{
412
413
414
  struct quoted_string: public spot::printable_value<std::string>
  {
    using spot::printable_value<std::string>::operator=;
415

416
417
418
419
420
421
422
423
    void
    print(std::ostream& os, const char* pos) const
    {
      os << '\'';
      this->spot::printable_value<std::string>::print(os, pos);
      os << '\'';
    }
  };
424

425
426
427
428
429
  struct printable_result_filename: public spot::printable_value<std::string>
  {
    unsigned translator_num;
    enum output_format { None, Spin, Lbtt };
    mutable output_format format;
430

431
432
433
434
435
436
    void reset(unsigned n)
    {
      val_.clear();
      translator_num = n;
      format = None;
    }
437

438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
    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_ << '\'';
    }
  };
453

454
455
456
  class translator_runner: protected spot::formater
  {
  private:
457
    spot::bdd_dict& dict;
458
459
460
461
    // Round-specific variables
    quoted_string string_ltl_spot;
    quoted_string string_ltl_spin;
    quoted_string string_ltl_lbt;
462
    quoted_string string_ltl_wring;
463
464
465
    quoted_string filename_ltl_spot;
    quoted_string filename_ltl_spin;
    quoted_string filename_ltl_lbt;
466
    quoted_string filename_ltl_wring;
467
468
469
    // Run-specific variables
    printable_result_filename output;
  public:
470
471
    using spot::formater::has;

472
473
    translator_runner(spot::bdd_dict& dict)
      : dict(dict)
474
475
476
477
    {
      declare('f', &string_ltl_spot);
      declare('s', &string_ltl_spin);
      declare('l', &string_ltl_lbt);
478
      declare('w', &string_ltl_wring);
479
480
481
      declare('F', &filename_ltl_spot);
      declare('S', &filename_ltl_spin);
      declare('L', &filename_ltl_lbt);
482
      declare('W', &filename_ltl_wring);
483
484
485
486
487
488
489
      declare('N', &output);
      declare('T', &output);

      size_t s = translators.size();
      assert(s);
      for (size_t n = 0; n < s; ++n)
	prime(translators[n]);
490

491
492
493
494
    }

    void
    string_to_tmp(std::string& str, unsigned n, std::string& tmpname)
495
    {
496
497
498
499
500
501
502
      int fd = create_tmpfile('i', n, tmpname);
      write(fd, str.c_str(), str.size());
      write(fd, "\n", 1);
      close(fd);
      toclean.push_back(tmpname);
    }

503
504
    const std::string&
    formula() const
505
506
507
508
509
510
    {
      // 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;
511
512
      if (!string_ltl_wring.val().empty())
	return string_ltl_wring;
513
514
515
516
517
518
      if (!string_ltl_lbt.val().empty())
	return string_ltl_lbt;
      error(2, 0, "None of the translators need the input formula?");
      return string_ltl_spot;
    }

519
520
    void
    round_formula(const spot::ltl::formula* f, unsigned serial)
521
522
523
524
525
526
527
    {
      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);
528
529
      if (has('w') || has('W'))
	string_ltl_wring = spot::ltl::to_wring_string(f);
530
531
532
533
534
535
      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);
536
537
      if (has('W'))
	string_to_tmp(string_ltl_wring, serial, filename_ltl_wring);
538
539
    }

540
541
    const spot::tgba*
    translate(unsigned int translator_num, char l, statistics_formula* fstats)
542
543
544
545
546
547
    {
      output.reset(translator_num);

      std::ostringstream command;
      format(command, translators[translator_num]);
      toclean.push_back(output.val());
548
549
550
551
552

      if (output.format == printable_result_filename::None)
	error(2, 0, "no output sequence used in %s",
	      translators[translator_num]);

553
554
555
      std::string cmd = command.str();
      std::cerr << "Running [" << l << translator_num << "]: "
		<< cmd << std::endl;
556
      xtime_t before = gethrxtime();
557
      int es = exec_with_timeout(cmd.c_str());
558
      xtime_t after = gethrxtime();
559
560

      const spot::tgba* res = 0;
561
562
      if (timed_out)
	{
563
564
	  // This is not considered to be a global error.
	  std::cerr << "warning: timeout during execution of command\n";
565
566
567
	}
      else if (WIFSIGNALED(es))
	{
568
569
	  global_error() << "error: execution terminated by signal "
			 << WTERMSIG(es) << ".\n";
570
571
	}
      else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
572
	{
573
574
	  global_error() << "error: execution returned exit code "
			 << WEXITSTATUS(es) << ".\n";
575
576
577
578
579
580
	}
      else
	{
	  switch (output.format)
	    {
	    case printable_result_filename::Spin:
581
	      {
582
583
584
585
		spot::neverclaim_parse_error_list pel;
		res = spot::neverclaim_parse(output, pel, &dict);
		if (!pel.empty())
		  {
586
587
588
		    std::ostream& err = global_error();
		    err << "error: failed to parse the produced neverclaim.\n";
		    spot::format_neverclaim_parse_errors(err, output, pel);
589
590
591
592
		    delete res;
		    res = 0;
		  }
		break;
593
	      }
594
	    case printable_result_filename::Lbtt:
595
	      {
596
		std::string error;
597
		std::ifstream f(output.val().c_str());
598
599
		if (!f)
		  {
600
601
602
		    global_error() << "Cannot open " << output.val()
				   << std::endl;
		    global_error_flag = true;
603
604
605
		  }
		else
		  {
606
		    res = spot::lbtt_parse(f, error, &dict);
607
		    if (!res)
608
		      global_error() << ("error: failed to parse output in "
609
610
					 "LBTT format: ")
				     << error << std::endl;
611
612
		  }
		break;
613
	      }
614
615
616
	    case printable_result_filename::None:
	      assert(!"unreachable code");
	    }
617
	}
618
      // Compute statistics.
619
      if (res && want_stats)
620
621
622
623
624
625
626
627
628
629
630
631
632
	{
	  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();
	  st->scc = m.scc_count();
	  st->nondetstates = spot::count_nondet_states(res);
	  st->nondeterministic = st->nondetstates != 0;
633
634
          double prec = XTIME_PRECISION;
	  st->time = (after - before) / prec;
635
	}
636
      return res;
637
    }
638
  };
639

640
641
642
643
644
645
646
647
648
649
650
651
652
653
  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();
654

655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
    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)
673
      {
674
675
	std::ostream& err = global_error();
	err << "error: {";
676
677
678
679
680
681
682
	bool first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && res[i])
	    {
	      if (first)
		first = false;
	      else
683
684
		err << ",";
	      err << l << i;
685
	    }
686
	err << "} disagree with {";
687
688
689
690
691
692
693
	first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && !res[i])
	    {
	      if (first)
		first = false;
	      else
694
695
		err << ",";
	      err << l << i;
696
	    }
697
	err << "} when evaluating the state-space\n";
698
      }
699
  }
700

701
  typedef std::set<spot::state*, spot::state_ptr_less_than> state_set;
702

703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
  // 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();
	    }
	}
  }
724

725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
  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;
    for (it = s.begin(); it != s.end(); it++)
      (*it)->destroy();
    return res;
  }
740

741
742
743
744
745
  typedef
  Sgi::hash_set<const spot::ltl::formula*,
		const spot::ptr_hash<const spot::ltl::formula> > fset_t;


746
747
  class processor: public job_processor
  {
748
    spot::bdd_dict dict;
749
    translator_runner runner;
750
    fset_t unique_set;
751
  public:
752
753
754
755
756
    processor()
      : runner(dict)
    {
    }

757
758
759
760
761
762
763
    ~processor()
    {
      fset_t::iterator i = unique_set.begin();
      while (i != unique_set.end())
	(*i++)->destroy();
    }

764
765
766
767
768
769
    int
    process_formula(const spot::ltl::formula* f,
		    const char* filename = 0, int linenum = 0)
    {
      (void) filename;
      (void) linenum;
770
      static unsigned round = 0;
771

772
773
774
775
776
777
778
779
780
781
      // 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;
	}

782
783
      // ---------- Positive Formula ----------

784
      runner.round_formula(f, round);
785

786
787
788
      // Call formula() before printing anything else, in case it
      // complains.
      std::string fstr = runner.formula();
789
790
791
792
793
794
      if (filename)
	std::cerr << filename << ":";
      if (linenum)
	std::cerr << linenum << ":";
      if (filename || linenum)
	std::cerr << " ";
795
      std::cerr << fstr << "\n";
796

797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
      // 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();
822
      vstats.resize(n + (no_checks ? 1 : 2));
823
      statistics_formula* pstats = &vstats[n];
824
      statistics_formula* nstats = 0;
825
      pstats->resize(m);
826
827
      formulas.push_back(fstr);

828
      for (size_t n = 0; n < m; ++n)
829
830
831
	pos[n] = runner.translate(n, 'P', pstats);

      // ---------- Negative Formula ----------
832

833
834
835
      // The negative formula is only needed when checks are
      // activated.
      if (!no_checks)
836
	{
837
838
	  nstats = &vstats[n + 1];
	  nstats->resize(m);
839

840
841
	  const spot::ltl::formula* nf =
	    spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone());
842

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

853
854
	  runner.round_formula(nf, round);
	  formulas.push_back(runner.formula());
855

856
857
858
859
	  for (size_t n = 0; n < m; ++n)
	    neg[n] = runner.translate(n, 'N', nstats);
	  nf->destroy();
	}
860

861
      f->destroy();
862
      cleanup();
863
      ++round;
864

865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
      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;
	}
888
889

      // build products with a random state-space.
890
      spot::ltl::atomic_prop_set* ap = spot::ltl::atomic_prop_collect(f);
891
      spot::tgba* statespace = spot::random_graph(states, density, ap, &dict);
892
      delete ap;
893
894
895
896
897
898
899
900
901
902
903
904
905

      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;
906
907

	    // Statistics
908
909
910
911
912
913
914
	    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;
	      }
915
	  }
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
      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;
		}
	    }
935

936
937
938
939
940
941
942
943
944
945
946
947
948
      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";
	}
949
950
951

      // Cleanup.

952
953
      if (!no_checks)
	for (size_t n = 0; n < m; ++n)
954
955
956
	{
	  delete neg_map[n];
	  delete neg_prod[n];
957
	  delete neg[n];
958
959
960
	}
      for (size_t n = 0; n < m; ++n)
	{
961
962
	  delete pos_map[n];
	  delete pos_prod[n];
963
964
	  delete pos[n];
	}
965
      delete statespace;
966
      std::cerr << std::endl;
967
968
969
970
971
      return 0;
    }
  };
}

972
static void
973
print_stats_csv(const char* filename)
974
{
975
976
977
978
979
980
981
982
983
984
985
986
987
988
  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();
989
  unsigned rounds = vstats.size();
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
  assert(rounds = formulas.size());

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

1026
  unsigned ntrans = translators.size();
1027
  unsigned rounds = vstats.size();
1028
1029
  assert(rounds = formulas.size());

1030
1031
  *out << "{\n  \"tools\": [\n    \"";
  spot::escape_str(*out, translators[0]);
1032
  for (unsigned t = 1; t < ntrans; ++t)
1033
1034
1035
1036
1037
1038
    {
      *out << "\",\n    \"";
      spot::escape_str(*out, translators[t]);
    }
  *out << "\"\n  ],\n  \"inputs\": [\n    \"";
  spot::escape_str(*out, formulas[0]);
1039
  for (unsigned r = 1; r < rounds; ++r)
1040
1041
1042
1043
1044
1045
1046
    {
      *out << "\",\n    \"";
      spot::escape_str(*out, formulas[r]);
    }
  *out << ("\"\n  ],\n  \"fields\": [\n    \"input\", \"tool\",");
  statistics::fields(*out);
  *out << "\n  ],\n  \"results\": [";
1047
1048
1049
1050
1051
1052
  bool notfirst = false;
  for (unsigned r = 0; r < rounds; ++r)
    for (unsigned t = 0; t < ntrans; ++t)
      if (vstats[r][t].ok)
	{
	  if (notfirst)
1053
	    *out << ",";
1054
	  notfirst = true;
1055
1056
1057
	  *out << "\n    [ " << r << ", " << t << ", ";
	  vstats[r][t].to_csv(*out);
	  *out << " ]";
1058
	}
1059
1060
1061
  *out << "\n  ]\n}\n";

  delete outfile;
1062
}
1063
1064
1065
1066
1067
1068
1069
1070
1071

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

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

1072
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
1073
1074
1075
1076
1077
1078
1079
1080
1081
    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);

1082
1083
  setup_sig_handler();

1084
1085
1086
  processor p;
  if (p.run())
    return 2;
1087

1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
  if (formulas.empty())
    {
      error(2, 0, "no formula to translate");
    }
  else
    {
      if (global_error_flag)
	std::cerr
	  << ("error: some error was detected during the above runs,\n"
	      "       please search for 'error:' messages in the above trace.")
	  << std::endl;
	else
	  std::cerr << "no problem detected" << std::endl;
    }

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

1108
  return global_error_flag;
1109
}