From cebc4b00b54628975b90dd0dba18662db9860355 Mon Sep 17 00:00:00 2001
From: Thomas Medioni <tmedioni@lrde.epita.fr>
Date: Fri, 17 Mar 2017 16:51:36 +0100
Subject: [PATCH] sum: Fix universal initial state bug

* spot/twaalgos/sum.cc: Fix the sum of automatas having universal
  initial transitions.
* tests/core/explsum.test: Add test case testing the handling of
  universal initial transitions in sum.
---
 spot/twaalgos/sum.cc    | 60 +++++++++++++++++++--------------
 tests/core/explsum.test | 74 +++++++++++++++++++++++++++++++++++++++--
 2 files changed, 106 insertions(+), 28 deletions(-)

diff --git a/spot/twaalgos/sum.cc b/spot/twaalgos/sum.cc
index ba1b8a429..61f4fa925 100644
--- a/spot/twaalgos/sum.cc
+++ b/spot/twaalgos/sum.cc
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include <spot/twaalgos/alternation.hh>
 #include <spot/twaalgos/sum.hh>
 #include <spot/twa/twagraph.hh>
 #include <vector>
@@ -30,25 +31,23 @@ namespace spot
     // in replacement of graph_init
     static
     void connect_init_state(const twa_graph_ptr& res,
-                            const const_twa_graph_ptr& graph,
                             unsigned init,
-                            unsigned graph_init,
-                            unsigned offset = 0U)
+                            const const_twa_graph_ptr& left,
+                            const const_twa_graph_ptr& right,
+                            unsigned left_init,
+                            unsigned right_init,
+                            unsigned offset)
     {
-      std::map<unsigned, bdd> edges;
-      std::vector<unsigned> dst;
-      for (auto& e : graph->out(graph_init))
-        {
-          for (auto& d : graph->univ_dests(e))
-            dst.push_back(d + offset);
-          if (dst.size() > 1)
-            res->new_univ_edge(init, dst.begin(), dst.end(), e.cond, 0U);
-          else
-            edges[dst[0]] |= e.cond;
-          dst.clear();
-        }
-      for (auto& p : edges)
-        res->new_edge(init, p.first, p.second);
+      bdd comb_left = bddtrue;
+      outedge_combiner oe(res);
+      for (unsigned c : left->univ_dests(left_init))
+        comb_left &= oe(c);
+
+      bdd comb_right = bddtrue;
+      for (unsigned c : right->univ_dests(right_init))
+        comb_right &= oe(c + offset);
+
+      oe.new_dests(init, comb_left | comb_right);
     }
 
     // Helper function that copies the states of graph into res, adding
@@ -60,14 +59,14 @@ namespace spot
                     acc_cond::mark_t mark = 0U,
                     unsigned offset = 0U)
     {
-      auto state_offset = res->num_states();
+      unsigned state_offset = res->num_states();
 
       res->new_states(graph->num_states());
 
       std::vector<unsigned> dst;
       for (auto& e : graph->edges())
         {
-          for (auto& d : graph->univ_dests(e))
+          for (unsigned d : graph->univ_dests(e))
             dst.push_back(d + state_offset);
 
           res->new_univ_edge(e.src + state_offset,
@@ -99,7 +98,7 @@ namespace spot
       acc_cond::mark_t markl = 0U;
       acc_cond::mark_t markr = 0U;
       auto left_acc = left->get_acceptance();
-      auto left_num_sets = left->num_sets();
+      unsigned left_num_sets = left->num_sets();
       if (!unsatl.first)
         {
           markl.set(0);
@@ -113,7 +112,7 @@ namespace spot
 
       auto unsatr = right->acc().unsat_mark();
       auto right_acc = right->get_acceptance();
-      auto right_num_sets = right->num_sets();
+      unsigned right_num_sets = right->num_sets();
       if (!unsatr.first)
         {
           markr.set(left_num_sets);
@@ -134,13 +133,24 @@ namespace spot
           unsigned init = res->new_state();
           res->set_init_state(init);
 
-          connect_init_state(res, left, init, left_state);
-          connect_init_state(res, right, init, right_state, left->num_states());
+          connect_init_state(res,
+                             init,
+                             left,
+                             right,
+                             left_state,
+                             right_state,
+                             left->num_states());
         }
       else
         {
-          res->set_univ_init_state({ left_state,
-                                     right_state + left->num_states() });
+          std::vector<unsigned> stl;
+          for (unsigned d : left->univ_dests(left_state))
+            stl.push_back(d);
+
+          for (unsigned d : right->univ_dests(right_state))
+            stl.push_back(d + left->num_states());
+
+          res->set_univ_init_state(stl.begin(), stl.end());
         }
       return res;
    }
diff --git a/tests/core/explsum.test b/tests/core/explsum.test
index b4883a18e..452d99e0a 100755
--- a/tests/core/explsum.test
+++ b/tests/core/explsum.test
@@ -135,8 +135,8 @@ State: 4
 [!0] 2 {2}
 [2] 3 {2}
 State: 5
-[1] 1
 [0] 3
+[1] 1
 [1] 4
 --END--
 HOA: v1
@@ -161,8 +161,8 @@ State: 4
 [2] 3 {0 1}
 State: 5
 [0] 0
-[1] 1
 [0] 3
+[1] 1
 [1] 4
 --END--
 HOA: v1
@@ -214,4 +214,72 @@ EOF
 
 run 0 autfilt false1 --sum false2 --hoaf=t | tee stdout
 diff stdout expected
-rm false1 false2 input1 input2 input3 input4 expected stdout
+rm stdout
+
+cat >expected <<EOF
+HOA: v1
+States: 7
+Start: 0&2&5
+AP: 3 "b" "a" "c"
+Acceptance: 4 Fin(0) | Inf(1) | (Inf(2)&Inf(3))
+properties: univ-branch trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[1] 0 {0}
+[0] 1
+State: 1
+[0] 1
+State: 2
+[1] 3 {0 1}
+[0] 4 {0 1}
+State: 3
+State: 4
+[!1] 2 {0 1}
+[2] 3 {0 1}
+State: 5
+[0] 6 {0 2}
+State: 6
+[1] 5 {0 3}
+--END--
+EOF
+
+run 0 autfilt input1 --sum-and input2 | tee temp
+run 0 autfilt input3 --sum-and temp | tee stdout
+diff stdout expected
+rm stdout
+
+cat >expected <<EOF
+HOA: v1
+States: 8
+Start: 7
+AP: 3 "b" "a" "c"
+Acceptance: 4 Fin(0) | Inf(1) | (Inf(2)&Inf(3))
+properties: univ-branch trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[1] 0 {0}
+[0] 1
+State: 1
+[0] 1
+State: 2
+[1] 3 {0 1}
+[0] 4 {0 1}
+State: 3
+State: 4
+[!1] 2 {0 1}
+[2] 3 {0 1}
+State: 5
+[0] 6 {0 2}
+State: 6
+[1] 5 {0 3}
+State: 7
+[0&1] 3&6
+[0] 1
+[0] 4&6
+[1] 0
+--END--
+EOF
+
+run 0 autfilt input3 --sum temp | tee stdout
+diff stdout expected
+rm false1 false2 input1 input2 input3 input4 expected stdout temp