From 096c78a3f89414a6d6fd99f036016614ae407438 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 28 Dec 2016 10:18:05 +0100
Subject: [PATCH] autfilt: handle alternation with --equivalent-to and friends

* bin/autfilt.cc (ensure_deterministic): Remove alternation on demand.
(process_automaton): Prefer twa::intersects() over
product()/is_empty().
* spot/twa/twa.cc (remove_fin_maybe): Also remove alternation.
* tests/core/alternating.test: More tests.
---
 bin/autfilt.cc              | 18 +++++-----
 spot/twa/twa.cc             |  8 +++--
 tests/core/alternating.test | 71 +++++++++++++++++++++++++++++++++++++
 3 files changed, 85 insertions(+), 12 deletions(-)

diff --git a/bin/autfilt.cc b/bin/autfilt.cc
index 90b1bba76..42d75be6a 100644
--- a/bin/autfilt.cc
+++ b/bin/autfilt.cc
@@ -468,9 +468,9 @@ static int opt_highlight_nondet_states = -1;
 static int opt_highlight_nondet_edges = -1;
 
 static spot::twa_graph_ptr
-ensure_deterministic(const spot::twa_graph_ptr& aut)
+ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
 {
-  if (spot::is_deterministic(aut))
+  if (!(nonalt && aut->is_alternating()) && spot::is_deterministic(aut))
     return aut;
   spot::postprocessor p;
   p.set_type(spot::postprocessor::Generic);
@@ -567,7 +567,7 @@ parse_opt(int key, char* arg, struct argp_state*)
         error(2, 0, "only one --equivalent-to option can be given");
       opt->equivalent_pos = read_automaton(arg, opt->dict);
       opt->equivalent_neg =
-        spot::dtwa_complement(ensure_deterministic(opt->equivalent_pos));
+        spot::dtwa_complement(ensure_deterministic(opt->equivalent_pos, true));
       break;
     case OPT_GENERALIZED_RABIN:
       if (arg)
@@ -638,7 +638,7 @@ parse_opt(int key, char* arg, struct argp_state*)
       break;
     case OPT_INCLUDED_IN:
       {
-        auto aut = ensure_deterministic(read_automaton(arg, opt->dict));
+        auto aut = ensure_deterministic(read_automaton(arg, opt->dict), true);
         aut = spot::dtwa_complement(aut);
         if (!opt->included_in)
           opt->included_in = aut;
@@ -1088,13 +1088,13 @@ namespace
       if (opt_is_empty)
         matched &= aut->is_empty();
       if (opt->intersect)
-        matched &= !spot::product(aut, opt->intersect)->is_empty();
+        matched &= aut->intersects(opt->intersect);
       if (opt->included_in)
-        matched &= spot::product(aut, opt->included_in)->is_empty();
+        matched &= !aut->intersects(opt->included_in);
       if (opt->equivalent_pos)
-        matched &= spot::product(aut, opt->equivalent_neg)->is_empty()
-          && spot::product(dtwa_complement(ensure_deterministic(aut)),
-                           opt->equivalent_pos)->is_empty();
+        matched &= !aut->intersects(opt->equivalent_neg)
+          && (!dtwa_complement(ensure_deterministic(aut, true))->
+              intersects(opt->equivalent_pos));
 
       if (matched && !opt->acc_words.empty())
         for (auto& word_aut: opt->acc_words)
diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc
index abdf5ed01..75b6e721d 100644
--- a/spot/twa/twa.cc
+++ b/spot/twa/twa.cc
@@ -25,6 +25,7 @@
 #include <spot/twaalgos/couvreurnew.hh>
 #include <spot/twaalgos/word.hh>
 #include <spot/twaalgos/remfin.hh>
+#include <spot/twaalgos/alternation.hh>
 #include <spot/twa/twaproduct.hh>
 #include <utility>
 
@@ -48,14 +49,15 @@ namespace spot
 
   namespace
   {
+    // Remove Fin-acceptance and alternation.
     const_twa_ptr remove_fin_maybe(const const_twa_ptr& a)
     {
-      if (!a->acc().uses_fin_acceptance())
-        return a;
       auto aa = std::dynamic_pointer_cast<const twa_graph>(a);
+      if ((!aa || !aa->is_alternating()) && !a->acc().uses_fin_acceptance())
+        return a;
       if (!aa)
         aa = make_twa_graph(a, twa::prop_set::all());
-      return remove_fin(aa);
+      return remove_fin(remove_alternation(aa));
     }
   }
 
diff --git a/tests/core/alternating.test b/tests/core/alternating.test
index 65343b2a4..32eb441d3 100644
--- a/tests/core/alternating.test
+++ b/tests/core/alternating.test
@@ -202,3 +202,74 @@ State: 1
 --END--
 EOF
 diff expected res
+
+
+cat >ex1<<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 1 "a"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: univ-branch trans-labels explicit-labels trans-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[0] 0
+[!0] 0&1
+State: 1
+[!0] 1 {0}
+[0] 2
+State: 2
+[t] 2
+--END--
+EOF
+
+cat >ex2<<EOF
+HOA: v1
+States: 3
+Start: 0&1
+AP: 1 "a"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: univ-branch trans-labels explicit-labels trans-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[0] 0
+[!0] 0&1
+State: 1
+[!0] 1 {0}
+[0] 2
+State: 2
+[t] 2
+--END--
+EOF
+
+cat >ex3<<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 1 "a"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: univ-branch trans-labels explicit-labels trans-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[0] 1
+[!0] 0&1
+State: 1
+[!0] 1 {0}
+[0] 2
+State: 2
+[t] 2
+--END--
+EOF
+
+autfilt -q --equivalent-to=ex1 ex2
+autfilt -q --included-in=ex1 ex2
+autfilt -q --equivalent-to=ex1 ex3 && exit 1
+autfilt -q --intersect=ex1 ex3
+
+: