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

Introduce a destroy() method on states, and use it instead of delete.

Browse source 
Right now, destroy() just executes "delete this".  But in a later
version, we will rewrite tgba_explicit so that it does not
allocate new states (and the destroy() method for explicit state
will do nothing).

* src/tgba/state.hh (state::destroy): New method, to replace
state::~state() in the future.
(shared_state_deleter): New function.
* src/evtgba/product.cc, src/evtgbaalgos/reachiter.cc,
src/evtgbaalgos/save.cc, src/evtgbaalgos/tgba2evtgba.cc,
src/tgba/tgba.cc, src/tgba/tgbaproduct.cc, src/tgba/tgbareduc.cc,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc,
src/tgba/tgbatba.cc, src/tgba/tgbaunion.cc, src/tgba/wdbacomp.cc,
src/tgbaalgos/cutscc.cc, src/tgbaalgos/emptiness.cc,
src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/explscc.cc,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/nsheap.cc,
src/tgbaalgos/gv04.cc, src/tgbaalgos/magic.cc,
src/tgbaalgos/minimize.cc, src/tgbaalgos/ndfs_result.hxx,
src/tgbaalgos/neverclaim.cc, src/tgbaalgos/powerset.hh,
src/tgbaalgos/reachiter.cc, src/tgbaalgos/reducerun.cc,
src/tgbaalgos/reductgba_sim.cc,
src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/replayrun.cc,
src/tgbaalgos/safety.cc, src/tgbaalgos/save.cc,
src/tgbaalgos/scc.cc, src/tgbaalgos/se05.cc,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Adjust to call
"s->destroy()" instead of "delete s".
* src/saba/sabacomplementtgba.cc, src/tgba/tgbakvcomplement.cc:
Pass shared_state_deleter to the shared_ptr constructor, so that
it calls destroy() instead of delete.
This commit is contained in:
Alexandre Duret-Lutz 2011-01-25 18:56:42 +01:00
parent 60930d7a12
commit 574a228583
39 changed files with 259 additions and 167 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/evtgba/product.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2008 Laboratoire de Recherche et Développement
// Copyright (C) 2008, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -43,7 +43,7 @@ namespace spot
~evtgba_product_state()
{
for (int j = 0; j < n_; ++j)
delete s_[j];
s_[j]->destroy();
delete[] s_;
}

6
src/evtgbaalgos/reachiter.cc
View file

@ -1,3 +1,5 @@
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -40,7 +42,7 @@ namespace spot
// Advance the iterator before deleting the "key" pointer.
const state* ptr = s->first;
++s;
delete ptr;
ptr->destroy();
}
}
@ -79,7 +81,7 @@ namespace spot
else
{
process_link(tn, s->second, si);
delete current;
current->destroy();
}
}
delete si;

6
src/evtgbaalgos/save.cc
View file

@ -1,3 +1,5 @@
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -48,7 +50,7 @@ namespace spot
{
const state* s = i->current_state();
os_ << " " << quote_unless_bare_word(automata_->format_state(s));
delete s;
s->destroy();
}
os_ << ";" << std::endl;
delete i;
@ -69,7 +71,7 @@ namespace spot
<< ",";
output_acc_set(si->current_acceptance_conditions());
os_ << ";" << std::endl;
delete dest;
dest->destroy();
}
}

4
src/evtgbaalgos/tgba2evtgba.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -72,7 +72,7 @@ namespace spot
{
const state* s = si->current_state();
process_state(s, out, 0);
delete s;
s->destroy();
}
rsymbol_set ss = acc_to_symbol_set(si->current_acceptance_conditions());

