From 4e99518da736dd08236f7562b4516b8c725c40fe Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 9 Mar 2020 14:55:51 +0100
Subject: [PATCH] ltlcross: do not use remove_fin anymore

* bin/ltlcross.cc: Since is_empty() now works with arbitrary
acceptance conditions, calling remove_fin() is not necessary anymore.
* tests/core/ltlcrossce.test: Adjust.
* NEWS: Mention the change.
---
 NEWS                       |  4 ++
 bin/ltlcross.cc            | 89 +++++++++++++-------------------------
 tests/core/ltlcrossce.test |  3 +-
 3 files changed, 35 insertions(+), 61 deletions(-)

diff --git a/NEWS b/NEWS
index 1d2afa9df..8072a641b 100644
--- a/NEWS
+++ b/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 is now using the generic emptiness check procedure
+    introduced in Spot 2.7, as opposed to removing Fin acceptance
+    before using a classical emptiness check.
+
   - 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.
diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc
index 4526d90cd..64f9a26b8 100644
--- a/bin/ltlcross.cc
+++ b/bin/ltlcross.cc
@@ -1264,6 +1264,33 @@ namespace
               unalt(neg, i, 'N');
             }
 
+          print_first = verbose;
+          auto tmp = [&](std::vector<spot::twa_graph_ptr>& x, unsigned i,
+                         const char* prefix, const char* suffix)
+            {
+              if (!x[i])
+                return;
+              unsigned before = x[i]->num_sets();
+              cleanup_acceptance_here(x[i]);
+              unsigned after = x[i]->num_sets();
+              if (verbose && before != after)
+                {
+                  if (print_first)
+                    {
+                      std::cerr << "info: removing unused sets...\n";
+                      print_first = false;
+                    }
+                  std::cerr << "info:   " << prefix << i
+                            << suffix << '\t' << before << " sets -> "
+                            << after << " sets\n";
+                }
+            };
+          for (size_t i = 0; i < m; ++i)
+            {
+              tmp(pos, i, "     P", " ");
+              tmp(neg, i, "     N", " ");
+            }
+
           // Complement
           if (!no_complement)
             {
@@ -1324,67 +1351,11 @@ namespace
                 }
             }
 
-          print_first = verbose;
-          auto tmp = [&](std::vector<spot::twa_graph_ptr>& x, unsigned i,
-                         const char* prefix, const char* suffix)
-            {
-              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:\t" << prefix << i
-                                << suffix << "\t(";
-                      printsize(x[i]);
-                      std::cerr << ") ->";
-                    }
-                  try
-                    {
-                      x[i] = remove_fin(x[i]);
-                    }
-                  catch (const std::runtime_error& err)
-                    {
-                      if (verbose)
-                        std::cerr << " failed (" << err.what() << ")\n";
-                      else
-                        std::cerr << "info: preprocessing "
-                                  << prefix << i << suffix
-                                  << " failed (" << err.what() << ")\n";
-                      x[i] = nullptr;
-                    }
-                  if (verbose && x[i])
-                    {
-                      std::cerr << " (";
-                      printsize(x[i]);
-                      std::cerr << ")\n";
-                    }
-                }
-              else
-                {
-                  // Remove useless sets nonetheless.
-                  cleanup_acceptance_here(x[i]);
-                }
-            };
-          for (size_t i = 0; i < m; ++i)
-            {
-              tmp(pos, i, "     P", " ");
-              tmp(neg, i, "     N", " ");
-              tmp(comp_pos, i, "Comp(P", ")");
-              tmp(comp_neg, i, "Comp(N", ")");
-            }
-
           if (smallest_pos_ref >= 0)
             {
-              // Recompute the smallest references now, because removing
-              // alternation and Fin acceptance might have changed the
-              // sizes.
+              // Recompute the smallest references now, because
+              // removing alternation and useless acceptance sets
+              // might have changed the sizes.
               smallest_pos_ref = smallest_ref(pos);
               smallest_neg_ref = smallest_ref(neg);
 
diff --git a/tests/core/ltlcrossce.test b/tests/core/ltlcrossce.test
index 5fcbcf47d..1316c4330 100755
--- a/tests/core/ltlcrossce.test
+++ b/tests/core/ltlcrossce.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2016, 2019 Laboratoire de Recherche et
+# Copyright (C) 2013, 2016, 2019, 2020 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -95,7 +95,6 @@ test `grep '^error:' errors | wc -l` = 4
 run 1 ltlcross --verbose -D -f 'G(F(p0) & F(G(!p1))) | (F(G(!p0)) & G(F(p1)))' \
   "ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors
 cat errors
-test `grep 'info:	Comp(' errors | wc -l` = 3
 grep 'error: P0\*N1 is nonempty' errors
 grep 'error: P1\*N0 is nonempty' errors
 grep 'error: P1\*N1 is nonempty' errors