ltlcross.cc 29 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 "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
  2  ltlcross aborted on error\n\
74
";
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
#define OPT_STOP_ERR 7
84
85
86
87
88
89
90

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

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

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

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

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

162
163
164
165
166
167
168
169
170
171
struct statistics
{
  bool ok;
  unsigned states;
  unsigned edges;
  unsigned transitions;
  unsigned acc;
  unsigned scc;
  unsigned nondetstates;
  bool nondeterministic;
172
  double time;
173
174
175
176
177
178
179
  unsigned product_states;
  unsigned product_transitions;
  unsigned product_scc;

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

  void
  to_csv(std::ostream& os)
  {
    os << states << ", "
       << edges << ", "
       << transitions << ", "
       << acc << ", "
       << scc << ", "
       << nondetstates << ", "
       << nondeterministic << ", "
203
       << time << ", "
204
205
206
207
208
209
210
211
212
213
214
       << 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;

215
216
217
218
219
220
221
222
223
224
225
// 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();
}

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
271
272
273
274
275
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;
276
277
    case 'T':
      timeout = to_pos_int(arg);
278
279
280
281
#if !ENABLE_TIMEOUT
      std::cerr << "warning: setting a timeout is not supported "
		<< "on your platform" << std::endl;
#endif
282
      break;
283
284
285
286
    case OPT_CSV:
      want_stats = true;
      csv_output = arg ? arg : "-";
      break;
287
288
289
    case OPT_DENSITY:
      density = to_probability(arg);
      break;
290
291
292
    case OPT_DUPS:
      allow_dups = true;
      break;
293
294
295
296
    case OPT_JSON:
      want_stats = true;
      json_output = arg ? arg : "-";
      break;
297
298
299
    case OPT_NOCHECKS:
      no_checks = true;
      break;
300
301
302
    case OPT_STATES:
      states = to_pos_int(arg);
      break;
303
304
305
    case OPT_STOP_ERR:
      stop_on_error = true;
      break;
306
307
308
309
310
311
312
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

static int
313
create_tmpfile(char c, unsigned int n, std::string& name)
314
315
{
  char tmpname[30];
316
  snprintf(tmpname, sizeof tmpname, "lck-%c%u-XXXXXX", c, n);
317
318
319
320
321
322
323
  int fd = mkstemp(tmpname);
  if (fd == -1)
    error(2, errno, "failed to create a temporary file");
  name = tmpname;
  return fd;
}

324
325

static volatile bool timed_out = false;
326
unsigned timeout_count = 0;
327

328
329
#if ENABLE_TIMEOUT
static volatile int alarm_on = 0;
330
331
332
333
334
335
336
337
338
339
340
341
342
343
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.
344
	  kill(-child_pid, SIGTERM);
345
346
347
348
349
350
351
	  // 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.
352
	  kill(-child_pid, SIGKILL);
353
354
355
356
357
	}
    }
  else
    {
      // forward signal
358
      kill(-child_pid, sig);
359
360
      // cleanup files
      cleanup();
361
362
      // and die verbosely
      error(2, 0, "received signal %d", sig);
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
    }
}

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'");
397
398
      // never reached
      return -1;
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
    }
  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;
}
416
417
418
419
#else // !ENABLE_TIMEOUT
#define exec_with_timeout(cmd) system(cmd)
#define setup_sig_handler() while (0);
#endif // !ENABLE_TIMEOUT
420

421
namespace
422
{
423
424
425
  struct quoted_string: public spot::printable_value<std::string>
  {
    using spot::printable_value<std::string>::operator=;
426

427
428
429
430
431
432
433
434
    void
    print(std::ostream& os, const char* pos) const
    {
      os << '\'';
      this->spot::printable_value<std::string>::print(os, pos);
      os << '\'';
    }
  };
435

436
437
438
439
440
  struct printable_result_filename: public spot::printable_value<std::string>
  {
    unsigned translator_num;
    enum output_format { None, Spin, Lbtt };
    mutable output_format format;
441

442
443
444
445
446
447
    void reset(unsigned n)
    {
      val_.clear();
      translator_num = n;
      format = None;
    }
448

449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
    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_ << '\'';
    }
  };
464

465
466
467
  class translator_runner: protected spot::formater
  {
  private:
468
    spot::bdd_dict& dict;
469
470
471
472
    // Round-specific variables
    quoted_string string_ltl_spot;
    quoted_string string_ltl_spin;
    quoted_string string_ltl_lbt;
473
    quoted_string string_ltl_wring;
474
475
476
    quoted_string filename_ltl_spot;
    quoted_string filename_ltl_spin;
    quoted_string filename_ltl_lbt;
477
    quoted_string filename_ltl_wring;
478
479
480
    // Run-specific variables
    printable_result_filename output;
  public:
481
482
    using spot::formater::has;

483
484
    translator_runner(spot::bdd_dict& dict)
      : dict(dict)
485
486
487
488
    {
      declare('f', &string_ltl_spot);
      declare('s', &string_ltl_spin);
      declare('l', &string_ltl_lbt);
489
      declare('w', &string_ltl_wring);
490
491
492
      declare('F', &filename_ltl_spot);
      declare('S', &filename_ltl_spin);
      declare('L', &filename_ltl_lbt);
493
      declare('W', &filename_ltl_wring);
494
495
496
      declare('N', &output);
      declare('T', &output);

497
      std::vector<bool> has(256);
498
499
500
      size_t s = translators.size();
      assert(s);
      for (size_t n = 0; n < s; ++n)
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
	{
	  // 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]);
	}
519

520
521
522
523
    }

    void
    string_to_tmp(std::string& str, unsigned n, std::string& tmpname)
524
    {
525
      int fd = create_tmpfile('i', n, tmpname);
526
527
528
529
530
531
      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());
532
533
534
      toclean.push_back(tmpname);
    }

535
536
    const std::string&
    formula() const
537
538
539
540
541
542
    {
      // 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;
543
544
      if (!string_ltl_wring.val().empty())
	return string_ltl_wring;
545
546
      if (!string_ltl_lbt.val().empty())
	return string_ltl_lbt;
547
      assert(!"None of the translators need the input formula?");
548
549
550
      return string_ltl_spot;
    }

551
552
    void
    round_formula(const spot::ltl::formula* f, unsigned serial)
553
554
555
556
557
558
559
    {
      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);
560
561
      if (has('w') || has('W'))
	string_ltl_wring = spot::ltl::to_wring_string(f);
562
563
564
565
566
567
      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);
568
569
      if (has('W'))
	string_to_tmp(string_ltl_wring, serial, filename_ltl_wring);
570
571
    }

572
573
    const spot::tgba*
    translate(unsigned int translator_num, char l, statistics_formula* fstats)
574
575
576
577
578
579
    {
      output.reset(translator_num);

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

581
      assert(output.format != printable_result_filename::None);
582

583
584
585
      std::string cmd = command.str();
      std::cerr << "Running [" << l << translator_num << "]: "
		<< cmd << std::endl;
586
      xtime_t before = gethrxtime();
587
      int es = exec_with_timeout(cmd.c_str());
588
      xtime_t after = gethrxtime();
589
590

      const spot::tgba* res = 0;
591
592
      if (timed_out)
	{
593
594
	  // This is not considered to be a global error.
	  std::cerr << "warning: timeout during execution of command\n";
595
	  ++timeout_count;
596
597
598
	}
      else if (WIFSIGNALED(es))
	{
599
600
	  global_error() << "error: execution terminated by signal "
			 << WTERMSIG(es) << ".\n";
601
602
	}
      else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
603
	{
604
605
	  global_error() << "error: execution returned exit code "
			 << WEXITSTATUS(es) << ".\n";
606
607
608
609
610
611
	}
      else
	{
	  switch (output.format)
	    {
	    case printable_result_filename::Spin:
612
	      {
613
614
615
616
		spot::neverclaim_parse_error_list pel;
		res = spot::neverclaim_parse(output, pel, &dict);
		if (!pel.empty())
		  {
617
618
619
		    std::ostream& err = global_error();
		    err << "error: failed to parse the produced neverclaim.\n";
		    spot::format_neverclaim_parse_errors(err, output, pel);
620
621
622
623
		    delete res;
		    res = 0;
		  }
		break;
624
	      }
625
	    case printable_result_filename::Lbtt:
626
	      {
627
		std::string error;
628
		std::ifstream f(output.val().c_str());
629
630
		if (!f)
		  {
631
632
633
		    global_error() << "Cannot open " << output.val()
				   << std::endl;
		    global_error_flag = true;
634
635
636
		  }
		else
		  {
637
		    res = spot::lbtt_parse(f, error, &dict);
638
		    if (!res)
639
		      global_error() << ("error: failed to parse output in "
640
641
					 "LBTT format: ")
				     << error << std::endl;
642
643
		  }
		break;
644
	      }
645
646
647
	    case printable_result_filename::None:
	      assert(!"unreachable code");
	    }
648
	}
649
      // Compute statistics.
650
      if (res && want_stats)
651
652
653
654
655
656
657
658
659
660
661
662
663
	{
	  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;
664
665
          double prec = XTIME_PRECISION;
	  st->time = (after - before) / prec;
666
	}
667
      return res;
668
    }
669
  };
670

671
672
673
674
675
676
677
678
679
680
681
682
683
684
  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();
685

686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
    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)
704
      {
705
706
	std::ostream& err = global_error();
	err << "error: {";
707
708
709
710
711
712
713
	bool first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && res[i])
	    {
	      if (first)
		first = false;
	      else
714
715
		err << ",";
	      err << l << i;
716
	    }
717
	err << "} disagree with {";
718
719
720
721
722
723
724
	first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && !res[i])
	    {
	      if (first)
		first = false;
	      else
725
726
		err << ",";
	      err << l << i;
727
	    }
728
	err << "} when evaluating the state-space\n";
729
      }
730
  }
731

732
  typedef std::set<spot::state*, spot::state_ptr_less_than> state_set;
733

734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
  // 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();
	    }
	}
  }
755

756
757
758
759
760
761
762
763
764
765
766
  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;
767
    for (it = s.begin(); it != s.end(); ++it)
768
769
770
      (*it)->destroy();
    return res;
  }
771

772
773
774
775
776
  typedef
  Sgi::hash_set<const spot::ltl::formula*,
		const spot::ptr_hash<const spot::ltl::formula> > fset_t;


777
778
  class processor: public job_processor
  {
779
    spot::bdd_dict dict;
780
    translator_runner runner;
781
    fset_t unique_set;
782
  public:
783
784
785
786
787
    processor()
      : runner(dict)
    {
    }

788
789
790
791
792
793
794
    ~processor()
    {
      fset_t::iterator i = unique_set.begin();
      while (i != unique_set.end())
	(*i++)->destroy();
    }

795
796
797
798
799
800
    int
    process_formula(const spot::ltl::formula* f,
		    const char* filename = 0, int linenum = 0)
    {
      (void) filename;
      (void) linenum;
801
      static unsigned round = 0;
802

803
804
805
806
807
808
809
810
811
812
      // 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;
	}

813
814
      // ---------- Positive Formula ----------

815
      runner.round_formula(f, round);
816

817
818
819
      // Call formula() before printing anything else, in case it
      // complains.
      std::string fstr = runner.formula();
820
821
822
823
824
825
      if (filename)
	std::cerr << filename << ":";
      if (linenum)
	std::cerr << linenum << ":";
      if (filename || linenum)
	std::cerr << " ";
826
      std::cerr << fstr << "\n";
827

828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
      // 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();
853
      vstats.resize(n + (no_checks ? 1 : 2));
854
      statistics_formula* pstats = &vstats[n];
855
      statistics_formula* nstats = 0;
856
      pstats->resize(m);
857
858
      formulas.push_back(fstr);

859
      for (size_t n = 0; n < m; ++n)
860
861
862
	pos[n] = runner.translate(n, 'P', pstats);

      // ---------- Negative Formula ----------
863

864
865
866
      // The negative formula is only needed when checks are
      // activated.
      if (!no_checks)
867
	{
868
869
	  nstats = &vstats[n + 1];
	  nstats->resize(m);
870

871
872
	  const spot::ltl::formula* nf =
	    spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone());
873

874
875
876
877
878
879
880
881
882
	  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;
	    }
883

884
885
	  runner.round_formula(nf, round);
	  formulas.push_back(runner.formula());
886

887
888
889
890
	  for (size_t n = 0; n < m; ++n)
	    neg[n] = runner.translate(n, 'N', nstats);
	  nf->destroy();
	}
891

892
      f->destroy();
893
      cleanup();
894
      ++round;
895

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

      // build products with a random state-space.
921
      spot::ltl::atomic_prop_set* ap = spot::ltl::atomic_prop_collect(f);
922
      spot::tgba* statespace = spot::random_graph(states, density, ap, &dict);
923
      delete ap;
924
925
926
927
928
929
930
931
932
933
934
935
936

      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;
937
938

	    // Statistics
939
940
941
942
943
944
945
	    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;
	      }
946
	  }
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
      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;
		}
	    }
966

967
968
969
970
971
972
973
974
975
976
977
978
979
      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";
	}
980
981
982

      // Cleanup.

983
984
      if (!no_checks)
	for (size_t n = 0; n < m; ++n)
985
986
987
	{
	  delete neg_map[n];
	  delete neg_prod[n];
988
	  delete neg[n];
989
990
991
	}
      for (size_t n = 0; n < m; ++n)
	{
992
993
	  delete pos_map[n];
	  delete pos_prod[n];
994
995
	  delete pos[n];
	}
996
      delete statespace;
997
      std::cerr << std::endl;
998
999
1000

      // Shall we stop processing formulas now?
      abort_run = global_error_flag && stop_on_error;