product_susp: fix handling of unsatisfiable/universal acceptances

Part of issue #546 reported by Rüdiger Ehlers

* spot/twaalgos/product.cc (product_susp): Fix detection and handling
of unsatisfiable/universal acceptances.
* tests/python/_product_susp.ipynb: Add test cases.

NEWS

@@ -112,6 +112,10 @@ New in spot 2.11.6.dev  (not yet released)
     (Issue #541.)  This has been fixed by disabled the use_simulation
     optimization in this case.
 
+  - product_or_susp() and product_susp() would behave incorrectly in
+    presence of unsatisifable or universal acceptance conditions that
+    were not f or t.  (Part of issue #546.)
+
 New in spot 2.11.6  (2023-08-01)
 
   Bug fixes:

spot/twaalgos/product.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2020, 2022 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2020, 2022, 2023 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -607,33 +607,36 @@ namespace spot
         throw std::runtime_error("product_susp(): left and right automata "
                                  "should share their bdd_dict");
 
-      auto false_or_left = [&] (bool ff)
+      auto const_automaton = [&left] (bool is_true)
-        {
+      {
-          if (ff)
+        auto res = make_twa_graph(left->get_dict());
-            {
+        res->new_state();
-              auto res = make_twa_graph(left->get_dict());
+        res->prop_terminal(true);
-              res->new_state();
+        res->prop_stutter_invariant(true);
-              res->prop_terminal(true);
+        res->prop_universal(true);
-              res->prop_stutter_invariant(true);
+        res->prop_complete(is_true);
-              res->prop_universal(true);
+        if (is_true)
-              res->prop_complete(false);
+          res->new_edge(0, 0, bddtrue);
-              return res;
+        return res;
-            }
+      };
-          return make_twa_graph(left, twa::prop_set::all());
-        };
 
       // We assume RIGHT is suspendable, but we want to deal with some
       // trivial true/false cases so we can later assume right has
       // more than one acceptance set.
       // Note: suspendable with "t" acceptance = universal language.
-      if (SPOT_UNLIKELY(right->num_sets() == 0))
+      if (SPOT_UNLIKELY(right->num_sets() == 0
+                        || right->num_edges() == 0
+                        || right->acc().is_t()
+                        || right->acc().is_f()))
         {
-          if (and_acc)
+        trivial:
-            return false_or_left(right->is_empty());
+          if (and_acc && right->is_empty())
-          else if (right->is_empty()) // left OR false = left
+            return const_automaton(false);
+          else if (!and_acc && !right->is_empty())
+            // suspendable with "t" acceptance = universal language.
+            return const_automaton(true);
+          else // left AND true = left; left OR false = left
             return make_twa_graph(left, twa::prop_set::all());
-          else // left OR true = true
-            return make_twa_graph(right, twa::prop_set::all());
         }
 
       auto res = make_twa_graph(left->get_dict());
@@ -644,8 +647,8 @@ namespace spot
       res->prop_state_acc(left->prop_state_acc() && right->prop_state_acc());
 
       auto rightunsatmark = right->acc().unsat_mark();
-      if (SPOT_UNLIKELY(!rightunsatmark.first))
+      if (SPOT_UNLIKELY(!rightunsatmark.first)) // right is universal
-        return false_or_left(and_acc);
+        goto trivial;
       acc_cond::mark_t rejmark = rightunsatmark.second;
 
       if (leftweak)