diff --git a/NEWS b/NEWS index 47bc514b9..198f803c2 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,15 @@ New in spot 2.0.2a (Not yet released) Nothing yet. + Bug fixes: + + * The degen-lcache=1 option of the degeneralization algorithm (which + is a default option) did not behave exactly as documented: instead + of reusing the first level ever created for a state where the + choice of the level is free, it used the last level used. This + caused some posterior simulation-based reductions to be less + efficient at reducing automata (on the average). + New in spot 2.0.2 (2016-06-17) Documentation: diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index b73f2afc1..73663ed32 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -519,6 +519,8 @@ namespace spot lvl = std::max(lvl_cache[d.first].first, lvl); else if (use_lvl_cache == 2) lvl = std::min(lvl_cache[d.first].first, lvl); + else + lvl = lvl_cache[d.first].first; // Do not change } lvl_cache[d.first] = std::make_pair(lvl, true); } diff --git a/tests/core/degendet.test b/tests/core/degendet.test index 89c1dfa32..c335ced42 100755 --- a/tests/core/degendet.test +++ b/tests/core/degendet.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2011, 2015 Laboratoire de Recherche et Développement +# Copyright (C) 2011, 2015, 2016 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -23,7 +23,7 @@ set -e -# The following command, reported by Tomáš Babiak, used to output many +# The following command, reported by Tomáš Babiak, used to output many # different automata, because state addresses were used to order the # successors in the degeneralization. @@ -36,3 +36,10 @@ for i in 2 3 4 5; do ../ikwiad -r7 -x -R3 -N "XF(Gp2 | F(p0 U (p1 & (! p4 | p3))))" > out cmp out out1 || exit 1 done + +# The next formula used to be translated into a 6-state automaton +# instead of a 4-state automaton, because of an error in the +# implementation of the degen-lcache=1 option causing the last level +# used to be reused, instead of the first one. +run 0 ltl2tgba -B -f '(b & Fa) U XXG(a M Gb)' --stats=%s,%t >out +test "4,14" = "`cat out`" diff --git a/tests/core/ltl2ta.test b/tests/core/ltl2ta.test index e95e92513..ec5298a8c 100755 --- a/tests/core/ltl2ta.test +++ b/tests/core/ltl2ta.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de -# Recherche et Développement de l'Epita (LRDE). +# Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire +# de Recherche et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -170,12 +170,12 @@ in: Fa & b & GFc & Gd -TA -DS -RT | 12 | 126 | 5 -TA -DS -lv | 29 | 315 | 13 -TA -DS -lv -RT | 13 | 140 | 4 --TA -DS -sp | 28 | 309 | 12 --TA -DS -sp -RT | 12 | 137 | 3 +-TA -DS -sp | 28 | 306 | 12 +-TA -DS -sp -RT | 12 | 134 | 3 -TA -DS -lv -sp | 29 | 315 | 13 -TA -DS -lv -sp -RT | 13 | 140 | 4 --x -TA -DS -in | 29 | 254 | 9 --x -TA -DS -in -RT | 12 | 96 | 3 +-x -TA -DS -in | 29 | 240 | 9 +-x -TA -DS -in -RT | 12 | 93 | 3 in: Fa & a & GFc & Gc -TGTA | 4 | 8 | XXX -TGTA -RT | 3 | 6 | XXX @@ -401,15 +401,15 @@ in: FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4) -TA -lv -sp | 45 | 676 | 9 -TA -lv -sp -RT | 35 | 566 | 4 -TA -DS | 54 | 722 | 26 --TA -DS -RT | 42 | 600 | 19 +-TA -DS -RT | 42 | 608 | 18 -TA -DS -lv | 55 | 800 | 19 --TA -DS -lv -RT | 44 | 694 | 13 --TA -DS -sp | 54 | 795 | 18 --TA -DS -sp -RT | 43 | 683 | 12 +-TA -DS -lv -RT | 44 | 702 | 13 +-TA -DS -sp | 54 | 789 | 18 +-TA -DS -sp -RT | 43 | 686 | 12 -TA -DS -lv -sp | 55 | 800 | 19 --TA -DS -lv -sp -RT | 44 | 694 | 13 --x -TA -DS -in | 55 | 700 | 11 --x -TA -DS -in -RT | 39 | 566 | 8 +-TA -DS -lv -sp -RT | 44 | 702 | 13 +-x -TA -DS -in | 55 | 694 | 11 +-x -TA -DS -in -RT | 41 | 597 | 8 in: G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2)) -TGTA | 69 | 1539 | XXX -TGTA -RT | 49 | 935 | XXX @@ -422,15 +422,15 @@ in: G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2)) -TA -lv -sp | 68 | 1443 | 16 -TA -lv -sp -RT | 56 | 1179 | 15 -TA -DS | 124 | 2964 | 44 --TA -DS -RT | 100 | 2285 | 42 +-TA -DS -RT | 96 | 2099 | 42 -TA -DS -lv | 125 | 3028 | 42 --TA -DS -lv -RT | 101 | 2339 | 40 +-TA -DS -lv -RT | 97 | 2149 | 40 -TA -DS -sp | 124 | 3012 | 41 --TA -DS -sp -RT | 100 | 2324 | 39 +-TA -DS -sp -RT | 96 | 2134 | 39 -TA -DS -lv -sp | 125 | 3028 | 42 --TA -DS -lv -sp -RT | 101 | 2339 | 40 +-TA -DS -lv -sp -RT | 97 | 2149 | 40 -x -TA -DS -in | 125 | 1838 | 25 --x -TA -DS -in -RT | 89 | 1344 | 25 +-x -TA -DS -in -RT | 87 | 1296 | 25 EOF sed -n 's/in: \(.*\)/\1/p' checkta.txt > input.txt