ltlcross: add option --save-inclusion-products

* NEWS: Mention it.
* bin/ltlcross.cc: Implement it.
* tests/core/ltlcross3.test: Test it.

NEWS

@@ -21,6 +21,10 @@ New in spot 2.8.6.dev (not yet released)
     conjunctions of Inf, or disjunction of Fin that appears in
     arbitrary conditions.
 
+  - ltlcross learned a --save-inclusion-products=FILENAME option.  Its
+    use cases are probably quite limited.  We use that to generate
+    benchmarks for our generic emptiness check procedure.
+
   Library:
 
   - Historically, Spot only supports LTL with infinite semantics

bin/ltlcross.cc

@@ -98,6 +98,7 @@ enum {
   OPT_OMIT,
   OPT_PRODUCTS,
   OPT_REFERENCE,
+  OPT_SAVE_INCLUSION_PRODUCTS,
   OPT_SEED,
   OPT_STATES,
   OPT_STOP_ERR,
@@ -180,6 +181,9 @@ static const argp_option options[] =
       "suppress all normal output in absence of error", 0 },
     { "save-bogus", OPT_BOGUS, "[>>]FILENAME", 0,
       "save formulas for which problems were detected in FILENAME", 0 },
+    { "save-inclusion-products",  OPT_SAVE_INCLUSION_PRODUCTS, "[>>]FILENAME",
+      0, "save automata representing products built to check inclusion "
+      "between automata", 0 },
     { "verbose", OPT_VERBOSE, nullptr, 0,
       "print what is being done, for debugging", 0 },
     { nullptr, 0, nullptr, 0,
@@ -221,6 +225,8 @@ static bool opt_omit = false;
 static const char* bogus_output_filename = nullptr;
 static output_file* bogus_output = nullptr;
 static output_file* grind_output = nullptr;
+static const char* saved_inclusion_products_filename = nullptr;
+static output_file* saved_inclusion_products = nullptr;
 static bool verbose = false;
 static bool quiet = false;
 static bool ignore_exec_fail = false;
@@ -539,6 +545,12 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_REFERENCE:
       tools_push_trans(arg, true);
       break;
+    case OPT_SAVE_INCLUSION_PRODUCTS:
+      {
+        saved_inclusion_products = new output_file(arg);
+        saved_inclusion_products_filename = arg;
+        break;
+      }
     case OPT_SEED:
       seed = to_pos_int(arg, "--seed");
       break;
@@ -785,6 +797,9 @@ namespace
 
     auto prod = spot::product(aut_i, aut_j);
 
+    if (saved_inclusion_products)
+      spot::print_hoa(saved_inclusion_products->ostream(), prod) << std::endl;
+
     if (verbose)
       {
         std::cerr << "info: check_empty ";
@@ -1804,8 +1819,12 @@ main(int argc, char** argv)
             }
         }
 
+      // FIXME: I think we should call close() on all these files
+      // before deleting them.  Otherwise we fail to report write
+      // errors.
       delete bogus_output;
       delete grind_output;
+      delete saved_inclusion_products;
 
       if (json_output)
         print_stats_json(json_output);

tests/core/ltlcross3.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012-2019 Laboratoire de Recherche et Développement de
+# Copyright (C) 2012-2020 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -347,3 +347,8 @@ grep 'max-edges.*incompatible' stderr
 ltlcross -f a ltl2tgba --determinize-max-edges=10 --determinize  2>stderr &&
     exit 1
 grep 'max-edges.*incompatible' stderr
+
+# Make sure save-inclusion-products outputs the expected number of products.
+ltlcross ltl2tgba 'ltl2tgba -D' -f GFa -f FGa \
+         --verbose --save-inclusion-products=prod.hoa
+test 12 = `autfilt -c prod.hoa`