ltlcross.cc 49.2 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 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 <cmath>
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_file.hh"
40
#include "common_finput.hh"
41
#include "common_hoaread.hh"
42
#include "common_aoutput.hh"
43
#include "common_color.hh"
44 45 46 47 48 49 50 51 52 53 54 55 56 57
#include <spot/parseaut/public.hh>
#include <spot/tl/print.hh>
#include <spot/tl/apcollect.hh>
#include <spot/tl/mutation.hh>
#include <spot/tl/relabel.hh>
#include <spot/twaalgos/lbtt.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/gtec/gtec.hh>
#include <spot/twaalgos/randomgraph.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/isweakscc.hh>
#include <spot/twaalgos/word.hh>
58
#include <spot/twaalgos/dualize.hh>
59
#include <spot/twaalgos/cleanacc.hh>
60
#include <spot/twaalgos/alternation.hh>
61 62 63 64
#include <spot/misc/formater.hh>
#include <spot/twaalgos/stats.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/isunamb.hh>
65
#include <spot/twaalgos/postproc.hh>
66 67 68 69 70
#include <spot/misc/escape.hh>
#include <spot/misc/hash.hh>
#include <spot/misc/random.hh>
#include <spot/misc/tmpfile.hh>
#include <spot/misc/timer.hh>
71 72 73

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

83
enum {
84 85
  OPT_AMBIGUOUS = 256,
  OPT_AUTOMATA,
86
  OPT_BOGUS,
87 88 89
  OPT_CSV,
  OPT_DENSITY,
  OPT_DUPS,
90
  OPT_FAIL_ON_TIMEOUT,
91 92 93 94 95 96 97 98 99 100
  OPT_GRIND,
  OPT_IGNORE_EXEC_FAIL,
  OPT_JSON,
  OPT_NOCHECKS,
  OPT_NOCOMP,
  OPT_OMIT,
  OPT_PRODUCTS,
  OPT_SEED,
  OPT_STATES,
  OPT_STOP_ERR,
101
  OPT_STRENGTH,
102 103
  OPT_VERBOSE,
};
104 105 106 107

