Commit b4670f85 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

bdddict: add an unregister_all_typed_variables() method

* src/tgba/, src/tgba/bdddict.hh
(unregister_all_typed_variables): New method.
* src/tgbaalgos/ (degeneralize): Use it.
* NEWS: Mention it.
parent 0c7c9338
......@@ -42,6 +42,10 @@ New in spot 1.1a (not yet released):
- ltlcross has a new option --seed, that makes it possible to
change the seed used by the random graph generator.
- bdd_dict::unregister_all_typed_variables() is a new function,
making it easy to unregister all BDD variables of a given type
owned by some object.
* Bug fixes:
- genltl --gh-r generated the wrong formulas due to a typo.
......@@ -246,6 +246,7 @@ namespace spot
assert(unsigned(v) < bdd_map.size());
ref_set& s = bdd_map[v].refs;
// If the variable is not owned by me, ignore it.
ref_set::iterator si = s.find(me);
if (si == s.end())
......@@ -314,6 +315,17 @@ namespace spot
bdd_dict::unregister_all_typed_variables(var_type type, const void* me)
unsigned s = bdd_map.size();
for (unsigned i = 0; i < s; ++i)
if (bdd_map[i].type == type)
unregister_variable(i, me);
if (type == anon)
bdd_dict::is_registered_proposition(const ltl::formula* f, const void* by_me)
......@@ -203,6 +203,10 @@ namespace spot
/// Usually called in the destructor if \a me.
void unregister_all_my_variables(const void* me);
/// \brief Release all variables of a given type, used by an
/// object.
void unregister_all_typed_variables(var_type type, const void* me);
/// \brief Release a variable used by \a me.
void unregister_variable(int var, const void* me);
......@@ -243,10 +243,13 @@ namespace spot
bdd_dict* dict = a->get_dict();
// The result (degeneralized) automaton uses numbered state.
// The result (degeneralized) automaton uses numbered states.
sba_explicit_number* res = new sba_explicit_number(dict);
// We use the same BDD variables as the input, except for the
// acceptance.
dict->register_all_variables_of(a, res);
// FIXME: unregister acceptance conditions.
dict->unregister_all_typed_variables(bdd_dict::acc, res);
// Invent a new acceptance set for the degeneralized automaton.
int accvar =
Supports Markdown
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