autcross.cc 26 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
3 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 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
// l'Epita (LRDE).
//
// 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>
#include <unistd.h>
#include <cmath>
#include <sys/wait.h>
#include <iomanip>
#include "error.h"
#include "argmatch.h"

#include "common_setup.hh"
#include "common_hoaread.hh"
#include "common_finput.hh"
#include "common_color.hh"
#include "common_trans.hh"
#include "common_cout.hh"
#include "common_aoutput.hh"
#include "common_post.hh"

#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/postproc.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/determinize.hh>
#include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/alternation.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/product.hh>
#include <spot/misc/escape.hh>
55
#include <spot/misc/timer.hh>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
56 57 58 59

const char argp_program_doc[] ="\
Call several tools that process automata and cross-compare their output \
to detect bugs, or to gather statistics.  The list of automata to use \
60
should be supplied on standard input, or using the -F option.\v\
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
61
Exit status:\n\
62
  0  everything went fine (without --fail-on-timeout, timeouts are OK)\n\
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
63 64 65 66 67 68 69 70 71
  1  some tools failed to output something we understand, or failed\n\
     sanity checks (statistics were output nonetheless)\n\
  2  autcross aborted on error\n\
";

enum {
  OPT_BOGUS = 256,
  OPT_CSV,
  OPT_HIGH,
72
  OPT_FAIL_ON_TIMEOUT,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95
  OPT_IGNORE_EXEC_FAIL,
  OPT_LANG,
  OPT_LOW,
  OPT_MEDIUM,
  OPT_NOCHECKS,
  OPT_OMIT,
  OPT_STOP_ERR,
  OPT_VERBOSE,
};