11
src/saba/sabacomplementtgba.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -220,7 +220,8 @@ namespace spot
{
bdd c = iterator->current_condition();
if ((c & condition) != bddfalse)
state_list.push_back(shared_state(iterator->current_state()));
state_list.push_back(shared_state(iterator->current_state(),
shared_state_deleter));
}
delete iterator;
@ -399,12 +400,14 @@ namespace spot
saba_state_complement_tgba* new_init;
if (automaton_->state_is_accepting(original_init_state))
new_init =
new saba_state_complement_tgba(shared_state(original_init_state),
new saba_state_complement_tgba(shared_state(original_init_state,
shared_state_deleter),
2 * nb_states_,
the_acceptance_cond_);
else
new_init =
new saba_state_complement_tgba(shared_state(original_init_state),
new saba_state_complement_tgba(shared_state(original_init_state,
shared_state_deleter),
2 * nb_states_,
bddfalse);

25
src/tgba/state.hh
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@ -74,6 +74,27 @@ namespace spot
/// Duplicate a state.
virtual state* clone() const = 0;
/// \brief Release a state.
///
/// Methods from the tgba or tgba_succ_iterator always return a
/// new state that you should deallocate with this function.
/// Before Spot 0.7, you had to "delete" your state directly.
/// Starting with Spot 0.7, you update your code to this function
/// instead (which simply calls "delete"). In a future version,
/// some subclasses will redefine destroy() to allow better memory
/// management (e.g. no memory allocation for explicit automata).
virtual void destroy() const
{
delete this;
}
// FIXME: Make the destructor protected after Spot 0.7.
//protected:
/// \brief Destructor.
///
/// \deprecated Client code should now call
/// <code>s->destroy();</code> instead of <code>delete s;</code>.
virtual ~state()
{
}
@ -156,6 +177,8 @@ namespace spot
typedef boost::shared_ptr<const state> shared_state;
inline void shared_state_deleter(state* s) { s->destroy(); }
/// \brief Strict Weak Ordering for \c shared_state
/// (shared_ptr<const state*>).
/// \ingroup tgba_essentials

14
src/tgba/tgba.cc
View file

@ -1,3 +1,5 @@
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'EPITA (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -32,8 +34,10 @@ namespace spot
tgba::~tgba()
{
delete last_support_conditions_input_;
delete last_support_variables_input_;
if (last_support_conditions_input_)
last_support_conditions_input_->destroy();
if (last_support_variables_input_)
last_support_variables_input_->destroy();
}
bdd
@ -43,7 +47,8 @@ namespace spot
|| last_support_conditions_input_->compare(state) != 0)
{
last_support_conditions_output_ = compute_support_conditions(state);
delete last_support_conditions_input_;
if (last_support_conditions_input_)
last_support_conditions_input_->destroy();
last_support_conditions_input_ = state->clone();
}
return last_support_conditions_output_;
@ -56,7 +61,8 @@ namespace spot
|| last_support_variables_input_->compare(state) != 0)
{
last_support_variables_output_ = compute_support_variables(state);
delete last_support_variables_input_;
if (last_support_variables_input_)
last_support_variables_input_->destroy();
last_support_variables_input_ = state->clone();
}
return last_support_variables_output_;

9
src/tgba/tgbakvcomplement.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -443,7 +443,7 @@ namespace spot
bdd c = iterator->current_condition();
if ((c & condition) != bddfalse)
{
shared_state s(iterator->current_state());
shared_state s(iterator->current_state(), shared_state_deleter);
if (highest_current_ranks_.find(s) != highest_current_ranks_.end())
{
if (i->second < highest_current_ranks_[s])
@ -470,7 +470,7 @@ namespace spot
bdd c = iterator->current_condition();
if ((c & condition) != bddfalse)
{
shared_state s(iterator->current_state());
shared_state s(iterator->current_state(), shared_state_deleter);
highest_state_set_.insert(s);
}
}
@ -621,7 +621,8 @@ namespace spot
{
state_kv_complement* init = new state_kv_complement();
rank_t r = {2 * nb_states_, bdd_ordered()};
init->add(shared_state(automaton_->get_init_state()), r);
init->add(shared_state(automaton_->get_init_state(), shared_state_deleter),
r);
return init;
}

4
src/tgba/tgbaproduct.cc
View file

@ -41,8 +41,8 @@ namespace spot
state_product::~state_product()
{
delete left_;
delete right_;
left_->destroy();
right_->destroy();
}
int

10
src/tgba/tgbareduc.cc
View file

@ -1,5 +1,5 @@
// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
@ -156,7 +156,7 @@ namespace spot
spot::state* init = automata_->get_init_state();
if (init->compare(s) == 0)
this->set_init_state(automata_->format_state(s));
delete init;
init->destroy();
transition* t;
for (si->first(); !si->done(); si->next())
@ -165,7 +165,7 @@ namespace spot
t = this->create_transition(s, init);
this->add_conditions(t, si->current_condition());
this->add_acceptance_conditions(t, si->current_acceptance_conditions());
delete init;
init->destroy();
}
}
@ -361,7 +361,7 @@ namespace spot
sim1 = sim2;
sim2 = simtmp;
}
delete init;
init->destroy();
sp_map::iterator i = state_predecessor_map_.find(s1);
if (i == state_predecessor_map_.end()) // 0 predecessor