static const argp_option options[] =
  {
    /**************************************************/
108 109
    { nullptr, 0, nullptr, 0, "ltlcross behavior:", 5 },
    { "allow-dups", OPT_DUPS, nullptr, 0,
110
      "translate duplicate formulas in input", 0 },
111
    { "no-checks", OPT_NOCHECKS, nullptr, 0,
112 113
      "do not perform any sanity checks (negated formulas "
      "will not be translated)", 0 },
114
    { "no-complement", OPT_NOCOMP, nullptr, 0,
115
      "do not complement deterministic automata to perform extra checks", 0 },
116 117 118
    { "determinize", 'D', nullptr, 0,
      "determinize non-deterministic automata so that they"
      "can be complemented; also implicitly sets --products=0", 0 },
119
    { "stop-on-error", OPT_STOP_ERR, nullptr, 0,
120 121
      "stop on first execution error or failure to pass"
      " sanity checks (timeouts are OK)", 0 },
122
    { "ignore-execution-failures", OPT_IGNORE_EXEC_FAIL, nullptr, 0,
123 124
      "ignore automata from translators that return with a non-zero exit code,"
      " but do not flag this as an error", 0 },
125 126
    { "fail-on-timeout", OPT_FAIL_ON_TIMEOUT, nullptr, 0,
      "consider timeouts as errors", 0 },
127
    /**************************************************/
128
    { nullptr, 0, nullptr, 0, "State-space generation:", 6 },
129 130 131 132 133
    { "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 },
134 135
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0 by default)", 0 },
136 137 138
    { "products", OPT_PRODUCTS, "[+]INT", 0,
      "number of products to perform (1 by default), statistics will be "
      "averaged unless the number is prefixed with '+'", 0 },
139
    /**************************************************/
140
    { nullptr, 0, nullptr, 0, "Statistics output:", 7 },
141
    { "json", OPT_JSON, "[>>]FILENAME", OPTION_ARG_OPTIONAL,
142
      "output statistics as JSON in FILENAME or on standard output", 0 },
143 144 145 146
    { "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 },
147
    { "omit-missing", OPT_OMIT, nullptr, 0,
148
      "do not output statistics for timeouts or failed translations", 0 },
149
    { "automata", OPT_AUTOMATA, nullptr, 0,
150
      "store automata (in the HOA format) into the CSV or JSON output", 0 },
151 152
    { "strength", OPT_STRENGTH, nullptr, 0,
      "output statistics about SCC strengths (non-accepting, terminal, weak, "
153
      "strong) [not supported for alternating automata]", 0 },
154
    { "ambiguous", OPT_AMBIGUOUS, nullptr, 0,
155 156
      "output statistics about ambiguous automata "
      "[not supported for alternating automata]", 0 },
157
    { "unambiguous", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
158
    /**************************************************/
159
    { nullptr, 0, nullptr, 0, "Output options:", -15 },
160
    { "grind", OPT_GRIND, "[>>]FILENAME", 0,
161 162
      "for each formula for which a problem was detected, write a simpler " \
      "formula that fails on the same test in FILENAME", 0 },
163
    { "save-bogus", OPT_BOGUS, "[>>]FILENAME", 0,
164
      "save formulas for which problems were detected in FILENAME", 0 },
165
    { "verbose", OPT_VERBOSE, nullptr, 0,
166
      "print what is being done, for debugging", 0 },
167
    { nullptr, 0, nullptr, 0,
168 169 170 171
      "If an output FILENAME is prefixed with '>>', it is open "
      "in append mode instead of being truncated.", -14 },
    /**************************************************/
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
172
    { nullptr, 0, nullptr, 0, nullptr, 0 }
173 174 175 176
  };

const struct argp_child children[] =
  {
177 178
    { &finput_argp, 0, nullptr, 1 },
    { &trans_argp, 0, nullptr, 0 },
179
    { &hoaread_argp, 0, "Parsing of automata:", 4 },
180
    { &color_argp, 0, nullptr, 0 },
181
    { &misc_argp, 0, nullptr, -1 },
182
    { nullptr, 0, nullptr, 0 }
183 184
  };

185 186
static unsigned states = 200;
static float density = 0.1;
187 188
static const char* json_output = nullptr;
static const char* csv_output = nullptr;
189 190 191 192
static bool want_stats = false;
static bool allow_dups = false;
static bool no_checks = false;
static bool no_complement = false;
193
static bool determinize = false;
194 195 196 197 198
static bool stop_on_error = false;
static int seed = 0;
static unsigned products = 1;
static bool products_avg = true;
static bool opt_omit = false;
199 200 201
static const char* bogus_output_filename = nullptr;
static output_file* bogus_output = nullptr;
static output_file* grind_output = nullptr;
202 203 204
static bool verbose = false;
static bool ignore_exec_fail = false;
static unsigned ignored_exec_fail = 0;
205
static bool fail_on_timeout = false;
206
static bool opt_automata = false;
207 208
static bool opt_strength = false;
static bool opt_ambiguous = false;
209 210

static bool global_error_flag = false;
211
static unsigned oom_count = 0U;
212 213 214 215 216

static std::ostream&
global_error()
{
  global_error_flag = true;
217
  std::cerr << bright_red;
218 219
  return std::cerr;
}
220

221 222 223
static std::ostream&
example()
{
224
  std::cerr << bold_std;
225 226 227
  return std::cerr;
}

228 229 230
static void
end_error()
{
231
  std::cerr << reset_color;
232 233 234
}


235 236
struct statistics
{
237 238
  statistics()
    : ok(false),
239
      alternating(false),
240
      status_str(nullptr),
241 242
      status_code(0),
      time(0),
243
      states(0),
244
      edges(0),
245 246 247 248 249 250 251 252 253 254 255
      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),
256
      strong_aut(false)
257 258 259
  {
  }

260 261
  // If OK is false, only the status_str, status_code, and time fields
  // should be valid.
262
  bool ok;
263
  bool alternating;
264 265 266
  const char* status_str;
  int status_code;
  double time;
267 268 269 270 271
  unsigned states;
  unsigned edges;
  unsigned transitions;
  unsigned acc;
  unsigned scc;
272 273 274 275
  unsigned nonacc_scc;
  unsigned terminal_scc;
  unsigned weak_scc;
  unsigned strong_scc;
276 277
  unsigned nondetstates;
  bool nondeterministic;
278 279 280
  bool terminal_aut;
  bool weak_aut;
  bool strong_aut;
281 282 283
  std::vector<double> product_states;
  std::vector<double> product_transitions;
  std::vector<double> product_scc;
284
  bool ambiguous;
285
  bool complete;
286
  std::string hoa_str;
287 288

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

  void
321
  to_csv(std::ostream& os, bool show_exit, const char* na = "",
322
         bool csv_escape = true)
323
  {
324
    if (show_exit)
325 326 327
      os << '"' << status_str << "\"," << status_code << ',';
    os << time << ',';
    if (ok)
328
      {
329 330 331 332
        os << states << ','
           << edges << ','
           << transitions << ','
           << acc << ','
333 334
           << scc << ',';
        if (opt_strength)
335 336 337 338 339 340 341 342 343
          {
            if (alternating)
              os << ",,,,";
            else
              os << nonacc_scc << ','
                 << terminal_scc << ','
                 << weak_scc << ','
                 << strong_scc << ',';
          }
344 345 346
        os << nondetstates << ','
           << nondeterministic << ',';
        if (opt_strength)
347 348 349 350 351 352 353 354
          {
            if (alternating)
              os << ",,,";
            else
              os << terminal_aut << ','
                 << weak_aut << ','
                 << strong_aut << ',';
          }
355
        if (opt_ambiguous)
356 357 358 359 360 361
          {
            if (alternating)
              os << ',';
            else
              os << ambiguous << ',';
          }
362
        os << complete;
363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384
        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);
          }
385
      }
386
    else
387
      {
388 389
        size_t m = products_avg ? 1U : products;
        m *= 3;
390 391 392 393 394
        m += 7;
        if (opt_strength)
          m += 7;
        if (opt_ambiguous)
          ++m;
395 396 397
        os << na;
        for (size_t i = 0; i < m; ++i)
          os << ',' << na;
398
      }
399 400
    if (opt_automata)
      {
401 402 403 404 405 406 407
        os << ',';
        if (hoa_str.empty())
          os << na;
        else if (csv_escape)
          spot::escape_rfc4180(os << '"', hoa_str) << '"';
        else
          spot::escape_str(os << '"', hoa_str) << '"';
408
      }
409 410 411 412 413 414 415 416
  }
};

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