static const argp_option options[] =
  {
    { nullptr, 0, nullptr, 0, "Input:", 1 },
    { "file", 'F', "FILENAME", 0,
      "process automata from FILENAME", 0 },
    /**************************************************/
    { nullptr, 0, nullptr, 0, "autcross behavior:", 5 },
    { "stop-on-error", OPT_STOP_ERR, nullptr, 0,
      "stop on first execution error or failure to pass"
      " sanity checks (timeouts are OK)", 0 },
    { "ignore-execution-failures", OPT_IGNORE_EXEC_FAIL, nullptr, 0,
      "ignore automata from translators that return with a non-zero exit code,"
      " but do not flag this as an error", 0 },
96 97
    { "fail-on-timeout", OPT_FAIL_ON_TIMEOUT, nullptr, 0,
      "consider timeouts as errors", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117
    { "language-preserved", OPT_LANG, nullptr, 0,
      "expect that each tool preserves the input language", 0 },
    { "no-checks", OPT_NOCHECKS, nullptr, 0,
      "do not perform any sanity checks", 0 },
    /**************************************************/
    { nullptr, 0, nullptr, 0, "Statistics output:", 7 },
    { "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 },
    { "omit-missing", OPT_OMIT, nullptr, 0,
      "do not output statistics for timeouts or failed translations", 0 },
    /**************************************************/
    { nullptr, 0, nullptr, 0, "Simplification level (for complementation):",
      21 },
    { "low", OPT_LOW, nullptr, 0, "minimal optimizations (fast)", 0 },
    { "medium", OPT_MEDIUM, nullptr, 0, "moderate optimizations", 0 },
    { "high", OPT_HIGH, nullptr, 0,
      "all available optimizations (slow, default)", 0 },
    /**************************************************/
118
    { nullptr, 0, nullptr, 0, "Output options:", -15 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
119
    { "save-bogus", OPT_BOGUS, "[>>]FILENAME", 0,
120
      "save formulas for which problems were detected in FILENAME", -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
121
    { "verbose", OPT_VERBOSE, nullptr, 0,
122 123 124 125 126 127
      "print what is being done, for debugging", -1 },
    { nullptr, 0, nullptr, 0,
      "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 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
128 129 130 131 132 133 134
    { nullptr, 0, nullptr, 0, nullptr, 0 }
  };

const struct argp_child children[] =
  {
    { &autproc_argp, 0, nullptr, 0 },
    { &hoaread_argp, 0, "Parsing of automata:", 4 },
135
    { &misc_argp, 0, nullptr, -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
136 137 138 139 140 141 142
    { &color_argp, 0, nullptr, 0 },
    { nullptr, 0, nullptr, 0 }
  };

static bool verbose = false;
static bool ignore_exec_fail = false;
static unsigned ignored_exec_fail = 0;
143
static bool fail_on_timeout = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169
static bool stop_on_error = false;
static bool no_checks = false;
static bool opt_language_preserved = false;
static bool opt_omit = false;
static const char* csv_output = nullptr;
static unsigned round_num = 0;
static const char* bogus_output_filename = nullptr;
static output_file* bogus_output = nullptr;

static int
parse_opt(int key, char* arg, struct argp_state*)
{
  switch (key)
    {
    case 'F':
      jobs.emplace_back(arg, true);
      break;
    case OPT_BOGUS:
      {
        bogus_output = new output_file(arg);
        bogus_output_filename = arg;
        break;
      }
    case OPT_CSV:
      csv_output = arg ? arg : "-";
      break;
170 171 172
    case OPT_FAIL_ON_TIMEOUT:
      fail_on_timeout = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392
    case OPT_HIGH:
      level = spot::postprocessor::High;
      level_set = true;
      break;
    case OPT_IGNORE_EXEC_FAIL:
      ignore_exec_fail = true;
      break;
    case OPT_LANG:
      opt_language_preserved = true;
      break;
    case OPT_LOW:
      level = spot::postprocessor::Low;
      level_set = true;
      break;
    case OPT_MEDIUM:
      level = spot::postprocessor::Medium;
      level_set = true;
      break;
    case OPT_NOCHECKS:
      no_checks = true;
      break;
    case OPT_OMIT:
      opt_omit = true;
      break;
    case OPT_STOP_ERR:
      stop_on_error = true;
      break;
    case OPT_VERBOSE:
      verbose = true;
      break;
    case ARGP_KEY_ARG:
      if (arg[0] == '-' && !arg[1])
        jobs.emplace_back(arg, true);
      else
        tools_push_autproc(arg);
      break;
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

static bool global_error_flag = false;
// static unsigned oom_count = 0U;

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

static void
end_error()
{
  std::cerr << reset_color;
}

static std::ostream&
example()
{
  std::cerr << bold_std;
  return std::cerr;
}


struct aut_statistics
{
  unsigned ap;
  unsigned states;
  unsigned edges;
  unsigned transitions;
  unsigned acc_sets;
  unsigned scc;
  unsigned nondetstates;
  bool nondeterministic;
  bool alternating;

  aut_statistics()
  {
  }

  void set(const spot::const_twa_graph_ptr& aut)
  {
    if (!csv_output)
      // Do not waste time.
      return;
    ap = aut->ap().size();
    spot::twa_sub_statistics s = sub_stats_reachable(aut);
    states = s.states;
    edges = s.edges;
    transitions = s.transitions;
    spot::scc_info m(aut);
    acc_sets = aut->num_sets();
    unsigned c = m.scc_count();
    scc = c;
    nondetstates = spot::count_nondet_states(aut);
    nondeterministic = nondetstates != 0;
    alternating = !aut->is_existential();
  }

  void to_csv(std::ostream& os) const
  {
    os << ap << ','
       << states << ','
       << edges << ','
       << transitions << ','
       << acc_sets << ','
       << scc << ','
       << nondetstates << ','
       << nondeterministic << ','
       << alternating;
  }

  void empty(std::ostream& os) const
  {
    os << ",,,,,,,,";
  }

  static void fields(std::ostream& os, const char* prefix)
  {
    os << '"'
       << prefix << "ap\",\""
       << prefix << "states\",\""
       << prefix << "edges\",\""
       << prefix << "transitions\",\""
       << prefix << "acc_sets\",\""
       << prefix << "scc\",\""
       << prefix << "nondetstates\",\""
       << prefix << "nondeterministic\",\""
       << prefix << "alternating\"";
  }
};

struct in_statistics
{
  std::string input_source;
  std::string input_name;
  aut_statistics input;

  static void fields(std::ostream& os)
  {
    os << "\"input.source\",\"input.name\",";
    aut_statistics::fields(os, "input.");
  }

  void to_csv(std::ostream& os) const
  {
    spot::escape_rfc4180(os << '"', input_source) << "\",";
    if (!input_name.empty())
      spot::escape_rfc4180(os << '"', input_name) << "\",";
    else
      os << ',';
    input.to_csv(os);
  }
};

struct out_statistics
{

  // If OK is false, output statistics are not available.
  bool ok;
  const char* status_str;
  int status_code;
  double time;
  aut_statistics output;

  out_statistics()
    : ok(false),
      status_str(nullptr),
      status_code(0),
      time(0)
  {
  }

  static void fields(std::ostream& os)
  {
    os << "\"exit_status\",\"exit_code\",\"time\",";
    aut_statistics::fields(os, "output.");
  }

  void to_csv(std::ostream& os) const
  {
    os << '"' << status_str << "\"," << status_code << ','
       << time << ',';
    if (ok)
      output.to_csv(os);
    else
      output.empty(os);
  }
};

std::vector<in_statistics> input_statistics;
typedef std::vector<out_statistics> vector_tool_statistics;
std::vector<vector_tool_statistics> output_statistics;

namespace
{
  class autcross_runner final: public autproc_runner
  {
    spot::bdd_dict_ptr dict;
  public:
    autcross_runner(spot::bdd_dict_ptr dict)
      : dict(dict)
    {
    }

    spot::twa_graph_ptr
    run_tool(unsigned int tool_num, char l, bool& problem,
             out_statistics& stats)
    {
      output.reset(tool_num);

      std::ostringstream command;
      format(command, tools[tool_num].cmd);

      std::string cmd = command.str();
      std::cerr << "Running [" << l << tool_num << "]: "
                << cmd << std::endl;
393
      spot::process_timer timer;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
394 395 396 397 398 399 400 401
      timer.start();
      int es = exec_with_timeout(cmd.c_str());
      timer.stop();
      const char* status_str = nullptr;

      spot::twa_graph_ptr res = nullptr;
      if (timed_out)
        {
402 403 404 405 406 407 408 409 410 411
          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;
            }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
412
          status_str = "timeout";
413
          problem = fail_on_timeout;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481
          es = -1;
        }
      else if (WIFSIGNALED(es))
        {
          status_str = "signal";
          problem = true;
          es = WTERMSIG(es);
          global_error() << "error: execution terminated by signal "
                         << es << ".\n";
          end_error();
        }
      else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
        {
          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;
            }
        }
      else
        {
          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;
            }
        }
      output.cleanup();

      stats.status_str = status_str;
      stats.status_code = es;
482
      stats.time = timer.walltime();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 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 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824
      if (res)
        {
          stats.ok = true;
          stats.output.set(res);
        }
      return res;
    }
  };

  static std::string
  autname(unsigned i, bool complemented = false)
  {
    std::ostringstream str;
    if (complemented)
      str << "Comp(";
    if (i < tools.size())
      str << 'A' << i;
    else
      str << "input";
    if (complemented)
      str << ')';
    return str.str();
  }

  static bool
  check_empty_prod(const spot::const_twa_graph_ptr& aut_i,
                   const spot::const_twa_graph_ptr& aut_j,
                   size_t i, size_t j)
  {
    if (aut_i->num_sets() + aut_j->num_sets()
        > 8 * sizeof(spot::acc_cond::mark_t::value_t))
      {
        std::cerr << "info: building " << autname(i)
                  << '*' << autname(j, true)
                  << " requires more acceptance sets than supported\n";
        return false;
      }

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

    if (verbose)
      std::cerr << "info: check_empty "
                << autname(i) << '*' << autname(j, true) << '\n';

    auto w = prod->accepting_word();
    if (w)
      {
        std::ostream& err = global_error();
        err << "error: " << autname(i) << '*' << autname(j, true)
            << (" is nonempty; both automata accept the infinite word:\n"
                "       ");
        example() << *w << '\n';
        end_error();
      }
    return !!w;
  }

  class autcross_processor final: public hoa_processor
  {
    autcross_runner runner;
  public:
    autcross_processor()
      : hoa_processor(spot::make_bdd_dict()), runner(dict_)
    {
    }

    int
    process_automaton(const spot::const_parsed_aut_ptr& haut) override
    {
      auto printsize = [](const spot::const_twa_graph_ptr& aut,
                          bool props)
        {
          std::cerr << '(' << aut->num_states() << " st.,"
          << aut->num_edges() << " ed.,"
          << aut->num_sets() << " sets)";
          if (props)
            {
              if (!aut->is_existential())
                std::cerr << " univ-edges";
              if (is_deterministic(aut))
                std::cerr << " deterministic";
              if (is_complete(aut))
                std::cerr << " complete";
              std::cerr << '\n';
            }
        };

      spot::twa_graph_ptr input = haut->aut;
      runner.round_automaton(input, round_num);

      std::string source = [&]()
        {
          std::ostringstream src;
          src << haut->filename << ':' << haut->loc;
          return src.str();
        }();

      input_statistics.push_back(in_statistics());

      std::cerr << bold << source << reset_color;
      input_statistics[round_num].input_source = std::move(source);
      if (auto name = input->get_named_prop<std::string>("automaton-name"))
        {
          std::cerr << '\t' << *name;
          input_statistics[round_num].input_name = *name;
        }
      std::cerr << '\n';
      input_statistics[round_num].input.set(input);

      int problems = 0;
      size_t m = tools.size();
      size_t mi = m + opt_language_preserved;
      std::vector<spot::twa_graph_ptr> pos(mi);
      std::vector<spot::twa_graph_ptr> neg(mi);
      vector_tool_statistics stats(m);

      if (opt_language_preserved)
        pos[mi - 1] = input;

      if (verbose)
        {
          std::cerr << "info: input\t";
          printsize(input, true);
        }

      for (size_t n = 0; n < m; ++n)
        {
          bool prob;
          pos[n] = runner.run_tool(n, 'A', prob, stats[n]);
          problems += prob;
        }
      spot::cleanup_tmpfiles();
      ++round_num;
      output_statistics.push_back(std::move(stats));

      if (verbose)
        {
          std::cerr << "info: collected automata:\n";
          for (unsigned i = 0; i < m; ++i)
            if (pos[i])
              {
                std::cerr << "info:   A" << i << '\t';
                printsize(pos[i], true);
              }
        }

      if (!no_checks)
        {
          std::cerr << "Performing sanity checks and gathering statistics..."
                    << std::endl;

          {
            bool print_first = true;
            for (unsigned i = 0; i < mi; ++i)
              {
                if (!pos[i])
                  continue;
                if (!pos[i]->is_existential())
                  {
                    if (verbose)
                      {
                        if (print_first)
                          {
                            std::cerr <<
                              "info: getting rid of universal edges...\n";
                            print_first = false;
                          }
                        std::cerr << "info:   "
                                  << std::setw(8) << autname(i) << '\t';
                        printsize(pos[i], false);
                        std::cerr << " -> ";
                      }
                    pos[i] = remove_alternation(pos[i]);
                    if (verbose)
                      {
                        printsize(pos[i], false);
                        std::cerr << '\n';
                      }
                  }
                if (is_universal(pos[i]))
                  neg[i] = dualize(pos[i]);
              }
          }

          {
            bool print_first = verbose;
            for (unsigned i = 0; i < mi; ++i)
              {
                if (pos[i] && !neg[i])
                  {
                    if (print_first)
                      {
                        std::cerr << "info: complementing non-deterministic "
                        "automata via determinization...\n";
                        print_first = false;
                      }
                    spot::postprocessor p;
                    p.set_type(spot::postprocessor::Generic);
                    p.set_pref(spot::postprocessor::Deterministic);
                    p.set_level(level);
                    neg[i] = dualize(p.run(pos[i]));
                    if (verbose)
                      {
                        std::cerr << "info:   "
                                  << std::setw(8) << autname(i) << '\t';
                        printsize(pos[i], false);
                        std::cerr << " -> ";
                        printsize(neg[i], false);
                        std::cerr << '\t' << autname(i, true) << '\n';
                      }
                  }
              };
          }

          {
            bool print_first = true;
            auto tmp = [&](std::vector<spot::twa_graph_ptr>& x, unsigned i,
                           bool neg)
              {
                if (!x[i])
                  return;
                if (x[i]->acc().uses_fin_acceptance())
                  {
                    if (verbose)
                      {
                        if (print_first)
                          {
                            std::cerr <<
                              "info: getting rid of any Fin acceptance...\n";
                            print_first = false;
                          }
                        std::cerr << "info:   "
                                  << std::setw(8) << autname(i, neg) << '\t';
                        printsize(x[i], false);
                        std::cerr << " ->";
                      }
                    cleanup_acceptance_here(x[i]);
                    x[i] = remove_fin(x[i]);
                    if (verbose)
                      {
                        std::cerr << ' ';
                        printsize(x[i], false);
                        std::cerr << '\n';
                      }
                  }
                else
                  {
                    // Remove useless sets nonetheless.
                    cleanup_acceptance_here(x[i]);
                  }
              };
            for (unsigned i = 0; i < mi; ++i)
              {
                tmp(pos, i, false);
                tmp(neg, i, true);
              }
          }

          // Just make a circular implication check
          // A0 <= A1, A1 <= A2, ..., AN <= A0
          unsigned ok = 0;
          for (size_t i = 0; i < mi; ++i)
            if (pos[i])
              {
                size_t j = ((i + 1) % mi);
                if (i != j && neg[j])
                  {
                    int res = check_empty_prod(pos[i], neg[j], i, j);
                    problems += res;
                    ok += !res;
                  }
              }
          // If the circular check failed, do the rest of all
          // mi(mi-1)/2 checks, as this will help diagnose the issue.
          if (ok != mi)
            for (size_t i = 0; i < mi; ++i)
              if (pos[i])
                {
                  size_t k = ((i + 1) % mi);
                  for (size_t j = 0; j < mi; ++j)
                  if (i != j && j != k && neg[j])
                    problems += check_empty_prod(pos[i], neg[j], i, j);
                }
        }
      else
        {
          std::cerr << "Gathering statistics..." << std::endl;
        }


      if (problems && bogus_output)
        print_hoa(bogus_output->ostream(), input) << std::endl;

      std::cerr << std::endl;

      // Shall we stop processing now?
      abort_run = global_error_flag && stop_on_error;
      return problems;
    }
  };
}

// Output an RFC4180-compatible CSV file.
static void
print_stats_csv(const char* filename)
{
  if (verbose)
    std::cerr << "info: writing CSV to " << filename << '\n';

  output_file outf(filename);
  std::ostream& out = outf.ostream();

  unsigned ntools = tools.size();
  assert(round_num == output_statistics.size());
  assert(round_num == input_statistics.size());

  if (!outf.append())
    {
      // Do not output the header line if we append to a file.
      // (Even if that file was empty initially.)
      in_statistics::fields(out);
      out << ",\"tool\",";
      out_statistics::fields(out);
      out << '\n';
    }
  for (unsigned r = 0; r < round_num; ++r)
    for (unsigned t = 0; t < ntools; ++t)
      if (!opt_omit || output_statistics[r][t].ok)
        {
          input_statistics[r].to_csv(out);
          out << ",\"";
          spot::escape_rfc4180(out, tools[t].name);
          out << "\",";
          output_statistics[r][t].to_csv(out);
          out << '\n';
        }
  outf.close(filename);
}

int
main(int argc, char** argv)
{
825 826 827
  return protected_main(argv, [&]() -> unsigned {
      const argp ap = { options, parse_opt, "[COMMANDFMT...]",
                        argp_program_doc, children, nullptr, nullptr };
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
828

829 830
      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
        exit(err);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
831

832
      check_no_automaton();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
833

834 835 836 837
      auto s = tools.size();
      if (s == 0)
        error(2, 0, "No tool to run?  Run '%s --help' for usage.",
              program_name);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
838

839 840 841
      if (s == 1 && !opt_language_preserved && !no_checks)
        error(2, 0, "Since --language-preserved is not used, you need "
              "at least two tools to compare.");
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
842 843


844 845
      setup_color();
      setup_sig_handler();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
846

847 848 849
      autcross_processor p;
      if (p.run())
        return 2;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
850

851
      if (round_num == 0)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
852
        {
853
          error(2, 0, "no automaton to translate");
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
854 855 856
        }
      else
        {
857
          if (global_error_flag)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
858
            {
859 860 861 862 863 864
              std::ostream& err = global_error();
              if (bogus_output)
                err << ("error: some error was detected during the above "
                        "runs.\n       Check file ")
                    << bogus_output_filename
                    << " for problematic automata.";
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
865
              else
866 867 868 869 870 871 872 873 874 875 876 877 878
                err << ("error: some error was detected during the above "
                        "runs,\n       please search for 'error:' messages"
                        " in the above trace.");
              err << std::endl;
              end_error();
            }
          else if (timeout_count == 0 && ignored_exec_fail == 0)
            {
              std::cerr << "No problem detected." << std::endl;
            }
          else
            {
              std::cerr << "No major problem detected." << std::endl;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
879 880
            }

881 882 883 884
          unsigned additional_errors = 0U;
          additional_errors += timeout_count > 0;
          additional_errors += ignored_exec_fail > 0;
          if (additional_errors)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
885
            {
886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909
              std::cerr << (global_error_flag ? "Additionally, " : "However, ");
              if (timeout_count)
                {
                  if (additional_errors > 1)
                    std::cerr << "\n  - ";
                  if (timeout_count == 1)
                    std::cerr << "1 timeout occurred";
                  else
                    std::cerr << timeout_count << " timeouts occurred";
                }

              if (ignored_exec_fail)
                {
                  if (additional_errors > 1)
                    std::cerr << "\n  - ";
                  if (ignored_exec_fail == 1)
                    std::cerr << "1 non-zero exit status was ignored";
                  else
                    std::cerr << ignored_exec_fail
                              << " non-zero exit statuses were ignored";
                }
              if (additional_errors == 1)
                std::cerr << '.';
              std::cerr << std::endl;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
910 911 912
            }
        }

913 914
      if (csv_output)
        print_stats_csv(csv_output);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
915

916 917
      return global_error_flag;
    });
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
918
}