defrag_states: do not take the argument by rvalue ref
Reported by Michaël Cadilhac. * spot/graph/graph.hh, spot/twa/twagraph.hh: Take the renaming vector by reference, not rvalue reference. Document that twa_graph::defrag_states may modify the vector. Keep a deprecated version of the old prototype just in case. While there, also hide this method from Swig. * spot/twa/twagraph.cc: Simplify all calls to defrag_states(). * NEWS: Mention the change.
This commit is contained in:
parent
0b048e1c05
commit
7a56ae958e
5 changed files with 43 additions and 11 deletions
7
NEWS
7
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
|
- Some formulas using ->, <->, or xor were not properly detected as
|
||||||
purely universal or pure eventualities.
|
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)
|
New in spot 2.9.6 (2021-01-18)
|
||||||
|
|
||||||
Build:
|
Build:
|
||||||
|
|
|
||||||
|
|
@ -1302,7 +1302,9 @@ namespace spot
|
||||||
///
|
///
|
||||||
/// \param used_states the number of states used (after
|
/// \param used_states the number of states used (after
|
||||||
/// renumbering)
|
/// renumbering)
|
||||||
void defrag_states(std::vector<unsigned>&& newst, unsigned used_states)
|
///
|
||||||
|
///@{
|
||||||
|
void defrag_states(const std::vector<unsigned>& newst, unsigned used_states)
|
||||||
{
|
{
|
||||||
SPOT_ASSERT(newst.size() >= states_.size());
|
SPOT_ASSERT(newst.size() >= states_.size());
|
||||||
SPOT_ASSERT(used_states > 0);
|
SPOT_ASSERT(used_states > 0);
|
||||||
|
|
@ -1368,5 +1370,13 @@ namespace spot
|
||||||
//std::cerr << "\nafter defrag\n";
|
//std::cerr << "\nafter defrag\n";
|
||||||
//dump_storage(std::cerr);
|
//dump_storage(std::cerr);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// prototype was changed in Spot 2.10
|
||||||
|
SPOT_DEPRECATED("use reference version of this method")
|
||||||
|
void defrag_states(std::vector<unsigned>&& newst, unsigned used_states)
|
||||||
|
{
|
||||||
|
return defrag_states(newst, used_states);
|
||||||
|
}
|
||||||
|
///@}
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
/* -*- coding: utf-8 -*-
|
/* -*- 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).
|
** de l'Epita (LRDE).
|
||||||
**
|
**
|
||||||
** This file is part of Spot, a model checking library.
|
** 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);
|
assert(s == (unsigned) res.states);
|
||||||
for (auto& i: res.start)
|
for (auto& i: res.start)
|
||||||
i.second.front() = rename[i.second.front()];
|
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());
|
res.info_states.resize(res.h->aut->num_states());
|
||||||
for (auto& s: res.info_states)
|
for (auto& s: res.info_states)
|
||||||
|
|
|
||||||
|
|
@ -328,7 +328,7 @@ namespace spot
|
||||||
else
|
else
|
||||||
s = -1U;
|
s = -1U;
|
||||||
|
|
||||||
defrag_states(std::move(remap), st);
|
defrag_states(remap, st);
|
||||||
}
|
}
|
||||||
|
|
||||||
void twa_graph::purge_unreachable_states(shift_action* f, void* action_data)
|
void twa_graph::purge_unreachable_states(shift_action* f, void* action_data)
|
||||||
|
|
@ -383,7 +383,7 @@ namespace spot
|
||||||
if (f)
|
if (f)
|
||||||
(*f)(todo, action_data);
|
(*f)(todo, action_data);
|
||||||
|
|
||||||
defrag_states(std::move(todo), current);
|
defrag_states(todo, current);
|
||||||
}
|
}
|
||||||
|
|
||||||
void twa_graph::purge_dead_states()
|
void twa_graph::purge_dead_states()
|
||||||
|
|
@ -580,13 +580,13 @@ namespace spot
|
||||||
if (prop_complete().is_false())
|
if (prop_complete().is_false())
|
||||||
prop_complete(trival::maybe());
|
prop_complete(trival::maybe());
|
||||||
|
|
||||||
defrag_states(std::move(useful), current);
|
defrag_states(useful, current);
|
||||||
|
|
||||||
if (purge_unreachable_needed)
|
if (purge_unreachable_needed)
|
||||||
purge_unreachable_states();
|
purge_unreachable_states();
|
||||||
}
|
}
|
||||||
|
|
||||||
void twa_graph::defrag_states(std::vector<unsigned>&& newst,
|
void twa_graph::defrag_states(std::vector<unsigned>& newst,
|
||||||
unsigned used_states)
|
unsigned used_states)
|
||||||
{
|
{
|
||||||
if (!is_existential())
|
if (!is_existential())
|
||||||
|
|
@ -660,7 +660,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
else
|
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
|
// newst, and use the index in newst to relabel
|
||||||
// the state so that graph::degrag_states() will
|
// the state so that graph::degrag_states() will
|
||||||
// eventually update it to the correct value.
|
// eventually update it to the correct value.
|
||||||
|
|
@ -738,7 +738,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
init_number_ = newst[init_number_];
|
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()
|
void twa_graph::remove_unused_ap()
|
||||||
|
|
|
||||||
|
|
@ -689,6 +689,7 @@ namespace spot
|
||||||
dests2.begin());
|
dests2.begin());
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#ifndef SWIG
|
||||||
/// \brief Renumber all states, and drop some.
|
/// \brief Renumber all states, and drop some.
|
||||||
///
|
///
|
||||||
/// This semi-internal function is a wrapper around
|
/// This semi-internal function is a wrapper around
|
||||||
|
|
@ -705,11 +706,25 @@ namespace spot
|
||||||
/// \param newst A vector indicating how each state should be
|
/// \param newst A vector indicating how each state should be
|
||||||
/// renumbered. Use -1U to mark an unreachable state for removal.
|
/// renumbered. Use -1U to mark an unreachable state for removal.
|
||||||
/// Ignoring the occurrences of -1U, the renumbering is expected
|
/// 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
|
/// \param used_states the number of states used after
|
||||||
/// renumbering.
|
/// renumbering.
|
||||||
void defrag_states(std::vector<unsigned>&& newst, unsigned used_states);
|
///@{
|
||||||
|
void defrag_states(std::vector<unsigned>& newst,
|
||||||
|
unsigned used_states);
|
||||||
|
|
||||||
|
// prototype was changed in Spot 2.10
|
||||||
|
SPOT_DEPRECATED("use reference version of this method")
|
||||||
|
void defrag_states(std::vector<unsigned>&& newst,
|
||||||
|
unsigned used_states)
|
||||||
|
{
|
||||||
|
return defrag_states(newst, used_states);
|
||||||
|
}
|
||||||
|
///@}
|
||||||
|
#endif // SWIG
|
||||||
|
|
||||||
/// \brief Print the data structures used to represent the
|
/// \brief Print the data structures used to represent the
|
||||||
/// automaton in dot's format.
|
/// automaton in dot's format.
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue