diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc index 91b286c4c..9089ee038 100644 --- a/src/tgba/tgba.cc +++ b/src/tgba/tgba.cc @@ -41,10 +41,7 @@ namespace spot if (last_support_conditions_input_) last_support_conditions_input_->destroy(); delete iter_cache_; - - // Destroy all named properties. - for (auto& np: named_prop_) - np.second.second(np.second.first); + release_named_properties(); } bdd diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index ae7359b99..14c616375 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -744,6 +744,14 @@ namespace spot } #endif + void release_named_properties() + { + // Destroy all named properties. + for (auto& np: named_prop_) + np.second.second(np.second.first); + named_prop_.clear(); + } + bool has_state_based_acc() const { return is.state_based_acc; diff --git a/src/tgbaalgos/complete.cc b/src/tgbaalgos/complete.cc index c5d56cfbe..ecd44dbb8 100644 --- a/src/tgbaalgos/complete.cc +++ b/src/tgbaalgos/complete.cc @@ -61,6 +61,8 @@ namespace spot } } + unsigned t = aut->num_transitions(); + // Now complete all states (including the sink). for (unsigned i = 0; i < n; ++i) { @@ -99,6 +101,13 @@ namespace spot aut->new_transition(i, sink, missingcond, acc); } } + + // Get rid of any named property if the automaton changed. + if (t < aut->num_transitions()) + aut->release_named_properties(); + else + assert(t == aut->num_transitions()); + return sink; } diff --git a/src/tgbaalgos/stripacc.cc b/src/tgbaalgos/stripacc.cc index 841e3d275..81a1c9a4b 100644 --- a/src/tgbaalgos/stripacc.cc +++ b/src/tgbaalgos/stripacc.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -29,5 +29,6 @@ namespace spot for (auto& t: a->out(s)) t.acc = 0U; a->set_generalized_buchi(0); + a->release_named_properties(); } }