From f0b77e21c834f4701ba1b70a56a344cdaefd76ae Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 7 Jun 2019 14:56:56 +0200
Subject: [PATCH] autcross: simplify code using complement() and
 intersecting_word()

* bin/autcross.cc: Let complement() decide how to complement automata.
Do not apply remove_fin(), because we have a generic emptiness check
now.  Use intersecting_word() instead of product()+accepting_word() so
that the former can maybe be optimized in the future.
* tests/core/autcross2.test: Adjust test case to use TGBA instead
of monitors, as calling complement() had a side-effect of setting
the "weak" property on the input.
---
 bin/autcross.cc           | 70 +++++----------------------------------
 tests/core/autcross2.test |  4 +--
 2 files changed, 10 insertions(+), 64 deletions(-)

diff --git a/bin/autcross.cc b/bin/autcross.cc
index e14a1393e..8067ea774 100644
--- a/bin/autcross.cc
+++ b/bin/autcross.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de
+// Copyright (C) 2017, 2018, 2019 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -45,12 +45,9 @@
 #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/complement.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>
 #include <spot/misc/timer.hh>
 
@@ -518,13 +515,11 @@ namespace
         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();
+    auto w = aut_i->intersecting_word(aut_j);
     if (w)
       {
         std::ostream& err = global_error();
@@ -637,6 +632,7 @@ namespace
               {
                 if (!pos[i])
                   continue;
+                cleanup_acceptance_here(pos[i]);
                 if (!pos[i]->is_existential())
                   {
                     if (verbose)
@@ -659,8 +655,6 @@ namespace
                         std::cerr << '\n';
                       }
                   }
-                if (is_universal(pos[i]))
-                  neg[i] = dualize(pos[i]);
               }
           }
 
@@ -668,19 +662,14 @@ namespace
             bool print_first = verbose;
             for (unsigned i = 0; i < mi; ++i)
               {
-                if (pos[i] && !neg[i])
+                if (pos[i])
                   {
                     if (print_first)
                       {
-                        std::cerr << "info: complementing non-deterministic "
-                        "automata via determinization...\n";
+                        std::cerr << "info: complementing automata...\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]));
+                    neg[i] = spot::complement(pos[i]);
                     if (verbose)
                       {
                         std::cerr << "info:   "
@@ -690,54 +679,11 @@ namespace
                         printsize(neg[i], false);
                         std::cerr << '\t' << autname(i, true) << '\n';
                       }
+                    cleanup_acceptance_here(pos[i]);
                   }
               };
           }
 
-          {
-            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;
diff --git a/tests/core/autcross2.test b/tests/core/autcross2.test
index c7ba9a36d..942aea94a 100755
--- a/tests/core/autcross2.test
+++ b/tests/core/autcross2.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de
+# Copyright (C) 2017, 2018, 2019 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -22,7 +22,7 @@
 set -e
 
 # Exercise %L while we are at it.
-randaut -n10 2 | tee input |
+randaut -n10 -A2..3 2 | tee input |
 autcross --language-preserve 'autfilt %L>%O' 'autfilt --complement' \
   --save-bogus=bogus.hoa 2>stderr && exit 1
 cat stderr
-- 
GitLab