10
src/tgba/tgbasafracomplement.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -170,7 +170,7 @@ namespace spot
delete *i;
for (subset_t::iterator i = nodes.begin(); i != nodes.end(); ++i)
delete *i;
(*i)->destroy();
}
const safra_tree&
@ -403,7 +403,7 @@ namespace spot
const state* s = *node_it;
(*child_it)->remove_node_from_children(*node_it);
(*child_it)->nodes.erase(node_it++);
delete s;
s->destroy();
}
else
{
@ -431,7 +431,7 @@ namespace spot
{
const spot::state* s = *it;
(*child_it)->nodes.erase(it);
delete s;
s->destroy();
}
(*child_it)->remove_node_from_children(state);
}
@ -679,7 +679,7 @@ namespace spot
for (safra_tree::tr_cache_t::iterator j = i->second.begin();
j != i->second.end();
++j)
delete j->second;
j->second->destroy();
// delete node;
}

4
src/tgba/tgbasgba.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -48,7 +48,7 @@ namespace spot
virtual
~state_sgba_proxy()
{
delete s_;
s_->destroy();
}
state*

18
src/tgba/tgbatba.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2010 Laboratoire de Recherche et Développement de
// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de
// l'Epita.
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -56,7 +56,7 @@ namespace spot
virtual
~state_tba_proxy()
{
delete s_;
s_->destroy();
}
state*
@ -204,7 +204,7 @@ namespace spot
else // Yes, combine labels.
{
id->second |= it->current_condition();
delete dest;
dest->destroy();
}
}
delete it;
@ -219,7 +219,7 @@ namespace spot
const state* d = i->first.first;
// Advance i before deleting d.
++i;
delete d;
d->destroy();
}
}
@ -318,7 +318,7 @@ namespace spot
// Advance the iterator before deleting the key.
const state* s = i->first;
++i;
delete s;
s->destroy();
}
}
@ -452,15 +452,15 @@ namespace spot
// duplication of the initial state.
// The cycle_start_ points to the right starting
// point already, so just return.
delete dest;
dest->destroy();
delete it;
delete init;
init->destroy();
return;
}
delete dest;
dest->destroy();
}
delete it;
delete init;
init->destroy();
}
// If we arrive here either because the number of acceptance

