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 .
+#include
#include
#include
#include
@@ -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 edges;
- std::vector 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 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 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 <expected <