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

Test previous patch.

Browse source 
* iface/dve2/finite.test: Add test case.
* NEWS: Mention the fix.
This commit is contained in:
Alexandre Duret-Lutz 2013-01-14 18:26:04 +01:00
parent 67b7b86d52
commit 361f594655
2 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
NEWS
View file

@ -9,6 +9,8 @@ New in spot 1.0a (not released):
- "P0.init" is parsed as an atomic even without the double quotes, - "P0.init" is parsed as an atomic even without the double quotes,
but it was always output with double quotes. This version will but it was always output with double quotes. This version will
not quote this atomic proposition anymore. not quote this atomic proposition anymore.
- tgba_product::transition_annotation() would segfault when
called in a product against a Kripke structure.
* Minor improvements: * Minor improvements:
- Four new LTL simplifications rules: - Four new LTL simplifications rules:
GF(a|Xb) = GF(a|b) GF(a|Xb) = GF(a|b)

6
iface/dve2/finite.test
View file

@ -1,5 +1,5 @@
#!/bin/sh #!/bin/sh
# Copyright (C) 2011 Laboratoire de Recherche et Développement # Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -51,3 +51,7 @@ run 0 ../dve2check -ddead -E $srcdir/finite.dve \
run 0 ../dve2check -ddead -e $srcdir/finite.dve \ run 0 ../dve2check -ddead -e $srcdir/finite.dve \
'!(G(dead -> ("P.a==2" | "P.b==3")))' '!(G(dead -> ("P.a==2" | "P.b==3")))'
# This used to segfault because of a bug in
# tgba_product::transition_annotation.
run 0 ../dve2check -gp $srcdir/finite.dve true