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

* iface/gspn/gspn.cc (tgba_succ_iterator_gspn::tgba_succ_iterator_gspn):

Browse source 
Set size_ to 1 when stuttering is needed, so that done() does not
return true immediately.
This commit is contained in:
Alexandre Duret-Lutz 2004-07-16 11:19:28 +00:00
parent 7abc2604f3
commit 44ebe5a746
2 changed files with 11 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
ChangeLog
View file

@ -1,3 +1,9 @@
2004-07-16 Alexandre Duret-Lutz <adl@src.lip6.fr>
* iface/gspn/gspn.cc (tgba_succ_iterator_gspn::tgba_succ_iterator_gspn):
Set size_ to 1 when stuttering is needed, so that done() does not
return true immediately.
2004-07-12 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/gtec/gtec.hh: Typos in comments.

7
iface/gspn/gspn.cc
View file

@ -146,10 +146,10 @@ namespace spot
// * If DEAD is any other string, this is the name a property
// that should be true when looping on a dead state, and false
// otherwise.
// We handle these three case by setting ALIVE_PROP and DEAD_PROP
// We handle these three cases by setting ALIVE_PROP and DEAD_PROP
// appropriately. ALIVE_PROP is the bdd that should be ANDed
// to all transitions leaving a live state, while DEAD_PROP should
// bdd ANDed to all transitions leaving a dead state.
// be ANDed to all transitions leaving a dead state.
if (!strcasecmp(dead.c_str(), "false"))
{
alive_prop = bddtrue;
@ -241,6 +241,9 @@ namespace spot
// GreatSPN should return successors_ == 0 and size_ == 0 when a
// state has no successors.
assert((size_ <= 0) ^ (successors_ != 0));
// If we have to stutter on a dead state, we have one successor.
if (size_ <= 0 && data_->dead_prop != bddfalse)
size_ = 1;
}
virtual