genem: implement the logic from the future journal version of ATVA19

This version of the generic emptiness-check, using smart selection and
extraction of the Fin (implemented here via fin_one_extract), was
suggested by Jan Strejček on 2020-06-26.

* spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: Add the spot210
variant.  Also use it for the ACD use-case.
* spot/twaalgos/zlktree.cc (zielonka_tree): Also use the same logic
here.
* tests/python/genem.py: Test the new version as well.

spot/twaalgos/genem.cc

@@ -25,7 +25,7 @@ namespace spot
 {
   namespace
   {
-    enum genem_version_t { spot28, atva19, spot29 };
+    enum genem_version_t { spot28, atva19, spot29, spot210 };
     static genem_version_t genem_version = spot29;
   }
 
@@ -33,13 +33,15 @@ namespace spot
   {
     if (emversion == nullptr || !strcasecmp(emversion, "spot29"))
       genem_version = spot29;
+    else if (!strcasecmp(emversion, "spot210"))
+      genem_version = spot210;
     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"
+      throw std::invalid_argument("generic_emptiness_check version should be "
-                                  " be one of {spot28, atva19, spot29}");
+                                  "one of {spot28, atva19, spot29, spot210}");
   }
 
   namespace
@@ -108,34 +110,39 @@ namespace spot
       acc_cond acc = autacc.restrict_to(sets);
       acc = acc.remove(si.common_sets_of(scc), false);
 
-      if (SPOT_LIKELY(genem_version == spot29 || !EarlyStop))
+      if (SPOT_LIKELY(genem_version == spot210 || !EarlyStop))
+        do
+          {
+            auto [fo, fpart] = acc.fin_one_extract();
+            assert(fo >= 0);
+            // Try to accept when Fin(fo) == true
+            acc_cond::mark_t fo_m = {(unsigned) fo};
+            if (!scc_split_check<EarlyStop, Extra>
+                (si, scc, fpart.remove(fo_m, true), extra, fo_m))
+              if constexpr (EarlyStop)
+                return false;
+            // Try to accept when Fin(fo) == false
+            acc = acc.force_inf(fo_m);
+          }
+        while (!acc.is_f());
+      else if (genem_version == spot29)
         do
           {
             acc_cond::acc_code rest = acc_cond::acc_code::f();
-            if (EarlyStop)
+            for (const acc_cond& disjunct: acc.top_disjuncts())
-              {
+              if (acc_cond::mark_t fu = disjunct.fin_unit())
-                for (const acc_cond& disjunct: acc.top_disjuncts())
+                {
-                  if (acc_cond::mark_t fu = disjunct.fin_unit())
+                  if (!scc_split_check<EarlyStop, Extra>
-                    {
+                      (si, scc, disjunct.remove(fu, true), extra, fu))
-                      if (!scc_split_check<EarlyStop, Extra>
+                    if constexpr (EarlyStop)
-                          (si, scc, disjunct.remove(fu, true), extra, fu))
+                      return false;
-                        if constexpr (EarlyStop)
+                }
-                          return false;
+              else
-                    }
+                {
-                  else
+                  rest |= disjunct.get_acceptance();
-                    {
+                }
-                      rest |= disjunct.get_acceptance();
+            if (rest.is_f())
-                    }
+              break;
-                if (rest.is_f())
-                  break;
-              }
-            else
-              {
-                rest = acc.get_acceptance();
-                if (acc_cond::mark_t fu = rest.fin_unit())
-                  return scc_split_check<EarlyStop, Extra>
-                    (si, scc, rest.remove(fu, true), extra, fu);
-              }
             acc_cond subacc(acc.num_sets(), std::move(rest));
             int fo = subacc.fin_one();
             assert(fo >= 0);

spot/twaalgos/genem.hh

@@ -99,6 +99,8 @@ namespace spot
   ///   \cite baier.19.atva , with the above bug fixed.
   /// - "spot29" improves upon the worst case of atva19.  This is
   ///   the default.
+  /// - "spot210" improves upon "spot29" in a few cases where a Fin
+  ///   is shared by multiple disjuncts.
   SPOT_API void
   generic_emptiness_check_select_version(const char* emversion = nullptr);
 

spot/twaalgos/zlktree.cc

@@ -92,15 +92,15 @@ namespace spot
         {
           max_models(cond.remove(fu, true), colors - fu, out);
         }
-      // Otherwise, we simply have to pick a random Fin(x) and see if
+      // Otherwise, we simply have to pick some arbitrary Fin(x) and
-      // we can satisfy the condition when x is present or absent.  In
+      // see if we can satisfy the condition when x is present or
-      // this case, we do not know whether the generated models will
+      // absent.  In this case, we do not know whether the generated
-      // be maximal, so this justifies the inclusion checks between
+      // models will be maximal, so this justifies the inclusion
-      // models at the top of this function.
+      // checks between models at the top of this function.
-      else if (int fo = cond.fin_one(); fo >= 0)
+      else if (auto [fo, fpart] = cond.fin_one_extract(); fo >= 0)
         {
           acc_cond::mark_t fo_m = {(unsigned) fo};
-          max_models(cond.remove(fo_m, true), colors - fo_m, out);
+          max_models(fpart.remove(fo_m, true), colors - fo_m, out);
           max_models(cond.remove(fo_m, false), colors, out);
         }
     }

tests/python/genem.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018-2020 Laboratoire de Recherche et Développement de l'Epita
+# Copyright (C) 2018-2021 Laboratoire de Recherche et Développement de l'Epita
 # (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -292,13 +292,16 @@ def run_bench(automata):
         res3b = spot.generic_emptiness_check(aut)
         spot.generic_emptiness_check_select_version("spot29")
         res3c = spot.generic_emptiness_check(aut)
+        spot.generic_emptiness_check_select_version("spot210")
+        res3d = spot.generic_emptiness_check(aut)
         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(res4)[0] + str(res5)[0])
+               + str(res3b)[0] + str(res3c)[0] + str(res3d)[0]
+               + str(res4)[0] + str(res5)[0])
         print(res)
-        assert res in ('TTTTTTT', 'FFFFFFF')
+        assert res in ('TTTTTTTT', 'FFFFFFFF')
-        if res == 'FFFFFFF':
+        if res == 'FFFFFFFF':
             run3 = spot.generic_accepting_run(aut)
             assert run3.replay(spot.get_cout()) is True