417 418 419 420 421 422
static int
parse_opt(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
423 424 425 426
    case 'D':
      determinize = true;
      products = 0;
      break;
427
    case ARGP_KEY_ARG:
428 429 430
      if (arg[0] == '-' && !arg[1])
        jobs.emplace_back(arg, true);
      else
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
431
        tools_push_trans(arg);
432
      break;
433 434 435
    case OPT_AUTOMATA:
      opt_automata = true;
      break;
436 437
    case OPT_BOGUS:
      {
438 439 440
        bogus_output = new output_file(arg);
        bogus_output_filename = arg;
        break;
441
      }
442 443 444 445
    case OPT_CSV:
      want_stats = true;
      csv_output = arg ? arg : "-";
      break;
446 447 448
    case OPT_DENSITY:
      density = to_probability(arg);
      break;
449 450 451
    case OPT_DUPS:
      allow_dups = true;
      break;
452 453 454
    case OPT_FAIL_ON_TIMEOUT:
      fail_on_timeout = true;
      break;
455
    case OPT_GRIND:
456
      grind_output = new output_file(arg);
457
      break;
458 459 460
    case OPT_IGNORE_EXEC_FAIL:
      ignore_exec_fail = true;
      break;
461 462 463 464
    case OPT_JSON:
      want_stats = true;
      json_output = arg ? arg : "-";
      break;
465
    case OPT_PRODUCTS:
466
      if (*arg == '+')
467 468 469 470
        {
          products_avg = false;
          ++arg;
        }
471
      products = to_pos_int(arg);
472 473
      if (products == 0)
        products_avg = false;
474
      break;
475 476
    case OPT_NOCHECKS:
      no_checks = true;
477 478 479 480
      no_complement = true;
      break;
    case OPT_NOCOMP:
      no_complement = true;
481
      break;
482 483 484
    case OPT_OMIT:
      opt_omit = true;
      break;
485 486 487
    case OPT_SEED:
      seed = to_pos_int(arg);
      break;
488 489 490
    case OPT_STATES:
      states = to_pos_int(arg);
      break;
491 492 493
    case OPT_STOP_ERR:
      stop_on_error = true;
      break;
494 495 496 497 498 499
    case OPT_STRENGTH:
      opt_strength = true;
      break;
    case OPT_AMBIGUOUS:
      opt_ambiguous = true;
      break;
500 501 502
    case OPT_VERBOSE:
      verbose = true;
      break;
503 504 505 506 507 508
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

509
namespace
510
{
511
  class xtranslator_runner final: public translator_runner
512 513
  {
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
514 515
    xtranslator_runner(spot::bdd_dict_ptr dict)
      : translator_runner(dict)
516 517 518
    {
    }

519
    spot::twa_graph_ptr
520
    translate(unsigned int translator_num, char l, statistics_formula* fstats,
521
              bool& problem)
522 523 524 525
    {
      output.reset(translator_num);

      std::ostringstream command;
526
      format(command, tools[translator_num].cmd);
527

528 529
      std::string cmd = command.str();
      std::cerr << "Running [" << l << translator_num << "]: "
530
                << cmd << std::endl;
531
      spot::process_timer timer;
532
      timer.start();
533
      int es = exec_with_timeout(cmd.c_str());
534
      timer.stop();
535
      const char* status_str = nullptr;
536

537
      spot::twa_graph_ptr res = nullptr;
538
      if (timed_out)
539
        {
540 541 542 543 544 545 546 547 548 549
          if (fail_on_timeout)
            {
              global_error() << "error: timeout during execution of command\n";
              end_error();
            }
          else
            {
              std::cerr << "warning: timeout during execution of command\n";
              ++timeout_count;
            }
550
          status_str = "timeout";
551
          problem = fail_on_timeout;
552 553
          es = -1;
        }
554
      else if (WIFSIGNALED(es))
555 556 557 558 559 560 561 562
        {
          status_str = "signal";
          problem = true;
          es = WTERMSIG(es);
          global_error() << "error: execution terminated by signal "
                         << es << ".\n";
          end_error();
        }
563
      else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581
        {
          es = WEXITSTATUS(es);
          status_str = "exit code";
          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;
            }
        }
582
      else
583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615
        {
          status_str = "ok";
          problem = false;
          es = 0;

          auto aut = spot::parse_aut(output.val()->name(), dict,
                                     spot::default_environment::instance(),
                                     opt_parse);
          if (!aut->errors.empty())
            {
              status_str = "parse error";
              problem = true;
              es = -1;
              std::ostream& err = global_error();
              err << "error: failed to parse the produced automaton.\n";
              aut->format_errors(err);
              end_error();
              res = nullptr;
            }
          else if (aut->aborted)
            {
              status_str = "aborted";
              problem = true;
              es = -1;
              global_error()  << "error: aborted HOA file.\n";
              end_error();
              res = nullptr;
            }
          else
            {
              res = aut->aut;
            }
        }
616 617

      if (want_stats)
618 619 620 621
        {
          statistics* st = &(*fstats)[translator_num];
          st->status_str = status_str;
          st->status_code = es;
622
          st->time = timer.walltime();
623 624 625 626 627 628 629

          // Compute statistics.
          if (res)
            {
              if (verbose)
                std::cerr << "info: getting statistics\n";
              st->ok = true;
630
              st->alternating = !res->is_existential();
631 632 633 634 635
              spot::twa_sub_statistics s = sub_stats_reachable(res);
              st->states = s.states;
              st->edges = s.edges;
              st->transitions = s.transitions;
              st->acc = res->acc().num_sets();
636 637 638 639
              spot::scc_info
                m(res, (opt_strength
                        ? spot::scc_info_options::TRACK_STATES
                        : spot::scc_info_options::NONE));
640 641 642 643
              unsigned c = m.scc_count();
              st->scc = c;
              st->nondetstates = spot::count_nondet_states(res);
              st->nondeterministic = st->nondetstates != 0;
644
              if (opt_strength && !st->alternating)
645
                {
646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661
                  m.determine_unknown_acceptance();
                  for (unsigned n = 0; n < c; ++n)
                    {
                      if (m.is_rejecting_scc(n))
                        ++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;
662
                  else
663
                    st->terminal_aut = true;
664
                }
665
              if (opt_ambiguous && !st->alternating)
666
                st->ambiguous = !spot::is_unambiguous(res);
667 668 669 670 671 672 673 674 675 676
              st->complete = spot::is_complete(res);

              if (opt_automata)
                {
                  std::ostringstream os;
                  spot::print_hoa(os, res, "l");
                  st->hoa_str = os.str();
                }
            }
        }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
677
      output.cleanup();
678
      return res;
679
    }
680
  };
681

682
  static bool
683
  check_empty_prod(const spot::const_twa_graph_ptr& aut_i,
684 685
                   const spot::const_twa_graph_ptr& aut_j,
                   size_t i, size_t j, bool icomp, bool jcomp)
686
  {
687
    if (aut_i->num_sets() + aut_j->num_sets()
688
        > 8 * sizeof(spot::acc_cond::mark_t::value_t))
689
      {
690 691 692 693 694 695 696 697 698 699 700 701 702 703 704
        // Report the skipped test if both automata are not
        // complemented, or the --verbose option is used,
        if (!verbose && (icomp || jcomp))
          return false;
        std::cerr << "info: building ";
        if (icomp)
          std::cerr << "Comp(N" << i << ')';
        else
          std::cerr << 'P' << i;
        if (jcomp)
          std::cerr << "*Comp(P" << j << ')';
        else
          std::cerr << "*N" << j;
        std::cerr << " requires more acceptance sets than supported\n";
        return false;
705 706
      }

707
    auto prod = spot::product(aut_i, aut_j);
708

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

723 724
    auto w = prod->accepting_word();
    if (w)
725
      {
726 727 728 729 730 731 732 733 734 735
        std::ostream& err = global_error();
        err << "error: ";
        if (icomp)
          err << "Comp(N" << i << ')';
        else
          err << 'P' << i;
        if (jcomp)
          err << "*Comp(P" << j << ')';
        else
          err << "*N" << j;
736
        err << " is nonempty; both automata accept the infinite word:\n"
737 738
            << "       ";
        example() << *w << '\n';
739
        end_error();
740
      }
741
    return !!w;
742 743
  }

744
  static bool
745
  cross_check(const std::vector<spot::scc_info*>& maps, char l, unsigned p)
746 747
  {
    size_t m = maps.size();
748 749
    if (verbose)
      {
750 751 752 753 754 755 756 757 758 759 760 761
        std::cerr << "info: cross_check {";
        bool first = true;
        for (size_t i = 0; i < m; ++i)
          if (maps[i])
            {
              if (first)
                first = false;
              else
                std::cerr << ',';
              std::cerr << l << i;
            }
        std::cerr << "}, state-space #" << p << '/' << products << '\n';
762
      }
763

764 765 766 767
    std::vector<bool> res(m);
    unsigned verified = 0;
    unsigned violated = 0;
    for (size_t i = 0; i < m; ++i)
768
      if (spot::scc_info* m = maps[i])
769
        {
770 771 772
          bool i_is_accepting = m->one_accepting_scc() >= 0;
          res[i] = i_is_accepting;
          if (i_is_accepting)
773 774 775 776
            ++verified;
          else
            ++violated;
        }
777
    if (verified != 0 && violated != 0)
778
      {
779 780 781 782 783 784 785 786 787 788 789 790 791
        std::ostream& err = global_error();
        err << "error: {";
        bool first = true;
        for (size_t i = 0; i < m; ++i)
          if (maps[i] && res[i])
            {
              if (first)
                first = false;
              else
                err << ',';
              err << l << i;
            }
        err << "} disagree with {";
792
        std::ostringstream os;
793 794 795 796 797 798 799
        first = true;
        for (size_t i = 0; i < m; ++i)
          if (maps[i] && !res[i])
            {
              if (first)
                first = false;
              else
800 801
                os << ',';
              os << l << i;
802
            }
803
        err << os.str() << "} when evaluating ";
804 805 806 807
        if (products > 1)
          err << "state-space #" << p << '/' << products << '\n';
        else
          err << "the state-space\n";
808 809 810 811 812 813 814 815
        err << "       the following word(s) are not accepted by {"
            << os.str() << "}:\n";
        for (size_t i = 0; i < m; ++i)
          if (maps[i] && res[i])
            {
              global_error() << "  " << l << i << " accepts: ";
              example() << *maps[i]->get_aut()->accepting_word() << '\n';
            }
816 817
        end_error();
        return true;
818
      }
819
    return false;
820
  }
821

822
  typedef std::set<unsigned> state_set;
823

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

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

849
  typedef
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
850
  std::unordered_set<spot::formula> fset_t;
851

852
  class processor final: public job_processor
853
  {
854
    spot::bdd_dict_ptr dict = spot::make_bdd_dict();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
855
    xtranslator_runner runner;
856
    fset_t unique_set;
857
  public:
858 859
    processor():
      runner(dict)
860 861 862
    {
    }

863 864
    int
    process_string(const std::string& input,
865
                   const char* filename,
866
                   int linenum) override
867
    {
868 869
      auto pf = parse_formula(input);
      if (!pf.f || !pf.errors.empty())
870 871 872 873 874 875
        {
          if (filename)
            error_at_line(0, 0, filename, linenum, "parse error:");
          pf.format_errors(std::cerr);
          return 1;
        }
876
      auto f = pf.f;
877

878 879 880
      int res = process_formula(f, filename, linenum);

      if (res && bogus_output)
881
        bogus_output->ostream() << input << std::endl;
882
      if (res && grind_output)
883 884 885 886 887 888 889
        {
          std::string bogus = input;
          std::vector<spot::formula> mutations;
          unsigned mutation_count;
          unsigned mutation_max;
          while        (res)
            {
890 891
              std::cerr << "Trying to find a bogus mutation of " << bold
                        << bogus << reset_color << "...\n";
892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915
              mutations = mutate(f);
              mutation_count = 1;
              mutation_max = mutations.size();
              res = 0;
              for (auto g: mutations)
                {
                  std::cerr << "Mutation " << mutation_count << '/'
                            << mutation_max << ": ";
                  f = g;
                  res = process_formula(g);
                  if (res)
                    break;
                  ++mutation_count;
                }
              if (res)
                {
                  if (lbt_input)
                    bogus = spot::str_lbt_ltl(f);
                  else
                    bogus = spot::str_psl(f);
                  if (bogus_output)
                    bogus_output->ostream() << bogus << std::endl;
                }
            }
916 917 918
          std::cerr << "Smallest bogus mutation found for "
                    << bold << input << reset_color << " is "
                    << bold << bogus << reset_color << ".\n\n";
919 920
          grind_output->ostream() << bogus << std::endl;
        }
921 922 923
      return 0;
    }

924
    void product_stats(statistics_formula* stats, unsigned i,
925
                        spot::scc_info* sm)
926 927
    {
      if (verbose && sm)
928 929
        std::cerr << "info:               " << sm->scc_count()
                  << " SCCs\n";
930 931
      // Statistics
      if (want_stats)
932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947
        {
          if (sm)
            {
              (*stats)[i].product_scc.push_back(sm->scc_count());
              spot::twa_statistics s = spot::stats_reachable(sm->get_aut());
              (*stats)[i].product_states.push_back(s.states);
              (*stats)[i].product_transitions.push_back(s.edges);
            }
          else
            {
              double n = nan("");
              (*stats)[i].product_scc.push_back(n);
              (*stats)[i].product_states.push_back(n);
              (*stats)[i].product_transitions.push_back(n);
            }
        }
948
    }
949

950
    int
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
951
    process_formula(spot::formula f,
952
                    const char* filename = nullptr, int linenum = 0) override
953
    {
954
      static unsigned round = 0;
955

956 957 958 959 960 961
      if (opt_relabel
          // If we need LBT atomic proposition in any of the input or
          // output, relabel the formula.
          ||  (!f.has_lbt_atomic_props() &&
               (runner.has('l') || runner.has('L') || runner.has('T')))
          // Likewise for Spin
962 963
          || (!f.has_spin_atomic_props() &&
              (runner.has('s') || runner.has('S'))))
964
        f = spot::relabel(f, spot::Pnn);
965

966 967
      // ---------- Positive Formula ----------

968
      runner.round_formula(f, round);
969

970 971 972
      // Call formula() before printing anything else, in case it
      // complains.
      std::string fstr = runner.formula();
973
      if (filename)
974
        std::cerr << filename << ':';
975
      if (linenum)
976
        std::cerr << linenum << ':';
977
      if (filename || linenum)
978
        std::cerr << ' ';