ltlcross.cc 35.6 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
		else if (!aut)
		  {
		    status_str = "empty output";
		    problem = true;
		    es = -1;
		    global_error() << "error: empty output.\n";
		    end_error();
		    res = nullptr;
		  }
610
611
612
613
614
		else if (aut->aborted)
		  {
		    status_str = "aborted";
		    problem = true;
		    es = -1;
615
		    global_error()  << "error: aborted HOA file.\n";
616
617
618
		    end_error();
		    res = nullptr;
		  }
619
620
621
622
623
624
		else
		  {
		    res = aut->aut;
		  }
		break;
	      }
625
	    case printable_result_filename::None:
626
	      SPOT_UNREACHABLE();
627
	    }
628
	}
629
630

      if (want_stats)
631
632
	{
	  statistics* st = &(*fstats)[translator_num];
633
634
	  st->status_str = status_str;
	  st->status_code = es;
635
	  st->time = duration;
636
637
638

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

677
  static bool
678
679
  check_empty_prod(const spot::const_tgba_digraph_ptr& aut_i,
		   const spot::const_tgba_digraph_ptr& aut_j,
680
		   size_t i, size_t j, bool icomp, bool jcomp)
681
  {
682
    auto prod = spot::product(aut_i, aut_j);
683
    auto res = spot::couvreur99(prod)->check();
684

685
686
687
688
689
690
    if (verbose)
      {
	std::cerr << "info: check_empty ";
	if (icomp)
	  std::cerr << "Comp(N" << i << ')';
	else
691
	  std::cerr << 'P' << i;
692
693
694
695
696
697
698
	if (jcomp)
	  std::cerr << "*Comp(P" << j << ')';
	else
	  std::cerr << "*N" << j;
	std::cerr << '\n';
      }

699
700
    if (res)
      {
701
702
703
	std::ostream& err = global_error();
	err << "error: ";
	if (icomp)
704
	  err << "Comp(N" << i << ')';
705
	else
706
	  err << 'P' << i;
707
	if (jcomp)
708
	  err << "*Comp(P" << j << ')';
709
710
711
	else
	  err << "*N" << j;
	err << " is nonempty";
712

713
	auto run = res->accepting_run();
714
715
	if (run)
	  {
716
	    run = reduce_run(prod, run);
717
718
	    std::cerr << "; both automata accept the infinite word\n"
		      << "       ";
719
	    spot::tgba_word w(run);
720
	    w.simplify();
721
	    w.print(example(), prod->get_dict()) << '\n';
722
723
724
	  }
	else
	  {
725
	    std::cerr << '\n';
726
727
728
	  }
	end_error();
      }
729
    return !!res;
730
731
  }

732
  static bool
733
  cross_check(const std::vector<spot::scc_info*>& maps, char l, unsigned p)
734
735
  {
    size_t m = maps.size();
736
737
738
739
740
741
742
743
744
745
746
747
    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;
	  }
748
	std::cerr << "}, state-space #" << p << '/' << products << '\n';
749
      }
750

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

807
  typedef std::set<unsigned> state_set;
808

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

823
  static bool
824
  consistency_check(const spot::scc_info* pos, const spot::scc_info* neg)
825
826
827
828
  {
    // the states of SSPACE should appear in the accepting SCC of at
    // least one of POS or NEG.  Maybe both.
    state_set s;
829
830
831
    states_in_acc(pos, s);
    states_in_acc(neg, s);
    return s.size() == states;
832
  }
833

834
  typedef
835
836
  std::unordered_set<const spot::ltl::formula*,
		     const spot::ptr_hash<const spot::ltl::formula> > fset_t;
837
838


839
840
  class processor: public job_processor
  {
841
    spot::bdd_dict_ptr dict = spot::make_bdd_dict();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
842
    xtranslator_runner runner;
843
    fset_t unique_set;
844
  public:
845
846
    processor():
      runner(dict)
847
848
849
    {
    }

850
851
852
853
854
855
856
    ~processor()
    {
      fset_t::iterator i = unique_set.begin();
      while (i != unique_set.end())
	(*i++)->destroy();
    }

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

      f->clone();
876
877
878
879
      int res = process_formula(f, filename, linenum);

      if (res && bogus_output)
	*bogus_output << input << std::endl;
880
881
882
883
884
885
886
887
      if (res && grind_output)
	{
	  std::string bogus = input;
	  std::vector<const spot::ltl::formula*> mutations;
	  unsigned mutation_count;
	  unsigned mutation_max;
	  while	(res)
	    {
888
889
890
891
892
893
894
895
896
	      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);
897
898
899
	      mutation_count = 1;
	      mutation_max = mutations.size();
	      res = 0;
900
	      for (auto g: mutations)
901
		{
902
903
		  std::cerr << "Mutation " << mutation_count << '/'
			    << mutation_max << ": ";
904
		  f->destroy();
905
906
907
908
		  f = g->clone();
		  res = process_formula(g->clone());
		  if (res)
		    break;
909
910
		  ++mutation_count;
		}
911
912
	      for (auto g: mutations)
		g->destroy();
913
914
915
916
917
918
919
920
921
922
	      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;
		}
	    }
923
	  std::cerr << "Smallest bogus mutation found for ";
924
925
926
927
928
	  if (color_opt)
	    std::cerr << bright_blue;
	  std::cerr << input;
	  if (color_opt)
	    std::cerr << reset_color;
929
	  std::cerr << " is ";
930
931
	  if (color_opt)
	    std::cerr << bright_blue;
932
	  std::cerr << bogus;
933
934
	  if (color_opt)
	    std::cerr << reset_color;
935
	  std::cerr << ".\n\n";
936
937
938
939
	  *grind_output << bogus << std::endl;
	}
      f->destroy();

940
941
942
943
      return 0;
    }


944
945
946
947
    int
    process_formula(const spot::ltl::formula* f,
		    const char* filename = 0, int linenum = 0)
    {
948
      static unsigned round = 0;
949

950
951
952
953
954
955
956
957
958
959
      // 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;
	}

960
961
      // ---------- Positive Formula ----------

962
      runner.round_formula(f, round);
963

964
965
966
      // Call formula() before printing anything else, in case it
      // complains.
      std::string fstr = runner.formula();
967
      if (filename)
968
	std::cerr << filename << ':';
969
      if (linenum)
970
	std::cerr << linenum << ':';
971
      if (filename || linenum)
972
	std::cerr << ' ';
973
      if (color_opt)
974
	std::cerr << bright_blue;
975
      std::cerr << fstr << '\n';
976
977
      if (color_opt)
	std::cerr << reset_color;
978

979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
      // 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;
	    }
	}

998
999
1000

      int problems = 0;

1001
1002
      // These store the result of the translation of the positive and
      // negative formulas.
1003
      size_t m = translators.size();
1004
1005
      std::vector<spot::const_tgba_digraph_ptr> pos(m);
      std::vector<spot::const_tgba_digraph_ptr> neg(m);
1006
1007
      // These store the complement of the above results, when we can
      // compute it easily.
1008
1009
      std::vector<spot::const_tgba_digraph_ptr> comp_pos(m);
      std::vector<spot::const_tgba_digraph_ptr> comp_neg(m);
1010

1011
1012

      unsigned n = vstats.size();
1013
      vstats.resize(n + (no_checks ? 1 : 2));
1014
      statistics_formula* pstats = &vstats[n];
1015
      statistics_formula* nstats = 0;
1016
      pstats->resize(m);
1017
1018
      formulas.push_back(fstr);

1019
      for (size_t n = 0; n < m; ++n)
1020
	{
1021
1022
1023
1024
	  bool prob;
	  pos[n] = runner.translate(n, 'P', pstats, prob);
	  problems += prob;

1025
1026
1027
1028
1029
1030
1031
	  // 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]))))
1032
	    comp_pos[n] = dtgba_complement(pos[n]);
1033
	}
1034
1035

      // ---------- Negative Formula ----------
1036

1037
1038
1039
      // The negative formula is only needed when checks are
      // activated.
      if (!no_checks)
1040
	{
1041
1042
	  nstats = &vstats[n + 1];
	  nstats->resize(m);
1043

1044
1045
	  const spot::ltl::formula* nf =
	    spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone());
1046

1047
1048
1049
1050
1051
1052
1053
1054
1055
	  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;
	    }
1056

1057
1058
	  runner.round_formula(nf, round);
	  formulas.push_back(runner.formula());