ltlcross.cc 38.2 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
26
27
28
//
// 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>
#include <cstdlib>
#include <cstdio>
#include <argp.h>
29
#include <unistd.h>
30
#include <sys/wait.h>
31
#include "error.h"
32
#include "argmatch.h"
33
34
35

#include "common_setup.hh"
#include "common_cout.hh"
36
#include "common_conv.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
37
#include "common_trans.hh"
38
#include "common_file.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
#include "tgbaalgos/remfin.hh"
51
52
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/randomgraph.hh"
53
#include "tgbaalgos/sccinfo.hh"
54
#include "tgbaalgos/isweakscc.hh"
55
56
#include "tgbaalgos/reducerun.hh"
#include "tgbaalgos/word.hh"
57
#include "tgbaalgos/dtgbacomp.hh"
58
#include "tgbaalgos/cleanacc.hh"
59
#include "misc/formater.hh"
60
61
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/isdet.hh"
62
#include "misc/escape.hh"
63
#include "misc/hash.hh"
64
#include "misc/random.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
65
#include "misc/tmpfile.hh"
66
#include "misc/timer.hh"
67
68
69

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

79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
enum {
  OPT_BOGUS = 256,
  OPT_COLOR,
  OPT_CSV,
  OPT_DENSITY,
  OPT_DUPS,
  OPT_GRIND,
  OPT_IGNORE_EXEC_FAIL,
  OPT_JSON,
  OPT_NOCHECKS,
  OPT_NOCOMP,
  OPT_OMIT,
  OPT_PRODUCTS,
  OPT_SEED,
  OPT_STATES,
  OPT_STOP_ERR,
  OPT_VERBOSE,
};
97
98
99
100

static const argp_option options[] =
  {
    /**************************************************/
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
101
    { 0, 0, 0, 0, "ltlcross behavior:", 5 },
102
103
104
105
106
    { "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 },
107
108
    { "no-complement", OPT_NOCOMP, 0, 0,
      "do not complement deterministic automata to perform extra checks", 0 },
109
110
111
    { "stop-on-error", OPT_STOP_ERR, 0, 0,
      "stop on first execution error or failure to pass"
      " sanity checks (timeouts are OK)", 0 },
112
113
114
    { "ignore-execution-failures", OPT_IGNORE_EXEC_FAIL, 0, 0,
      "ignore automata from translators that return with a non-zero exit code,"
      " but do not flag this as an error", 0 },
115
    /**************************************************/
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
116
    { 0, 0, 0, 0, "State-space generation:", 6 },
117
118
119
120
121
    { "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 },
122
123
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0 by default)", 0 },
124
125
126
    { "products", OPT_PRODUCTS, "[+]INT", 0,
      "number of products to perform (1 by default), statistics will be "
      "averaged unless the number is prefixed with '+'", 0 },
127
    /**************************************************/
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
128
    { 0, 0, 0, 0, "Statistics output:", 7 },
129
    { "json", OPT_JSON, "[>>]FILENAME", OPTION_ARG_OPTIONAL,
130
      "output statistics as JSON in FILENAME or on standard output", 0 },
131
132
133
134
    { "csv", OPT_CSV, "[>>]FILENAME", OPTION_ARG_OPTIONAL,
      "output statistics as CSV in FILENAME or on standard output "
      "(if '>>' is used to request append mode, the header line is "
      "not output)", 0 },
135
136
    { "omit-missing", OPT_OMIT, 0, 0,
      "do not output statistics for timeouts or failed translations", 0 },
137
    /**************************************************/
138
    { 0, 0, 0, 0, "Miscellaneous options:", -2 },
139
140
141
142
    { "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 },
143
    { "grind", OPT_GRIND, "[>>]FILENAME", 0,
144
145
      "for each formula for which a problem was detected, write a simpler " \
      "formula that fails on the same test in FILENAME", 0 },
146
    { "save-bogus", OPT_BOGUS, "[>>]FILENAME", 0,
147
      "save formulas for which problems were detected in FILENAME", 0 },
148
149
    { "verbose", OPT_VERBOSE, 0, 0,
      "print what is being done, for debugging", 0 },
150
151
    { 0, 0, 0, 0, "If an output FILENAME is prefixed with '>>', is it open "
      "in append mode instead of being truncated.", -1 },
152
153
154
155
156
157
    { 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
158
    { &trans_argp, 0, 0, 0 },
159
    { &misc_argp, 0, 0, -2 },
160
161
162
    { 0, 0, 0, 0 }
  };

163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
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);

179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
static color_type color_opt = color_if_tty;
static const char* bright_red = "\033[01;31m";
static const char* bright_blue = "\033[01;34m";
static const char* bright_yellow = "\033[01;33m";
static const char* reset_color = "\033[m";

static unsigned states = 200;
static float density = 0.1;
static const char* json_output = 0;
static const char* csv_output = 0;
static bool want_stats = false;
static bool allow_dups = false;
static bool no_checks = false;
static bool no_complement = false;
static bool stop_on_error = false;
static int seed = 0;
static unsigned products = 1;
static bool products_avg = true;
static bool opt_omit = false;
static bool has_sr = false; // Has Streett or Rabin automata to process.
static const char* bogus_output_filename = 0;
200
201
static output_file* bogus_output = 0;
static output_file* grind_output = 0;
202
203
204
205
206
static bool verbose = false;
static bool ignore_exec_fail = false;
static unsigned ignored_exec_fail = 0;

static bool global_error_flag = false;
207
208
209
210
211

static std::ostream&
global_error()
{
  global_error_flag = true;
212
213
  if (color_opt)
    std::cerr << bright_red;
214
215
  return std::cerr;
}
216

217
218
219
220
221
222
223
224
225
static std::ostream&
example()
{
  if (color_opt)
    std::cerr << bright_yellow;
  return std::cerr;
}


226
227
228
229
230
231
232
233
static void
end_error()
{
  if (color_opt)
    std::cerr << reset_color;
}


234
235
struct statistics
{
236
237
  statistics()
    : ok(false),
238
      has_in(false),
239
240
241
      status_str(0),
      status_code(0),
      time(0),
242
243
244
245
246
247
      in_type(0),
      in_states(0),
      in_edges(0),
      in_transitions(0),
      in_acc(0),
      in_scc(0),
248
      states(0),
249
      edges(0),
250
251
252
253
254
255
256
257
258
259
260
      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),
261
      strong_aut(false)
262
263
264
  {
  }

265
266
  // If OK is false, only the status_str, status_code, and time fields
  // should be valid.
267
  bool ok;
268
269
  // has in_* data to display.
  bool has_in;
270
271
272
  const char* status_str;
  int status_code;
  double time;
273
274
275
276
277
278
  const char* in_type;
  unsigned in_states;
  unsigned in_edges;
  unsigned in_transitions;
  unsigned in_acc;
  unsigned in_scc;
279
280
281
282
283
  unsigned states;
  unsigned edges;
  unsigned transitions;
  unsigned acc;
  unsigned scc;
284
285
286
287
  unsigned nonacc_scc;
  unsigned terminal_scc;
  unsigned weak_scc;
  unsigned strong_scc;
288
289
  unsigned nondetstates;
  bool nondeterministic;
290
291
292
  bool terminal_aut;
  bool weak_aut;
  bool strong_aut;
293
294
295
  std::vector<double> product_states;
  std::vector<double> product_transitions;
  std::vector<double> product_scc;
296
297

  static void
298
  fields(std::ostream& os, bool show_exit, bool show_sr)
299
  {
300
    if (show_exit)
301
      os << "\"exit_status\",\"exit_code\",";
302
303
304
305
306
    os << "\"time\",";
    if (show_sr)
      os << ("\"in_type\",\"in_states\",\"in_edges\",\"in_transitions\","
	     "\"in_acc\",\"in_scc\",");
    os << ("\"states\","
307
308
309
310
311
312
313
314
315
316
317
318
	   "\"edges\","
	   "\"transitions\","
	   "\"acc\","
	   "\"scc\","
	   "\"nonacc_scc\","
	   "\"terminal_scc\","
	   "\"weak_scc\","
	   "\"strong_scc\","
	   "\"nondet_states\","
	   "\"nondet_aut\","
	   "\"terminal_aut\","
	   "\"weak_aut\","
319
320
321
322
	   "\"strong_aut\"");
    size_t m = products_avg ? 1U : products;
    for (size_t i = 0; i < m; ++i)
      os << ",\"product_states\",\"product_transitions\",\"product_scc\"";
323
324
325
  }

  void
326
  to_csv(std::ostream& os, bool show_exit, bool show_sr, const char* na = "")
327
  {
328
    if (show_exit)
329
330
331
      os << '"' << status_str << "\"," << status_code << ',';
    os << time << ',';
    if (ok)
332
      {
333
334
335
336
337
338
339
340
341
342
	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 << ',';
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
368
369
370
371
372
373
374
375
376
377
378
379
	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);
	  }
      }
380
    else
381
382
      {
	size_t m = products_avg ? 1U : products;
383
384
385
	m *= 3;
	m += 13 + show_sr * 6;
	os << na;
386
	for (size_t i = 0; i < m; ++i)
387
	  os << ',' << na;
388
      }
389
390
391
392
393
394
395
396
  }
};

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

