ltlcross.cc 36.9 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
#define OPT_IGNORE_EXEC_FAIL 16
94
95
96
97

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

156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
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);

172
173
174
175
176
177
178
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;
static std::ofstream* bogus_output = 0;
static std::ofstream* grind_output = 0;
static bool verbose = false;
static bool ignore_exec_fail = false;
static unsigned ignored_exec_fail = 0;

static bool global_error_flag = false;
200
201
202
203
204

static std::ostream&
global_error()
{
  global_error_flag = true;
205
206
  if (color_opt)
    std::cerr << bright_red;
207
208
  return std::cerr;
}
209

210
211
212
213
214
215
216
217
218
static std::ostream&
example()
{
  if (color_opt)
    std::cerr << bright_yellow;
  return std::cerr;
}


219
220
221
222
223
224
225
226
static void
end_error()
{
  if (color_opt)
    std::cerr << reset_color;
}


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

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

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

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

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

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

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

484
    spot::const_tgba_digraph_ptr
485
486
    translate(unsigned int translator_num, char l, statistics_formula* fstats,
	      bool& problem)
487
488
489
490
    {
      output.reset(translator_num);

      std::ostringstream command;
491
      format(command, translators[translator_num].cmd);
492

493
      assert(output.format != printable_result_filename::None);
494

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

503
504
      const char* status_str = 0;

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

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

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

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

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

695
  static bool
696
697
  check_empty_prod(const spot::const_tgba_digraph_ptr& aut_i,
		   const spot::const_tgba_digraph_ptr& aut_j,
698
		   size_t i, size_t j, bool icomp, bool jcomp)
699
  {
700
    auto prod = spot::product(aut_i, aut_j);
701
    auto res = spot::couvreur99(prod)->check();
702

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

717
718
    if (res)
      {
719
720
721
	std::ostream& err = global_error();
	err << "error: ";
	if (icomp)
722
	  err << "Comp(N" << i << ')';
723
	else
724
	  err << 'P' << i;
725
	if (jcomp)
726
	  err << "*Comp(P" << j << ')';
727
728
729
	else
	  err << "*N" << j;
	err << " is nonempty";
730

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

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

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

825
  typedef std::set<unsigned> state_set;
826

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

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

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


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

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

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

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

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

958
959
960
961
      return 0;
    }


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

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

978
979
      // ---------- Positive Formula ----------

980
      runner.round_formula(f, round);
981

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

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

1016
1017
1018

      int problems = 0;

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

1029
1030

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

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

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

      // ---------- Negative Formula ----------
1054

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

1062
1063
	  const spot::ltl::formula* nf =
	    spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone());
1064

1065
1066
1067
1068
1069
1070
1071
1072
1073
	  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;
	    }
1074

1075
1076
	  runner.round_formula(nf, round);
	  formulas.push_back(runner.formula());
1077

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

1084
1085
1086
1087
1088
1089
1090
	      // 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 && neg[n]
		  && ((want_stats && !(*nstats)[n].nondeterministic)
		      || (!want_stats && is_deterministic(neg[n]))))
1091
		comp_neg[n] = dtgba_complement(neg[n]);
1092
	    }
1093
1094
	  nf->destroy();
	}