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

Fix a longstanding bug in our implementation of GV04.

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2010-01-21 11:30:03 +01:00
parent 04827ef4a1
commit 99884e8e0f
3 changed files with 63 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

10
ChangeLog
View file

@ -1,3 +1,13 @@
2010-01-21 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <dam@lrde.epita.fr> 2010-01-20 Damien Lefortier <dam@lrde.epita.fr>
When iterating a hash_map, be careful not to delete i->first When iterating a hash_map, be careful not to delete i->first

16
src/tgbaalgos/gv04.cc
View file

@ -1,6 +1,8 @@
// Copyright (C) 2004, 2005, 2008 Laboratoire d'Informatique de Paris // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Université Pierre et Marie Curie. // 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. // This file is part of Spot, a model checking library.
// //
@ -175,13 +177,14 @@ namespace spot
stack_entry ss = { s, 0, top, dftop, 0 }; stack_entry ss = { s, 0, top, dftop, 0 };
if (accepting) 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) else if (dftop >= 0)
ss.acc = stack[dftop].acc; ss.acc = stack[dftop].acc;
else else
ss.acc = -1; 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); stack.push_back(ss);
dftop = top; dftop = top;
@ -216,7 +219,8 @@ namespace spot
trace << " lowlinkupdate(f = " << f << ", t = " << t trace << " lowlinkupdate(f = " << f << ", t = " << t
<< ")" << std::endl << ")" << std::endl
<< " t.lowlink = " << stack[t].lowlink << 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; int stack_t_lowlink = stack[t].lowlink;
if (stack_t_lowlink <= stack[f].lowlink) if (stack_t_lowlink <= stack[f].lowlink)
{ {

44
src/tgbatest/emptchk.test
View file

@ -1,7 +1,9 @@
#!/bin/sh #!/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), # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
# Université Pierre et Marie Curie. # 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. # 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 '!((FF a) <=> (F a))' 4
expect_no 'Xa && (!a U b) && !b && X!b' 4 expect_no 'Xa && (!a U b) && !b && X!b' 4
expect_no '(a U !b) && Gb' 3 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 <<EOF
acc = "a0";
"S0", "S12", "1",;
"S12", "S17", "1",;
"S12", "S8", "1",;
"S17", "S6", "1",;
"S17", "S9", "1", "a0";
"S17", "S2", "1",;
"S8", "S14", "1",;
"S8", "S2", "1",;
"S6", "S1", "1",;
"S9", "S18", "1",;
"S2", "S17", "1",;
"S14", "S19", "1",;
"S14", "S10", "1",;
"S1", "S15", "1",;
"S18", "S5", "1",;
"S19", "S5", "1",;
"S19", "S7", "1",;
"S19", "S11", "1",;
"S10", "S17", "1",;
"S15", "S8", "1",;
"S5", "S4", "1",;
"S11", "S6", "1",;
"S4", "S13", "1",;
"S13", "S3", "1",;
"S3", "S16", "1",;
"S3", "S19", "1",;
EOF
run 0 ../ltl2tgba -eCou99 -X state-space
run 0 ../ltl2tgba -eCVWY90 -X state-space
run 0 ../ltl2tgba -eGV04 -X state-space
run 0 ../ltl2tgba -eSE05 -X state-space
run 0 ../ltl2tgba -eTau03 -X state-space