ltlcross.cc 36 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 "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_finput.hh"
39
#include "dstarparse/public.hh"
40
#include "hoaparse/public.hh"
41
42
43
#include "ltlast/unop.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/apcollect.hh"
44
#include "ltlvisit/mutation.hh"
45
#include "ltlvisit/relabel.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
46
#include "ltlvisit/lbt.hh"
47
#include "tgbaalgos/lbtt.hh"
48
#include "tgbaalgos/product.hh"
49
50
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/randomgraph.hh"
51
#include "tgbaalgos/sccinfo.hh"
52
#include "tgbaalgos/isweakscc.hh"
53
54
#include "tgbaalgos/reducerun.hh"
#include "tgbaalgos/word.hh"
55
#include "tgbaalgos/dtgbacomp.hh"
56
#include "misc/formater.hh"
57
58
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/isdet.hh"
59
#include "misc/escape.hh"
60
#include "misc/hash.hh"
61
#include "misc/random.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
62
#include "misc/tmpfile.hh"
63
#include "misc/timer.hh"
64
65
66

const char argp_program_doc[] ="\
Call several LTL/PSL translators and cross-compare their output to detect \
67
bugs, or to gather statistics.  The list of formulas to use should be \
68
supplied on standard input, or using the -f or -F options.\v\
69
70
71
72
Exit status:\n\
  0  everything went fine (timeouts are OK too)\n\
  1  some translator failed to output something we understand, or failed\n\
     sanity checks (statistics were output nonetheless)\n\
73
  2  ltlcross aborted on error\n\
74
";
75
76
77
78


#define OPT_STATES 1
#define OPT_DENSITY 2
79
80
#define OPT_JSON 3
#define OPT_CSV 4
81
#define OPT_DUPS 5
82
#define OPT_NOCHECKS 6
83
#define OPT_STOP_ERR 7
84
#define OPT_SEED 8
85
#define OPT_PRODUCTS 9
86
#define OPT_COLOR 10
87
#define OPT_NOCOMP 11
88
#define OPT_OMIT 12
89
#define OPT_BOGUS 13
90
#define OPT_VERBOSE 14
91
#define OPT_GRIND 15
92
93
94
95

static const argp_option options[] =
  {
    /**************************************************/
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
96
    { 0, 0, 0, 0, "ltlcross behavior:", 5 },
97
98
99
100
101
    { "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 },
102
103
    { "no-complement", OPT_NOCOMP, 0, 0,
      "do not complement deterministic automata to perform extra checks", 0 },
104
105
106
    { "stop-on-error", OPT_STOP_ERR, 0, 0,
      "stop on first execution error or failure to pass"
      " sanity checks (timeouts are OK)", 0 },
107
    /**************************************************/
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
108
    { 0, 0, 0, 0, "State-space generation:", 6 },
109
110
111
112
113
    { "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 },
114
115
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0 by default)", 0 },
116
117
118
    { "products", OPT_PRODUCTS, "[+]INT", 0,
      "number of products to perform (1 by default), statistics will be "
      "averaged unless the number is prefixed with '+'", 0 },
119
    /**************************************************/
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
120
    { 0, 0, 0, 0, "Statistics output:", 7 },
121
122
123
124
    { "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 },
125
126
    { "omit-missing", OPT_OMIT, 0, 0,
      "do not output statistics for timeouts or failed translations", 0 },
127
    /**************************************************/
128
    { 0, 0, 0, 0, "Miscellaneous options:", -1 },
129
130
131
132
    { "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 },
133
134
135
    { "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 },
136
137
    { "save-bogus", OPT_BOGUS, "FILENAME", 0,
      "save formulas for which problems were detected in FILENAME", 0 },
138
139
    { "verbose", OPT_VERBOSE, 0, 0,
      "print what is being done, for debugging", 0 },
140
141
142
143
144
145
    { 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
146
    { &trans_argp, 0, 0, 0 },
147
    { &misc_argp, 0, 0, -1 },
148
149
150
    { 0, 0, 0, 0 }
  };

151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
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";
169
const char* bright_blue = "\033[01;34m";
170
const char* bright_yellow = "\033[01;33m";
171
172
const char* reset_color = "\033[m";

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


193
194
195
196
197
198
bool global_error_flag = false;

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

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


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


221
222
struct statistics
{
223
224
  statistics()
    : ok(false),
225
      has_in(false),
226
227
228
      status_str(0),
      status_code(0),
      time(0),
229
230
231
232
233
234
      in_type(0),
      in_states(0),
      in_edges(0),
      in_transitions(0),
      in_acc(0),
      in_scc(0),
235
      states(0),
236
      edges(0),
237
238
239
240
241
242
243
244
245
246
247
      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),
248
      strong_aut(false)
249
250
251
  {
  }

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

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

  void
313
  to_csv(std::ostream& os, bool show_exit, bool show_sr, const char* na = "")
314
  {
315
    if (show_exit)
316
317
318
      os << '"' << status_str << "\"," << status_code << ',';
    os << time << ',';
    if (ok)
319
      {
320
321
322
323
324
325
326
327
328
329
	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 << ',';
330
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
	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);
	  }
      }
367
    else
368
369
      {
	size_t m = products_avg ? 1U : products;
370
371
372
	m *= 3;
	m += 13 + show_sr * 6;
	os << na;
373
	for (size_t i = 0; i < m; ++i)
374
	  os << ',' << na;
375
      }
376
377
378
379
380
381
382
383
  }
};

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

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

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

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

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

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

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

494
495
      const char* status_str = 0;

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

591
592
593
594
595
		    // Gather statistics about the input automaton
		    if (want_stats)
		      {
			statistics* st = &(*fstats)[translator_num];
			st->has_in = true;
596
			st->in_type = type;
597
598
599
600
601
602
603
			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;

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

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

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

697
  static bool
698
699
  check_empty_prod(const spot::const_tgba_digraph_ptr& aut_i,
		   const spot::const_tgba_digraph_ptr& aut_j,
700
		   size_t i, size_t j, bool icomp, bool jcomp)
701
  {
702
    auto prod = spot::product(aut_i, aut_j);
703
    auto res = spot::couvreur99(prod)->check();
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
720
    if (res)
      {
721
722
723
	std::ostream& err = global_error();
	err << "error: ";
	if (icomp)
724
	  err << "Comp(N" << i << ')';
725
	else
726
	  err << 'P' << i;
727
	if (jcomp)
728
	  err << "*Comp(P" << j << ')';
729
730
731
	else
	  err << "*N" << j;
	err << " is nonempty";
732

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

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

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

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

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

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

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


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

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

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

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

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

960
961
962
963
      return 0;
    }


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

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

980
981
      // ---------- Positive Formula ----------

982
      runner.round_formula(f, round);
983

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

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

1018
1019
1020

      int problems = 0;

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

1031
1032

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

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

1045
1046
1047
1048
1049
1050
1051
	  // 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]))))
Alexandre Duret-Lutz's avatar