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

bdd_dict: remove register_all_propositions_of

Browse source 
* spot/twa/bdddict.cc, spot/twa/bdddict.hh: Here.
* NEWS: Mention this removal.
This commit is contained in:
Alexandre Duret-Lutz 2017-11-05 09:43:01 +01:00
parent 0f26125f08
commit df73b84a47
3 changed files with 10 additions and 53 deletions
Download patch file Download diff file Expand all files Collapse all files

8
NEWS
View file

@ -173,14 +173,18 @@ New in spot 2.4.1.dev (not yet released)
- The spot::closure(), spot::sl2(), spot::is_stutter_invariant()
functions no longuer takes && arguments. The former two have
spot::closure_inplace() and spot::sl2_inplace() variant. These
function also do not take to list of atomic propositions as an
spot::closure_inplace() and spot::sl2_inplace() variants. These
functions also do not take a list of atomic propositions as an
argument anymore.
- The spot::bmrand() and spot::prand() functions have been removed.
They were not used at all in Spot, and it's not Spot's objective
to provide such random functions.
- The spot::bdd_dict::register_all_propositions_of() function has
been removed. It's a low-level function was not used anywhere in
Spot anymore, since it's better to use spot::twa::copy_ap_of().
Bugs fixed:
- Automata produced by "genaut --ks-nca=N" were incorrectly marked

18
spot/twa/bdddict.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012, 2013, 2014, 2015, 2016 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2009, 2012-2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
@ -197,20 +197,6 @@ namespace spot
}
void
bdd_dict::register_all_propositions_of(const void* from_other,
const void* for_me)
{
for (auto& i: bdd_map)
{
if (i.type != var_type::var)
continue;
ref_set& s = i.refs;
if (s.find(from_other) != s.end())
s.insert(for_me);
}
}
void
bdd_dict::unregister_variable(int v, const void* me)
{

37
spot/twa/bdddict.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2011-2017 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
@ -199,39 +199,6 @@ namespace spot
}
/// @}
/// \brief Register the same propositions as another object.
///
/// This tells this dictionary that the \a for_me object will be
/// using the same BDD variable used for atomic propositions by
/// the \a from_other object. This ensures that the variables
/// won't be freed when \a from_other is deleted if \a from_other
/// is still alive.
/// @{
void register_all_propositions_of(const void* from_other,
const void* for_me);
template <typename T>
void register_all_propositions_of(const void* from_other,
std::shared_ptr<T> for_me)
{
register_all_propositions_of(from_other, for_me.get());
}
template <typename T>
void register_all_propositions_of(std::shared_ptr<T> from_other,
const void* for_me)
{
register_all_propositions_of(from_other.get(), for_me);
}
template <typename T, typename U>
void register_all_propositions_of(std::shared_ptr<T> from_other,
std::shared_ptr<U> for_me)
{
register_all_propositions_of(from_other.get(), for_me.get());
}
/// @}
/// \brief Release all variables used by an object.
///
/// Usually called in the destructor if \a me.