From 8e685e00c926f220635a48c554b8df001b7bffe7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 25 Jul 2017 11:18:03 +0200 Subject: [PATCH] deprecate copy() in favor of make_twa_graph() Fixes #258. * spot/twaalgos/copy.cc: Delete, and move the code... * spot/twa/twagraph.cc: ... in some anonymous namespace here. * spot/twa/twagraph.hh: Adjust the make_twa_graph() overload. * spot/twaalgos/copy.hh, NEWS: Mark copy() as deprecated and redirect to make_twa_graph(). * doc/org/upgrade2.org, doc/org/tut51.org, python/spot/impl.i, spot/twaalgos/dot.cc, spot/twaalgos/langmap.cc, tests/core/ikwiad.cc: Adjust callers. * spot/twaalgos/Makefile.am: Remove copy.cc. --- NEWS | 3 + doc/org/tut51.org | 20 ++--- doc/org/upgrade2.org | 4 +- python/spot/impl.i | 2 - spot/twa/twagraph.cc | 133 ++++++++++++++++++++++++++++++++++ spot/twa/twagraph.hh | 31 +++++--- spot/twaalgos/Makefile.am | 1 - spot/twaalgos/copy.cc | 149 -------------------------------------- spot/twaalgos/copy.hh | 20 ++--- spot/twaalgos/dot.cc | 3 +- spot/twaalgos/langmap.cc | 34 ++++----- tests/core/ikwiad.cc | 3 +- 12 files changed, 197 insertions(+), 206 deletions(-) delete mode 100644 spot/twaalgos/copy.cc diff --git a/NEWS b/NEWS index cb643390b..2391f79ca 100644 --- a/NEWS +++ b/NEWS @@ -196,6 +196,9 @@ New in spot 2.3.5.dev (not yet released) spot::twa::prop_deterministic() as a deprecated synonym for spot::twa::prop_universal() to help backward compatibility. + - The spot::copy() function is deprecated. Use + spot::make_twa_graph() instead. + New in spot 2.3.5 (2017-06-22) Bugs fixed: diff --git a/doc/org/tut51.org b/doc/org/tut51.org index 2920fc363..650568610 100644 --- a/doc/org/tut51.org +++ b/doc/org/tut51.org @@ -471,7 +471,7 @@ With a small variant of the above code, we could also display the counterexample on the state space, but only because our state space is so small: displaying large state spaces is not sensible. Besides, highlighting a run only works on =twa_graph= automata, so we need to convert the -Kripke structure to a =twa_graph=: this can be done with =copy()=. But +Kripke structure to a =twa_graph=: this can be done with =make_twa_graph()=. But now =k= is no longer a Kripke structure (also not generated on-the-fly anymore), so the =print_dot()= function will display it as a classical automaton with conditions on edges rather than state: @@ -493,7 +493,6 @@ passing the option "~k~" to =print_dot()= will fix that. #include #include #include - #include <> int main() { @@ -509,8 +508,9 @@ passing the option "~k~" to =print_dot()= will fix that. spot::twa_graph_ptr af = spot::translator(d).run(f); // Convert demo_kripke into an explicit graph - spot::twa_graph_ptr k = spot::copy(std::make_shared(d), - spot::twa::prop_set::all(), true); + spot::twa_graph_ptr k = + spot::make_twa_graph(std::make_shared(d), + spot::twa::prop_set::all(), true); // Find a run of or demo_kripke that intersects af. if (auto run = k->intersecting_run(af)) { @@ -518,14 +518,14 @@ passing the option "~k~" to =print_dot()= will fix that. spot::print_dot(std::cout, k, ".k"); } } - #+END_SRC +#+END_SRC - #+BEGIN_SRC dot :file kripke-3.png :cmdline -Tpng :cmd circo :var txt=demo-3 :exportss results - $txt - #+END_SRC +#+BEGIN_SRC dot :file kripke-3.png :cmdline -Tpng :cmd circo :var txt=demo-3 :exportss results +$txt +#+END_SRC - #+RESULTS: - [[file:kripke-3.png]] +#+RESULTS: +[[file:kripke-3.png]] * Possible improvements diff --git a/doc/org/upgrade2.org b/doc/org/upgrade2.org index 2a5c7c5ef..c3631d064 100644 --- a/doc/org/upgrade2.org +++ b/doc/org/upgrade2.org @@ -263,7 +263,7 @@ that provide a function with a similar service. | ~tgbaalgos/dtbasat.hh~ | ~spot/twaalgos/dtbasat.hh~ | | | ~tgbaalgos/dtgbacomp.hh~ | ~spot/twaalgos/complement.hh~ | | | ~tgbaalgos/dtgbasat.hh~ | ~spot/twaalgos/dtwasat.hh~ | | -| ~tgbaalgos/dupexp.hh~ | ~spot/twaalgos/copy.hh~ | also a copy constructor of twa | +| ~tgbaalgos/dupexp.hh~ | ~spot/twaalgos/twagraph.hh~ | constructor of twa_graph | | ~tgbaalgos/eltl2tgba_lacim.hh~ | | not supported anymore | | ~tgbaalgos/emptiness.hh~ | ~spot/twaalgos/emptiness.hh~ | | | ~tgbaalgos/emptiness_stats.hh~ | ~spot/twaalgos/emptiness_stats.hh~ | | @@ -615,7 +615,7 @@ for (auto i: aut->succ(s)) | ~dstar_parse()~ | ~parse_aut()~ | single parser for all automata | | ~dtgba_complement()~ | ~dtwa_complement()~ | | | ~dupexp_bfs()~ | | deleted | -| ~dupexp_dfs()~ | ~copy()~ | | +| ~dupexp_dfs()~ | ~make_twa_graph()~ | | | ~format_parse_aut_errors()~ | ~parsed_aut::format_errors()~ | | | ~emptiness_check_instantiator::construct()~ | ~make_emptiness_check_instantiator()~ | | | ~emptiness_check_instantiator::max_acceptance_conditions()~ | ~emptiness_check_instantiator::max_sets()~ | | diff --git a/python/spot/impl.i b/python/spot/impl.i index eaa12edfb..d629c0cc5 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -121,7 +121,6 @@ #include #include #include -#include #include #include #include @@ -537,7 +536,6 @@ def state_is_accepting(self, src) -> "bool": %include %include %include -%include %include %feature("flatnested") spot::twa_run::step; %include diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index bc8fd342a..f99f13771 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -20,6 +20,7 @@ #include #include #include +#include namespace spot { @@ -715,4 +716,136 @@ namespace spot set_named_prop("state-names", names.release()); } + namespace + { + twa_graph_ptr + copy(const const_twa_ptr& aut, twa::prop_set p, + bool preserve_names, unsigned max_states) + { + twa_graph_ptr out = make_twa_graph(aut->get_dict()); + out->copy_acceptance_of(aut); + out->copy_ap_of(aut); + out->prop_copy(aut, p); + + std::vector* names = nullptr; + std::set* incomplete = nullptr; + + // Old highlighting maps + typedef std::map hmap; + hmap* ohstates = nullptr; + hmap* ohedges = nullptr; + const_twa_graph_ptr aut_g = nullptr; + // New highlighting maps + hmap* nhstates = nullptr; + hmap* nhedges = nullptr; + + if (preserve_names) + { + names = new std::vector; + out->set_named_prop("state-names", names); + + // If the input is a twa_graph and we were asked to preserve + // names, also preserve highlights. + aut_g = std::dynamic_pointer_cast(aut); + if (aut_g) + { + ohstates = aut->get_named_prop("highlight-states"); + if (ohstates) + nhstates = out->get_or_set_named_prop("highlight-states"); + ohedges = aut->get_named_prop("highlight-edges"); + if (ohedges) + nhedges = out->get_or_set_named_prop("highlight-edges"); + } + } + + // States already seen. + state_map seen; + // States to process + std::deque::const_iterator> todo; + + auto new_state = [&](const state* s) -> unsigned + { + auto p = seen.emplace(s, 0); + if (p.second) + { + p.first->second = out->new_state(); + todo.emplace_back(p.first); + if (names) + names->emplace_back(aut->format_state(s)); + if (ohstates) + { + auto q = ohstates->find(aut_g->state_number(s)); + if (q != ohstates->end()) + nhstates->emplace(p.first->second, q->second); + } + } + else + { + s->destroy(); + } + return p.first->second; + }; + + out->set_init_state(new_state(aut->get_init_state())); + while (!todo.empty()) + { + const state* src1; + unsigned src2; + std::tie(src1, src2) = *todo.front(); + todo.pop_front(); + for (auto* t: aut->succ(src1)) + { + unsigned edgenum = 0; + if (SPOT_UNLIKELY(max_states < out->num_states())) + { + // If we have reached the max number of state, never try + // to create a new one. + auto i = seen.find(t->dst()); + if (i == seen.end()) + { + if (!incomplete) + incomplete = new std::set; + incomplete->insert(src2); + continue; + } + edgenum = out->new_edge(src2, i->second, t->cond(), t->acc()); + } + else + { + edgenum = out->new_edge(src2, new_state(t->dst()), + t->cond(), t->acc()); + } + if (ohedges) + { + auto q = ohedges->find(aut_g->edge_number(t)); + if (q != ohedges->end()) + nhedges->emplace(edgenum, q->second); + } + } + } + + + auto s = seen.begin(); + while (s != seen.end()) + { + // Advance the iterator before deleting the "key" pointer. + const state* ptr = s->first; + ++s; + ptr->destroy(); + } + + if (incomplete) + out->set_named_prop("incomplete-states", incomplete); + return out; + } + } + + twa_graph_ptr make_twa_graph(const const_twa_ptr& aut, twa::prop_set p, + bool preserve_names, unsigned max_states) + { + if (max_states == -1U && !preserve_names) + if (auto a = std::dynamic_pointer_cast(aut)) + return std::make_shared(a, p); + return copy(aut, p, preserve_names, max_states); + } } diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index e71eb481c..fa738aefc 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -23,7 +23,6 @@ #include #include #include -#include #include #include @@ -612,30 +611,42 @@ namespace spot void defrag_states(std::vector&& newst, unsigned used_states); }; + /// \ingroup twa + /// \brief Build an explicit automaton from all states of \a aut, inline twa_graph_ptr make_twa_graph(const bdd_dict_ptr& dict) { return std::make_shared(dict); } + /// \ingroup twa + /// \brief Build an explicit automaton from all states of \a aut, inline twa_graph_ptr make_twa_graph(const twa_graph_ptr& aut, twa::prop_set p) { return std::make_shared(aut, p); } + /// \ingroup twa + /// \brief Build an explicit automaton from all states of \a aut, inline twa_graph_ptr make_twa_graph(const const_twa_graph_ptr& aut, twa::prop_set p) { return std::make_shared(aut, p); } - inline twa_graph_ptr make_twa_graph(const const_twa_ptr& aut, - twa::prop_set p) - { - auto a = std::dynamic_pointer_cast(aut); - if (a) - return std::make_shared(a, p); - else - return copy(aut, p); - } + /// \ingroup twa + /// \brief Build an explicit automaton from all states of \a aut, + /// + /// This overload works using the abstract interface for automata. + /// + /// Set \a preserve_names to preserve state names, and set \a max_states + /// to a maximum number of states to keep. States with successors that + /// have not been kept will be marked as incomplete; this is mostly useful + /// to display a subset of a large state space. + SPOT_API twa_graph_ptr + make_twa_graph(const const_twa_ptr& aut, twa::prop_set p, + bool preserve_names = false, + // parentheses for SWIG, see + // https://github.com/swig/swig/issues/993 + unsigned max_states = -(1U)); } diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index c78a82e00..ab43d0bab 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -98,7 +98,6 @@ libtwaalgos_la_SOURCES = \ complete.cc \ complement.cc \ compsusp.cc \ - copy.cc \ cycles.cc \ degen.cc \ determinize.cc \ diff --git a/spot/twaalgos/copy.cc b/spot/twaalgos/copy.cc deleted file mode 100644 index e2c18f9e0..000000000 --- a/spot/twaalgos/copy.cc +++ /dev/null @@ -1,149 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include -#include -#include - -namespace spot -{ - twa_graph_ptr - copy(const const_twa_ptr& aut, twa::prop_set p, - bool preserve_names, unsigned max_states) - { - twa_graph_ptr out = make_twa_graph(aut->get_dict()); - out->copy_acceptance_of(aut); - out->copy_ap_of(aut); - out->prop_copy(aut, p); - - std::vector* names = nullptr; - std::set* incomplete = nullptr; - - // Old highlighting maps - typedef std::map hmap; - hmap* ohstates = nullptr; - hmap* ohedges = nullptr; - const_twa_graph_ptr aut_g = nullptr; - // New highlighting maps - hmap* nhstates = nullptr; - hmap* nhedges = nullptr; - - if (preserve_names) - { - names = new std::vector; - out->set_named_prop("state-names", names); - - // If the input is a twa_graph and we were asked to preserve - // names, also preserve highlights. - aut_g = std::dynamic_pointer_cast(aut); - if (aut_g) - { - ohstates = aut->get_named_prop("highlight-states"); - if (ohstates) - nhstates = out->get_or_set_named_prop("highlight-states"); - ohedges = aut->get_named_prop("highlight-edges"); - if (ohedges) - nhedges = out->get_or_set_named_prop("highlight-edges"); - } - } - - // States already seen. - state_map seen; - // States to process - std::deque::const_iterator> todo; - - auto new_state = [&](const state* s) -> unsigned - { - auto p = seen.emplace(s, 0); - if (p.second) - { - p.first->second = out->new_state(); - todo.emplace_back(p.first); - if (names) - names->emplace_back(aut->format_state(s)); - if (ohstates) - { - auto q = ohstates->find(aut_g->state_number(s)); - if (q != ohstates->end()) - nhstates->emplace(p.first->second, q->second); - } - } - else - { - s->destroy(); - } - return p.first->second; - }; - - out->set_init_state(new_state(aut->get_init_state())); - while (!todo.empty()) - { - const state* src1; - unsigned src2; - std::tie(src1, src2) = *todo.front(); - todo.pop_front(); - for (auto* t: aut->succ(src1)) - { - unsigned edgenum = 0; - if (SPOT_UNLIKELY(max_states < out->num_states())) - { - // If we have reached the max number of state, never try - // to create a new one. - auto i = seen.find(t->dst()); - if (i == seen.end()) - { - if (!incomplete) - incomplete = new std::set; - incomplete->insert(src2); - continue; - } - edgenum = out->new_edge(src2, i->second, t->cond(), t->acc()); - } - else - { - edgenum = - out->new_edge(src2, new_state(t->dst()), t->cond(), t->acc()); - } - if (ohedges) - { - auto q = ohedges->find(aut_g->edge_number(t)); - if (q != ohedges->end()) - nhedges->emplace(edgenum, q->second); - } - } - } - - - auto s = seen.begin(); - while (s != seen.end()) - { - // Advance the iterator before deleting the "key" pointer. - const state* ptr = s->first; - ++s; - ptr->destroy(); - } - - if (incomplete) - out->set_named_prop("incomplete-states", incomplete); - return out; - } -} diff --git a/spot/twaalgos/copy.hh b/spot/twaalgos/copy.hh index 2ae4f90ad..47c762d5a 100644 --- a/spot/twaalgos/copy.hh +++ b/spot/twaalgos/copy.hh @@ -1,7 +1,7 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2012-2017 Laboratoire de Recherche et // Développement de l'Epita (LRDE). -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris +// Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. // @@ -23,18 +23,20 @@ #pragma once #include -#include -#include +#include namespace spot { /// \ingroup twa_misc /// \brief Build an explicit automaton from all states of \a aut, /// - /// This works using the abstract interface for automata. If you - /// have a twa_graph that you want to copy, it is more efficient - /// to call make_twa_graph() instead. + /// This function was deprecated in Spot 2.4. Use the + /// function make_twa_graph() instead. + SPOT_DEPRECATED("use make_twa_graph() instead") SPOT_API twa_graph_ptr - copy(const const_twa_ptr& aut, twa::prop_set p, - bool preserve_names = false, unsigned max_states = -1U); + inline copy(const const_twa_ptr& aut, twa::prop_set p, + bool preserve_names = false, unsigned max_states = -1U) + { + return make_twa_graph(aut, p, preserve_names, max_states); + } } diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index 20a3a8b40..2678df55a 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -30,7 +30,6 @@ #include #include #include -#include #include #include #include @@ -833,7 +832,7 @@ namespace spot d.parse_opts("k"); auto aut = std::dynamic_pointer_cast(g); if (!aut || (d.max_states_given() && aut->num_states() >= d.max_states())) - aut = copy(g, twa::prop_set::all(), true, d.max_states() - 1); + aut = make_twa_graph(g, twa::prop_set::all(), true, d.max_states() - 1); d.print(aut); return os; } diff --git a/spot/twaalgos/langmap.cc b/spot/twaalgos/langmap.cc index a457846a6..0c6e74272 100644 --- a/spot/twaalgos/langmap.cc +++ b/spot/twaalgos/langmap.cc @@ -19,7 +19,6 @@ #include #include -#include #include #include #include @@ -43,29 +42,26 @@ namespace spot // Prepare all automatons needed. for (unsigned i = 0; i < n_states; ++i) - { - twa_graph_ptr c = copy(aut, twa::prop_set::all()); - c->set_init_state(i); - alt_init_st_auts[i] = c; - - twa_graph_ptr cc = - remove_fin(dualize(copy(c, twa::prop_set::all()))); - compl_alt_init_st_auts[i] = cc; - } + { + twa_graph_ptr c = make_twa_graph(aut, twa::prop_set::all()); + c->set_init_state(i); + alt_init_st_auts[i] = c; + compl_alt_init_st_auts[i] = remove_fin(dualize(c)); + } for (unsigned i = 1; i < n_states; ++i) for (unsigned j = 0; j < i; ++j) - { - if (res[j] != j) - continue; - - if (!alt_init_st_auts[i]->intersects(compl_alt_init_st_auts[j]) - && (!compl_alt_init_st_auts[i]->intersects(alt_init_st_auts[j]))) { - res[i] = res[j]; - break; + if (res[j] != j) + continue; + + if (!alt_init_st_auts[i]->intersects(compl_alt_init_st_auts[j]) + && (!compl_alt_init_st_auts[i]->intersects(alt_init_st_auts[j]))) + { + res[i] = res[j]; + break; + } } - } return res; } diff --git a/tests/core/ikwiad.cc b/tests/core/ikwiad.cc index 535f6e499..ada62e4de 100644 --- a/tests/core/ikwiad.cc +++ b/tests/core/ikwiad.cc @@ -39,7 +39,6 @@ #include #include #include -#include #include #include #include @@ -1185,7 +1184,7 @@ checked_main(int argc, char** argv) } if (dupexp) - a = copy(a, spot::twa::prop_set::all()); + a = make_twa_graph(a, spot::twa::prop_set::all()); //TA, STA, GTA, SGTA and TGTA if (ta_opt || tgta_opt)