ltlcross.cc 38.3 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


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

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

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

178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198
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;
199 200
static output_file* bogus_output = 0;
static output_file* grind_output = 0;
201 202 203 204 205
static bool verbose = false;
static bool ignore_exec_fail = false;
static unsigned ignored_exec_fail = 0;

static bool global_error_flag = false;
206 207 208 209 210

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

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


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


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

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

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

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

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

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

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

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

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

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

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

505 506
      const char* status_str = 0;

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

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

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

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

718
    auto res = spot::couvreur99(prod)->check();
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
      int res = process_formula(f, filename, linenum);

      if (res && bogus_output)
899
	bogus_output->ostream() << 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
	      if (res)
		{
		  if (lbt_input)
		    bogus = spot::ltl::to_lbt_string(f);
		  else
		    bogus = spot::ltl::to_string(f);
		  if (bogus_output)
940
		    bogus_output->ostream() << bogus << std::endl;
941 942
		}
	    }