From 81af8359f5d4ca61ca1aea9b516e9861010c9cd6 Mon Sep 17 00:00:00 2001
From: Alexandre GBAGUIDI AISSE <gbagui_a@epita.fr>
Date: Fri, 22 Sep 2017 18:46:57 +0200
Subject: [PATCH] twaalgos/cobuchi: Optimize aug. subset construction when aut.
 is det

* spot/twaalgos/cobuchi.cc: Avoid the product of an automaton A and its
power construction Pow(A) when A is deterministic.
---
 spot/twaalgos/cobuchi.cc | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc
index d92f9f48e..3f1536cdc 100644
--- a/spot/twaalgos/cobuchi.cc
+++ b/spot/twaalgos/cobuchi.cc
@@ -32,7 +32,6 @@
 #include <spot/twaalgos/isdet.hh>
 #include <spot/twaalgos/strength.hh>
 #include <spot/twaalgos/sbacc.hh>  // For issue #317
-
 #include <stack>
 #include <unordered_map>
 
@@ -69,7 +68,22 @@ namespace spot
                     bool named_states,
                     struct power_map& pmap)
     {
-      twa_graph_ptr res = product(aut_prod, tgba_powerset(aut_power, pmap));
+      twa_graph_ptr res = nullptr;
+
+      if (is_deterministic(aut_prod))
+        {
+          res = make_twa_graph(aut_prod, twa::prop_set::all());
+          auto v = new product_states;
+          res->set_named_prop("product-states", v);
+          for (unsigned s = 0; s < aut_power->num_states(); ++s)
+            v->emplace_back(s, s);
+          for (unsigned s = 0; s < aut_power->num_states(); ++s)
+            pmap.map_.push_back({s});
+        }
+      else
+        {
+          res = product(aut_prod, tgba_powerset(aut_power, pmap));
+        }
 
       if (named_states)
         {