diff --git a/src/tgbaalgos/cycles.cc b/src/tgbaalgos/cycles.cc index 907e3e636..351103815 100644 --- a/src/tgbaalgos/cycles.cc +++ b/src/tgbaalgos/cycles.cc @@ -71,7 +71,7 @@ namespace spot { std::pair p = tags_.insert(std::make_pair(s, state_info())); - if (p.second) + if (!p.second) s->destroy(); return p.first; } diff --git a/src/tgbatest/cycles.test b/src/tgbatest/cycles.test index 8a51cc031..5c479bca8 100755 --- a/src/tgbatest/cycles.test +++ b/src/tgbatest/cycles.test @@ -19,20 +19,12 @@ # Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA # 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 - set -e # GNU systems have seq, # BSD systems have jot. +# Neither of those are POSIX... if test "*`(seq 1 1 2>/dev/null)`" = "1"; then have_seq=true else @@ -89,8 +81,10 @@ echo "s$x,s$w,,;" run 0 ../ltl2tgba -KC -X johnson-fig1.tgba > out test `wc -l < out` -eq 10 - - run 0 ../ltl2tgba -KW '(Ga -> Gb) W c' > out test `grep 'is weak' out | wc -l` -eq 4 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