ltlcheck.cc 27 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
95
96
97
98
    /**************************************************/
    { 0, 0, 0, 0,
      "COMMANDFMT should specify input and output arguments using the "
      "following character sequences:", 3 },
    { "%f,%s,%l", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the formula as a (quoted) string in Spot, Spin, or LBT's syntax", 0 },
    { "%F,%S,%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the formula as a file in Spot, Spin, or LBT's syntax", 0 },
99
100
    { "%N,%T", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the output automaton as a Never claim, or in LBTT's format", 0 },
101
102
103
104
    { 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 },
105
    /**************************************************/
106
107
108
109
110
111
112
113
    { 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 },
114
115
116
117
118
119
    { "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 },
    /**************************************************/
120
    { 0, 0, 0, 0, "Statistics output:", 6 },
121
122
123
124
125
    { "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 },
    /**************************************************/
126
127
128
129
130
131
132
    { 0, 0, 0, 0, "Miscellaneous options:", -1 },
    { 0, 0, 0, 0, 0, 0 }
  };

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

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

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

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

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

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

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

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

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

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

315
316

static volatile bool timed_out = false;
317

318
319
#if ENABLE_TIMEOUT
static volatile int alarm_on = 0;
320
321
322
323
324
325
326
327
328
329
330
331
332
333
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.
334
	  kill(-child_pid, SIGTERM);
335
336
337
338
339
340
341
	  // 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.
342
	  kill(-child_pid, SIGKILL);
343
344
345
346
347
	}
    }
  else
    {
      // forward signal
348
      kill(-child_pid, sig);
349
350
      // cleanup files
      cleanup();
351
352
      // and die verbosely
      error(2, 0, "received signal %d", sig);
353
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
    }
}

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

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

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

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

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

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

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

469
470
    translator_runner(spot::bdd_dict& dict)
      : dict(dict)
471
472
473
474
475
476
477
478
479
480
481
482
483
484
    {
      declare('f', &string_ltl_spot);
      declare('s', &string_ltl_spin);
      declare('l', &string_ltl_lbt);
      declare('F', &filename_ltl_spot);
      declare('S', &filename_ltl_spin);
      declare('L', &filename_ltl_lbt);
      declare('N', &output);
      declare('T', &output);

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

486
487
488
489
    }

    void
    string_to_tmp(std::string& str, unsigned n, std::string& tmpname)
490
    {
491
492
493
494
495
496
497
      int fd = create_tmpfile('i', n, tmpname);
      write(fd, str.c_str(), str.size());
      write(fd, "\n", 1);
      close(fd);
      toclean.push_back(tmpname);
    }

498
499
    const std::string&
    formula() const
500
501
502
503
504
505
506
507
508
509
510
511
    {
      // 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;
      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;
    }

512
513
    void
    round_formula(const spot::ltl::formula* f, unsigned serial)
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
    {
      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);
      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);
    }

529
530
    const spot::tgba*
    translate(unsigned int translator_num, char l, statistics_formula* fstats)
531
532
533
534
535
536
    {
      output.reset(translator_num);

      std::ostringstream command;
      format(command, translators[translator_num]);
      toclean.push_back(output.val());
537
538
539
540
541

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

542
543
544
      std::string cmd = command.str();
      std::cerr << "Running [" << l << translator_num << "]: "
		<< cmd << std::endl;
545
      xtime_t before = gethrxtime();
546
      int es = exec_with_timeout(cmd.c_str());
547
      xtime_t after = gethrxtime();
548
549

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

629
630
631
632
633
634
635
636
637
638
639
640
641
642
  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();
643

644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
    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)
662
      {
663
664
	std::ostream& err = global_error();
	err << "error: {";
665
666
667
668
669
670
671
	bool first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && res[i])
	    {
	      if (first)
		first = false;
	      else
672
673
		err << ",";
	      err << l << i;
674
	    }
675
	err << "} disagree with {";
676
677
678
679
680
681
682
	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 << "} when evaluating the state-space\n";
687
      }
688
  }
