diff --git a/NEWS b/NEWS index 266b973bd..b699c3acc 100644 --- a/NEWS +++ b/NEWS @@ -27,6 +27,11 @@ New in spot 2.5.2.dev (not yet released) simplified to {1} or {SERE} depending on whether SERE accepts the empty word or not. + 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) Bugs fixed: diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc index 634b3f6b2..40b0d86a7 100644 --- a/spot/twaalgos/cobuchi.cc +++ b/spot/twaalgos/cobuchi.cc @@ -338,6 +338,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; @@ -684,8 +687,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 <