diff --git a/NEWS b/NEWS index 830294eba..4de8a86ae 100644 --- a/NEWS +++ b/NEWS @@ -33,7 +33,8 @@ New in spot 2.4.4.dev (net yet released) - ltl2tgba, autfilt, and dstar2tgba have some new '--cobuchi' option to force co-Büchi acceptance on the output. Beware: if the input language is not co-Büchi realizable the output automaton will - recognize a superset of the input. + recognize a superset of the input. Currently, the output is + always state-based. - genltl learned to generate six new families of formulas, taken from the SYNTCOMP competition on reactive synthesis, and from from @@ -97,7 +98,7 @@ New in spot 2.4.4.dev (net yet released) these four functions. The language of produced automata include the original language, but may be larger if the original automaton is not co-Büchi realizable. Based on Boker & Kupferman FOSSACS'11 - paper. + paper. Currently only supports state-based output. - spot::scc_info::states_on_acc_cycle_of() return all states visited by any accepting cycle of the specified SCC. It only diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc index 8c1405d97..d92f9f48e 100644 --- a/spot/twaalgos/cobuchi.cc +++ b/spot/twaalgos/cobuchi.cc @@ -31,6 +31,7 @@ #include #include #include +#include // For issue #317 #include #include @@ -274,6 +275,11 @@ namespace spot throw std::runtime_error("dnf_to_nca() only works with DNF acceptance " "condition"); + // FIXME: At the moment this algorithm does not support + // transition-based acceptance. See issue #317. Once that is + // fixed we may remove the next line. + ref = sbacc(std::const_pointer_cast(ref)); + auto streett_aut = spot::dnf_to_streett(ref, true); std::vector pairs; @@ -609,6 +615,11 @@ namespace spot throw std::runtime_error("nsa_to_dca() only works with Streett-like or " "Parity acceptance condition"); + // FIXME: At the moment this algorithm does not support + // transition-based acceptance. See issue #317. Once that is + // fixed we may remove the next line. + aut = sbacc(std::const_pointer_cast(aut)); + // Get states that must be visited infinitely often in NCA. vect_nca_info nca_info; nsa_to_nca(aut, named_states, &nca_info); @@ -635,6 +646,11 @@ namespace spot throw std::runtime_error("dnf_to_dca() only works with DNF (Rabin-like " "included) acceptance condition"); + // FIXME: At the moment this algorithm does not support + // transition-based acceptance. See issue #317. Once that is + // fixed we may remove the next line. + aut = sbacc(std::const_pointer_cast(aut)); + // Get states that must be visited infinitely often in NCA. vect_nca_info nca_info; dnf_to_nca(aut, false, &nca_info); diff --git a/tests/Makefile.am b/tests/Makefile.am index c9e9781d2..39b2e4a90 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -315,9 +315,6 @@ TESTS_twa = \ core/parity2.test \ core/ltlsynt.test -# Issue #317. -XFAIL_TESTS = core/dca2.test - ############################## PYTHON ############################## if USE_PYTHON