From af67c04a67ede554b853a79ca3440a4f968d9f0b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 19 Mar 2019 17:11:43 +0100
Subject: [PATCH] genem: minor simplifications

* tests/python/genem.py: Use SPOT_ON_ACC explicitely.
* spot/twaalgos/genem.cc: Do not keep track of states.  Don't
check that the clauses of the disjuncts are Fin-less: they aren't
(this was discovered while discussing with Jan and Fanda).
---
 spot/twaalgos/genem.cc | 37 +++++++++++++++++--------------------
 tests/python/genem.py  |  2 +-
 2 files changed, 18 insertions(+), 21 deletions(-)

diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc
index c1fe01815..c6e35039d 100644
--- a/spot/twaalgos/genem.cc
+++ b/spot/twaalgos/genem.cc
@@ -86,8 +86,7 @@ namespace spot
       acc = acc.remove(si.common_sets_of(scc), false);
       temporary_acc_set tmp(si.get_aut(), acc);
       scc_info upper_si(si.get_aut(), si.one_state_of(scc), filter, &data,
-                        scc_info_options::STOP_ON_ACC
-                        | scc_info_options::TRACK_STATES);
+                        scc_info_options::STOP_ON_ACC);
 
       const int accepting_scc = upper_si.one_accepting_scc();
       if (accepting_scc >= 0)
@@ -144,22 +143,21 @@ namespace spot
               do
                 {
                   --pos;
-                  if (pos->sub.op != acc_cond::acc_op::Inf)
-                    {
-                      acc_cond::acc_code one(pos);
-                      tmp.set(one);
-                      if (si.get_aut()->acc().uses_fin_acceptance())
-                        {
-                          acc_cond::mark_t plus = {};
-                          if (acc_cond::mark_t fu = one.fin_unit())
-                            plus = fu;
-                          if (!scc_split_check
-                              (si, scc, run, tocut | plus,
-                               generic_emptiness_check_for_scc_nocopy
-                               <deal_with_disjunct>))
-                            return false;
-                        }
-                    }
+                  acc_cond::acc_code one(pos);
+                  // This sets the acceptance of the automaton we
+                  // are working on.
+                  tmp.set(one);
+                  // Because we use scc_info with STOP_ON_ACC and test
+                  // for this, every clauses should contain a Fin.  Also
+                  assert(si.get_aut()->acc().uses_fin_acceptance());
+                  acc_cond::mark_t plus = {};
+                  if (acc_cond::mark_t fu = one.fin_unit())
+                    plus = fu;
+                  if (!scc_split_check
+                      (si, scc, run, tocut | plus,
+                       generic_emptiness_check_for_scc_nocopy
+                       <deal_with_disjunct>))
+                    return false;
                   pos -= pos->sub.size;
                 }
               while (pos > start);
@@ -216,8 +214,7 @@ namespace spot
         return aut->is_empty();
       }
 
-      scc_info si(aut, scc_info_options::STOP_ON_ACC
-                  | scc_info_options::TRACK_STATES);
+      scc_info si(aut, scc_info_options::STOP_ON_ACC);
 
       const int accepting_scc = si.one_accepting_scc();
       if (accepting_scc >= 0)
diff --git a/tests/python/genem.py b/tests/python/genem.py
index 58db36910..fc0c26614 100644
--- a/tests/python/genem.py
+++ b/tests/python/genem.py
@@ -141,7 +141,7 @@ def generic_emptiness2_rec(aut):
     # algorithm.
     if not aut.acc().uses_fin_acceptance():
         return aut.is_empty()
-    si = spot.scc_info(aut, True)
+    si = spot.scc_info(aut, spot.scc_info_options_STOP_ON_ACC)
     acc_scc = si.one_accepting_scc()
     if acc_scc >= 0:
         return False