From 0ca40d72d7fee8c9ffb4f0f854e7c90eeb50a6b0 Mon Sep 17 00:00:00 2001 From: Ala-Eddine Ben-Salem Date: Thu, 5 Jan 2012 19:16:44 +0100 Subject: [PATCH] Fix detection of the last iteration of minimize_dfa(). * src/tgbaalgos/minimize.cc (minimize_dfa): Fix detection of the last iteration. An extra iteration case could be missed in case where a split generates only singletons, and yet predecessor classes need to be refined. --- AUTHORS | 1 + ChangeLog | 9 +++++++++ NEWS | 4 ++++ src/tgbaalgos/minimize.cc | 4 ++-- 4 files changed, 16 insertions(+), 2 deletions(-) diff --git a/AUTHORS b/AUTHORS index 7698dc3cb..83f21fcf2 100644 --- a/AUTHORS +++ b/AUTHORS @@ -1,5 +1,6 @@ Have contributed to Spot: +Ala-Eddine Ben-Salem Alexandre Duret-Lutz Damien Lefortier Denis Poitrenaud diff --git a/ChangeLog b/ChangeLog index baeeead25..223569e22 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2012-01-05 Ala-Eddine Ben-Salem + + Fix detection of the last iteration of minimize_dfa(). + + * src/tgbaalgos/minimize.cc (minimize_dfa): Fix detection of the + last iteration. An extra iteration case could be missed in case + where a split generates only singletons, and yet predecessor + classes need to be refined. + 2012-01-05 Alexandre Duret-Lutz Fix computation of length of LTL formulas. diff --git a/NEWS b/NEWS index a0d52ce4d..058c39838 100644 --- a/NEWS +++ b/NEWS @@ -3,6 +3,10 @@ New in spot 0.8.1a: * Bug fixes: - spot::ltl::length() forgot to count the '&' and '|' operators in an LTL formula. + - minimize_dfa() could produce incorrect automata, but it's not + clear whether this could have had an inpact on WDBA minimization + (the worse case is that some TGBA would not have been minimized + when they could). New in spot 0.8.1: diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index c83abe77d..978b4e9a1 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -425,6 +425,7 @@ namespace spot } else { + did_split = true; for (; bsi != bdd_map.end(); ++bsi) { hash_set* set = bsi->second; @@ -457,7 +458,6 @@ namespace spot } else { - did_split = true; trace << "set " << format_hash_set(set, det_a) << " should be processed further" << std::endl; next_run.push_back(set);