autcross: implement --language-complemented

Suggested by Ondřej Lengál.  Fixes #504.

* bin/autcross.cc: Implement the --language-complemented option.
* NEWS, doc/org/autcross.org: Document it.
* tests/core/autcross.test: Test it.
* THANKS: Add Ondřej.

NEWS

@@ -14,6 +14,9 @@ New in spot 2.10.4.dev  (net yet released)
     associated option --sonf-aps allows listing the newly introduced
     atomic propositions.
 
+  - autcross learned a --language-complemented option to assist in the
+    case one is testing tools that complement automata.  (issue #504).
+
   Library:
 
   - The new function suffix_operator_normal_form() implements

THANKS

@@ -41,6 +41,7 @@ Michael Weber
 Mikuláš Klokočka
 Ming-Hsien Tsai
 Nikos Gorogiannis
+Ondřej Lengál
 Paul Guénézan
 Reuben Rowe
 Roei Nahum

bin/autcross.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017-2020 Laboratoire de Recherche et Développement de
+// Copyright (C) 2017-2020, 2022 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -64,6 +64,7 @@ Exit status:\n\
 
 enum {
   OPT_BOGUS = 256,
+  OPT_COMPLEMENTED,
   OPT_CSV,
   OPT_HIGH,
   OPT_FAIL_ON_TIMEOUT,
@@ -94,6 +95,8 @@ static const argp_option options[] =
       "consider timeouts as errors", 0 },
     { "language-preserved", OPT_LANG, nullptr, 0,
       "expect that each tool preserves the input language", 0 },
+    { "language-complemented", OPT_COMPLEMENTED, nullptr, 0,
+      "expect that each tool complements the input language", 0 },
     { "no-checks", OPT_NOCHECKS, nullptr, 0,
       "do not perform any sanity checks", 0 },
     /**************************************************/
@@ -144,6 +147,7 @@ static bool fail_on_timeout = false;
 static bool stop_on_error = false;
 static bool no_checks = false;
 static bool opt_language_preserved = false;
+static bool opt_language_complemented = false;
 static bool opt_omit = false;
 static const char* csv_output = nullptr;
 static unsigned round_num = 0;
@@ -170,6 +174,9 @@ parse_opt(int key, char* arg, struct argp_state*)
         bogus_output_filename = arg;
         break;
       }
+    case OPT_COMPLEMENTED:
+      opt_language_complemented = true;
+      break;
     case OPT_CSV:
       csv_output = arg ? arg : "-";
       break;
@@ -533,25 +540,32 @@ namespace
                    const spot::const_twa_graph_ptr& aut_j,
                    size_t i, size_t j)
   {
+    auto is_really_comp = [lc = opt_language_complemented,
+                           ts = tools.size()](unsigned i) {
+        return lc && i == ts;
+    };
+
     if (aut_i->num_sets() + aut_j->num_sets() >
         spot::acc_cond::mark_t::max_accsets())
       {
         if (!quiet)
-          std::cerr << "info: building " << autname(i)
+          std::cerr << "info: building " << autname(i, is_really_comp(i))
-                    << '*' << autname(j, true)
+                    << '*' << autname(j, true ^ is_really_comp(j))
                     << " requires more acceptance sets than supported\n";
         return false;
       }
 
     if (verbose)
       std::cerr << "info: check_empty "
-                << autname(i) << '*' << autname(j, true) << '\n';
+                << autname(i, is_really_comp(i))
+                << '*' << autname(j, true ^ is_really_comp(j)) << '\n';
 
     auto w = aut_i->intersecting_word(aut_j);
     if (w)
       {
         std::ostream& err = global_error();
-        err << "error: " << autname(i) << '*' << autname(j, true)
+        err << "error: " << autname(i, is_really_comp(i))
+            << '*' << autname(j, true ^ is_really_comp(j))
             << (" is nonempty; both automata accept the infinite word:\n"
                 "       ");
         example() << *w << '\n';
@@ -621,12 +635,15 @@ namespace
 
       int problems = 0;
       size_t m = tools.size();
-      size_t mi = m + opt_language_preserved;
+      size_t mi = m + opt_language_preserved + opt_language_complemented;
       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)
+      // For --language-complemented, we store the input automata in
+      // pos and will compute its complement in neg.  Before running
+      // checks we will swap both automata.
+      if (opt_language_preserved || opt_language_complemented)
         pos[mi - 1] = input;
 
       if (verbose)
@@ -718,6 +735,9 @@ namespace
               };
           }
 
+          if (opt_language_complemented)
+            std::swap(pos[mi - 1], neg[mi - 1]);
+
           // Just make a circular implication check
           // A0 <= A1, A1 <= A2, ..., AN <= A0
           unsigned ok = 0;
@@ -824,10 +844,15 @@ main(int argc, char** argv)
 
       check_no_automaton();
 
-      if (s == 1 && !opt_language_preserved && !no_checks)
+      if (s == 1 && !no_checks
-        error(2, 0, "Since --language-preserved is not used, you need "
+          && !opt_language_preserved
-              "at least two tools to compare.");
+          && !opt_language_complemented)
+        error(2, 0, "Since --language-preserved and --language-complemented "
+              "are not used, you need at least two tools to compare.");
 
+      if (opt_language_preserved && opt_language_complemented)
+        error(2, 0, "Options --language-preserved and --language-complemented "
+              "are incompatible.");
 
       setup_color();
       setup_sig_handler();

doc/org/autcross.org

@@ -249,7 +249,7 @@ EOF
 | -:95.1-140.7 | automaton 2 |        2 |           10 |          26 |                26 |              1 |         2 |                  6 |                      1 |                 0 | AF   | ok          |         0 |  0.0211636 |         2 |            21 |           66 |                 84 |               2 |          4 |                   0 |                       0 |                  0 |
 | -:95.1-140.7 | automaton 2 |        2 |           10 |          26 |                26 |              1 |         2 |                  6 |                      1 |                 0 | L2D  | ok          |         0 |  0.0028508 |         2 |            24 |           74 |                 96 |               2 |          4 |                   0 |                       0 |                  0 |
 
-* Language preserving transformation
+* Transformation that preserve or complement languages
 
 By default =autcross= assumes that for a given input the automata
 produced by all tools should be equivalent.  However it does not
@@ -261,6 +261,13 @@ automaton, it is worth to pass the =--language-preserved= option to
 =autfilt=.  Doing so a bit like adding =cat %H>%O= as another tool: it
 will also ensure that the output is equivalent to the input.
 
+Similarly, if the tools being tested implement complementation
+algorithm, adding the =--language-complemented= will additionally
+compare the outputs using this own complementation algorithm.  Using
+this option is more efficient than passing =autfilt --complement= as a
+tool, since =autcross= can save on complementation by using the input
+automaton.
+
 * Detecting problems
    :PROPERTIES:
    :CUSTOM_ID: checks

tests/core/autcross.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
+# Copyright (C) 2017, 2018, 2022 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -46,3 +46,17 @@ for f in out.csv out2.csv; do
   sed 's/,[0-9]*\.[0-9]*,/,TIME,/' $f > _$f
 done
 diff _out.csv _out2.csv
+
+
+# The {autfilt {complement}} name makes sure we can nest braces.
+randaut -n10 2 |
+    autcross 'ltl2dstar --complement-input=yes' 'autfilt --complement' \
+  --language-complemented --csv=out3.csv --verbose 2>stderr
+test 10 = `grep 'check_empty Comp(input)\*Comp(A0)' stderr | wc -l`
+
+
+randaut -n1 2 |
+    autcross 'ltl2dstar --complement-input=yes' 'autfilt --complement' \
+             --language-complemented --language-preserved 2> stderr && exit 1
+cat stderr
+grep 'preserved.*complemented.*incompatible' stderr