diff --git a/NEWS b/NEWS index 03dd5bd3a..c55eb1513 100644 --- a/NEWS +++ b/NEWS @@ -189,6 +189,13 @@ New in spot 2.9.6.dev (not yet released) - Some formulas using ->, <->, or xor were not properly detected as purely universal or pure eventualities. + Deprecation notices: + + - twa_graph::defrag_states() and digraph::defrag_states() now take + the renaming vector by reference instead of rvalue reference. The + old prototype is still supported but will emit a deprecation + warning. + New in spot 2.9.6 (2021-01-18) Build: diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index 507bc849e..efb83abf0 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -1302,7 +1302,9 @@ namespace spot /// /// \param used_states the number of states used (after /// renumbering) - void defrag_states(std::vector&& newst, unsigned used_states) + /// + ///@{ + void defrag_states(const std::vector& newst, unsigned used_states) { SPOT_ASSERT(newst.size() >= states_.size()); SPOT_ASSERT(used_states > 0); @@ -1368,5 +1370,13 @@ namespace spot //std::cerr << "\nafter defrag\n"; //dump_storage(std::cerr); } + + // prototype was changed in Spot 2.10 + SPOT_DEPRECATED("use reference version of this method") + void defrag_states(std::vector&& newst, unsigned used_states) + { + return defrag_states(newst, used_states); + } + ///@} }; } diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 12a7a0e5a..f42f92876 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -1,5 +1,5 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2014-2020 Laboratoire de Recherche et Développement +** Copyright (C) 2014-2021 Laboratoire de Recherche et Développement ** de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. @@ -2077,7 +2077,7 @@ lbtt: lbtt-header lbtt-body ENDAUT assert(s == (unsigned) res.states); for (auto& i: res.start) i.second.front() = rename[i.second.front()]; - res.h->aut->get_graph().defrag_states(std::move(rename), s); + res.h->aut->get_graph().defrag_states(rename, s); } res.info_states.resize(res.h->aut->num_states()); for (auto& s: res.info_states) diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 68cbd289d..c19585b69 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -328,7 +328,7 @@ namespace spot else s = -1U; - defrag_states(std::move(remap), st); + defrag_states(remap, st); } void twa_graph::purge_unreachable_states(shift_action* f, void* action_data) @@ -383,7 +383,7 @@ namespace spot if (f) (*f)(todo, action_data); - defrag_states(std::move(todo), current); + defrag_states(todo, current); } void twa_graph::purge_dead_states() @@ -580,13 +580,13 @@ namespace spot if (prop_complete().is_false()) prop_complete(trival::maybe()); - defrag_states(std::move(useful), current); + defrag_states(useful, current); if (purge_unreachable_needed) purge_unreachable_states(); } - void twa_graph::defrag_states(std::vector&& newst, + void twa_graph::defrag_states(std::vector& newst, unsigned used_states) { if (!is_existential()) @@ -660,7 +660,7 @@ namespace spot } else { - // register this new destination group, add et two + // register this new destination group, add it to // newst, and use the index in newst to relabel // the state so that graph::degrag_states() will // eventually update it to the correct value. @@ -738,7 +738,7 @@ namespace spot } } init_number_ = newst[init_number_]; - g_.defrag_states(std::move(newst), used_states); + g_.defrag_states(newst, used_states); } void twa_graph::remove_unused_ap() diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index b8e248916..072a0d04c 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -689,6 +689,7 @@ namespace spot dests2.begin()); } +#ifndef SWIG /// \brief Renumber all states, and drop some. /// /// This semi-internal function is a wrapper around @@ -705,11 +706,25 @@ namespace spot /// \param newst A vector indicating how each state should be /// renumbered. Use -1U to mark an unreachable state for removal. /// Ignoring the occurrences of -1U, the renumbering is expected - /// to satisfy newst[i] ≤ i for all i. + /// to satisfy newst[i] ≤ i for all i. If the automaton contains + /// universal branching, this vector is likely to be modified by + /// this function, so do not reuse it afterwards. /// /// \param used_states the number of states used after /// renumbering. - void defrag_states(std::vector&& newst, unsigned used_states); + ///@{ + void defrag_states(std::vector& newst, + unsigned used_states); + + // prototype was changed in Spot 2.10 + SPOT_DEPRECATED("use reference version of this method") + void defrag_states(std::vector&& newst, + unsigned used_states) + { + return defrag_states(newst, used_states); + } + ///@} +#endif // SWIG /// \brief Print the data structures used to represent the /// automaton in dot's format.