diff --git a/spot/twaalgos/complete.cc b/spot/twaalgos/complete.cc index 41db648cf..2373eeaf8 100644 --- a/spot/twaalgos/complete.cc +++ b/spot/twaalgos/complete.cc @@ -108,6 +108,7 @@ namespace spot { bdd missingcond = bddtrue; acc_cond::mark_t acc = 0U; + unsigned edge_to_sink = 0; for (auto& t: aut->out(i)) { missingcond -= t.cond; @@ -125,6 +126,8 @@ namespace spot // acceptance sets as the last outgoing edge of the // state. acc = t.acc; + if (t.dst == sink) + edge_to_sink = aut->edge_number(t); } // If the state has incomplete successors, we need to add a // edge to some sink state. @@ -136,11 +139,20 @@ namespace spot sink = aut->new_state(); aut->new_edge(sink, sink, bddtrue, um.second); } - // In case the automaton use state-based acceptance, propagate - // the acceptance of the first edge to the one we add. - if (aut->prop_state_acc() != true) - acc = 0U; - aut->new_edge(i, sink, missingcond, acc); + // If we already have a brother-edge to the sink, + // add the missing condition to that edge. + if (edge_to_sink) + { + aut->edge_data(edge_to_sink).cond |= missingcond; + } + else // otherwise, create the new edge. + { + // in case the automaton use state-based acceptance, propagate + // the acceptance of the first edge to the one we add. + if (!aut->prop_state_acc().is_true()) + acc = 0U; + aut->new_edge(i, sink, missingcond, acc); + } } } diff --git a/tests/core/complete.test b/tests/core/complete.test index c05b436f4..8b2a7f947 100755 --- a/tests/core/complete.test +++ b/tests/core/complete.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement +# Copyright (C) 2015-2017 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -152,11 +152,9 @@ properties: trans-labels explicit-labels state-acc complete properties: deterministic --BODY-- State: 0 -[0] 1 -[!0] 1 +[t] 1 State: 1 -[0] 1 -[!0] 1 +[t] 1 --END-- HOA: v1 States: 3 @@ -186,8 +184,7 @@ properties: trans-labels explicit-labels state-acc complete properties: deterministic --BODY-- State: 0 -[0] 1 -[!0] 1 +[t] 1 State: 1 {0} [0] 1 [!0] 1 @@ -205,8 +202,7 @@ State: 0 [!0 | 1] 0 [0&!1] 0&1 State: 1 {0} -[0&!1] 1 -[!0 | 1] 1 +[t] 1 --END-- HOA: v1 States: 2 diff --git a/tests/python/dualize.py b/tests/python/dualize.py index c3601f5b3..768b18359 100755 --- a/tests/python/dualize.py +++ b/tests/python/dualize.py @@ -408,13 +408,11 @@ properties: deterministic --BODY-- State: 0 [0&1] 1 -[0&!1] 2 -[!0] 2 +[!0 | !1] 2 State: 1 {0} [t] 1 State: 2 -[0] 2 -[!0] 2 +[t] 2 --END--""" aut = spot.automaton("""