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

Impacts of the new method state.destroy()

Browse source 
* src/ta/taexplicit.cc, src/ta/taproduct.cc,
src/taalgos/minimize.cc, src/taalgos/sba2ta.cc:
changes to use the new method destroy() added to state.hh
This commit is contained in:
Ala Eddine 2011-04-04 11:01:27 +02:00 • committed by Alexandre Duret-Lutz
parent cd04d9acf3
commit bf01501e15
4 changed files with 47 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ta/taexplicit.cc
View file

@ -266,7 +266,7 @@ namespace spot
delete *it_trans;
}
delete trans;
delete get_tgba_state();
get_tgba_state()->destroy();
Sgi::hash_map<int, transitions*, Sgi::hash<int> >::iterator i =
transitions_by_condition.begin();

6
src/ta/taproduct.cc
View file

@ -38,7 +38,7 @@ namespace spot
state_ta_product::~state_ta_product()
{
//see ta_product::free_state() method
delete kripke_state_;
kripke_state_->destroy();
}
int
@ -170,7 +170,7 @@ namespace spot
return;
}
delete kripke_succ_it_current_state;
kripke_succ_it_current_state->destroy();
step_();
}
}
@ -263,7 +263,7 @@ namespace spot
}
else
{
delete kripke_init_state;
kripke_init_state->destroy();
}
}

59
src/taalgos/minimize.cc
View file

@ -103,7 +103,7 @@ namespace spot
const state* src = *hit;
unsigned src_num = state_num[src];
state* tgba_state = new state_explicit(tgba->add_state(src_num));
state* tgba_state = tgba->add_state(src_num);
bdd tgba_condition = bddtrue;
bool is_initial_state = a->is_initial_state(src);
if (is_initial_state)
@ -119,8 +119,8 @@ namespace spot
if (ta_src != new_src)
{
delete new_src;
delete tgba_state;
new_src->destroy();
tgba_state->destroy();
}
else if (is_initial_state)
ta->add_to_initial_states_set(new_src);
@ -135,7 +135,7 @@ namespace spot
if (i == state_num.end()) // Ignore useless destinations.
continue;
state* tgba_state = new state_explicit(tgba->add_state(i->second));
state* tgba_state = tgba->add_state(i->second);
bdd tgba_condition = bddtrue;
is_initial_state = a->is_initial_state(dst);
if (is_initial_state)
@ -150,9 +150,10 @@ namespace spot
state_ta_explicit* ta_dst = ta->add_state(new_dst);
if (ta_dst != new_dst) {
delete new_dst;
delete tgba_state;
if (ta_dst != new_dst)
{
new_dst->destroy();
tgba_state->destroy();
}
else if (is_initial_state)
ta->add_to_initial_states_set(new_dst);
@ -179,6 +180,8 @@ namespace spot
std::set<const state*> states_set = get_states_set(ta_);
hash_set* I = new hash_set;
// livelock acceptance states
hash_set* G = new hash_set;
@ -199,9 +202,7 @@ namespace spot
if (ta_->is_initial_state(s))
{
hash_set* i = new hash_set;
i->insert(s);
done.push_back(i);
I->insert(s);
}
else if (ta_->is_livelock_accepting_state(s)
&& ta_->is_accepting_state(s))
@ -237,17 +238,34 @@ namespace spot
free_var.insert(i);
std::map<int, int> used_var;
{
for (hash_set::const_iterator i = I->begin(); i != I->end(); ++i)
{
hash_set* cI = new hash_set;
cI->insert(*i);
done.push_back(cI);
used_var[set_num] = 1;
free_var.erase(set_num);
state_set_map[*i] = set_num;
set_num++;
}
}
if (!G->empty())
{
unsigned s = G->size();
used_var[set_num] = s;
free_var.erase(set_num);
unsigned num = ++set_num;
used_var[num] = s;
free_var.erase(num);
if (s > 1)
cur_run.push_back(G);
else
done.push_back(G);
for (hash_set::const_iterator i = G->begin(); i != G->end(); ++i)
state_set_map[*i] = set_num;
state_set_map[*i] = num;
}
else
@ -256,7 +274,7 @@ namespace spot
if (!F->empty())
{
unsigned s = F->size();
unsigned num = set_num + 1;
unsigned num = ++set_num;
used_var[num] = s;
free_var.erase(num);
if (s > 1)
@ -272,7 +290,7 @@ namespace spot
if (!G_F->empty())
{
unsigned s = G_F->size();
unsigned num = set_num + 2;
unsigned num = ++set_num;
used_var[num] = s;
free_var.erase(num);
if (s > 1)
@ -288,7 +306,7 @@ namespace spot
if (!S->empty())
{
unsigned s = S->size();
unsigned num = set_num + 3;
unsigned num = ++set_num;
used_var[num] = s;
free_var.erase(num);
if (s > 1)
@ -331,14 +349,7 @@ namespace spot
const state* dst = si->current_state();
hash_map::const_iterator i = state_set_map.find(dst);
if (i == state_set_map.end())
// The destination state is not in our
// partition. This can happen if the initial
// FINAL and NON_FINAL supplied to the algorithm
// do not cover the whole automaton (because we
// want to ignore some useless states). Simply
// ignore these states here.
continue;
assert(i != state_set_map.end());
f |= (bdd_ithvar(i->second) & si->current_condition());
}
delete si;

16
src/taalgos/sba2ta.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2010 Laboratoire de Recherche et Developpement
// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement
// de l Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -61,7 +61,7 @@ namespace spot
ta->add_to_initial_states_set(is);
todo.push(init_state);
}
delete tgba_init_state;
tgba_init_state->destroy();
while (!todo.empty())
{
@ -97,7 +97,7 @@ namespace spot
if (dest != new_dest)
{
// the state dest already exists in the testing automata
delete new_dest->get_tgba_state();
new_dest->get_tgba_state()->destroy();
delete new_dest;
}
else
@ -111,7 +111,7 @@ namespace spot
}
}
delete tgba_state;
tgba_state->destroy();
}
delete tgba_succ_it;
@ -158,7 +158,7 @@ namespace spot
ta::states_set_t init_states = testing_automata->get_initial_states_set();
for (it = init_states.begin(); it != init_states.end(); it++)
{
state* init_state = dynamic_cast<state_ta_explicit*> (*it);
state* init_state = down_cast<state_ta_explicit*> (*it);
init_set.push(init_state);
}
@ -168,7 +168,7 @@ namespace spot
// Setup depth-first search from initial states.
{
state_ta_explicit* init =
dynamic_cast<state_ta_explicit*> (init_set.top());
down_cast<state_ta_explicit*> (init_set.top());
init_set.pop();
state_ta_explicit* init_clone = init->clone();
numbered_state_heap::state_index_p h_init = h->find(init_clone);
@ -239,7 +239,7 @@ namespace spot
//add the state to G (=the livelock-accepting states set)
state_ta_explicit * livelock_accepting_state =
dynamic_cast<state_ta_explicit*> (*i);
down_cast<state_ta_explicit*> (*i);
livelock_accepting_state->set_livelock_accepting_state(
true);
@ -281,7 +281,7 @@ namespace spot
if (!is_stuttering_transition)
{
init_set.push(dest);
delete dest_clone;
dest_clone->destroy();
continue;
}