genem: Add yet another version of the algorithm

* spot/twa/acc.hh, spot/twa/acc.cc (fin_unit_one_split_improved): New
function.
* python/spot/impl.i: Add bindings for fin_unit_one_split_improved.
* spot/twaalgos/genem.cc: Add the spot212 version.
* tests/python/genem.py: Test it.

python/spot/impl.i

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009-2022 Laboratoire de Recherche et Développement
+// Copyright (C) 2009-2023 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -564,6 +564,16 @@ namespace std {
                              swig::from(std::get<2>(v)));
   }
 %}
+// Must occur before the twa declaration
+%typemap(out) SWIGTYPE spot::acc_cond::fin_unit_one_split_improved %{
+  {
+      auto& v = static_cast<const std::tuple<int, spot::acc_cond, spot::acc_cond>>($1);
+      $result = PyTuple_Pack(3,
+                             swig::from(std::get<0>(v)),
+                             swig::from(std::get<1>(v)),
+                             swig::from(std::get<2>(v)));
+  }
+%}
 
 %include <spot/twa/acc.hh>
 %template(pair_bool_mark) std::pair<bool, spot::acc_cond::mark_t>;

spot/twa/acc.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2022 Laboratoire de Recherche et Développement
+// Copyright (C) 2015-2023 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -2707,8 +2707,9 @@ namespace spot
       return false;
     }
 
-    // Check wheter pos looks like Fin(f) or Fin(f)&rest
+    // Check if pos contains Fin(f) in a substree
-    bool is_conj_fin(const acc_cond::acc_word* pos, acc_cond::mark_t f)
+    template<bool top_conjunct_only = false>
+    bool has_fin(const acc_cond::acc_word* pos, acc_cond::mark_t f)
     {
       auto sub = pos - pos->sub.size;
       do
@@ -2719,7 +2720,10 @@ namespace spot
               --pos;
               break;
             case acc_cond::acc_op::Or:
+              if constexpr (top_conjunct_only)
                 pos -= pos->sub.size + 1;
+              else
+                --pos;
               break;
             case acc_cond::acc_op::Fin:
               if (pos[-1].mark & f)
@@ -2736,6 +2740,12 @@ namespace spot
       return false;
     }
 
+    // Check whether pos looks like Fin(f) or Fin(f)&rest
+    bool is_conj_fin(const acc_cond::acc_word* pos, acc_cond::mark_t f)
+    {
+      return has_fin<true>(pos, f);
+    }
+
     acc_cond::acc_code extract_fin(const acc_cond::acc_word* pos,
                                    acc_cond::mark_t f)
     {
@@ -2772,6 +2782,7 @@ namespace spot
       return {};
     }
 
+    template<bool deeper_check = false>
     std::pair<acc_cond::acc_code, acc_cond::acc_code>
     split_top_fin(const acc_cond::acc_word* pos, acc_cond::mark_t f)
     {
@@ -2798,6 +2809,17 @@ namespace spot
                     tmp |= std::move(left);
                     std::swap(tmp, left);
                   }
+                else if (deeper_check
+                         && has_top_fin(pos) == -1
+                         && has_fin(pos, f))
+                  {
+                    auto tmp = strip_rec(pos, f, true, false);
+                    tmp |= std::move(left);
+                    std::swap(tmp, left);
+                    tmp = force_inf_rec(pos, f);
+                    tmp |= std::move(right);
+                    std::swap(tmp, right);
+                  }
                 else
                   {
                     acc_cond::acc_code tmp(pos);
@@ -2851,6 +2873,27 @@ namespace spot
     return {selected_fin, extract_fin(pos, fo_m), force_inf(fo_m)};
   }
 
+  std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
+  acc_cond::acc_code::fin_unit_one_split_improved() const
+  {
+    if (SPOT_UNLIKELY(is_t() || is_f()))
+    err:
+      throw std::runtime_error("fin_unit_one_split_improved(): no Fin");
+    const acc_cond::acc_word* pos = &back();
+    int selected_fin = has_top_fin(pos);
+    if (selected_fin >= 0)
+      {
+        auto [left, right] =
+          split_top_fin<true>(pos, {(unsigned) selected_fin});
+        return {selected_fin, std::move(left), std::move(right)};
+      }
+    selected_fin = fin_one();
+    if (selected_fin < 0)
+      goto err;
+    acc_cond::mark_t fo_m = {(unsigned) selected_fin};
+    return {selected_fin, extract_fin(pos, fo_m), force_inf(fo_m)};
+  }
+
   namespace
   {
     bool

spot/twa/acc.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2022 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2023 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -1300,21 +1300,26 @@ namespace spot
       /// \brief Split an acceptance condition, trying to select one
       /// unit-Fin.
       ///
-      /// If the condition is a disjunction and one of the disjunct as
+      /// If the condition is a disjunction and one of the disjunct has
-      /// has the shape `...&Fin(i)&...`, then this will return
+      /// the shape `...&Fin(i)&...`, then this will return (i, left,
-      /// (i, left, right), where left is all disjunct of this form, and
+      /// right), where left is all disjunct of this form (with Fin(i)
-      /// right are all the others.
+      /// replaced by true), and right are all the others.
       ///
       /// If the input formula has the shape `...&Fin(i)&...` then left
-      /// is set to the entire formula, and right is empty.
+      /// is set to the entire formula (with Fin(i) replaced by true),
+      /// and right is empty.
       ///
       /// If no disjunct has the right shape, then a random Fin(i) is
       /// searched in the formula, and the output (i, left, right).
       /// is such that left contains all disjuncts containing Fin(i)
       /// (at any depth), and right contains the original formlula
       /// where Fin(i) has been replaced by false.
+      /// @{
       std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
       fin_unit_one_split() const;
+      std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
+      fin_unit_one_split_improved() const;
+      /// @}
 
       /// \brief Help closing accepting or rejecting cycle.
       ///
@@ -2258,25 +2263,34 @@ namespace spot
     /// \brief Split an acceptance condition, trying to select one
     /// unit-Fin.
     ///
-    /// If the condition is a disjunction and one of the disjunct as
+    /// If the condition is a disjunction and one of the disjunct has
-    /// has the shape `...&Fin(i)&...`, then this will return
+    /// the shape `...&Fin(i)&...`, then this will return (i, left,
-    /// (i, left, right), where left is all disjunct of this form, and
+    /// right), where left is all disjunct of this form (with Fin(i)
-    /// right are all the others.
+    /// replaced by true), and right are all the others.
     ///
     /// If the input formula has the shape `...&Fin(i)&...` then left
-    /// is set to the entire formula, and right is empty.
+    /// is set to the entire formula (with Fin(i) replaced by true),
+    /// and right is empty.
     ///
     /// If no disjunct has the right shape, then a random Fin(i) is
     /// searched in the formula, and the output (i, left, right).
     /// is such that left contains all disjuncts containing Fin(i)
     /// (at any depth), and right contains the original formlula
     /// where Fin(i) has been replaced by false.
+    /// @{
     std::tuple<int, acc_cond, acc_cond>
     fin_unit_one_split() const
     {
       auto [f, l, r] = code_.fin_unit_one_split();
       return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}};
     }
