remove_fin: use simplify_acceptance

* spot/twaalgos/remfin.cc: Simplify acceptance before trying the
different strategies.
* spot/twaalgos/cleanacc.cc: Skip simplify_complementary_marks_here()
on generalized Büchi.
* tests/core/remfin.test, tests/python/tra2tba.py: Adjust.
* spot/twaalgos/totgba.cc: Simplify the result of Streett->GBA.
* NEWS: Adjust.

NEWS

@@ -186,6 +186,9 @@ New in spot 2.4.4.dev (net yet released)
     are not very smart: if the input does not already have parity
     acceptance, it will simply be degeneralized or determinized.
 
+  - spot::remove_fin() will now call simplify_acceptance(), introduced
+    in 2.4, before attempting its different Fin-removal strategies.
+
   - acc_cond::name(fmt) is a new method that name well-known acceptance
     conditions.   The fmt parameter specify the format to use for that
     name (e.g. to the style used in HOA, or that used by print_dot()).
@@ -258,10 +261,10 @@ New in spot 2.4.4.dev (net yet released)
 
   Bugs fixed:
 
-  - spot::simplify_acceptance() could produce incorrect output
-    if the first edge of the automaton was the only one with no
-    acceptance set.  In spot 2.4.x this function was only used
-    by autfilt --simplify-acceptance.
+  - spot::simplify_acceptance() could produce incorrect output if the
+    first edge of the automaton was the only one with no acceptance
+    set.  In spot 2.4.x this function was only used by autfilt
+    --simplify-acceptance; in 2.5 it is now used in remove_fin().
 
 New in spot 2.4.4 (2017-12-25)
 

spot/twaalgos/cleanacc.cc

@@ -325,7 +325,8 @@ namespace spot
   {
     cleanup_acceptance_here(aut, false);
     merge_identical_marks_here(aut);
-    simplify_complementary_marks_here(aut);
+    if (!aut->acc().is_generalized_buchi())
+      simplify_complementary_marks_here(aut);
     cleanup_acceptance_here(aut, true);
 
     return aut;

spot/twaalgos/remfin.cc

 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -256,11 +256,8 @@ namespace spot
     // TBA-typeness of the SCC, but the resulting automaton should
     // be correct nonetheless.
     twa_graph_ptr
-    tra_to_tba(const const_twa_graph_ptr& inaut)
+    tra_to_tba(const const_twa_graph_ptr& aut)
     {
-      // cleanup acceptance for easy detection of alone fins and infs
-      auto aut = cleanup_acceptance(inaut);
-
       std::vector<acc_cond::rs_pair> pairs;
       if (!aut->acc().is_rabin_like(pairs))
         return nullptr;
@@ -501,20 +498,6 @@ namespace spot
 
     twa_graph_ptr default_strategy(const const_twa_graph_ptr& aut)
     {
-      {
-        // We want a clean acceptance condition, i.e., one where all
-        // sets are useful.  If that is not the case, clean it first.
-        acc_cond::mark_t unused = aut->acc().all_sets();
-        for (auto& t: aut->edges())
-          {
-            unused -= t.acc;
-            if (!unused)
-              break;
-          }
-        if (unused)
-          return remove_fin(cleanup_acceptance(aut));
-      }
-
       std::vector<acc_cond::acc_code> code;
       std::vector<acc_cond::mark_t> rem;
       std::vector<acc_cond::mark_t> keep;
@@ -525,10 +508,21 @@ namespace spot
       {
         auto acccode = aut->get_acceptance();
         if (!acccode.is_dnf())
-          acccode = acccode.to_dnf();
+          {
+            acccode = acccode.to_dnf();
 
-        auto split = split_dnf_acc_by_fin(acccode);
+            if (acccode.is_f())
+              {
+                // The original acceptance was equivalent to
+                // "f". Simply return an empty automaton.
+                auto res = make_twa_graph(aut->get_dict());
+                res->set_acceptance(0, acccode);
+                res->set_init_state(res->new_state());
+                return res;
+              }
+          }
 
+        auto split = split_dnf_acc_by_fin(acccode);
         auto sz = split.size();
         assert(sz > 0);
 
@@ -759,9 +753,11 @@ namespace spot
     twa_graph_ptr remove_fin_impl(const const_twa_graph_ptr& aut,
                                   const strategy_t skip = {})
     {
+      auto simp = simplify_acceptance(aut);
+
       auto handle = [&](strategy stra, strategy_t type) -> twa_graph_ptr
       {
-        return (type & skip) ? nullptr : stra(aut);
+        return (type & skip) ? nullptr : stra(simp);
       };
 
       if (auto maybe = handle(trivial_strategy, strategy_t::trivial))
@@ -785,7 +781,7 @@ namespace spot
         return maybe;
       if (auto maybe = handle(streett_strategy, strategy_t::streett))
         return maybe;
-      return default_strategy(aut);
+      return default_strategy(simp);
     }
   }
 

spot/twaalgos/totgba.cc

 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
-// Développement de l'Epita.
+// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
+// de l'Epita.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -724,6 +724,7 @@ namespace spot
               }
           }
       }
+    simplify_acceptance_here(out);
     return out;
   }
 

tests/core/remfin.test

 #!/bin/sh
 # -*- coding: utf-8 -*-
 
-# Copyright (C) 2015-2017 Laboratoire de Recherche et Développement de
+# Copyright (C) 2015-2018 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -394,7 +394,8 @@ State: 0
 [!0] 0
 [0] 1
 State: 1 {0}
-[t] 1
+[!0] 1
+[0] 1
 --END--
 HOA: v1
 States: 10
@@ -589,9 +590,8 @@ HOA: v1
 States: 37
 Start: 0
 AP: 2 "a" "b"
-acc-name: generalized-Buchi 12
-Acceptance: 12 Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)&Inf(6)\
-&Inf(7)&Inf(8)&Inf(9)&Inf(10)&Inf(11)
+acc-name: Buchi
+Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc complete
 --BODY--
 State: 0
@@ -731,7 +731,7 @@ State: 32
 State: 33
 [t] 33
 [!1] 36
-State: 34 {0 1 2 3 4 5 6 7 8 9 10 11}
+State: 34 {0}
 [t] 34
 State: 35
 [1] 34
@@ -750,11 +750,11 @@ properties: trans-labels explicit-labels state-acc complete
 properties: deterministic
 --BODY--
 State: 0
-[!0] 0
 [0] 1
-State: 1 {0}
 [!0] 0
+State: 1 {0}
 [0] 1
+[!0] 0
 --END--
 HOA: v1
 States: 21

tests/python/tra2tba.py

@@ -94,8 +94,8 @@ exp = """HOA: v1
 States: 2
 Start: 0
 AP: 2 "a" "b"
-acc-name: Buchi
-Acceptance: 1 Inf(0)
+acc-name: none
+Acceptance: 0 f
 properties: trans-labels explicit-labels state-acc deterministic
 --BODY--
 State: 0
@@ -383,11 +383,11 @@ Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc deterministic
 --BODY--
 State: 0 {0}
-[!1&!2] 0
 [1&!2] 1
-State: 1
 [!1&!2] 0
+State: 1
 [1&!2] 1
+[!1&!2] 0
 --END--"""
 
 res = spot.remove_fin(aut)