diff --git a/tests/core/bdd.test b/tests/core/bdd.test index 82c1bd912..0b17fb586 100755 --- a/tests/core/bdd.test +++ b/tests/core/bdd.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -23,7 +23,14 @@ set -e # Make sure that setting the SPOT_BDD_TRACE envvar actually does # something. -SPOT_BDD_TRACE=1 ltl2tgba a >out 2>err +genltl --kr-nlogn=2 | SPOT_BDD_TRACE=1 ltl2tgba -D >out 2>err +cat err grep spot: out && exit 1 grep 'spot: BDD package initialized' err -grep 'spot: BDD stats:' err +# This value below, which is the number of time we need to garbage +# collect might change if we improve the tool or change the way BuDDy +# is initialized. +test 63 = `grep -c 'spot: BDD GC' err` +# Minimal size for this automaton. +# See also https://www.lrde.epita.fr/dload/spot/mochart10-fixes.pdf +test "147,207" = `autfilt --stats=%s,%e out`