+    std::tuple<int, acc_cond, acc_cond>
+    fin_unit_one_split_improved() const
+    {
+      auto [f, l, r] = code_.fin_unit_one_split_improved();
+      return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}};
+    }
+    /// @}
 
     /// \brief Return the top-level disjuncts.
     ///

spot/twaalgos/genem.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017-2022 Laboratoire de Recherche et Developpement
+// Copyright (C) 2017-2023 Laboratoire de Recherche et Developpement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -25,7 +25,7 @@ namespace spot
 {
   namespace
   {
-    enum genem_version_t { spot28, atva19, spot29, spot210, spot211 };
+    enum genem_version_t { spot28, atva19, spot29, spot210, spot211, spot212 };
     static genem_version_t genem_version = spot29;
   }
 
@@ -33,6 +33,8 @@ namespace spot
   {
     if (emversion == nullptr || !strcasecmp(emversion, "spot29"))
       genem_version = spot29;
+    else if (!strcasecmp(emversion, "spot212"))
+      genem_version = spot212;
     else if (!strcasecmp(emversion, "spot211"))
       genem_version = spot211;
     else if (!strcasecmp(emversion, "spot210"))
@@ -44,7 +46,7 @@ namespace spot
     else
       throw std::invalid_argument("generic_emptiness_check version should be "
                                   "one of {spot28, atva19, spot29, spot210, "
-                                  "spot211}");
+                                  "spot211, spot212}");
   }
 
   namespace
@@ -87,7 +89,9 @@ namespace spot
     scc_split_check(const scc_info& si, unsigned scc, const acc_cond& acc,
                     Extra extra, acc_cond::mark_t tocut)
     {
-      if (genem_version == spot211 || genem_version == spot210)
+      if (genem_version == spot211
+          || genem_version == spot212
+          || genem_version == spot210)
         tocut |= acc.fin_unit();
       scc_and_mark_filter filt(si, scc, tocut);
       filt.override_acceptance(acc);
@@ -144,6 +148,20 @@ namespace spot
             }
           while (!acc.is_f());
         }
+      else if (genem_version == spot212)
+        {
+          do
+            {
+              auto [fo, fpart, rest] = acc.fin_unit_one_split_improved();
+              acc_cond::mark_t fo_m = {(unsigned) fo};
+              if (!scc_split_check<EarlyStop, Extra>
+                  (si, scc, fpart, extra, fo_m))
+                if constexpr (EarlyStop)
+                  return false;
+              acc = rest;
+            }
+          while (!acc.is_f());
+        }
       else if (genem_version == spot29)
         do
           {

tests/python/genem.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018-2022 Laboratoire de Recherche et Développement de
+# Copyright (C) 2018-2023 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -307,15 +307,18 @@ def run_bench(automata):
         res3d = spot.generic_emptiness_check(aut)
         spot.generic_emptiness_check_select_version("spot211")
         res3e = spot.generic_emptiness_check(aut)
+        spot.generic_emptiness_check_select_version("spot212")
+        res3f = spot.generic_emptiness_check(aut)
         spot.generic_emptiness_check_select_version("spot29")
         res2 = spot.remove_fin(aut).is_empty()
         res1 = generic_emptiness2(aut)
         res = (str(res1)[0] + str(res2)[0] + str(res3a)[0]
                + str(res3b)[0] + str(res3c)[0] + str(res3d)[0]
-               + str(res3e)[0] + str(res4)[0] + str(res5)[0])
+               + str(res3e)[0] + str(res3f)[0] + str(res4)[0]
+               + str(res5)[0])
         print(res)
-        tc.assertIn(res, ('TTTTTTTTT', 'FFFFFFFFF'))
+        tc.assertIn(res, ('TTTTTTTTTT', 'FFFFFFFFFF'))
-        if res == 'FFFFFFFFF':
+        if res == 'FFFFFFFFFF':
             run3 = spot.generic_accepting_run(aut)
             tc.assertTrue(run3.replay(spot.get_cout()))