tgba: add a release_named_properties() method
Fixes #67. * src/tgba/tgba.cc, src/tgba/tgba.hh: Here. * src/tgbaalgos/complete.cc, src/tgbaalgos/stripacc.cc: Use it.
This commit is contained in:
parent
d1efe9a75a
commit
c26457b02b
4 changed files with 21 additions and 6 deletions
|
|
@ -41,10 +41,7 @@ namespace spot
|
||||||
if (last_support_conditions_input_)
|
if (last_support_conditions_input_)
|
||||||
last_support_conditions_input_->destroy();
|
last_support_conditions_input_->destroy();
|
||||||
delete iter_cache_;
|
delete iter_cache_;
|
||||||
|
release_named_properties();
|
||||||
// Destroy all named properties.
|
|
||||||
for (auto& np: named_prop_)
|
|
||||||
np.second.second(np.second.first);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
bdd
|
bdd
|
||||||
|
|
|
||||||
|
|
@ -744,6 +744,14 @@ namespace spot
|
||||||
}
|
}
|
||||||
#endif
|
#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
|
bool has_state_based_acc() const
|
||||||
{
|
{
|
||||||
return is.state_based_acc;
|
return is.state_based_acc;
|
||||||
|
|
|
||||||
|
|
@ -61,6 +61,8 @@ namespace spot
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
unsigned t = aut->num_transitions();
|
||||||
|
|
||||||
// Now complete all states (including the sink).
|
// Now complete all states (including the sink).
|
||||||
for (unsigned i = 0; i < n; ++i)
|
for (unsigned i = 0; i < n; ++i)
|
||||||
{
|
{
|
||||||
|
|
@ -99,6 +101,13 @@ namespace spot
|
||||||
aut->new_transition(i, sink, missingcond, acc);
|
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;
|
return sink;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement
|
// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et
|
||||||
// de l'Epita (LRDE).
|
// Développement de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -29,5 +29,6 @@ namespace spot
|
||||||
for (auto& t: a->out(s))
|
for (auto& t: a->out(s))
|
||||||
t.acc = 0U;
|
t.acc = 0U;
|
||||||
a->set_generalized_buchi(0);
|
a->set_generalized_buchi(0);
|
||||||
|
a->release_named_properties();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue