From 99884e8e0f616e022908d20889638a08ccff8351 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Jan 2010 11:30:03 +0100 Subject: [PATCH] Fix a longstanding bug in our implementation of GV04. * src/tgbaalgos/gv04.cc (push): Fix the tracking of the accepting link. This bug was discovered on a random generated graph with a complex accepting cycle. * src/tgbatest/emptchk.test: Add the troublesome graph as test case. --- ChangeLog | 10 +++++++++ src/tgbaalgos/gv04.cc | 16 ++++++++------ src/tgbatest/emptchk.test | 44 ++++++++++++++++++++++++++++++++++++++- 3 files changed, 63 insertions(+), 7 deletions(-) diff --git a/ChangeLog b/ChangeLog index 511ea8c89..7e463d32e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +2010-01-21 Alexandre Duret-Lutz + + Fix a longstanding bug in our implementation of GV04. + + * src/tgbaalgos/gv04.cc (push): Fix the tracking of the accepting + link. This bug was discovered on a random generated graph with + a complex accepting cycle. + * src/tgbatest/emptchk.test: Add the troublesome graph as + test case. + 2010-01-20 Damien Lefortier When iterating a hash_map, be careful not to delete i->first diff --git a/src/tgbaalgos/gv04.cc b/src/tgbaalgos/gv04.cc index f0c66f48b..9a5e338c8 100644 --- a/src/tgbaalgos/gv04.cc +++ b/src/tgbaalgos/gv04.cc @@ -1,6 +1,8 @@ -// Copyright (C) 2004, 2005, 2008 Laboratoire d'Informatique de Paris -// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 +// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +// Pierre et Marie Curie. +// Copyright (C) 2008, 2010 Laboratoire de recherche et développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -175,13 +177,14 @@ namespace spot stack_entry ss = { s, 0, top, dftop, 0 }; if (accepting) - ss.acc = dftop; // This differs from GV04 to support TBA. + ss.acc = top - 1; // This differs from GV04 to support TBA. else if (dftop >= 0) ss.acc = stack[dftop].acc; else ss.acc = -1; - trace << " s.lowlink = " << top << std::endl; + trace << " s.lowlink = " << top << std::endl + << " s.acc = " << ss.acc << std::endl; stack.push_back(ss); dftop = top; @@ -216,7 +219,8 @@ namespace spot trace << " lowlinkupdate(f = " << f << ", t = " << t << ")" << std::endl << " t.lowlink = " << stack[t].lowlink << std::endl - << " f.lowlink = " << stack[f].lowlink << std::endl; + << " f.lowlink = " << stack[f].lowlink << std::endl + << " f.acc = " << stack[f].acc << std::endl; int stack_t_lowlink = stack[t].lowlink; if (stack_t_lowlink <= stack[f].lowlink) { diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index d6ab2151d..d4b05643e 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -1,7 +1,9 @@ #!/bin/sh -# Copyright (C) 2003, 2004, 2005, 2008, 2009 Laboratoire d'Informatique de +# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), # Université Pierre et Marie Curie. +# Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -95,3 +97,43 @@ expect_ce '!((FF a) <=> (F x))' 3 expect_no '!((FF a) <=> (F a))' 4 expect_no 'Xa && (!a U b) && !b && X!b' 4 expect_no '(a U !b) && Gb' 3 + + +# This graph was randomly generated, and contains one accepting path. +# It triggered a bug in our implementation of GV04 (that didn't see any +# accepting path). +cat >state-space <