degen: fix handling of degen-lcache=1
* spot/twaalgos/degen.cc: Here. * tests/core/degendet.test: Add test case. * tests/core/ltl2ta.test: Adjust expected output. * NEWS: Mention the issue.
This commit is contained in:
Alexandre Duret-Lutz
parent
a78f5feecf
commit
a4c7016f52
4 changed files with 38 additions and 20 deletions
9
NEWS
9
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:
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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`"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue