From 7fd9459a63cf78f2f1958bc3be17ee1ab683cfdf Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 5 Apr 2004 12:43:06 +0000 Subject: [PATCH] * src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle): Do not visit a state more than once. Report from Soheib Baarir. --- ChangeLog | 5 +++++ src/tgbaalgos/emptinesscheck.cc | 4 ++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/ChangeLog b/ChangeLog index 166acf0c2..06f38ca50 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2004-04-05 Alexandre Duret-Lutz + + * src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle): + Do not visit a state more than once. Report from Soheib Baarir. + 2004-03-25 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict): Reuse Acc and Var diff --git a/src/tgbaalgos/emptinesscheck.cc b/src/tgbaalgos/emptinesscheck.cc index 702a7727f..eb9a47913 100644 --- a/src/tgbaalgos/emptinesscheck.cc +++ b/src/tgbaalgos/emptinesscheck.cc @@ -616,8 +616,8 @@ namespace spot { const state* dest = i->current_state(); - // Do not escape this SCC. - if (!scc.has_state(dest)) + // Do not escape this SCC or visit a state already visited. + if (!scc.has_state(dest) || father.find(dest) != father.end()) { delete dest; continue;