diff --git a/NEWS b/NEWS index 185c33fa7..cbb7e6b95 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,9 @@ New in spot 2.5.2.dev (not yet released) - Nothing yet. + Bugs fixed: + + - "autfilt --cobuchi --small/--det" would turn a transition-based + co-Büchi automaton into a state-based co-Büchi. New in spot 2.5.2 (2018-03-25) diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc index 73d0f5661..a2a4a2a42 100644 --- a/spot/twaalgos/cobuchi.cc +++ b/spot/twaalgos/cobuchi.cc @@ -337,6 +337,9 @@ namespace spot twa_graph_ptr to_nca(const_twa_graph_ptr aut, bool named_states) { + if (aut->acc().is_co_buchi()) + return make_twa_graph(aut, twa::prop_set::all()); + if (auto weak = weak_to_cobuchi(aut)) return weak; @@ -683,8 +686,12 @@ namespace spot to_dca(const_twa_graph_ptr aut, bool named_states) { if (is_deterministic(aut)) - if (auto weak = weak_to_cobuchi(aut)) - return weak; + { + if (aut->acc().is_co_buchi()) + return make_twa_graph(aut, twa::prop_set::all()); + if (auto weak = weak_to_cobuchi(aut)) + return weak; + } const acc_cond::acc_code& code = aut->get_acceptance(); diff --git a/tests/core/dca.test b/tests/core/dca.test index a5ca7e9f1..8d9f3fcd6 100644 --- a/tests/core/dca.test +++ b/tests/core/dca.test @@ -369,3 +369,25 @@ State: 1 [!1] 1 {0 2} [!0&!1] 2 [1] 3 [!0&1] 4 State: 2 [!0&!1] 2 {0 3} [1] 7 {2} [!1] 8 {2} State: 9 [1] 3 {2} [!0] 4 [!1] 9 {2} State: 10 [1] 7 [!1] 10 {0 2} --END-- EOF + +cat >in.hoa <