diff --git a/NEWS b/NEWS index 827a300df..dfbb36451 100644 --- a/NEWS +++ b/NEWS @@ -72,6 +72,14 @@ New in spot 2.3.2.dev (not yet released) synonym for spot::twa::prop_universal() to help backward compatibility. + Deprecation notice: + + - spot::dtwa_complement() used to work only on deterministic + automatons. Due to the recent implementation of spot::dualize(), + that does the same job but on any type of automaton, + spot::dtwa_complement() is now kept as a proxy of spot::dualize() + in order to help backward compatibility, but is now deprecated. + New in spot 2.3.2 (2017-03-15) Tools: diff --git a/bench/stutter/stutter_invariance_randomgraph.cc b/bench/stutter/stutter_invariance_randomgraph.cc index e0a55e8ad..be2a7ff64 100644 --- a/bench/stutter/stutter_invariance_randomgraph.cc +++ b/bench/stutter/stutter_invariance_randomgraph.cc @@ -19,7 +19,7 @@ #include #include -#include +#include #include #include #include @@ -81,7 +81,7 @@ main(int argc, char** argv) true); } while (a->is_empty()); - auto na = spot::remove_fin(spot::dtwa_complement(a)); + auto na = spot::remove_fin(spot::dualize(a)); std::cout << d << ',' << props_n << ',' << seed; stats.print(a); diff --git a/bin/autfilt.cc b/bin/autfilt.cc index be2ef6537..ce24b1c4f 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -60,7 +60,7 @@ #include #include #include -#include +#include #include #include #include @@ -601,7 +601,7 @@ parse_opt(int key, char* arg, struct argp_state*) error(2, 0, "only one --equivalent-to option can be given"); opt->equivalent_pos = read_automaton(arg, opt->dict); opt->equivalent_neg = - spot::dtwa_complement(ensure_deterministic(opt->equivalent_pos, true)); + spot::dualize(ensure_deterministic(opt->equivalent_pos, true)); break; case OPT_GENERALIZED_RABIN: if (arg) @@ -675,7 +675,7 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_INCLUDED_IN: { auto aut = ensure_deterministic(read_automaton(arg, opt->dict), true); - aut = spot::dtwa_complement(aut); + aut = spot::dualize(aut); if (!opt->included_in) opt->included_in = aut; else @@ -1159,7 +1159,7 @@ namespace matched &= !aut->intersects(opt->included_in); if (opt->equivalent_pos) matched &= !aut->intersects(opt->equivalent_neg) - && (!dtwa_complement(ensure_deterministic(aut, true))-> + && (!dualize(ensure_deterministic(aut, true))-> intersects(opt->equivalent_pos)); if (matched && !opt->acc_words.empty()) @@ -1247,7 +1247,7 @@ namespace } if (opt_complement) - aut = spot::dtwa_complement(ensure_deterministic(aut)); + aut = spot::dualize(ensure_deterministic(aut)); aut = post.run(aut, nullptr); diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index 5cbed97a1..d8408b533 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -54,7 +54,7 @@ #include #include #include -#include +#include #include #include #include @@ -1169,7 +1169,7 @@ namespace unsigned i) { if (!no_complement && x[i] && is_deterministic(x[i])) - comp[i] = dtwa_complement(x[i]); + comp[i] = dualize(x[i]); }; for (unsigned i = 0; i < m; ++i) @@ -1199,7 +1199,7 @@ namespace p.set_type(spot::postprocessor::Generic); p.set_pref(spot::postprocessor::Deterministic); p.set_level(spot::postprocessor::Low); - to[i] = dtwa_complement(p.run(from[i])); + to[i] = dualize(p.run(from[i])); if (verbose) { std::cerr << "info: " << prefix << i << "\t("; diff --git a/doc/org/upgrade2.org b/doc/org/upgrade2.org index 942b05eaf..f9b461084 100644 --- a/doc/org/upgrade2.org +++ b/doc/org/upgrade2.org @@ -324,7 +324,7 @@ that provide a function with a similar service. | ~tgba/tgbabddfactory.hh~ | | not supported anymore | | ~tgba/tgbaexplicit.hh~ | ~spot/twa/twagraph.hh~ | | | ~tgba/tgba.hh~ | ~spot/twa/twa.hh~ | | -| ~tgba/tgbakvcomplement.hh~ | | use ~tgba_determinize()~ and ~dtwa_complement()~ | +| ~tgba/tgbakvcomplement.hh~ | | use ~tgba_determinize()~ and ~dualize()~ | | ~tgba/tgbamask.hh~ | ~spot/twa/tgbamask.hh~ | | | ~tgba/tgbaproduct.hh~ | ~spot/twa/tgbaproduct.hh~ | | | ~tgba/tgbaproxy.hh~ | | not supported anymore | @@ -333,7 +333,7 @@ that provide a function with a similar service. | ~tgba/tgbasgba.hh~ | ~spot/twaalgos/sbacc.hh~ | | | ~tgba/tgbatba.hh~ | ~spot/twaalgos/degen.hh~ | | | ~tgba/tgbaunion.hh~ | | not yet reimplemented | -| ~tgba/wdbacomp.hh~ | ~spot/twaalgos/complement.hh~ | use ~dtwa_complement()~ instead | +| ~tgba/wdbacomp.hh~ | ~spot/twaalgos/dualize.hh~ | use ~dualize()~ instead | |------------------------------------+------------------------------------+--------------------------------------------------| | ~tgbaparse/public.hh~ | ~spot/parseaut/public.hh~ | single parser for all automata | diff --git a/python/spot/impl.i b/python/spot/impl.i index 4273e61db..be594f45f 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -532,7 +532,6 @@ def state_is_accepting(self, src) -> "bool": %include %include %include -%include %feature("flatnested") spot::twa_run::step; %include %template(list_step) std::list; @@ -570,6 +569,13 @@ def state_is_accepting(self, src) -> "bool": %include %template(list_bdd) std::list; +%pythonprepend spot::twa::dtwa_complement %{ + from warnings import warn + warn("use dualize() instead of dtwa_complement()", + DeprecationWarning) +%} + +%include %include diff --git a/spot/twaalgos/complement.hh b/spot/twaalgos/complement.hh index 94dbe6b47..0b64b43fa 100644 --- a/spot/twaalgos/complement.hh +++ b/spot/twaalgos/complement.hh @@ -36,6 +36,11 @@ namespace spot /// Functions like to_generalized_buchi() or remove_fin() are /// frequently called after dtwa_complement() to obtain an easier /// acceptance condition (maybe at the cost of losing determinism.) + /// + /// This function was deprecated in spot 2.4. Call the function + /// spot::dualize() instead, that is able to complement any input + /// automaton, not only deterministic ones. + SPOT_DEPRECATED("use spot::dualize() instead") SPOT_API twa_graph_ptr dtwa_complement(const const_twa_graph_ptr& aut); } diff --git a/spot/twaalgos/langmap.cc b/spot/twaalgos/langmap.cc index 0899547c2..a457846a6 100644 --- a/spot/twaalgos/langmap.cc +++ b/spot/twaalgos/langmap.cc @@ -19,8 +19,8 @@ #include #include -#include #include +#include #include #include #include @@ -49,7 +49,7 @@ namespace spot alt_init_st_auts[i] = c; twa_graph_ptr cc = - remove_fin(dtwa_complement(copy(c, twa::prop_set::all()))); + remove_fin(dualize(copy(c, twa::prop_set::all()))); compl_alt_init_st_auts[i] = cc; } diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index 33c0637d8..01e6ea2f0 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -44,7 +44,7 @@ #include #include #include -#include +#include #include namespace spot @@ -661,7 +661,7 @@ namespace spot { // If the automaton is deterministic, complementing is // easy. - aut_neg_f = remove_fin(dtwa_complement(aut_f)); + aut_neg_f = remove_fin(dualize(aut_f)); } else { @@ -681,7 +681,7 @@ namespace spot { // Complement the minimized WDBA. assert((bool)min_aut_f->prop_weak()); - auto neg_min_aut_f = remove_fin(dtwa_complement(min_aut_f)); + auto neg_min_aut_f = remove_fin(dualize(min_aut_f)); if (product(aut_f, neg_min_aut_f)->is_empty()) // Finally, we are now sure that it was safe // to minimize the automaton. diff --git a/spot/twaalgos/powerset.cc b/spot/twaalgos/powerset.cc index 6edfcc290..2bc397590 100644 --- a/spot/twaalgos/powerset.cc +++ b/spot/twaalgos/powerset.cc @@ -34,7 +34,7 @@ #include #include #include -#include +#include #include #include #include @@ -407,7 +407,7 @@ namespace spot if (product(det, neg_aut)->is_empty()) // Complement the DBA. - if (product(aut, remove_fin(dtwa_complement(det)))->is_empty()) + if (product(aut, remove_fin(dualize(det)))->is_empty()) // Finally, we are now sure that it was safe // to determinize the automaton. return det; diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index 6ecb1717a..474ba4d87 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -27,7 +27,7 @@ #include #include #include -#include +#include #include #include #include @@ -631,7 +631,7 @@ namespace spot p.set_level(spot::postprocessor::Low); tmp = p.run(aut); } - neg = dtwa_complement(tmp); + neg = dualize(tmp); } is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()), diff --git a/tests/core/ikwiad.cc b/tests/core/ikwiad.cc index 73a0e9ac8..3c81ac380 100644 --- a/tests/core/ikwiad.cc +++ b/tests/core/ikwiad.cc @@ -57,7 +57,7 @@ #include #include #include -#include +#include #include #include #include @@ -1146,7 +1146,7 @@ checked_main(int argc, char** argv) if (opt_dtwacomp) { tm.start("DTωA complement"); - a = remove_fin(dtwa_complement(ensure_digraph(a))); + a = remove_fin(dualize(ensure_digraph(a))); tm.stop("DTωA complement"); } diff --git a/tests/python/bugdet.py b/tests/python/bugdet.py index ea159ecc3..0d84d9d43 100644 --- a/tests/python/bugdet.py +++ b/tests/python/bugdet.py @@ -81,11 +81,11 @@ State: 7 {0} print("use_simulation=True") b1 = spot.tgba_determinize(b, False, True, True, True) assert b1.num_states() == 5 -b1 = spot.remove_fin(spot.dtwa_complement(b1)) +b1 = spot.remove_fin(spot.dualize(b1)) assert not a.intersects(b1); print("\nuse_simulation=False") b2 = spot.tgba_determinize(b, False, True, False, True) assert b2.num_states() == 5 -b2 = spot.remove_fin(spot.dtwa_complement(b2)) +b2 = spot.remove_fin(spot.dualize(b2)) assert not a.intersects(b1); diff --git a/tests/python/remfin.py b/tests/python/remfin.py index f09dcf947..02a55dda9 100644 --- a/tests/python/remfin.py +++ b/tests/python/remfin.py @@ -19,7 +19,7 @@ State: 2 --END-- """) aut.prop_inherently_weak(True) -aut = spot.dtwa_complement(aut) +aut = spot.dualize(aut) aut1 = spot.scc_filter_states(aut) assert(aut1.to_str('hoa') == """HOA: v1 States: 2 diff --git a/tests/python/sum.py b/tests/python/sum.py index 08f084125..43b96ae94 100644 --- a/tests/python/sum.py +++ b/tests/python/sum.py @@ -57,7 +57,7 @@ def produce_phi(rg, n): def equivalent(a, phi): negphi = spot.formula.Not(phi) - nega = spot.dtwa_complement(spot.tgba_determinize(a)) + nega = spot.dualize(spot.tgba_determinize(a)) a2 = spot.ltl_to_tgba_fm(phi, dict) nega2 = spot.ltl_to_tgba_fm(negphi, dict) return spot.product(a, nega2).is_empty()\