10
src/tgba/tgbaunion.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -38,8 +38,8 @@ namespace spot
state_union::~state_union()
{
delete left_;
delete right_;
left_->destroy();
right_->destroy();
}
int
@ -293,8 +293,8 @@ namespace spot
right_acc_missing_,
left_var_missing_,
right_var_missing_);
delete left_init;
delete right_init;
left_init->destroy();
right_init->destroy();
}
else
{

3
src/tgba/wdbacomp.cc
View file

@ -44,7 +44,8 @@ namespace spot
virtual
~state_wdba_comp_proxy()
{
delete s_;
if (s_)
s_->destroy();
}
state*

14
src/tgbaalgos/cutscc.cc
View file

@ -1,5 +1,5 @@
// Copyright (C) 2009 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -72,7 +72,7 @@ namespace spot
}
else
{
delete dst;
dst->destroy();
}
tgba_explicit::transition* t =
sub_a->create_transition(cur_format, dst_format);
@ -83,7 +83,7 @@ namespace spot
}
else
{
delete dst;
dst->destroy();
}
}
delete sit;
@ -93,7 +93,7 @@ namespace spot
// Free visited states.
for (it2 = seen.begin(); it2 != seen.end(); it2++)
{
delete *it2;
(*it2)->destroy();
}
return sub_a;
}
@ -255,7 +255,7 @@ namespace spot
scc_sizes[i] = m.states_of(i).size();
state* initial_state = a->get_init_state();
unsigned init = m.scc_of_state(initial_state);
delete initial_state;
initial_state->destroy();
// Find all interesting pathes in our automaton.
find_paths_sub(init, m, d, scc_sizes);
@ -272,7 +272,7 @@ namespace spot
std::vector<std::vector<sccs_set* > >* rec_paths = find_paths(a, m);
state* initial_state = a->get_init_state();
unsigned init = m.scc_of_state(initial_state);
delete initial_state;
initial_state->destroy();
std::vector<sccs_set*>* final_sets =&(*rec_paths)[init];
if (rec_paths->empty())
{

12
src/tgbaalgos/emptiness.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -42,9 +42,9 @@ namespace spot
tgba_run::~tgba_run()
{
for (steps::const_iterator i = prefix.begin(); i != prefix.end(); ++i)
delete i->s;
i->s->destroy();
for (steps::const_iterator i = cycle.begin(); i != cycle.end(); ++i)
delete i->s;
i->s->destroy();
}
tgba_run::tgba_run(const tgba_run& run)
@ -345,7 +345,7 @@ namespace spot
// browse the actual outgoing transitions
tgba_succ_iterator* j = a->succ_iter(s);
delete s;
s->destroy(); // FIXME: is it always legitimate to destroy s before j?
for (j->first(); !j->done(); j->next())
{
if (j->current_condition() != label
@ -355,7 +355,7 @@ namespace spot
const state* s2 = j->current_state();
if (s2->compare(next) != 0)
{
delete s2;
s2->destroy();
continue;
}
else
@ -386,7 +386,7 @@ namespace spot
if (l == &run->cycle && i != l->begin())
seen_acc |= acc;
}
delete s;
s->destroy();
assert(seen_acc == a->all_acceptance_conditions());

10
src/tgbaalgos/gtec/ce.cc
View file

@ -1,8 +1,8 @@
// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
// Copyright (C) 2010 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -55,7 +55,7 @@ namespace spot
// Ignore unknown states ...
if (!sip.first)
{
delete s;
s->destroy();
return 0;
}
// ... as well as dead states.
@ -129,7 +129,7 @@ namespace spot
if (ps != ss.end())
{
// The initial state is on the cycle.
delete prefix_start;
prefix_start->destroy();
cycle_entry_point = *ps;
}
else
@ -198,7 +198,7 @@ namespace spot
// Ignore unknown states.
if (!sip.first)
{
delete s;
s->destroy();
return 0;
}
// Stay in the final SCC.

4
src/tgbaalgos/gtec/explscc.cc
View file

@ -1,3 +1,5 @@
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -30,7 +32,7 @@ namespace spot
if (it != states.end())
{
if (s != *it)
delete s;
s->destroy();
return *it;
}
else

4
src/tgbaalgos/gtec/gtec.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2008 Laboratoire de Recherche et Développement
// Copyright (C) 2008, 2011 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),
@ -376,7 +376,7 @@ namespace spot
numbered_state_heap::state_index_p spi = ecs_->h->index(q->s);
// ... or if it is an unknown state.
if (spi.first == 0)
delete q->s;
q->s->destroy();
}
dec_depth(todo.back().q.size() + 1);
todo.pop_back();

8
src/tgbaalgos/gtec/nsheap.cc
View file

@ -1,3 +1,5 @@
// Copyright (C) 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -84,7 +86,7 @@ namespace spot
// Advance the iterator before deleting the key.
const state* s = i->first;
++i;
delete s;
s->destroy();
}
}
@ -105,7 +107,7 @@ namespace spot
res.second = i->second;
if (s != i->first)
delete s;
s->destroy();
}
return res;
}
@ -127,7 +129,7 @@ namespace spot
res.second = &i->second;
if (s != i->first)
delete s;
s->destroy();
}
return res;
}

12
src/tgbaalgos/gv04.cc
View file

@ -1,8 +1,8 @@
// Copyright (C) 2008, 2010, 2011 Laboratoire de recherche et
// développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Pierre et Marie Curie.
// Copyright (C) 2008, 2010 Laboratoire de recherche et développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -88,7 +88,7 @@ namespace spot
// Advance the iterator before deleting the "key" pointer.
const state* ptr = s->first;
++s;
delete ptr;
ptr->destroy();
}
}
@ -156,7 +156,7 @@ namespace spot
<< std::endl;
}
delete s_prime;
s_prime->destroy();
}
}
set_states(h.size());
@ -355,11 +355,11 @@ namespace spot
// Or it is still on the stack but not in the SCC
|| data.stack[j->second].lowlink < scc_root)
{
delete s;
s->destroy();
return 0;
}
r->inc_ars_cycle_states();
delete s;
s->destroy();
return j->first;
}

10
src/tgbaalgos/magic.cc
View file

@ -1,3 +1,5 @@
// Copyright (C) 2011 Laboratoire de recherche et développement de
// l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -292,7 +294,7 @@ namespace spot
// to visit white states either if a cycle can be missed
// with bit-state hashing search.
trace << " It is white, pop it" << std::endl;
delete s_prime;
s_prime->destroy();
}
else if (c.get_color() == BLUE)
{
@ -463,7 +465,7 @@ namespace spot
// Advance the iterator before deleting the "key" pointer.
const state* ptr = s->first;
++s;
delete ptr;
ptr->destroy();
}
}
@ -474,7 +476,7 @@ namespace spot
return color_ref(0);
if (s!=it->first)
{
delete s;
s->destroy();
s = it->first;
}
return color_ref(&(it->second));
@ -564,7 +566,7 @@ namespace spot
void pop_notify(const state* s) const
{
delete s;
s->destroy();
}
bool has_been_visited(const state* s) const

20
src/tgbaalgos/minimize.cc
View file

@ -105,7 +105,7 @@ namespace spot
seen->insert(dst);
}
else
delete dst;
dst->destroy();
}
delete sit;
}
@ -151,7 +151,7 @@ namespace spot
{
const state* dst = succit->current_state();
unsigned dst_num = state_num[dst];
delete dst;
dst->destroy();
trs* t = res->create_transition(src_num, dst_num);
res->add_conditions(t, succit->current_condition());
if (accepting)
@ -163,7 +163,7 @@ namespace spot
res->merge_transitions();
const state* init_state = a->get_init_state();
unsigned init_num = state_num[init_state];
delete init_state;
init_state->destroy();
res->set_init_state(init_num);
return res;
}
@ -190,7 +190,7 @@ namespace spot
{
hash_set::const_iterator old = i;
++i;
delete *old;
(*old)->destroy();
}
}
@ -205,7 +205,7 @@ namespace spot
}
else
{
delete s;
s->destroy();
s = *i;
}
// Ignore states outside SCC #n.
@ -250,11 +250,11 @@ namespace spot
for (n = 1, i = loop.begin(); n < loop_size; ++n, ++i)
{
loop_a.create_transition(n - 1, n)->condition = i->label;
delete i->s;
i->s->destroy();
}
assert(i != loop.end());
loop_a.create_transition(n - 1, 0)->condition = i->label;
delete i->s;
i->s->destroy();
assert(++i == loop.end());
const state* loop_a_init = loop_a.get_init_state();
@ -284,7 +284,7 @@ namespace spot
delete p;
}
delete loop_a_init;
loop_a_init->destroy();
return accepting;
}
@ -383,7 +383,7 @@ namespace spot
{
const state* dst = si->current_state();
unsigned dst_set = state_set_map[dst];
delete dst;
dst->destroy();
f |= (bdd_ithvar(dst_set) & si->current_condition());
}
delete si;
@ -480,7 +480,7 @@ namespace spot
for (hit = state_set_map.begin(); hit != state_set_map.end();)
{
hash_map::iterator old = hit++;
delete old->first;
old->first->destroy();
}
std::list<hash_set*>::iterator it;
for (it = done.begin(); it != done.end(); ++it)

34
src/tgbaalgos/ndfs_result.hxx
View file

@ -1,3 +1,5 @@
// Copyright (C) 2011 Laboratoire de recherche et développement de
// l'Epita (LRDE).
// Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -190,7 +192,7 @@ namespace spot
(void) b;
}
delete start;
start->destroy();
assert(!acc_trans.empty());
@ -205,8 +207,8 @@ namespace spot
for (typename accepting_transitions_list::const_iterator i =
acc_trans.begin(); i != acc_trans.end(); ++i)
{
delete i->source;
delete i->dest;
i->source->destroy();
i->dest->destroy();
}
return run;
@ -240,13 +242,13 @@ namespace spot
{
const state* s = *i;
++i;
delete s;
s->destroy();
}
for (state_set::iterator i = dead.begin(); i != dead.end();)
{
const state* s = *i;
++i;
delete s;
s->destroy();
}
}
@ -282,7 +284,7 @@ namespace spot
if (dead.find(s_prime) != dead.end())
{
ndfsr_trace << " it is dead, pop it" << std::endl;
delete s_prime;
s_prime->destroy();
}
else if (seen.find(s_prime) == seen.end())
{
@ -309,23 +311,23 @@ namespace spot
if (covered_acc == a_->all_acceptance_conditions())
{
clean(st1, seen, dead);
delete s_prime;
s_prime->destroy();
return true;
}
}
delete s_prime;
s_prime->destroy();
}
else
{
ndfsr_trace << " already seen, pop it" << std::endl;
delete s_prime;
s_prime->destroy();
}
}
else
{
ndfsr_trace << " not seen during the search, pop it"
<< std::endl;
delete s_prime;
s_prime->destroy();
}
}
else
@ -384,7 +386,7 @@ namespace spot
{
const state* ptr = *i;
++i;
delete ptr;
ptr->destroy();
}
}
@ -403,7 +405,7 @@ namespace spot
|| seen.find(s) != seen.end()
|| dead.find(s) != dead.end())
{
delete s;
s->destroy();
return 0;
}
ars->inc_ars_cycle_states();
@ -477,7 +479,7 @@ namespace spot
{
const state* ptr = *i;
++i;
delete ptr;
ptr->destroy();
}
}
@ -499,7 +501,7 @@ namespace spot
ndfsr_trace << " not visited" << std::endl;
else
ndfsr_trace << " already seen" << std::endl;
delete s;
s->destroy();
return 0;
}
ndfsr_trace << " OK" << std::endl;
@ -634,7 +636,7 @@ namespace spot
if (ps != target.end())
{
// The initial state is on the cycle.
delete prefix_start;
prefix_start->destroy();
cycle_entry_point = ps->first->clone();
}
else
@ -653,7 +655,7 @@ namespace spot
&& cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it)
continue;
assert(cycle_ep_it != run->cycle.end());
delete cycle_entry_point;
cycle_entry_point->destroy();
// Now shift the cycle so it starts on cycle_entry_point.
run->cycle.splice(run->cycle.end(), run->cycle,

10
src/tgbaalgos/neverclaim.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -71,7 +71,7 @@ namespace spot
os_ << " skip" << std::endl;
}
os_ << "}" << std::endl;
delete init_;
init_->destroy();
}
bool
@ -110,7 +110,7 @@ namespace spot
label = "accept_S" + ns;
else
label = "accept_all";
delete current;
current->destroy();
}
delete it;
}
@ -156,7 +156,7 @@ namespace spot
os_ << " if" << std::endl;
fi_needed_ = true;
}
delete current;
current->destroy();
}
delete it;
}
@ -174,7 +174,7 @@ namespace spot
f->destroy();
state* current = si->current_state();
os_ << ") -> goto " << get_state_label(current, out) << std::endl;
delete current;
current->destroy();
}
}

4
src/tgbaalgos/powerset.hh
View file

@ -47,7 +47,7 @@ namespace spot
// Advance the iterator before deleting the key.
const state* s = *i;
++i;
delete s;
s->destroy();
}
}
@ -63,7 +63,7 @@ namespace spot
state_set::const_iterator i = states.find(s);
if (i != states.end())
{
delete s;
s->destroy();
s = *i;
}
else

6
src/tgbaalgos/reachiter.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -42,7 +42,7 @@ namespace spot
// Advance the iterator before deleting the "key" pointer.
const state* ptr = s->first;
++s;
delete ptr;
ptr->destroy();
}
}
@ -80,7 +80,7 @@ namespace spot
{
if (ws)
process_link(t, tn, s->first, s->second, si);
delete current;
current->destroy();
}
}
delete si;

8
src/tgbaalgos/reducerun.cc
View file

@ -1,3 +1,5 @@
// Copyright (C) 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -46,7 +48,7 @@ namespace spot
{
const state* ptr = *i;
++i;
delete ptr;
ptr->destroy();
}
}
@ -70,7 +72,7 @@ namespace spot
seen.insert(s);
else
{
delete s;
s->destroy();
s = *i;
}
return s;
@ -162,7 +164,7 @@ namespace spot
if (ps != ss.end())
{
// The initial state is on the cycle.
delete prefix_start;
prefix_start->destroy();
cycle_entry_point = *ps;
}
else

10
src/tgbaalgos/reductgba_sim.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -469,7 +469,7 @@ namespace spot
else
delete p;
}
delete s;
s->destroy();
}
delete si;
}
@ -513,7 +513,7 @@ namespace spot
(*j)->add_succ(*i);
++nb_ds;
}
delete s;
s->destroy();
}
delete si;
}
@ -534,7 +534,7 @@ namespace spot
(*i)->add_succ(*j);
++nb_sd;
}
delete s;
s->destroy();
}
delete si;
}
@ -656,7 +656,7 @@ namespace spot
{
const state* ptr = j->first;
++j;
delete ptr;
ptr->destroy();
}
}

12
src/tgbaalgos/reductgba_sim_del.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2008 Laboratoire de Recherche et Développement
// Copyright (C) 2008, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -410,7 +410,7 @@ namespace spot
s = si->current_state();
if (s->compare(*i1) == 0)
{
delete s;
s->destroy();
duplicator_node_delayed* dn
= add_duplicator_node_delayed(*i1,
sn->get_duplicator_node(),
@ -426,7 +426,7 @@ namespace spot
build_recurse_successor_duplicator(dn, sn, os2);
}
else
delete s;
s->destroy();
}
}
@ -463,7 +463,7 @@ namespace spot
if (s->compare(*i1) == 0)
{
delete s;
s->destroy();
spoiler_node_delayed* sn_n
= add_spoiler_node_delayed(dn->get_spoiler_node(),
*i1,
@ -478,7 +478,7 @@ namespace spot
build_recurse_successor_spoiler(sn_n, os2);
}
else
delete s;
s->destroy();
}
}
@ -668,7 +668,7 @@ namespace spot
{
const state* ptr = j->first;
++j;
delete ptr;
ptr->destroy();
}
}

18
src/tgbaalgos/replayrun.cc
View file

@ -1,3 +1,5 @@
// Copyright (C) 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -80,7 +82,7 @@ namespace spot
<< a->format_state(i->s) << std::endl
<< "does not match initial state of automata: "
<< a->format_state(s) << std::endl;
delete s;
s->destroy();
return false;
}
@ -98,7 +100,7 @@ namespace spot
for (d = o->second.begin(); d != o->second.end(); ++d)
msg << " == " << *d;
o->second.insert(serial);
delete s;
s->destroy();
s = o->first;
}
else
@ -142,7 +144,7 @@ namespace spot
// When not debugging, S is not used as key in SEEN, so we can
// delete it right now.
if (!debug)
delete s;
s->destroy();
for (j->first(); !j->done(); j->next())
{
if (j->current_condition() != label
@ -152,7 +154,7 @@ namespace spot
const state* s2 = j->current_state();
if (s2->compare(next))
{
delete s2;
s2->destroy();
continue;
}
else
@ -185,11 +187,11 @@ namespace spot
<< bdd_format_accset(a->get_dict(),
j->current_acceptance_conditions())
<< " going to " << a->format_state(s2) << std::endl;
delete s2;
s2->destroy();
}
}
delete j;
delete s;
s->destroy();
return false;
}
if (debug)
@ -232,7 +234,7 @@ namespace spot
}
}
}
delete s;
s->destroy();
if (all_acc != expected_all_acc)
{
if (debug)
@ -251,7 +253,7 @@ namespace spot
// Advance the iterator before deleting the "key" pointer.
const state* ptr = o->first;
++o;
delete ptr;
ptr->destroy();
}
return true;

4
src/tgbaalgos/safety.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2010 Laboratoire de Recherche et Développement de
// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de
// l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
@ -58,7 +58,7 @@ namespace spot
bdd cond = it->current_condition();
it->next();
result = (!dest->compare(s)) && it->done() && (cond == bddtrue);
delete dest;
dest->destroy();
delete it;
}

10
src/tgbaalgos/save.cc
View file

@ -1,6 +1,8 @@
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
// Copyright (C) 2011 Laboratoire de Recherche et Développement de
// l'Epita (LRDE)
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@ -59,7 +61,7 @@ namespace spot
escape_str(os_, bdd_format_formula(d, si->current_condition()));
os_ << "\",";
print_acc(si->current_acceptance_conditions()) << ";" << std::endl;
delete dest;
dest->destroy();
}
}

6
src/tgbaalgos/scc.cc
View file

@ -54,7 +54,7 @@ namespace spot
// Advance the iterator before deleting the key.
const state* s = i->first;
++i;
delete s;
s->destroy();
}
}
@ -63,7 +63,7 @@ namespace spot
{
state* in = aut_->get_init_state();
int val = scc_of_state(in);
delete in;
in->destroy();
return val;
}
@ -231,7 +231,7 @@ namespace spot
}
// If we know the state, reuse the previous object.
delete dest;
dest->destroy();
dest = spi->first;
// Have we reached a maximal SCC?

14
src/tgbaalgos/se05.cc
View file

@ -1,3 +1,5 @@
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -292,7 +294,7 @@ namespace spot
// collision, this property does not hold.
trace << " It is white (due to collision), pop it"
<< std::endl;
delete s_prime;
s_prime->destroy();
}
else if (c.get_color() == RED)
{
@ -499,14 +501,14 @@ namespace spot
{
const state* ptr = *sc;
++sc;
delete ptr;
ptr->destroy();
}
hash_type::const_iterator s = h.begin();
while (s != h.end())
{
const state* ptr = s->first;
++s;
delete ptr;
ptr->destroy();
}
}
@ -520,14 +522,14 @@ namespace spot
return color_ref(0); // white state
if (s!=it->first)
{
delete s;
s->destroy();
s = it->first;
}
return color_ref(&(it->second)); // blue or red state
}
if (s!=*ic)
{
delete s;
s->destroy();
s = *ic;
}
return color_ref(&h, &hc, *ic); // cyan state
@ -651,7 +653,7 @@ namespace spot
void pop_notify(const state* s) const
{
delete s;
s->destroy();
}
bool has_been_visited(const state* s) const

8
src/tgbaalgos/tau03.cc
View file

@ -1,3 +1,5 @@
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -251,7 +253,7 @@ namespace spot
if (c_prime.is_white())
{
trace << " It is white, pop it" << std::endl;
delete s_prime;
s_prime->destroy();
}
else if ((c_prime.get_acc() & acu) != acu)
{
@ -328,7 +330,7 @@ namespace spot
// Advance the iterator before deleting the "key" pointer.
const state* ptr = s->first;
++s;
delete ptr;
ptr->destroy();
}
}
@ -339,7 +341,7 @@ namespace spot
return color_ref(0, 0);
if (s!=it->first)
{
delete s;
s->destroy();
s = it->first;
}
return color_ref(&(it->second.first), &(it->second.second));

12
src/tgbaalgos/tau03opt.cc
View file

@ -1,3 +1,5 @@
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -340,7 +342,7 @@ namespace spot
if (c_prime.is_white())
{
trace << " It is white, pop it" << std::endl;
delete s_prime;
s_prime->destroy();
continue;
}
else if (c_prime.get_color() == CYAN &&
@ -492,14 +494,14 @@ namespace spot
{
const state* ptr = sc->first;
++sc;
delete ptr;
ptr->destroy();
}
hash_type::const_iterator s = h.begin();
while (s != h.end())
{
const state* ptr = s->first;
++s;
delete ptr;
ptr->destroy();
}
}
@ -514,7 +516,7 @@ namespace spot
return color_ref(0, 0);
if (s!=it->first)
{
delete s;
s->destroy();
s = it->first;
}
// blue or red state
@ -522,7 +524,7 @@ namespace spot
}
if (s!=ic->first)
{
delete s;
s->destroy();
s = ic->first;
}
// cyan state