ltlcross.cc 35.4 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
3
// 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
#include <unistd.h>
31
#include <sys/wait.h>
32
#include "error.h"
33
#include "argmatch.h"
34
35
36

#include "common_setup.hh"
#include "common_cout.hh"
37
#include "common_conv.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
38
#include "common_trans.hh"
39
#include "common_finput.hh"
40
#include "dstarparse/public.hh"
41
#include "hoaparse/public.hh"
42
43
44
#include "ltlast/unop.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/apcollect.hh"
45
#include "ltlvisit/mutation.hh"
46
#include "ltlvisit/relabel.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
47
#include "ltlvisit/lbt.hh"
48
#include "tgbaalgos/lbtt.hh"
49
#include "tgbaalgos/product.hh"
50
51
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/randomgraph.hh"
52
#include "tgbaalgos/sccinfo.hh"
53
#include "tgbaalgos/isweakscc.hh"
54
55
#include "tgbaalgos/reducerun.hh"
#include "tgbaalgos/word.hh"
56
#include "tgbaalgos/dtgbacomp.hh"
57
#include "misc/formater.hh"
58
59
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/isdet.hh"
60
#include "misc/escape.hh"
61
#include "misc/hash.hh"
62
#include "misc/random.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
63
#include "misc/tmpfile.hh"
64
#include "misc/timer.hh"
65
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
#define OPT_SEED 8
86
#define OPT_PRODUCTS 9
87
#define OPT_COLOR 10
88
#define OPT_NOCOMP 11
89
#define OPT_OMIT 12
90
#define OPT_BOGUS 13
91
#define OPT_VERBOSE 14
92
#define OPT_GRIND 15
93
94
95
96

static const argp_option options[] =
  {
    /**************************************************/
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
97
    { 0, 0, 0, 0, "ltlcross behavior:", 5 },
98
99
100
101
102
    { "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 },
103
104
    { "no-complement", OPT_NOCOMP, 0, 0,
      "do not complement deterministic automata to perform extra checks", 0 },
105
106
107
    { "stop-on-error", OPT_STOP_ERR, 0, 0,
      "stop on first execution error or failure to pass"
      " sanity checks (timeouts are OK)", 0 },
108
    /**************************************************/
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
109
    { 0, 0, 0, 0, "State-space generation:", 6 },
110
111
112
113
114
    { "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 },
115
116
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0 by default)", 0 },
117
118
119
    { "products", OPT_PRODUCTS, "[+]INT", 0,
      "number of products to perform (1 by default), statistics will be "
      "averaged unless the number is prefixed with '+'", 0 },
120
    /**************************************************/
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
121
    { 0, 0, 0, 0, "Statistics output:", 7 },
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
    { "omit-missing", OPT_OMIT, 0, 0,
      "do not output statistics for timeouts or failed translations", 0 },
128
    /**************************************************/
129
    { 0, 0, 0, 0, "Miscellaneous options:", -1 },
130
131
132
133
    { "color", OPT_COLOR, "WHEN", OPTION_ARG_OPTIONAL,
      "colorize output; WHEN can be 'never', 'always' (the default if "
      "--color is used without argument), or "
      "'auto' (the default if --color is not used)", 0 },
134
135
136
    { "grind", OPT_GRIND, "FILENAME", 0,
      "for each formula for which a problem was detected, write a simpler " \
      "formula that fails on the same test in FILENAME", 0 },
137
138
    { "save-bogus", OPT_BOGUS, "FILENAME", 0,
      "save formulas for which problems were detected in FILENAME", 0 },
139
140
    { "verbose", OPT_VERBOSE, 0, 0,
      "print what is being done, for debugging", 0 },
141
142
143
144
145
146
    { 0, 0, 0, 0, 0, 0 }
  };

const struct argp_child children[] =
  {
    { &finput_argp, 0, 0, 1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
147
    { &trans_argp, 0, 0, 0 },
148
    { &misc_argp, 0, 0, -1 },
149
150
151
    { 0, 0, 0, 0 }
  };

152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
enum color_type { color_never, color_always, color_if_tty };

static char const *const color_args[] =
{
  "always", "yes", "force",
  "never", "no", "none",
  "auto", "tty", "if-tty", 0
};
static color_type const color_types[] =
{
  color_always, color_always, color_always,
  color_never, color_never, color_never,
  color_if_tty, color_if_tty, color_if_tty
};
ARGMATCH_VERIFY(color_args, color_types);

color_type color_opt = color_if_tty;
const char* bright_red = "\033[01;31m";
170
const char* bright_blue = "\033[01;34m";
171
const char* bright_yellow = "\033[01;33m";
172
173
const char* reset_color = "\033[m";

174
175
unsigned states = 200;
float density = 0.1;
176
177
178
const char* json_output = 0;
const char* csv_output = 0;
bool want_stats = false;
179
bool allow_dups = false;
180
bool no_checks = false;
181
bool no_complement = false;
182
bool stop_on_error = false;
183
int seed = 0;
184
unsigned products = 1;
185
bool products_avg = true;
186
bool opt_omit = false;
187
bool has_sr = false; // Has Streett or Rabin automata to process.
188
189
const char* bogus_output_filename = 0;
std::ofstream* bogus_output = 0;
190
std::ofstream* grind_output = 0;
191
bool verbose = false;
192
193


194
195
196
197
198
199
bool global_error_flag = false;

static std::ostream&
global_error()
{
  global_error_flag = true;
200
201
  if (color_opt)
    std::cerr << bright_red;
202
203
  return std::cerr;
}
204

205
206
207
208
209
210
211
212
213
static std::ostream&
example()
{
  if (color_opt)
    std::cerr << bright_yellow;
  return std::cerr;
}


214
215
216
217
218
219
220
221
static void
end_error()
{
  if (color_opt)
    std::cerr << reset_color;
}


222
223
struct statistics
{
224
225
  statistics()
    : ok(false),
226
      has_in(false),
227
228
229
      status_str(0),
      status_code(0),
      time(0),
230
231
232
233
234
235
      in_type(0),
      in_states(0),
      in_edges(0),
      in_transitions(0),
      in_acc(0),
      in_scc(0),
236
      states(0),
237
      edges(0),
238
239
240
241
242
243
244
245
246
247
248
      transitions(0),
      acc(0),
      scc(0),
      nonacc_scc(0),
      terminal_scc(0),
      weak_scc(0),
      strong_scc(0),
      nondetstates(0),
      nondeterministic(false),
      terminal_aut(false),
      weak_aut(false),
249
      strong_aut(false)
250
251
252
  {
  }

253
254
  // If OK is false, only the status_str, status_code, and time fields
  // should be valid.
255
  bool ok;
256
257
  // has in_* data to display.
  bool has_in;
258
259
260
  const char* status_str;
  int status_code;
  double time;
261
262
263
264
265
266
  const char* in_type;
  unsigned in_states;
  unsigned in_edges;
  unsigned in_transitions;
  unsigned in_acc;
  unsigned in_scc;
267
268
269
270
271
  unsigned states;
  unsigned edges;
  unsigned transitions;
  unsigned acc;
  unsigned scc;
272
273
274
275
  unsigned nonacc_scc;
  unsigned terminal_scc;
  unsigned weak_scc;
  unsigned strong_scc;
276
277
  unsigned nondetstates;
  bool nondeterministic;
278
279
280
  bool terminal_aut;
  bool weak_aut;
  bool strong_aut;
281
282
283
  std::vector<double> product_states;
  std::vector<double> product_transitions;
  std::vector<double> product_scc;
284
285

  static void
286
  fields(std::ostream& os, bool show_exit, bool show_sr)
287
  {
288
    if (show_exit)
289
      os << "\"exit_status\",\"exit_code\",";
290
291
292
293
294
    os << "\"time\",";
    if (show_sr)
      os << ("\"in_type\",\"in_states\",\"in_edges\",\"in_transitions\","
	     "\"in_acc\",\"in_scc\",");
    os << ("\"states\","
295
296
297
298
299
300
301
302
303
304
305
306
	   "\"edges\","
	   "\"transitions\","
	   "\"acc\","
	   "\"scc\","
	   "\"nonacc_scc\","
	   "\"terminal_scc\","
	   "\"weak_scc\","
	   "\"strong_scc\","
	   "\"nondet_states\","
	   "\"nondet_aut\","
	   "\"terminal_aut\","
	   "\"weak_aut\","
307
308
309
310
	   "\"strong_aut\"");
    size_t m = products_avg ? 1U : products;
    for (size_t i = 0; i < m; ++i)
      os << ",\"product_states\",\"product_transitions\",\"product_scc\"";
311
312
313
  }

  void
314
  to_csv(std::ostream& os, bool show_exit, bool show_sr, const char* na = "")
315
  {
316
    if (show_exit)
317
318
319
      os << '"' << status_str << "\"," << status_code << ',';
    os << time << ',';
    if (ok)
320
      {
321
322
323
324
325
326
327
328
329
330
	if (has_in)
	  os << '"' << in_type << "\","
	     << in_states << ','
	     << in_edges << ','
	     << in_transitions << ','
	     << in_acc << ','
	     << in_scc << ',';
	else if (show_sr)
	  os << na << ',' << na << ',' << na << ','
	     << na << ',' << na << ',' << na << ',';
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
	os << states << ','
	   << edges << ','
	   << transitions << ','
	   << acc << ','
	   << scc << ','
	   << nonacc_scc << ','
	   << terminal_scc << ','
	   << weak_scc << ','
	   << strong_scc << ','
	   << nondetstates << ','
	   << nondeterministic << ','
	   << terminal_aut << ','
	   << weak_aut << ','
	   << strong_aut;
	if (!products_avg)
	  {
	    for (size_t i = 0; i < products; ++i)
	      os << ',' << product_states[i]
		 << ',' << product_transitions[i]
		 << ',' << product_scc[i];
	  }
	else
	  {
	    double st = 0.0;
	    double tr = 0.0;
	    double sc = 0.0;
	    for (size_t i = 0; i < products; ++i)
	      {
		st += product_states[i];
		tr += product_transitions[i];
		sc += product_scc[i];
	      }
	    os << ',' << (st / products)
	       << ',' << (tr / products)
	       << ',' << (sc / products);
	  }
      }
368
    else
369
370
      {
	size_t m = products_avg ? 1U : products;
371
372
373
	m *= 3;
	m += 13 + show_sr * 6;
	os << na;
374
	for (size_t i = 0; i < m; ++i)
375
	  os << ',' << na;
376
      }
377
378
379
380
381
382
383
384
  }
};

typedef std::vector<statistics> statistics_formula;
typedef std::vector<statistics_formula> statistics_vector;
statistics_vector vstats;
std::vector<std::string> formulas;

385
386
387
388
389
390
391
392
393
static int
parse_opt(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case ARGP_KEY_ARG:
      translators.push_back(arg);
      break;
394
395
396
397
398
399
400
401
    case OPT_BOGUS:
      {
	bogus_output = new std::ofstream(arg);
	if (!*bogus_output)
	  error(2, errno, "cannot open '%s'", arg);
	bogus_output_filename = arg;
	break;
      }
402
403
404
405
406
407
408
409
    case OPT_COLOR:
      {
	if (arg)
	  color_opt = XARGMATCH("--color", arg, color_args, color_types);
	else
	  color_opt = color_always;
	break;
      }
410
411
412
413
    case OPT_CSV:
      want_stats = true;
      csv_output = arg ? arg : "-";
      break;
414
415
416
    case OPT_DENSITY:
      density = to_probability(arg);
      break;
417
418
419
    case OPT_DUPS:
      allow_dups = true;
      break;
420
421
422
423
424
    case OPT_GRIND:
      grind_output = new std::ofstream(arg);
      if (!*grind_output)
	error(2, errno, "cannot open '%s'", arg);
      break;
425
426
427
428
    case OPT_JSON:
      want_stats = true;
      json_output = arg ? arg : "-";
      break;
429
    case OPT_PRODUCTS:
430
431
432
433
434
      if (*arg == '+')
	{
	  products_avg = false;
	  ++arg;
	}
435
436
      products = to_pos_int(arg);
      break;
437
438
    case OPT_NOCHECKS:
      no_checks = true;
439
440
441
442
      no_complement = true;
      break;
    case OPT_NOCOMP:
      no_complement = true;
443
      break;
444
445
446
    case OPT_OMIT:
      opt_omit = true;
      break;
447
448
449
    case OPT_SEED:
      seed = to_pos_int(arg);
      break;
450
451
452
    case OPT_STATES:
      states = to_pos_int(arg);
      break;
453
454
455
    case OPT_STOP_ERR:
      stop_on_error = true;
      break;
456
457
458
    case OPT_VERBOSE:
      verbose = true;
      break;
459
460
461
462
463
464
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

465
namespace
466
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
467
  class xtranslator_runner: public translator_runner
468
469
  {
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
470
471
    xtranslator_runner(spot::bdd_dict_ptr dict)
      : translator_runner(dict)
472
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
473
      has_sr = has('D');
474
475
    }

476
    spot::const_tgba_digraph_ptr
477
478
    translate(unsigned int translator_num, char l, statistics_formula* fstats,
	      bool& problem)
479
480
481
482
    {
      output.reset(translator_num);

      std::ostringstream command;
483
      format(command, translators[translator_num].cmd);
484

485
      assert(output.format != printable_result_filename::None);
486

487
488
489
      std::string cmd = command.str();
      std::cerr << "Running [" << l << translator_num << "]: "
		<< cmd << std::endl;
490
491
      spot::stopwatch sw;
      sw.start();
492
      int es = exec_with_timeout(cmd.c_str());
493
      double duration = sw.stop();
494

495
496
      const char* status_str = 0;

497
      spot::const_tgba_digraph_ptr res = 0;
498
499
      if (timed_out)
	{
500
501
	  // This is not considered to be a global error.
	  std::cerr << "warning: timeout during execution of command\n";
502
	  ++timeout_count;
503
	  status_str = "timeout";
504
	  problem = false;	// A timeout is not a sign of a bug
505
	  es = -1;
506
507
508
	}
      else if (WIFSIGNALED(es))
	{
509
	  status_str = "signal";
510
	  problem = true;
511
	  es = WTERMSIG(es);
512
	  global_error() << "error: execution terminated by signal "
513
			 << es << ".\n";
514
	  end_error();
515
516
	}
      else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
517
	{
518
519
	  es = WEXITSTATUS(es);
	  status_str = "exit code";
520
	  problem = true;
521
	  global_error() << "error: execution returned exit code "
522
			 << es << ".\n";
523
	  end_error();
524
525
526
	}
      else
	{
527
	  status_str = "ok";
528
	  problem = false;
529
	  es = 0;
530
531
	  switch (output.format)
	    {
532
533
534
535
	    case printable_result_filename::Dstar:
	      {
		spot::dstar_parse_error_list pel;
		std::string filename = output.val()->name();
536
		auto aut = spot::dstar_parse(filename, pel, dict);
537
538
		if (!pel.empty())
		  {
539
		    status_str = "parse error";
540
		    problem = true;
541
		    es = -1;
542
543
544
545
546
		    std::ostream& err = global_error();
		    err << "error: failed to parse the produced DSTAR"
		      " output.\n";
		    spot::format_dstar_parse_errors(err, filename, pel);
		    end_error();
547
		    res = nullptr;
548
549
		  }
		else
550
		  {
551
552
553
554
555
556
557
558
559
560
561
562
		    const char* type = 0;
		    switch (aut->type)
		      {
		      case spot::Rabin:
			type = "DRA";
			break;
		      case spot::Streett:
			type = "DSA";
			break;
		      }
		    assert(type);

563
564
565
566
567
		    // Gather statistics about the input automaton
		    if (want_stats)
		      {
			statistics* st = &(*fstats)[translator_num];
			st->has_in = true;
568
			st->in_type = type;
569
570
571
572
573
574
575
			spot::tgba_sub_statistics s =
			  sub_stats_reachable(aut->aut);
			st->in_states= s.states;
			st->in_edges = s.transitions;
			st->in_transitions = s.sub_transitions;
			st->in_acc = aut->accpair_count;

576
			st->in_scc = spot::scc_info(aut->aut).scc_count();
577
578
		      }
		    // convert it into TGBA for further processing
579
580
		    if (verbose)
		      std::cerr << "info: converting " << type << " to TGBA\n";
581
582
		    res = dstar_to_tgba(aut);
		  }
583
584
		break;
	      }
585
	    case printable_result_filename::Hoa: // Will also read neverclaims
586
587
588
589
590
591
592
593
594
595
	      {
		spot::hoa_parse_error_list pel;
		std::string filename = output.val()->name();
		auto aut = spot::hoa_parse(filename, pel, dict);
		if (!pel.empty())
		  {
		    status_str = "parse error";
		    problem = true;
		    es = -1;
		    std::ostream& err = global_error();
596
		    err << "error: failed to parse the produced automaton.\n";
597
598
599
600
		    spot::format_hoa_parse_errors(err, filename, pel);
		    end_error();
		    res = nullptr;
		  }
601
602
603
604
605
606
607
608
609
610
		else if (aut->aborted)
		  {
		    status_str = "aborted";
		    problem = true;
		    es = -1;
		    std::ostream& err = global_error();
		    err << "error: aborted HOA file.\n";
		    end_error();
		    res = nullptr;
		  }
611
612
613
614
615
616
		else
		  {
		    res = aut->aut;
		  }
		break;
	      }
617
	    case printable_result_filename::None:
618
	      SPOT_UNREACHABLE();
619
	    }
620
	}
621
622

      if (want_stats)
623
624
	{
	  statistics* st = &(*fstats)[translator_num];
625
626
	  st->status_str = status_str;
	  st->status_code = es;
627
	  st->time = duration;
628
629
630

	  // Compute statistics.
	  if (res)
631
	    {
632
633
	      if (verbose)
		std::cerr << "info: getting statistics\n";
634
635
636
637
638
	      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;
639
	      st->acc = res->acc().num_sets();
640
	      spot::scc_info m(res);
641
	      unsigned c = m.scc_count();
642
	      st->scc = c;
643
644
645
646
	      st->nondetstates = spot::count_nondet_states(res);
	      st->nondeterministic = st->nondetstates != 0;
	      for (unsigned n = 0; n < c; ++n)
		{
647
		  if (!m.is_accepting_scc(n))
648
649
650
651
652
653
654
655
656
657
658
659
		    ++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;
660
	      else
661
		st->terminal_aut = true;
662
	    }
663
	}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
664
      output.cleanup();
665
      return res;
666
    }
667
  };
668

669
  static bool
670
671
  check_empty_prod(const spot::const_tgba_digraph_ptr& aut_i,
		   const spot::const_tgba_digraph_ptr& aut_j,
672
		   size_t i, size_t j, bool icomp, bool jcomp)
673
  {
674
    auto prod = spot::product(aut_i, aut_j);
675
    auto res = spot::couvreur99(prod)->check();
676

677
678
679
680
681
682
    if (verbose)
      {
	std::cerr << "info: check_empty ";
	if (icomp)
	  std::cerr << "Comp(N" << i << ')';
	else
683
	  std::cerr << 'P' << i;
684
685
686
687
688
689
690
	if (jcomp)
	  std::cerr << "*Comp(P" << j << ')';
	else
	  std::cerr << "*N" << j;
	std::cerr << '\n';
      }

691
692
    if (res)
      {
693
694
695
	std::ostream& err = global_error();
	err << "error: ";
	if (icomp)
696
	  err << "Comp(N" << i << ')';
697
	else
698
	  err << 'P' << i;
699
	if (jcomp)
700
	  err << "*Comp(P" << j << ')';
701
702
703
	else
	  err << "*N" << j;
	err << " is nonempty";
704

705
	auto run = res->accepting_run();
706
707
	if (run)
	  {
708
	    run = reduce_run(prod, run);
709
710
	    std::cerr << "; both automata accept the infinite word\n"
		      << "       ";
711
	    spot::tgba_word w(run);
712
	    w.simplify();
713
	    w.print(example(), prod->get_dict()) << '\n';
714
715
716
	  }
	else
	  {
717
	    std::cerr << '\n';
718
719
720
	  }
	end_error();
      }
721
    return !!res;
722
723
  }

724
  static bool
725
  cross_check(const std::vector<spot::scc_info*>& maps, char l, unsigned p)
726
727
  {
    size_t m = maps.size();
728
729
730
731
732
733
734
735
736
737
738
739
    if (verbose)
      {
	std::cerr << "info: cross_check {";
	bool first = true;
	for (size_t i = 0; i < m; ++i)
	  {
	    if (first)
	      first = false;
	    else
	      std::cerr << ',';
	    std::cerr << l << i;
	  }
740
	std::cerr << "}, state-space #" << p << '/' << products << '\n';
741
      }
742

743
744
745
746
    std::vector<bool> res(m);
    unsigned verified = 0;
    unsigned violated = 0;
    for (size_t i = 0; i < m; ++i)
747
      if (spot::scc_info* m = maps[i])
748
749
750
	{
	  // r == true iff the automaton i is accepting.
	  bool r = false;
751
752
	  for (auto& scc: *m)
	    if (scc.is_accepting())
753
754
755
756
	      {
		r = true;
		break;
	      }
757
758
759
760
761
762
763
	  res[i] = r;
	  if (r)
	    ++verified;
	  else
	    ++violated;
	}
    if (verified != 0 && violated != 0)
764
      {
765
766
	std::ostream& err = global_error();
	err << "error: {";
767
768
769
770
771
772
773
	bool first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && res[i])
	    {
	      if (first)
		first = false;
	      else
774
		err << ',';
775
	      err << l << i;
776
	    }
777
	err << "} disagree with {";
778
779
780
781
782
783
784
	first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && !res[i])
	    {
	      if (first)
		first = false;
	      else
785
		err << ',';
786
	      err << l << i;
787
	    }
788
789
	err << "} when evaluating ";
	if (products > 1)
790
	  err << "state-space #" << p << '/' << products << '\n';
791
	else
792
	  err << "the state-space\n";
793
	end_error();
794
	return true;
795
      }
796
    return false;
797
  }
798

799
  typedef std::set<unsigned> state_set;
800

801
  // Collect all the states of SSPACE that appear in the accepting SCCs
802
  // of PROD.  (Trivial SCCs are considered accepting.)
803
  static void
804
  states_in_acc(const spot::scc_info* m, state_set& s)
805
  {
806
    auto aut = m->get_aut();
807
    auto ps = aut->get_named_prop<const spot::product_states>("product-states");
808
809
810
    for (auto& scc: *m)
      if (scc.is_accepting() || scc.is_trivial())
	for (auto i: scc.states())
811
812
	  // Get the projection on sspace.
	  s.insert((*ps)[i].second);
813
  }
814

815
  static bool
816
  consistency_check(const spot::scc_info* pos, const spot::scc_info* neg)
817
818
819
820
  {
    // the states of SSPACE should appear in the accepting SCC of at
    // least one of POS or NEG.  Maybe both.
    state_set s;
821
822
823
    states_in_acc(pos, s);
    states_in_acc(neg, s);
    return s.size() == states;
824
  }
825

826
  typedef
827
828
  std::unordered_set<const spot::ltl::formula*,
		     const spot::ptr_hash<const spot::ltl::formula> > fset_t;
829
830


831
832
  class processor: public job_processor
  {
833
    spot::bdd_dict_ptr dict = spot::make_bdd_dict();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
834
    xtranslator_runner runner;
835
    fset_t unique_set;
836
  public:
837
838
    processor():
      runner(dict)
839
840
841
    {
    }

842
843
844
845
846
847
848
    ~processor()
    {
      fset_t::iterator i = unique_set.begin();
      while (i != unique_set.end())
	(*i++)->destroy();
    }

849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
    int
    process_string(const std::string& input,
		   const char* filename,
		   int linenum)
    {
      spot::ltl::parse_error_list pel;
      const spot::ltl::formula* f = parse_formula(input, pel);

      if (!f || !pel.empty())
	{
	  if (filename)
	    error_at_line(0, 0, filename, linenum, "parse error:");
	  spot::ltl::format_parse_errors(std::cerr, input, pel);
	  if (f)
	    f->destroy();
	  return 1;
	}
866
867

      f->clone();
868
869
870
871
      int res = process_formula(f, filename, linenum);

      if (res && bogus_output)
	*bogus_output << input << std::endl;
872
873
874
875
876
877
878
879
      if (res && grind_output)
	{
	  std::string bogus = input;
	  std::vector<const spot::ltl::formula*> mutations;
	  unsigned mutation_count;
	  unsigned mutation_max;
	  while	(res)
	    {
880
881
882
883
884
885
886
887
888
	      std::cerr << "Trying to find a bogus mutation of ";
	      if (color_opt)
		std::cerr << bright_blue;
	      std::cerr << bogus;
	      if (color_opt)
		std::cerr << reset_color;
	      std::cerr << "...\n";

	      mutations = mutate(f);
889
890
891
	      mutation_count = 1;
	      mutation_max = mutations.size();
	      res = 0;
892
	      for (auto g: mutations)
893
		{
894
895
		  std::cerr << "Mutation " << mutation_count << '/'
			    << mutation_max << ": ";
896
		  f->destroy();
897
898
899
900
		  f = g->clone();
		  res = process_formula(g->clone());
		  if (res)
		    break;
901
902
		  ++mutation_count;
		}
903
904
	      for (auto g: mutations)
		g->destroy();
905
906
907
908
909
910
911
912
913
914
	      if (res)
		{
		  if (lbt_input)
		    bogus = spot::ltl::to_lbt_string(f);
		  else
		    bogus = spot::ltl::to_string(f);
		  if (bogus_output)
		    *bogus_output << bogus << std::endl;
		}
	    }
915
	  std::cerr << "Smallest bogus mutation found for ";
916
917
918
919
920
	  if (color_opt)
	    std::cerr << bright_blue;
	  std::cerr << input;
	  if (color_opt)
	    std::cerr << reset_color;
921
	  std::cerr << " is ";
922
923
	  if (color_opt)
	    std::cerr << bright_blue;
924
	  std::cerr << bogus;
925
926
	  if (color_opt)
	    std::cerr << reset_color;
927
	  std::cerr << ".\n\n";
928
929
930
931
	  *grind_output << bogus << std::endl;
	}
      f->destroy();

932
933
934
935
      return 0;
    }


936
937
938
939
    int
    process_formula(const spot::ltl::formula* f,
		    const char* filename = 0, int linenum = 0)
    {
940
      static unsigned round = 0;
941

942
943
944
945
946
947
948
949
950
951
      // 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;
	}

952
953
      // ---------- Positive Formula ----------

954
      runner.round_formula(f, round);
955

956
957
958
      // Call formula() before printing anything else, in case it
      // complains.
      std::string fstr = runner.formula();
959
      if (filename)
960
	std::cerr << filename << ':';
961
      if (linenum)
962
	std::cerr << linenum << ':';
963
      if (filename || linenum)
964
	std::cerr << ' ';
965
      if (color_opt)
966
	std::cerr << bright_blue;
967
      std::cerr << fstr << '\n';
968
969
      if (color_opt)
	std::cerr << reset_color;
970

971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
      // 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;
	    }
	}

990
991
992

      int problems = 0;

993
994
      // These store the result of the translation of the positive and
      // negative formulas.
995
      size_t m = translators.size();
996
997
      std::vector<spot::const_tgba_digraph_ptr> pos(m);
      std::vector<spot::const_tgba_digraph_ptr> neg(m);
998
999
      // These store the complement of the above results, when we can
      // compute it easily.
1000
1001
      std::vector<spot::const_tgba_digraph_ptr> comp_pos(m);
      std::vector<spot::const_tgba_digraph_ptr> comp_neg(m);
1002

1003
1004

      unsigned n = vstats.size();
1005
      vstats.resize(n + (no_checks ? 1 : 2));
1006
      statistics_formula* pstats = &vstats[n];
1007
      statistics_formula* nstats = 0;
1008
      pstats->resize(m);
1009
1010
      formulas.push_back(fstr);

1011
      for (size_t n = 0; n < m; ++n)
1012
	{
1013
1014
1015
1016
	  bool prob;
	  pos[n] = runner.translate(n, 'P', pstats, prob);
	  problems += prob;

1017
1018
1019
1020
1021
1022
1023
	  // If the automaton is deterministic, compute its complement
	  // as well.  Note that if we have computed statistics
	  // already, there is no need to call is_deterministic()
	  // again.
	  if (!no_complement && pos[n]
	      && ((want_stats && !(*pstats)[n].nondeterministic)
		  || (!want_stats && is_deterministic(pos[n]))))
1024
	    comp_pos[n] = dtgba_complement(pos[n]);
1025
	}
1026
1027

      // ---------- Negative Formula ----------
1028

1029
1030
1031
      // The negative formula is only needed when checks are
      // activated.
      if (!no_checks)
1032
	{
1033
1034
	  nstats = &vstats[n + 1];
	  nstats->resize(m);
1035

1036
1037
	  const spot::ltl::formula* nf =
	    spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone());
1038

1039
1040
1041
1042
1043
1044
1045
1046
1047
	  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;
	    }
1048

1049
1050
	  runner.round_formula(nf, round);
	  formulas.push_back(runner.formula());
1051

1052
	  for (size_t n = 0; n < m; ++n)
1053
	    {
1054
1055
1056
1057
	      bool prob;
	      neg[n] = runner.translate(n, 'N', nstats, prob);
	      problems += prob;