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

enumerate_cycles: fix memory management.

Browse source 
* src/tgbaalgos/cycles.cc (tag_state): Destroy duplicate states, not
new states!
* src/tgbatest/cycles.test: Add a test case that used to segfault.
Reported by Étienne Renault.
This commit is contained in:
Alexandre Duret-Lutz 2012-09-30 15:19:05 +02:00
parent 4ed4e4d2a8
commit dd16f58ef4
2 changed files with 6 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tgbaalgos/cycles.cc
View file

@ -71,7 +71,7 @@ namespace spot
{ {
std::pair<tagged_state, bool> p = std::pair<tagged_state, bool> p =
tags_.insert(std::make_pair(s, state_info())); tags_.insert(std::make_pair(s, state_info()));
if (p.second) if (!p.second)
s->destroy(); s->destroy();
return p.first; return p.first;
} }

16
src/tgbatest/cycles.test
View file

@ -19,20 +19,12 @@
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA # Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
# 02111-1307, USA. # 02111-1307, USA.
# While running some benchmark, Tomáš Babiak found that Spot took too
# much time (i.e. >1h) to translate those six formulae. It turns out
# that the WDBA minimization was performed after the degeneralization
# algorithm, while this is not necessary (WDBA will produce a BA, so
# we may as well skip degeneralization). Translating these formulae
# in the test-suite ensure that they don't take too much time (the
# buildfarm will timeout if it does).
. ./defs . ./defs
set -e set -e
# GNU systems have seq, # GNU systems have seq,
# BSD systems have jot. # BSD systems have jot.
# Neither of those are POSIX...
if test "*`(seq 1 1 2>/dev/null)`" = "1"; then if test "*`(seq 1 1 2>/dev/null)`" = "1"; then
have_seq=true have_seq=true
else else
@ -89,8 +81,10 @@ echo "s$x,s$w,,;"
run 0 ../ltl2tgba -KC -X johnson-fig1.tgba > out run 0 ../ltl2tgba -KC -X johnson-fig1.tgba > out
test `wc -l < out` -eq 10 test `wc -l < out` -eq 10
run 0 ../ltl2tgba -KW '(Ga -> Gb) W c' > out run 0 ../ltl2tgba -KW '(Ga -> Gb) W c' > out
test `grep 'is weak' out | wc -l` -eq 4 test `grep 'is weak' out | wc -l` -eq 4
test `grep 'is not weak' out | wc -l` -eq 1 test `grep 'is not weak' out | wc -l` -eq 1
run 0 ../ltl2tgba -l -KW 'F(Fa R (Gb & !a))' > out
test `grep 'is weak' out | wc -l` -eq 7
test `grep 'is not weak' out | wc -l` -eq 1