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

* src/tgba/taatgba.cc, src/tgba/taatbga.hh: Fix a memory issue on

Browse source 
Darwin.
This commit is contained in:
Felix Abecassis 2010-01-29 15:26:39 +01:00
parent 58d6b7912c
commit 1fbdf0bcaf
3 changed files with 35 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,3 +1,8 @@
2010-01-29 Felix Abecassis <felix.abecassis@lrde.epita.fr>
* src/tgba/taatgba.cc, src/tgba/taatbga.hh: Fix a memory issue on
Darwin.
2010-01-25 Damien Lefortier <dam@lrde.epita.fr>
* wrap/python/cgi/ltl2tgba.in, wrap/python/spot.i: Add a new

37
src/tgba/taatgba.cc
View file

@ -246,30 +246,35 @@ namespace spot
// If no contradiction, then look for another transition to
// merge with the new one.
seen_map::iterator i;
std::vector<taa_tgba::transition*>::iterator j;
if (t->condition != bddfalse)
{
for (i = seen_.find(b); i != seen_.end(); ++i)
i = seen_.find(b);
if (i != seen_.end())
for (j = i->second.begin(); j != i->second.end(); ++j)
{
if (*i->second->dst == *t->dst
&& i->second->condition == t->condition)
taa_tgba::transition* current = *j;
if (*current->dst == *t->dst
&& current->condition == t->condition)
{
i->second->acceptance_conditions &= t->acceptance_conditions;
current->acceptance_conditions &= t->acceptance_conditions;
break;
}
if (*i->second->dst == *t->dst
&& i->second->acceptance_conditions == t->acceptance_conditions)
if (*current->dst == *t->dst
&& current->acceptance_conditions == t->acceptance_conditions)
{
i->second->condition |= t->condition;
current->condition |= t->condition;
break;
}
}
}
// Mark the new transition as seen and keep it if we have not
// found any contraction and no other transition to merge with,
// or delete it otherwise.
if (t->condition != bddfalse && i == seen_.end())
// found any contradiction and no other transition to merge
// with, or delete it otherwise.
if (t->condition != bddfalse
&& (i == seen_.end() || j == i->second.end()))
{
seen_.insert(std::make_pair(b, t));
seen_[b].push_back(t);
succ_.push_back(t);
}
else
@ -296,11 +301,6 @@ namespace spot
taa_succ_iterator::~taa_succ_iterator()
{
for (unsigned i = 0; i < succ_.size(); ++i)
{
delete succ_[i]->dst;
delete succ_[i];
}
for (seen_map::iterator i = seen_.begin(); i != seen_.end();)
{
// Advance the iterator before deleting the state set.
@ -308,6 +308,11 @@ namespace spot
++i;
delete s;
}
for (unsigned i = 0; i < succ_.size(); ++i)
{
delete succ_[i]->dst;
delete succ_[i];
}
}
void

6
src/tgba/taatgba.hh
View file

@ -128,9 +128,9 @@ namespace spot
typedef taa_tgba::state::const_iterator iterator;
typedef std::pair<iterator, iterator> iterator_pair;
typedef std::vector<iterator_pair> bounds_t;
typedef Sgi::hash_multimap<
const spot::state_set*, taa_tgba::transition*, state_ptr_hash,
state_ptr_equal> seen_map;
typedef Sgi::hash_map<
const spot::state_set*, std::vector<taa_tgba::transition*>,
state_ptr_hash, state_ptr_equal> seen_map;
struct distance_sort :
public std::binary_function<const iterator_pair&,