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

* src/tgbaalgos/gtec/gtec.cc (emptiness_check::remove_component):

Browse source 
Do not try to erase state that are not found in H.
Report from Soheib Baarir.
This commit is contained in:
Alexandre Duret-Lutz 2004-05-14 09:05:17 +00:00
parent 0c44ca35b3
commit 6f4ab3af6c
2 changed files with 13 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,5 +1,9 @@
2004-05-14 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-05-14 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/gtec/gtec.cc (emptiness_check::remove_component):
Do not try to erase state that are not found in H.
Report from Soheib Baarir.
* src/ltltest/reduc.test: Use ./defs and clean result.data. * src/ltltest/reduc.test: Use ./defs and clean result.data.
* src/ltltest/Makefile.am (CLEANFILES): Clean result.data. * src/ltltest/Makefile.am (CLEANFILES): Clean result.data.

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

@ -64,7 +64,15 @@ namespace spot
{ {
state* s = i->current_state(); state* s = i->current_state();
numbered_state_heap::state_index_p spi = ecs_->h->index(s); numbered_state_heap::state_index_p spi = ecs_->h->index(s);
assert(spi.second);
// This state is not necessary in H, because if we were
// doing inclusion checking during the emptiness-check
// (redefining find()), the index `s' can be included in a
// larger state and will not be found by index(). We can
// safely ignore such states.
if (!spi.first)
continue;
if (*spi.second != -1) if (*spi.second != -1)
{ {
*spi.second = -1; *spi.second = -1;