397
398
399
400
401
402
403
404
405
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;
406
407
    case OPT_BOGUS:
      {
408
	bogus_output = new output_file(arg);
409
410
411
	bogus_output_filename = arg;
	break;
      }
412
413
414
415
416
417
418
419
    case OPT_COLOR:
      {
	if (arg)
	  color_opt = XARGMATCH("--color", arg, color_args, color_types);
	else
	  color_opt = color_always;
	break;
      }
420
421
422
423
    case OPT_CSV:
      want_stats = true;
      csv_output = arg ? arg : "-";
      break;
424
425
426
    case OPT_DENSITY:
      density = to_probability(arg);
      break;
427
428
429
    case OPT_DUPS:
      allow_dups = true;
      break;
430
    case OPT_GRIND:
431
      grind_output = new output_file(arg);
432
      break;
433
434
435
    case OPT_IGNORE_EXEC_FAIL:
      ignore_exec_fail = true;
      break;
436
437
438
439
    case OPT_JSON:
      want_stats = true;
      json_output = arg ? arg : "-";
      break;
440
    case OPT_PRODUCTS:
441
442
443
444
445
      if (*arg == '+')
	{
	  products_avg = false;
	  ++arg;
	}
446
447
      products = to_pos_int(arg);
      break;
448
449
    case OPT_NOCHECKS:
      no_checks = true;
450
451
452
453
      no_complement = true;
      break;
    case OPT_NOCOMP:
      no_complement = true;
454
      break;
455
456
457
    case OPT_OMIT:
      opt_omit = true;
      break;
458
459
460
    case OPT_SEED:
      seed = to_pos_int(arg);
      break;
461
462
463
    case OPT_STATES:
      states = to_pos_int(arg);
      break;
464
465
466
    case OPT_STOP_ERR:
      stop_on_error = true;
      break;
467
468
469
    case OPT_VERBOSE:
      verbose = true;
      break;
470
471
472
473
474
475
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

476
namespace
477
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
478
  class xtranslator_runner: public translator_runner
479
480
  {
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
481
482
    xtranslator_runner(spot::bdd_dict_ptr dict)
      : translator_runner(dict)
483
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
484
      has_sr = has('D');
485
486
    }

487
    spot::tgba_digraph_ptr
488
489
    translate(unsigned int translator_num, char l, statistics_formula* fstats,
	      bool& problem)
490
491
492
493
    {
      output.reset(translator_num);

      std::ostringstream command;
494
      format(command, translators[translator_num].cmd);
495

496
      assert(output.format != printable_result_filename::None);
497

498
499
500
      std::string cmd = command.str();
      std::cerr << "Running [" << l << translator_num << "]: "
		<< cmd << std::endl;
501
502
      spot::stopwatch sw;
      sw.start();
503
      int es = exec_with_timeout(cmd.c_str());
504
      double duration = sw.stop();
505

506
507
      const char* status_str = 0;

508
      spot::tgba_digraph_ptr res = 0;
509
510
      if (timed_out)
	{
511
512
	  // This is not considered to be a global error.
	  std::cerr << "warning: timeout during execution of command\n";
513
	  ++timeout_count;
514
	  status_str = "timeout";
515
	  problem = false;	// A timeout is not a sign of a bug
516
	  es = -1;
517
518
519
	}
      else if (WIFSIGNALED(es))
	{
520
	  status_str = "signal";
521
	  problem = true;
522
	  es = WTERMSIG(es);
523
	  global_error() << "error: execution terminated by signal "
524
			 << es << ".\n";
525
	  end_error();
526
527
	}
      else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
528
	{
529
530
	  es = WEXITSTATUS(es);
	  status_str = "exit code";
531
532
533
534
535
536
537
538
539
540
541
542
543
544
	  if (!ignore_exec_fail)
	    {
	      problem = true;
	      global_error() << "error: execution returned exit code "
			     << es << ".\n";
	      end_error();
	    }
	  else
	    {
	      problem = false;
	      std::cerr << "warning: execution returned exit code "
			<< es << ".\n";
	      ++ignored_exec_fail;
	    }
545
546
547
	}
      else
	{
548
	  status_str = "ok";
549
	  problem = false;
550
	  es = 0;
551
552
	  switch (output.format)
	    {
553
554
555
556
	    case printable_result_filename::Dstar:
	      {
		spot::dstar_parse_error_list pel;
		std::string filename = output.val()->name();
557
		auto aut = spot::dstar_parse(filename, pel, dict);
558
559
		if (!pel.empty())
		  {
560
		    status_str = "parse error";
561
		    problem = true;
562
		    es = -1;
563
564
565
566
567
		    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();
568
		    res = nullptr;
569
570
		  }
		else
571
		  {
572
573
574
575
576
577
578
579
580
581
582
583
		    const char* type = 0;
		    switch (aut->type)
		      {
		      case spot::Rabin:
			type = "DRA";
			break;
		      case spot::Streett:
			type = "DSA";
			break;
		      }
		    assert(type);

584
585
586
587
588
		    // Gather statistics about the input automaton
		    if (want_stats)
		      {
			statistics* st = &(*fstats)[translator_num];
			st->has_in = true;
589
			st->in_type = type;
590
591
592
593
594
595
596
			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;

597
			st->in_scc = spot::scc_info(aut->aut).scc_count();
598
599
		      }
		    // convert it into TGBA for further processing
600
601
		    if (verbose)
		      std::cerr << "info: converting " << type << " to TGBA\n";
602
603
		    res = dstar_to_tgba(aut);
		  }
604
605
		break;
	      }
606
	    case printable_result_filename::Hoa: // Will also read neverclaims
607
608
609
610
611
612
613
614
615
616
	      {
		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();
617
		    err << "error: failed to parse the produced automaton.\n";
618
619
620
621
		    spot::format_hoa_parse_errors(err, filename, pel);
		    end_error();
		    res = nullptr;
		  }
622
623
624
625
626
627
628
629
630
		else if (!aut)
		  {
		    status_str = "empty output";
		    problem = true;
		    es = -1;
		    global_error() << "error: empty output.\n";
		    end_error();
		    res = nullptr;
		  }
631
632
633
634
635
		else if (aut->aborted)
		  {
		    status_str = "aborted";
		    problem = true;
		    es = -1;
636
		    global_error()  << "error: aborted HOA file.\n";
637
638
639
		    end_error();
		    res = nullptr;
		  }
640
641
642
643
644
645
		else
		  {
		    res = aut->aut;
		  }
		break;
	      }
646
	    case printable_result_filename::None:
647
	      SPOT_UNREACHABLE();
648
	    }
649
	}
650
651

      if (want_stats)
652
653
	{
	  statistics* st = &(*fstats)[translator_num];
654
655
	  st->status_str = status_str;
	  st->status_code = es;
656
	  st->time = duration;
657
658
659

	  // Compute statistics.
	  if (res)
660
	    {
661
662
	      if (verbose)
		std::cerr << "info: getting statistics\n";
663
664
665
666
667
	      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;
668
	      st->acc = res->acc().num_sets();
669
	      spot::scc_info m(res);
670
	      unsigned c = m.scc_count();
671
	      st->scc = c;
672
673
674
675
	      st->nondetstates = spot::count_nondet_states(res);
	      st->nondeterministic = st->nondetstates != 0;
	      for (unsigned n = 0; n < c; ++n)
		{
676
		  if (m.is_rejecting_scc(n))
677
678
679
680
681
682
683
684
685
686
687
688
		    ++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;
689
	      else
690
		st->terminal_aut = true;
691
	    }
692
	}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
693
      output.cleanup();
694
      return res;
695
    }
696
  };
697

698
  static bool
699
700
  check_empty_prod(const spot::const_tgba_digraph_ptr& aut_i,
		   const spot::const_tgba_digraph_ptr& aut_j,
701
		   size_t i, size_t j, bool icomp, bool jcomp)
702
  {
703
    auto prod = spot::product(aut_i, aut_j);
704

705
706
707
708
709
710
    if (verbose)
      {
	std::cerr << "info: check_empty ";
	if (icomp)
	  std::cerr << "Comp(N" << i << ')';
	else
711
	  std::cerr << 'P' << i;
712
713
714
715
716
717
718
	if (jcomp)
	  std::cerr << "*Comp(P" << j << ')';
	else
	  std::cerr << "*N" << j;
	std::cerr << '\n';
      }

719
    auto res = spot::couvreur99(prod)->check();
720
721
    if (res)
      {
722
723
724
	std::ostream& err = global_error();
	err << "error: ";
	if (icomp)
725
	  err << "Comp(N" << i << ')';
726
	else
727
	  err << 'P' << i;
728
	if (jcomp)
729
	  err << "*Comp(P" << j << ')';
730
731
732
	else
	  err << "*N" << j;
	err << " is nonempty";
733

734
	auto run = res->accepting_run();
735
736
	if (run)
	  {
737
	    run = reduce_run(prod, run);
738
739
	    std::cerr << "; both automata accept the infinite word\n"
		      << "       ";
740
	    spot::tgba_word w(run);
741
	    w.simplify();
742
	    w.print(example(), prod->get_dict()) << '\n';
743
744
745
	  }
	else
	  {
746
	    std::cerr << '\n';
747
748
749
	  }
	end_error();
      }
750
    return !!res;
751
752
  }

753
  static bool
754
  cross_check(const std::vector<spot::scc_info*>& maps, char l, unsigned p)
755
756
  {
    size_t m = maps.size();
757
758
759
760
761
762
763
764
765
766
767
768
    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;
	  }
769
	std::cerr << "}, state-space #" << p << '/' << products << '\n';
770
      }
771

772
773
774
775
    std::vector<bool> res(m);
    unsigned verified = 0;
    unsigned violated = 0;
    for (size_t i = 0; i < m; ++i)
776
      if (spot::scc_info* m = maps[i])
777
778
779
	{
	  // r == true iff the automaton i is accepting.
	  bool r = false;
780
781
	  for (auto& scc: *m)
	    if (scc.is_accepting())
782
783
784
785
	      {
		r = true;
		break;
	      }
786
787
788
789
790
791
792
	  res[i] = r;
	  if (r)
	    ++verified;
	  else
	    ++violated;
	}
    if (verified != 0 && violated != 0)
793
      {
794
795
	std::ostream& err = global_error();
	err << "error: {";
796
797
798
799
800
801
802
	bool first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && res[i])
	    {
	      if (first)
		first = false;
	      else
803
		err << ',';
804
	      err << l << i;
805
	    }
806
	err << "} disagree with {";
807
808
809
810
811
812
813
	first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && !res[i])
	    {
	      if (first)
		first = false;
	      else
814
		err << ',';
815
	      err << l << i;
816
	    }
817
818
	err << "} when evaluating ";
	if (products > 1)
819
	  err << "state-space #" << p << '/' << products << '\n';
820
	else
821
	  err << "the state-space\n";
822
	end_error();
823
	return true;
824
      }
825
    return false;
826
  }
827

828
  typedef std::set<unsigned> state_set;
829

830
  // Collect all the states of SSPACE that appear in the accepting SCCs
831
  // of PROD.  (Trivial SCCs are considered accepting.)
832
  static void
833
  states_in_acc(const spot::scc_info* m, state_set& s)
834
  {
835
    auto aut = m->get_aut();
836
    auto ps = aut->get_named_prop<const spot::product_states>("product-states");
837
838
839
    for (auto& scc: *m)
      if (scc.is_accepting() || scc.is_trivial())
	for (auto i: scc.states())
840
841
	  // Get the projection on sspace.
	  s.insert((*ps)[i].second);
842
  }
843

844
  static bool
845
  consistency_check(const spot::scc_info* pos, const spot::scc_info* neg)
846
847
848
849
  {
    // the states of SSPACE should appear in the accepting SCC of at
    // least one of POS or NEG.  Maybe both.
    state_set s;
850
851
852
    states_in_acc(pos, s);
    states_in_acc(neg, s);
    return s.size() == states;
853
  }
854

855
  typedef
856
857
  std::unordered_set<const spot::ltl::formula*,
		     const spot::ptr_hash<const spot::ltl::formula> > fset_t;
858
859


860
861
  class processor: public job_processor
  {
862
    spot::bdd_dict_ptr dict = spot::make_bdd_dict();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
863
    xtranslator_runner runner;
864
    fset_t unique_set;
865
  public:
866
867
    processor():
      runner(dict)
868
869
870
    {
    }

871
872
873
874
875
876
877
    ~processor()
    {
      fset_t::iterator i = unique_set.begin();
      while (i != unique_set.end())
	(*i++)->destroy();
    }

878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
    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;
	}
895
896

      f->clone();
897
898
899
      int res = process_formula(f, filename, linenum);

      if (res && bogus_output)
900
	bogus_output->ostream() << input << std::endl;
901
902
903
904
905
906
907
908
      if (res && grind_output)
	{
	  std::string bogus = input;
	  std::vector<const spot::ltl::formula*> mutations;
	  unsigned mutation_count;
	  unsigned mutation_max;
	  while	(res)
	    {
909
910
911
912
913
914
915
916
917
	      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);
918
919
920
	      mutation_count = 1;
	      mutation_max = mutations.size();
	      res = 0;
921
	      for (auto g: mutations)
922
		{
923
924
		  std::cerr << "Mutation " << mutation_count << '/'
			    << mutation_max << ": ";
925
		  f->destroy();
926
927
928
929
		  f = g->clone();
		  res = process_formula(g->clone());
		  if (res)
		    break;
930
931
		  ++mutation_count;
		}
932
933
	      for (auto g: mutations)
		g->destroy();
934
935
936
937
938
939
940
	      if (res)
		{
		  if (lbt_input)
		    bogus = spot::ltl::to_lbt_string(f);
		  else
		    bogus = spot::ltl::to_string(f);
		  if (bogus_output)
941
		    bogus_output->ostream() << bogus << std::endl;
942
943
		}
	    }
