diff --git a/NEWS b/NEWS index bd82deb0d..7ed8f04c5 100644 --- a/NEWS +++ b/NEWS @@ -248,6 +248,10 @@ New in spot 2.4.3.dev (not yet released) Fin-less & CNF version of the acceptance condition had several unit clauses. + - If the automaton passed to sbacc() was incomplete because of some + unreachable states, then it was possible that the output would + marked incomplete while it was in fact complete. + New in spot 2.4.3 (2017-12-19) Bugs fixed: diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index 2dd4d9916..a5fae38c4 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -168,6 +168,17 @@ namespace spot } } res->merge_edges(); + + // If the automaton was marked as not complete, and we have + // ignored some unreachable state, then it is possible that the + // result becomes complete. + if (res->prop_complete().is_false()) + for (unsigned i = 0; i < ns; ++i) + if (!si.reachable_state(i)) + { + res->prop_complete(trival::maybe()); + break; + } return res; } } diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test index 4223624a3..a3a96ba8f 100755 --- a/tests/core/sbacc.test +++ b/tests/core/sbacc.test @@ -262,3 +262,17 @@ EOF autfilt --sbacc alt.hoa > out.hoa diff out.hoa expect.hoa + +# Issue #312 +autfilt -S <