alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

dtwa_complement: deprecated, use dualize() instead.

Browse source 
* NEWS: Mention of the deprecation
* bench/stutter/stutter_invariance_randomgraph.cc,
  bin/autfilt.cc, bin/ltlcross.cc, spot/twaalgos/langmap.cc,
  spot/twaalgos/minimize.cc, spot/twaalgos/powerset.cc,
  spot/twaalgos/stutter.cc, tests/core/ikwiad.cc,
  tests/python/bugdet.py, tests/python/remfin.py,
  tests/python/sum.py: Refactor calls to dtwa_complement() with calls
  to dualize().
* doc/org/upgrade2.org: Change mention of dtwa_complement with dualize.
* spot/twaalgos/complement.hh: Add deprecation notice.
* python/spot/impl.i: Add deprecation notice for the python bindings.
This commit is contained in:
Thomas Medioni 2017-03-31 11:54:34 +02:00
parent 073a6e8198
commit 152b5d0d30
15 changed files with 47 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

8
NEWS
View file

@ -72,6 +72,14 @@ New in spot 2.3.2.dev (not yet released)
synonym for spot::twa::prop_universal() to help backward synonym for spot::twa::prop_universal() to help backward
compatibility. 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) New in spot 2.3.2 (2017-03-15)
Tools: Tools:

4
bench/stutter/stutter_invariance_randomgraph.cc
View file

@ -19,7 +19,7 @@
#include <spot/misc/timer.hh> #include <spot/misc/timer.hh>
#include <spot/tl/apcollect.hh> #include <spot/tl/apcollect.hh>
#include <spot/twaalgos/complement.hh> #include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/remfin.hh> #include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/randomgraph.hh> #include <spot/twaalgos/randomgraph.hh>
#include <spot/twaalgos/dot.hh> #include <spot/twaalgos/dot.hh>
@ -81,7 +81,7 @@ main(int argc, char** argv)
true); true);
} }
while (a->is_empty()); 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; std::cout << d << ',' << props_n << ',' << seed;
stats.print(a); stats.print(a);

10
bin/autfilt.cc
View file

@ -60,7 +60,7 @@
#include <spot/twaalgos/remfin.hh> #include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/cleanacc.hh> #include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/dtwasat.hh> #include <spot/twaalgos/dtwasat.hh>
#include <spot/twaalgos/complement.hh> #include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/strength.hh> #include <spot/twaalgos/strength.hh>
#include <spot/twaalgos/hoa.hh> #include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/sccinfo.hh> #include <spot/twaalgos/sccinfo.hh>
@ -601,7 +601,7 @@ parse_opt(int key, char* arg, struct argp_state*)
error(2, 0, "only one --equivalent-to option can be given"); error(2, 0, "only one --equivalent-to option can be given");
opt->equivalent_pos = read_automaton(arg, opt->dict); opt->equivalent_pos = read_automaton(arg, opt->dict);
opt->equivalent_neg = opt->equivalent_neg =
spot::dtwa_complement(ensure_deterministic(opt->equivalent_pos, true)); spot::dualize(ensure_deterministic(opt->equivalent_pos, true));
break; break;
case OPT_GENERALIZED_RABIN: case OPT_GENERALIZED_RABIN:
if (arg) if (arg)
@ -675,7 +675,7 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_INCLUDED_IN: case OPT_INCLUDED_IN:
{ {
auto aut = ensure_deterministic(read_automaton(arg, opt->dict), true); auto aut = ensure_deterministic(read_automaton(arg, opt->dict), true);
aut = spot::dtwa_complement(aut); aut = spot::dualize(aut);
if (!opt->included_in) if (!opt->included_in)
opt->included_in = aut; opt->included_in = aut;
else else
@ -1159,7 +1159,7 @@ namespace
matched &= !aut->intersects(opt->included_in); matched &= !aut->intersects(opt->included_in);
if (opt->equivalent_pos) if (opt->equivalent_pos)
matched &= !aut->intersects(opt->equivalent_neg) matched &= !aut->intersects(opt->equivalent_neg)
&& (!dtwa_complement(ensure_deterministic(aut, true))-> && (!dualize(ensure_deterministic(aut, true))->
intersects(opt->equivalent_pos)); intersects(opt->equivalent_pos));
if (matched && !opt->acc_words.empty()) if (matched && !opt->acc_words.empty())
@ -1247,7 +1247,7 @@ namespace
} }
if (opt_complement) if (opt_complement)
aut = spot::dtwa_complement(ensure_deterministic(aut)); aut = spot::dualize(ensure_deterministic(aut));
aut = post.run(aut, nullptr); aut = post.run(aut, nullptr);

6
bin/ltlcross.cc
View file

@ -54,7 +54,7 @@
#include <spot/twaalgos/sccinfo.hh> #include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/isweakscc.hh> #include <spot/twaalgos/isweakscc.hh>
#include <spot/twaalgos/word.hh> #include <spot/twaalgos/word.hh>
#include <spot/twaalgos/complement.hh> #include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/cleanacc.hh> #include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/alternation.hh> #include <spot/twaalgos/alternation.hh>
#include <spot/misc/formater.hh> #include <spot/misc/formater.hh>
@ -1169,7 +1169,7 @@ namespace
unsigned i) unsigned i)
{ {
if (!no_complement && x[i] && is_deterministic(x[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) for (unsigned i = 0; i < m; ++i)
@ -1199,7 +1199,7 @@ namespace
p.set_type(spot::postprocessor::Generic); p.set_type(spot::postprocessor::Generic);
p.set_pref(spot::postprocessor::Deterministic); p.set_pref(spot::postprocessor::Deterministic);
p.set_level(spot::postprocessor::Low); p.set_level(spot::postprocessor::Low);
to[i] = dtwa_complement(p.run(from[i])); to[i] = dualize(p.run(from[i]));
if (verbose) if (verbose)
{ {
std::cerr << "info: " << prefix << i << "\t("; std::cerr << "info: " << prefix << i << "\t(";

4
doc/org/upgrade2.org
View file

@ -324,7 +324,7 @@ that provide a function with a similar service.
| ~tgba/tgbabddfactory.hh~ | | not supported anymore | | ~tgba/tgbabddfactory.hh~ | | not supported anymore |
| ~tgba/tgbaexplicit.hh~ | ~spot/twa/twagraph.hh~ | | | ~tgba/tgbaexplicit.hh~ | ~spot/twa/twagraph.hh~ | |
| ~tgba/tgba.hh~ | ~spot/twa/twa.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/tgbamask.hh~ | ~spot/twa/tgbamask.hh~ | |
| ~tgba/tgbaproduct.hh~ | ~spot/twa/tgbaproduct.hh~ | | | ~tgba/tgbaproduct.hh~ | ~spot/twa/tgbaproduct.hh~ | |
| ~tgba/tgbaproxy.hh~ | | not supported anymore | | ~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/tgbasgba.hh~ | ~spot/twaalgos/sbacc.hh~ | |
| ~tgba/tgbatba.hh~ | ~spot/twaalgos/degen.hh~ | | | ~tgba/tgbatba.hh~ | ~spot/twaalgos/degen.hh~ | |
| ~tgba/tgbaunion.hh~ | | not yet reimplemented | | ~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 | | ~tgbaparse/public.hh~ | ~spot/parseaut/public.hh~ | single parser for all automata |

8
python/spot/impl.i
View file

@ -532,7 +532,6 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/twaalgos/dot.hh> %include <spot/twaalgos/dot.hh>
%include <spot/twaalgos/copy.hh> %include <spot/twaalgos/copy.hh>
%include <spot/twaalgos/complete.hh> %include <spot/twaalgos/complete.hh>
%include <spot/twaalgos/complement.hh>
%feature("flatnested") spot::twa_run::step; %feature("flatnested") spot::twa_run::step;
%include <spot/twaalgos/emptiness.hh> %include <spot/twaalgos/emptiness.hh>
%template(list_step) std::list<spot::twa_run::step>; %template(list_step) std::list<spot::twa_run::step>;
@ -570,6 +569,13 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/twaalgos/word.hh> %include <spot/twaalgos/word.hh>
%template(list_bdd) std::list<bdd>; %template(list_bdd) std::list<bdd>;
%pythonprepend spot::twa::dtwa_complement %{
from warnings import warn
warn("use dualize() instead of dtwa_complement()",
DeprecationWarning)
%}
%include <spot/twaalgos/complement.hh>
%include <spot/parseaut/public.hh> %include <spot/parseaut/public.hh>

5
spot/twaalgos/complement.hh
View file

@ -36,6 +36,11 @@ namespace spot
/// Functions like to_generalized_buchi() or remove_fin() are /// Functions like to_generalized_buchi() or remove_fin() are
/// frequently called after dtwa_complement() to obtain an easier /// frequently called after dtwa_complement() to obtain an easier
/// acceptance condition (maybe at the cost of losing determinism.) /// 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 SPOT_API twa_graph_ptr
dtwa_complement(const const_twa_graph_ptr& aut); dtwa_complement(const const_twa_graph_ptr& aut);
} }

4
spot/twaalgos/langmap.cc
View file

@ -19,8 +19,8 @@
#include <numeric> #include <numeric>
#include <spot/twa/twa.hh> #include <spot/twa/twa.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/copy.hh> #include <spot/twaalgos/copy.hh>
#include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/isdet.hh> #include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/langmap.hh> #include <spot/twaalgos/langmap.hh>
#include <spot/twaalgos/remfin.hh> #include <spot/twaalgos/remfin.hh>
@ -49,7 +49,7 @@ namespace spot
alt_init_st_auts[i] = c; alt_init_st_auts[i] = c;
twa_graph_ptr cc = 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; compl_alt_init_st_auts[i] = cc;
} }

6
spot/twaalgos/minimize.cc
View file

@ -44,7 +44,7 @@
#include <spot/twaalgos/ltl2tgba_fm.hh> #include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/bfssteps.hh> #include <spot/twaalgos/bfssteps.hh>
#include <spot/twaalgos/isdet.hh> #include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/complement.hh> #include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/remfin.hh> #include <spot/twaalgos/remfin.hh>
namespace spot namespace spot
@ -661,7 +661,7 @@ namespace spot
{ {
// If the automaton is deterministic, complementing is // If the automaton is deterministic, complementing is
// easy. // easy.
aut_neg_f = remove_fin(dtwa_complement(aut_f)); aut_neg_f = remove_fin(dualize(aut_f));
} }
else else
{ {
@ -681,7 +681,7 @@ namespace spot
{ {
// Complement the minimized WDBA. // Complement the minimized WDBA.
assert((bool)min_aut_f->prop_weak()); 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()) if (product(aut_f, neg_min_aut_f)->is_empty())
// Finally, we are now sure that it was safe // Finally, we are now sure that it was safe
// to minimize the automaton. // to minimize the automaton.

4
spot/twaalgos/powerset.cc
View file

@ -34,7 +34,7 @@
#include <spot/twaalgos/gtec/gtec.hh> #include <spot/twaalgos/gtec/gtec.hh>
#include <spot/twaalgos/sccfilter.hh> #include <spot/twaalgos/sccfilter.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh> #include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/complement.hh> #include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/remfin.hh> #include <spot/twaalgos/remfin.hh>
#include <spot/misc/bitvect.hh> #include <spot/misc/bitvect.hh>
#include <spot/misc/bddlt.hh> #include <spot/misc/bddlt.hh>
@ -407,7 +407,7 @@ namespace spot
if (product(det, neg_aut)->is_empty()) if (product(det, neg_aut)->is_empty())
// Complement the DBA. // 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 // Finally, we are now sure that it was safe
// to determinize the automaton. // to determinize the automaton.
return det; return det;

4
spot/twaalgos/stutter.cc
View file

@ -27,7 +27,7 @@
#include <spot/twaalgos/product.hh> #include <spot/twaalgos/product.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh> #include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/isdet.hh> #include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/complement.hh> #include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/remfin.hh> #include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/postproc.hh> #include <spot/twaalgos/postproc.hh>
#include <spot/twa/twaproduct.hh> #include <spot/twa/twaproduct.hh>
@ -631,7 +631,7 @@ namespace spot
p.set_level(spot::postprocessor::Low); p.set_level(spot::postprocessor::Low);
tmp = p.run(aut); tmp = p.run(aut);
} }
neg = dtwa_complement(tmp); neg = dualize(tmp);
} }
is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()), is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()),

4
tests/core/ikwiad.cc
View file

@ -57,7 +57,7 @@
#include <spot/twaalgos/simulation.hh> #include <spot/twaalgos/simulation.hh>
#include <spot/twaalgos/compsusp.hh> #include <spot/twaalgos/compsusp.hh>
#include <spot/twaalgos/powerset.hh> #include <spot/twaalgos/powerset.hh>
#include <spot/twaalgos/complement.hh> #include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/remfin.hh> #include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/complete.hh> #include <spot/twaalgos/complete.hh>
#include <spot/twaalgos/dtbasat.hh> #include <spot/twaalgos/dtbasat.hh>
@ -1146,7 +1146,7 @@ checked_main(int argc, char** argv)
if (opt_dtwacomp) if (opt_dtwacomp)
{ {
tm.start("DTωA complement"); 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"); tm.stop("DTωA complement");
} }

4
tests/python/bugdet.py
View file

@ -81,11 +81,11 @@ State: 7 {0}
print("use_simulation=True") print("use_simulation=True")
b1 = spot.tgba_determinize(b, False, True, True, True) b1 = spot.tgba_determinize(b, False, True, True, True)
assert b1.num_states() == 5 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); assert not a.intersects(b1);
print("\nuse_simulation=False") print("\nuse_simulation=False")
b2 = spot.tgba_determinize(b, False, True, False, True) b2 = spot.tgba_determinize(b, False, True, False, True)
assert b2.num_states() == 5 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); assert not a.intersects(b1);

2
tests/python/remfin.py
View file

@ -19,7 +19,7 @@ State: 2
--END-- --END--
""") """)
aut.prop_inherently_weak(True) aut.prop_inherently_weak(True)
aut = spot.dtwa_complement(aut) aut = spot.dualize(aut)
aut1 = spot.scc_filter_states(aut) aut1 = spot.scc_filter_states(aut)
assert(aut1.to_str('hoa') == """HOA: v1 assert(aut1.to_str('hoa') == """HOA: v1
States: 2 States: 2

2
tests/python/sum.py
View file

@ -57,7 +57,7 @@ def produce_phi(rg, n):
def equivalent(a, phi): def equivalent(a, phi):
negphi = spot.formula.Not(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) a2 = spot.ltl_to_tgba_fm(phi, dict)
nega2 = spot.ltl_to_tgba_fm(negphi, dict) nega2 = spot.ltl_to_tgba_fm(negphi, dict)
return spot.product(a, nega2).is_empty()\ return spot.product(a, nega2).is_empty()\