944
	  std::cerr << "Smallest bogus mutation found for ";
945
946
947
948
949
	  if (color_opt)
	    std::cerr << bright_blue;
	  std::cerr << input;
	  if (color_opt)
	    std::cerr << reset_color;
950
	  std::cerr << " is ";
951
952
	  if (color_opt)
	    std::cerr << bright_blue;
953
	  std::cerr << bogus;
954
955
	  if (color_opt)
	    std::cerr << reset_color;
956
	  std::cerr << ".\n\n";
957
	  grind_output->ostream() << bogus << std::endl;
958
959
960
	}
      f->destroy();

961
962
963
964
      return 0;
    }


965
966
967
968
    int
    process_formula(const spot::ltl::formula* f,
		    const char* filename = 0, int linenum = 0)
    {
969
      static unsigned round = 0;
970

971
972
973
974
975
976
977
978
979
980
      // 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;
	}

981
982
      // ---------- Positive Formula ----------

983
      runner.round_formula(f, round);
984

985
986
987
      // Call formula() before printing anything else, in case it
      // complains.
      std::string fstr = runner.formula();
988
      if (filename)
989
	std::cerr << filename << ':';
990
      if (linenum)
991
	std::cerr << linenum << ':';
992
      if (filename || linenum)
993
	std::cerr << ' ';
994
      if (color_opt)
995
	std::cerr << bright_blue;
996
      std::cerr << fstr << '\n';
997
998
      if (color_opt)
	std::cerr << reset_color;
999

1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
      // 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;
	    }
	}

1019
1020
1021

      int problems = 0;

1022
1023
      // These store the result of the translation of the positive and
      // negative formulas.
1024
      size_t m = translators.size();
1025
1026
      std::vector<spot::tgba_digraph_ptr> pos(m);
      std::vector<spot::tgba_digraph_ptr> neg(m);
1027
1028
      // These store the complement of the above results, when we can
      // compute it easily.
1029
1030
      std::vector<spot::tgba_digraph_ptr> comp_pos(m);
      std::vector<spot::tgba_digraph_ptr> comp_neg(m);
1031

1032
1033

      unsigned n = vstats.size();
1034
      vstats.resize(n + (no_checks ? 1 : 2));
1035
      statistics_formula* pstats = &vstats[n];
1036
      statistics_formula* nstats = 0;
1037
      pstats->resize(m);
1038
1039
      formulas.push_back(fstr);

1040
      for (size_t n = 0; n < m; ++n)
1041
	{
1042
1043
1044
1045
	  bool prob;
	  pos[n] = runner.translate(n, 'P', pstats, prob);
	  problems += prob;

1046
1047
1048
1049
1050
1051
1052
	  // 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]))))
1053
	    comp_pos[n] = dtgba_complement(pos[n]);
1054
	}
1055
1056

      // ---------- Negative Formula ----------
1057

1058
1059
1060
      // The negative formula is only needed when checks are
      // activated.
      if (!no_checks)
1061
	{
1062
1063
	  nstats = &vstats[n + 1];
	  nstats->resize(m);
1064

1065
1066
	  const spot::ltl::formula* nf =
	    spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone());
1067

1068
1069
1070
1071
1072
1073
1074
1075
1076
	  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;
	    }
1077

1078
1079
	  runner.round_formula(nf, round);
	  formulas.push_back(runner.formula());
1080

1081
	  for (size_t n = 0; n < m; ++n)
1082
	    {
1083
1084
1085
1086
	      bool prob;
	      neg[n] = runner.translate(n, 'N', nstats, prob);
	      problems += prob;

1087
1088