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

Don't compare memory consumption between 2 runs of dve2check

Browse source 
* iface/dve2/dve2check.test: Here.
This commit is contained in:
Alexandre Duret-Lutz 2012-04-27 20:31:40 +02:00
parent 8aa653e010
commit 03aca91648
1 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

7
iface/dve2/dve2check.test
View file

@ -1,5 +1,5 @@
#!/bin/sh #!/bin/sh
# Copyright (C) 2011 Laboratoire de Recherche et Développement # Copyright (C) 2011, 2012 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.
@ -33,7 +33,6 @@ fi
set -e set -e
for opt in '' '-z'; do for opt in '' '-z'; do
# The three examples from the README. # The three examples from the README.
# (Don't run the first one using "run 0" because it would take too much # (Don't run the first one using "run 0" because it would take too much
@ -42,10 +41,10 @@ for opt in '' '-z'; do
../dve2check $opt -E $srcdir/beem-peterson.4.dve \ ../dve2check $opt -E $srcdir/beem-peterson.4.dve \
'!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve \ run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve \
'!G(P_0.wait -> F P_0.CS)' > stdout1 '!G(P_0.wait -> F P_0.CS)' | grep -v pages > stdout1
# same formula, different syntax. # same formula, different syntax.
run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve \ run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve \
'!G("P_0 == wait" -> F "P_0 == CS")' > stdout2 '!G("P_0 == wait" -> F "P_0 == CS")' | grep -v pages > stdout2
cmp stdout1 stdout2 cmp stdout1 stdout2
run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")'
done done