689

690
  typedef std::set<spot::state*, spot::state_ptr_less_than> state_set;
691

692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
  // 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();
	    }
	}
  }
713

714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
  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;
  }
729

730
731
732
733
734
  typedef
  Sgi::hash_set<const spot::ltl::formula*,
		const spot::ptr_hash<const spot::ltl::formula> > fset_t;


735
736
  class processor: public job_processor
  {
737
    spot::bdd_dict dict;
738
    translator_runner runner;
739
    fset_t unique_set;
740
  public:
741
742
743
744
745
    processor()
      : runner(dict)
    {
    }

746
747
748
749
750
751
752
    ~processor()
    {
      fset_t::iterator i = unique_set.begin();
      while (i != unique_set.end())
	(*i++)->destroy();
    }

753
754
755
756
757
758
    int
    process_formula(const spot::ltl::formula* f,
		    const char* filename = 0, int linenum = 0)
    {
      (void) filename;
      (void) linenum;
759
      static unsigned round = 0;
760

761
762
763
764
765
766
767
768
769
770
      // 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;
	}

771
772
      // ---------- Positive Formula ----------

773
      runner.round_formula(f, round);
774

775
776
777
      // Call formula() before printing anything else, in case it
      // complains.
      std::string fstr = runner.formula();
778
779
780
781
782
783
      if (filename)
	std::cerr << filename << ":";
      if (linenum)
	std::cerr << linenum << ":";
      if (filename || linenum)
	std::cerr << " ";
784
      std::cerr << fstr << "\n";
785

786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
      // 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();
811
      vstats.resize(n + (no_checks ? 1 : 2));
812
      statistics_formula* pstats = &vstats[n];
813
      statistics_formula* nstats = 0;
814
      pstats->resize(m);
815
816
      formulas.push_back(fstr);

817
      for (size_t n = 0; n < m; ++n)
818
819
820
	pos[n] = runner.translate(n, 'P', pstats);

      // ---------- Negative Formula ----------
821

822
823
824
      // The negative formula is only needed when checks are
      // activated.
      if (!no_checks)
825
	{
826
827
	  nstats = &vstats[n + 1];
	  nstats->resize(m);
828

829
830
	  const spot::ltl::formula* nf =
	    spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone());
831

832
833
834
835
836
837
838
839
840
	  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;
	    }
841

842
843
	  runner.round_formula(nf, round);
	  formulas.push_back(runner.formula());
844

845
846
847
848
	  for (size_t n = 0; n < m; ++n)
	    neg[n] = runner.translate(n, 'N', nstats);
	  nf->destroy();
	}
849

850
      f->destroy();
851
      cleanup();
852
      ++round;
853

854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
      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;
	}
877
878

      // build products with a random state-space.
879
      spot::ltl::atomic_prop_set* ap = spot::ltl::atomic_prop_collect(f);
880
      spot::tgba* statespace = spot::random_graph(states, density, ap, &dict);
881
      delete ap;
882
883
884
885
886
887
888
889
890
891
892
893
894

      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;
895
896

	    // Statistics
897
898
899
900
901
902
903
	    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;
	      }
904
	  }
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
      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;
		}
	    }
924

925
926
927
928
929
930
931
932
933
934
935
936
937
      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";
	}
938
939
940

      // Cleanup.

941
942
      if (!no_checks)
	for (size_t n = 0; n < m; ++n)
943
944
945
	{
	  delete neg_map[n];
	  delete neg_prod[n];
946
	  delete neg[n];
947
948
949
	}
      for (size_t n = 0; n < m; ++n)
	{
950
951
	  delete pos_map[n];
	  delete pos_prod[n];
952
953
	  delete pos[n];
	}
954
      delete statespace;
955
      std::cerr << std::endl;
956
957
958
959
960
      return 0;
    }
  };
}

961
static void
962
print_stats_csv(const char* filename)
963
{
964
965
966
967
968
969
970
971
972
973
974
975
976
977
  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();
978
  unsigned rounds = vstats.size();
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
  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)