diff --git a/NEWS b/NEWS index ff522766e..1bbb7c628 100644 --- a/NEWS +++ b/NEWS @@ -130,6 +130,8 @@ New in spot 1.99.6a (not yet released) was registered several times. * product() would incorrectly mark the product of two sttuter-sensitive automata as stutter-sensitive as well. + * complete() could incorrectly reuse an existing (but accepting!) + state as a sink. New in spot 1.99.6 (2015-12-04) diff --git a/spot/twaalgos/complete.cc b/spot/twaalgos/complete.cc index 1c6bfd9b2..cdccfde6b 100644 --- a/spot/twaalgos/complete.cc +++ b/spot/twaalgos/complete.cc @@ -45,27 +45,38 @@ namespace spot } else { - // Loop over the states and seek a state that has only self - // loops, and that is not accepting. This will be our sink - // state. Note that we do not even have to ensure that the - // state is complete as we will complete the whole automaton - // in a second pass. + // Loop over the states and search a state that has only self + // loop labeled by the same non-accepting mark. This will be + // our sink state. Note that we do not even have to ensure + // that the state is complete as we will complete the whole + // automaton in a second pass. for (unsigned i = 0; i < n; ++i) { - bool selfloop = true; - acc_cond::mark_t accsum = 0U; + bool sinkable = true; + bool first = true; + acc_cond::mark_t commonacc = 0U; for (auto& t: aut->out(i)) { if (t.dst != i) // Not a self-loop { - selfloop = false; + sinkable = false; + break; + } + if (first) + { + commonacc = t.acc; + first = false; + } + else if (t.acc != commonacc) + { + sinkable = false; break; } - accsum |= t.acc; } - if (selfloop && !aut->acc().accepting(accsum)) + if (sinkable && !aut->acc().accepting(commonacc)) { // We have found a sink! + um.second = commonacc; sink = i; break; } @@ -74,8 +85,7 @@ namespace spot unsigned t = aut->num_edges(); - // If the automaton is empty, - // pretend that state + // If the automaton is empty, pretend that state 0 is a sink. if (t == 0) sink = init; diff --git a/tests/core/complete.test b/tests/core/complete.test index 19f82465a..27a76d931 100755 --- a/tests/core/complete.test +++ b/tests/core/complete.test @@ -1,7 +1,7 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -57,6 +57,31 @@ State: 0 State: 1 [0] 1 --END-- +/* This example comes from Alexandre Lewkowicz */ +HOA: v1 +States: 2 +Start: 0 +AP: 1 "a" +Acceptance: 2 Fin(0)&Inf(1) +--BODY-- +State: 0 +[0] 1 +State: 1 +[0] 1 {0} +[!0] 1 {1} +--END-- +HOA: v1 +States: 2 +Start: 0 +AP: 1 "a" +Acceptance: 2 Fin(0)&Inf(1) +--BODY-- +State: 0 +[0] 1 +State: 1 +[0] 1 {0} +[!0] 1 {0} +--END-- EOF cat >expected <out