genem: improve the worst case

* spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: Improve the worst
case by not recurring twice into each disjunct individually.  Keep
the previous two implementation available and add a function
generic_emptiness_check_select_version() so we can benchmark the
difference.
* tests/python/genem.py: Test the three versions.

spot/twaalgos/genem.cc

@@ -23,6 +23,25 @@
 
 namespace spot
 {
+  namespace
+  {
+    enum genem_version_t { spot28, atva19, spot29 };
+    static genem_version_t genem_version = spot29;
+  }
+
+  void generic_emptiness_check_select_version(const char* emversion)
+  {
+    if (emversion == nullptr || !strcasecmp(emversion, "spot29"))
+      genem_version = spot29;
+    else if (!strcasecmp(emversion, "spot28"))
+      genem_version = spot28;
+    else if (!strcasecmp(emversion, "atva19"))
+      genem_version = atva19;
+    else
+      throw std::invalid_argument("generic_emptiness_check version should"
+                                  " be one of {spot28, atva19, spot29}");
+  }
+
   namespace
   {
     static bool
@@ -65,6 +84,26 @@ namespace spot
       acc_cond acc = autacc.restrict_to(sets);
       acc = acc.remove(si.common_sets_of(scc), false);
 
+      auto generic_recurse =
+        [&] (const acc_cond& subacc)
+        {
+          int fo = (SPOT_UNLIKELY(genem_version == spot28)
+                    ? acc.fin_one() : subacc.fin_one());
+          assert(fo >= 0);
+          // Try to accept when Fin(fo) == true
+          acc_cond::mark_t fo_m = {(unsigned) fo};
+          if (!scc_split_check
+              (si, scc, subacc.remove(fo_m, true), run, fo_m))
+            return false;
+          // Try to accept when Fin(fo) == false
+          if (!is_scc_empty(si, scc, subacc.force_inf(fo_m), run, tocut))
+            return false;
+          return true;
+        };
+
+      if (SPOT_LIKELY(genem_version == spot29))
+        {
+          acc_cond::acc_code rest = acc_cond::acc_code::f();
           for (const acc_cond& disjunct: acc.top_disjuncts())
             if (acc_cond::mark_t fu = disjunct.fin_unit())
               {
@@ -74,17 +113,26 @@ namespace spot
               }
             else
               {
-            int fo = disjunct.fin_one();
-            assert(fo >= 0);
-            // Try to accept when Fin(fo) == true
-            acc_cond::mark_t fo_m = {(unsigned) fo};
+                rest |= disjunct.get_acceptance();
+              }
+          if (!rest.is_f() && !generic_recurse(acc_cond(acc.num_sets(), rest)))
+            return false;
+        }
+      else
+        {
+          for (const acc_cond& disjunct: acc.top_disjuncts())
+            if (acc_cond::mark_t fu = disjunct.fin_unit())
+              {
                 if (!scc_split_check
-                (si, scc, disjunct.remove(fo_m, true), run, fo_m))
+                    (si, scc, disjunct.remove(fu, true), run, fu))
                   return false;
-            // Try to accept when Fin(fo) == false
-            if (!is_scc_empty(si, scc, disjunct.force_inf(fo_m), run, tocut))
+              }
+            else
+              {
+                if (!generic_recurse(disjunct))
                   return false;
               }
+        }
       return true;
     }
 

spot/twaalgos/genem.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017-2019 Laboratoire de Recherche et Developpement
+// Copyright (C) 2017-2020 Laboratoire de Recherche et Developpement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -61,4 +61,23 @@ namespace spot
   SPOT_API bool
   generic_emptiness_check_for_scc(const scc_info& si, unsigned scc,
                                   const acc_cond& forced_acc);
+
+
+  /// \ingroup emptiness_check_algorithms
+  ///
+  /// Select the version of the generic-emptiness check to use, this
+  /// is mainly for benchmarking purpose.
+  ///
+  /// We currently have three versions:
+  /// - "spot28" is similar to the algorithm described our ATVA'19 paper
+  ///   \cite baier.19.atva , however it has an implementation bug
+  ///   that cause superfluous recursive calls to be performed (the
+  ///   result is still correct.
+  /// - "atva19" is similar to the algorithm described our ATVA'19 paper
+  ///   \cite baier.19.atva , with the above bug fixed.
+  /// - "spot29" improves upon the worst case of atva19.  This is
+  ///   the default.
+  SPOT_API void
+  generic_emptiness_check_select_version(const char* emversion = nullptr);
+
 }

tests/python/genem.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018-2019 Laboratoire de Recherche et Développement de l'Epita
+# Copyright (C) 2018-2020 Laboratoire de Recherche et Développement de l'Epita
 # (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -283,17 +283,22 @@ def is_scc_empty2(si, scc_num, acc=None):
 
 def run_bench(automata):
     for aut in automata:
-        # Make sure our three implementation behave identically
+        # Make sure all our implementations behave identically
         res5 = is_empty2(aut)
         res4 = is_empty1(aut)
-        res3 = spot.generic_emptiness_check(aut)
+        spot.generic_emptiness_check_select_version("spot28")
+        res3a = spot.generic_emptiness_check(aut)
+        spot.generic_emptiness_check_select_version("atva19")
+        res3b = spot.generic_emptiness_check(aut)
+        spot.generic_emptiness_check_select_version("spot29")
+        res3c = spot.generic_emptiness_check(aut)
         res2 = spot.remove_fin(aut).is_empty()
         res1 = generic_emptiness2(aut)
-        res = (str(res1)[0] + str(res2)[0] + str(res3)[0]
-               + str(res4)[0] + str(res5)[0])
+        res = (str(res1)[0] + str(res2)[0] + str(res3a)[0]
+               + str(res3b)[0] + str(res3c)[0] + str(res4)[0] + str(res5)[0])
         print(res)
-        assert res in ('TTTTT', 'FFFFF')
-        if res == 'FFFFF':
+        assert res in ('TTTTTTT', 'FFFFFFF')
+        if res == 'FFFFFFF':
             run3 = spot.generic_accepting_run(aut)
             assert run3.replay(spot.get_cout()) is True