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

add test-case for bdd_noderesize

Browse source 
* tests/core/ltl2tgba.test: Add new test-case,
reported by Tomáš Babiak.
* NEWS: Mention the bug fixed by previous patch.
This commit is contained in:
Alexandre Duret-Lutz 2016-11-19 14:49:46 +01:00
parent 38c4fc8812
commit 4e1c8dfd74
2 changed files with 9 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -1,6 +1,8 @@
New in spot 2.2.0.dev (not yet released) New in spot 2.2.0.dev (not yet released)
Nothing yet. Bugs:
* The bdd_noderesize() function, as modified in 2.2, would crash.
New in spot 2.2 (2016-11-14) New in spot 2.2 (2016-11-14)

6
tests/core/ltl2tgba.test
View file

@ -224,3 +224,9 @@ grep 'ltl2tgba: unknown option.*@' stderr
# Make sure the count of AP is correct through never claims or LBTT # Make sure the count of AP is correct through never claims or LBTT
ltl2tgba -f a -s | autfilt -q --ap=1 --lbtt | autfilt -q --ap=1 ltl2tgba -f a -s | autfilt -q --ap=1 --lbtt | autfilt -q --ap=1
# Such a large formula will fill the BuDDy unicity table and trigger a
# resize. At the time this test is introduced, this is the only place
# of the test-suite where this resize is triggered, so do not remove
# it unless you can find another place that triggers that.
genltl --go-theta=18 | ltl2tgba --low --any -q