modelcheck: update tests
* tests/ltsmin/check.test, tests/ltsmin/check2.test, tests/ltsmin/check3.test, tests/ltsmin/finite2.test, tests/ltsmin/finite3.test: here.
This commit is contained in:
Etienne Renault
parent
0b917af762
commit
80746e4332
5 changed files with 58 additions and 43 deletions
|
|
@ -23,6 +23,21 @@
|
|||
|
||||
divine compile > output 2>&1
|
||||
|
||||
set -e
|
||||
|
||||
if ! test -x "`command -v spins`"; then
|
||||
echo "spins not installed."
|
||||
else
|
||||
# Promela
|
||||
for opt in '' '--compress 1'; do
|
||||
|
||||
run 0 ../modelcheck --is-empty $opt --model $srcdir/elevator2.1.pm \
|
||||
--formula '!G("req[1]==1" -> (F("p==1" && "cabin_0._pc==2")))'
|
||||
run 1 ../modelcheck --is-empty $opt --model $srcdir/elevator2.1.pm \
|
||||
--formula 'F("p==2")'
|
||||
done
|
||||
fi
|
||||
|
||||
if grep -i -- --ltsmin output; then
|
||||
:
|
||||
else
|
||||
|
|
@ -30,16 +45,6 @@ else
|
|||
exit 77
|
||||
fi
|
||||
|
||||
set -e
|
||||
|
||||
# Promela
|
||||
for opt in '' '--compress 1'; do
|
||||
|
||||
run 0 ../modelcheck --is-emtpy $opt --model $srcdir/elevator2.1.pm \
|
||||
--formula '!G("req[1]==1" -> (F("p==1" && "cabin_0._pc==2")))'
|
||||
run 1 ../modelcheck --is-empty $opt --model $srcdir/elevator2.1.pm \
|
||||
--formula 'F("p==2")'
|
||||
done
|
||||
|
||||
# dve2
|
||||
for opt in '' '--compress 1'; do
|
||||
|
|
@ -69,6 +74,6 @@ grep 'Cannot open' stderr
|
|||
run 2 ../modelcheck --model beem-peterson.4.dve2C \
|
||||
--formula 'Xfoo | P_0.f & X"P_0.k < 2xx" | G"pos[0]"' 2>stderr
|
||||
cat stderr
|
||||
grep 'Proposition "foo"' stderr
|
||||
grep 'Proposition "P_0.f"' stderr
|
||||
grep 'Proposition "P_0.k<2xx"' stderr
|
||||
grep 'No variable' stderr
|
||||
grep 'No state' stderr
|
||||
grep 'Unexpected' stderr
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche
|
||||
# Copyright (C) 2011, 2012, 2014, 2015, 2016, 2017 Laboratoire de Recherche
|
||||
# et Développement de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -28,10 +28,9 @@ fi
|
|||
|
||||
set -e
|
||||
|
||||
for opt in '' '-z'; do
|
||||
|
||||
run 0 ../modelcheck $opt -E $srcdir/elevator2.1.pm \
|
||||
'!G("req[1]==1" -> (F("p==1" && "cabin_0._pc==2")))'
|
||||
run 0 ../modelcheck $opt -e $srcdir/elevator2.1.pm \
|
||||
'F("p==2")'
|
||||
for opt in '' '--compress 1'; do
|
||||
run 0 ../modelcheck $opt --is-empty --model $srcdir/elevator2.1.pm \
|
||||
--formula '!G("req[1]==1" -> (F("p==1" && "cabin_0._pc==2")))'
|
||||
run 1 ../modelcheck $opt --is-empty --model $srcdir/elevator2.1.pm \
|
||||
--formula 'F("p==2")'
|
||||
done
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2016 Laboratoire de Recherche
|
||||
# Copyright (C) 2016, 2017 Laboratoire de Recherche
|
||||
# et Développement de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -27,12 +27,13 @@ fi
|
|||
|
||||
set -e
|
||||
|
||||
for opt in '' '-z'; do
|
||||
for opt in '' '--compress 1'; do
|
||||
# The three examples from the README.
|
||||
# (Don't run the first one using "run 0" because it would take too much
|
||||
# time with valgrind.).
|
||||
|
||||
run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.gal \
|
||||
'!G("P_0.state==2" -> F "P_0.state==1")'
|
||||
run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.gal '!G("pos[1] < 3")'
|
||||
run 1 ../modelcheck $opt --is-empty --model $srcdir/beem-peterson.4.gal \
|
||||
--formula '!G("P_0.state==2" -> F "P_0.state==1")'
|
||||
run 1 ../modelcheck $opt --is-empty --model $srcdir/beem-peterson.4.gal \
|
||||
--formula '!G("pos[1] < 3")'
|
||||
done
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2011, 2013, 2014, 2016 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
# Copyright (C) 2011, 2013, 2014, 2016, 2017 Laboratoire de Recherche
|
||||
# et Développement de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
#
|
||||
|
|
@ -33,25 +33,30 @@ run 0 ../modelcheck --dot model --model $srcdir/finite.pm \
|
|||
test `grep ' -> ' stdout | wc -l` = 25
|
||||
test `grep 'P_0.a=' stdout | wc -l` = 15
|
||||
|
||||
run 0 ../modelcheck --selfloopize true --dot model --model $srcdir/finite.pm \
|
||||
run 0 ../modelcheck --selfloopize true --dot model \
|
||||
--model $srcdir/finite.pm \
|
||||
--formula '"P_0.a < 10"' > stdout2
|
||||
diff stdout stdout2
|
||||
|
||||
run 0 ../modelcheck --selfloopize dfalse --dot model --model $srcdir/finite.pm \
|
||||
run 0 ../modelcheck --selfloopize false --dot model \
|
||||
--model $srcdir/finite.pm \
|
||||
--formula '"P_0.a < 10"' > stdout
|
||||
test `grep ' -> ' stdout | wc -l` = 19
|
||||
test `grep 'P_0.a=' stdout | wc -l` = 15
|
||||
|
||||
# the same with compressed states
|
||||
run 0 ../modelcheck -compress --selfloopize false --dot model \
|
||||
run 0 ../modelcheck --compress 1 --selfloopize false --dot model \
|
||||
--model $srcdir/finite.pm --formula '"P_0.a < 10"' > stdout
|
||||
test `grep ' -> ' stdout | wc -l` = 19
|
||||
test `grep 'P_0.a=' stdout | wc -l` = 15
|
||||
|
||||
run 0 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.pm \
|
||||
run 0 ../modelcheck --is-empty --selfloopize dead \
|
||||
--model $srcdir/finite.pm \
|
||||
--formula '!(G(dead -> ("P_0.a==3" | "P_0.b==3")))'
|
||||
|
||||
run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.pm \
|
||||
run 1 ../modelcheck --is-empty --selfloopize dead \
|
||||
--model $srcdir/finite.pm \
|
||||
--formula '!(G(dead -> ("P_0.a==2" | "P_0.b==3")))'
|
||||
|
||||
run 0 ../modelcheck --dot product --model $srcdir/finite.pm --formula true
|
||||
run 0 ../modelcheck --dot product --model $srcdir/finite.pm \
|
||||
--formula true
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2011, 2013, 2014, 2016 Laboratoire de Recherche et
|
||||
# Copyright (C) 2011, 2013, 2014, 2016, 2017 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -28,28 +28,33 @@ if ! gal2c $srcdir/finite.gal; then
|
|||
fi
|
||||
|
||||
set -e
|
||||
run 0 ../modelcheck -gm $srcdir/finite.gal '"P.a < 10"' > stdout
|
||||
run 0 ../modelcheck --model $srcdir/finite.gal \
|
||||
--formula '"P.a < 10"' --dot model > stdout
|
||||
test `grep ' -> ' stdout | wc -l` = 25
|
||||
test `grep 'P.a=' stdout | wc -l` = 15
|
||||
|
||||
run 0 ../modelcheck -dtrue -gm $srcdir/finite.gal '"P.a < 10"' > stdout2
|
||||
run 0 ../modelcheck --selfloopize true --model $srcdir/finite.gal \
|
||||
--formula '"P.a < 10"' > stdout2
|
||||
cmp stdout stdout2
|
||||
|
||||
run 0 ../modelcheck -dfalse -gm $srcdir/finite.gal '"P.a < 10"' > stdout
|
||||
run 0 ../modelcheck --selfloopize false --model $srcdir/finite.gal \
|
||||
--formula '"P.a < 10"' --dot model > stdout
|
||||
test `grep ' -> ' stdout | wc -l` = 19
|
||||
test `grep 'P.a=' stdout | wc -l` = 15
|
||||
|
||||
# the same with compressed states
|
||||
run 0 ../modelcheck -z -dfalse -gm $srcdir/finite.gal '"P.a < 10"' > stdout
|
||||
run 0 ../modelcheck --compress 1 --selfloopize false \
|
||||
--model $srcdir/finite.gal \
|
||||
--formula '"P.a < 10"' --dot model > stdout
|
||||
test `grep ' -> ' stdout | wc -l` = 19
|
||||
test `grep 'P.a=' stdout | wc -l` = 15
|
||||
|
||||
run 0 ../modelcheck -ddead -E $srcdir/finite.gal \
|
||||
'!(G(dead -> ("P.a==3" | "P.b==3")))'
|
||||
run 0 ../modelcheck --selfloopize dead --is-empty $srcdir/finite.gal \
|
||||
--formula '!(G(dead -> ("P.a==3" | "P.b==3")))'
|
||||
|
||||
run 0 ../modelcheck -ddead -e $srcdir/finite.gal \
|
||||
'!(G(dead -> ("P.a==2" | "P.b==3")))'
|
||||
run 1 ../modelcheck --selfloopize dead --is-empty $srcdir/finite.gal \
|
||||
--formula '!(G(dead -> ("P.a==2" | "P.b==3")))'
|
||||
|
||||
# This used to segfault because of a bug in a
|
||||
# function that do not exist anymore.
|
||||
run 0 ../modelcheck -gp $srcdir/finite.gal true
|
||||
run 0 ../modelcheck --dot product $srcdir/finite.gal --formula 'true'
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue