From 44ebe5a746e056f9e11b3d4a85ea95336e2190ff Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 16 Jul 2004 11:19:28 +0000 Subject: [PATCH] * 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. --- ChangeLog | 6 ++++++ iface/gspn/gspn.cc | 7 +++++-- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/ChangeLog b/ChangeLog index 2b52b106b..baf362703 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,9 @@ +2004-07-16 Alexandre Duret-Lutz + + * 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 * src/tgbaalgos/gtec/gtec.hh: Typos in comments. diff --git a/iface/gspn/gspn.cc b/iface/gspn/gspn.cc index c9bc35a94..10b8723ee 100644 --- a/iface/gspn/gspn.cc +++ b/iface/gspn/gspn.cc @@ -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