Skip to content

GitLab

Commit 6db37f8e authored by Thomas Medioni's avatar Thomas Medioni
Browse files

dtwa_complement: deprecated, use dualize() instead. 

* NEWS: Mention of the deprecation.
* 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().
* spot/twaalgos/complement.hh: Adds deprecation notice.
parent 19df9117
Hide whitespace changes
Inline Side-by-side
NEWS
View file @ 6db37f8e
......@@ -60,6 +60,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:
......
bin/autfilt.cc
View file @ 6db37f8e
......@@ -60,7 +60,7 @@
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/dtwasat.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/strength.hh>
#include <spot/twaalgos/hoa.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");
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);
......
bin/ltlcross.cc
View file @ 6db37f8e
......@@ -54,7 +54,7 @@
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/isweakscc.hh>
#include <spot/twaalgos/word.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/alternation.hh>
#include <spot/misc/formater.hh>
......@@ -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(";
......
spot/twaalgos/complement.hh
View file @ 6db37f8e
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement
// Copyright (C) 2013-2016, 2017 Laboratoire de Recherche et Développement
Please register or sign in to reply
// de l'Epita.
//
// This file is part of Spot, a model checking library.
......@@ -23,19 +23,9 @@
namespace spot
{
/// \brief Complement a deterministic TωA
///
/// The automaton \a aut should be deterministic. It will be
/// completed if it isn't already. In these conditions,
/// complementing the automaton can be done by just complementing
/// the acceptance condition.
///
/// In particular, this implies that an input that use
/// generalized Büchi will be output as generalized co-Büchi.
///
/// 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 loosing determinism.)
SPOT_API twa_graph_ptr
dtwa_complement(const const_twa_graph_ptr& aut);
// Call the function spot::dualize() instead, that is able to complement any
// input automaton, not only deterministic ones.
Please register or sign in to reply
SPOT_DEPRECATED("use spot::dualize() instead")
SPOT_API
twa_graph_ptr dtwa_complement(const const_twa_graph_ptr& aut);
}
spot/twaalgos/langmap.cc
View file @ 6db37f8e
......@@ -19,8 +19,8 @@
#include <numeric>
#include <spot/twa/twa.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/copy.hh>
#include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/langmap.hh>
#include <spot/twaalgos/remfin.hh>
......@@ -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;
}
......
spot/twaalgos/minimize.cc
View file @ 6db37f8e
......@@ -44,7 +44,7 @@
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/bfssteps.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/remfin.hh>
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.
......
spot/twaalgos/powerset.cc
View file @ 6db37f8e
......@@ -34,7 +34,7 @@
#include <spot/twaalgos/gtec/gtec.hh>
#include <spot/twaalgos/sccfilter.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/remfin.hh>
#include <spot/misc/bitvect.hh>
#include <spot/misc/bddlt.hh>
......@@ -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;
......
spot/twaalgos/stutter.cc
View file @ 6db37f8e
......@@ -27,7 +27,7 @@
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/postproc.hh>
#include <spot/twa/twaproduct.hh>
......@@ -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()),
......
tests/core/ikwiad.cc
View file @ 6db37f8e
......@@ -57,7 +57,7 @@
#include <spot/twaalgos/simulation.hh>
#include <spot/twaalgos/compsusp.hh>
#include <spot/twaalgos/powerset.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/complete.hh>
#include <spot/twaalgos/dtbasat.hh>
......@@ -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");
}
......
tests/python/bugdet.py
View file @ 6db37f8e
......@@ -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);
tests/python/remfin.py
View file @ 6db37f8e
......@@ -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
......
tests/python/sum.py
View file @ 6db37f8e
......@@ -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()\
......
  • Alexandre Duret-Lutz @adl ·
    Owner

    dtwa_complement is also mentioned twice on doc/org/upgrade2.org.

  • Alexandre Duret-Lutz @adl ·
    Owner

    And you can deprecate the Python bindings for dtwa_complement using the same thing I did in f6e6099d. (The %pythonprepend stuff needs to occur before the relevant *.h file is %included.)

    To see the deprecation warnings in action, you have to use python3 -Wall or even python3 -Werror, but currently we cannot activate this in the test suite due to other issues.

Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment