diff --git a/NEWS b/NEWS index 4ca413e07..12176da5e 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,10 @@ New in spot 2.10.2.dev (not yet released) - Nothing yet. + Bugs fixed: + + - On automata where the absence of color is not rejecting + (e.g. co-Büchi) and where the initial state was in a rejecting + SCC, sbacc() could output a superflous state. (Issue #492) New in spot 2.10.2 (2021-12-03) diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index c64ca321f..e79cba774 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -145,6 +145,8 @@ namespace spot // Use any edge going into the initial state to set the first // acceptance mark. init_acc = one_in[s] | common_out[s]; + else + init_acc = unsat_mark.second; old_st.push_back(new_state(s, init_acc)); } diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test index d694fa831..715001b7b 100755 --- a/tests/core/sbacc.test +++ b/tests/core/sbacc.test @@ -289,3 +289,37 @@ State: 0 [0] 0 {0} State: 1 [0] 1 [0] 0 --END-- EOF + +autfilt -S > out <exp <