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

eltl2tgba: slight cleanup of the tests.

Browse source 
* src/eltltest/acc.test, src/tgbatest/eltl2tgba.test: Simplify use of
here documents, and also test for ltl2tgba's -lo option with valgrind.
This commit is contained in:
Alexandre Duret-Lutz 2013-01-17 11:30:16 +01:00
parent d580cce685
commit dcd4644d42
2 changed files with 48 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/eltltest/acc.test
View file

@ -1,5 +1,6 @@
#!/bin/sh
# Copyright (C) 2009 Laboratoire de Recherche et Développement
# -*- coding: utf-8 -*-
# Copyright (C) 2009, 2013 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -20,18 +21,18 @@
. ./defs || exit 1
set -e
cat >prelude <<EOF
cat >prelude <<'EOF'
X=(
0 1 \$0
0 1 $0
accept 1
)
EOF
cat >input <<EOF
cat >input <<'EOF'
include prelude
A=(
0 1 \$2
1 2 \$0
0 1 $2
1 2 $0
accept 0
)
%
@ -39,11 +40,11 @@ A(1,a,a|b)&X(!f)
EOF
run 0 ../acc input || exit 1
cat >input <<EOF
cat >input <<'EOF'
include prelude
A=(
0 1 \$2
1 2 \$0
0 1 $2
1 2 $0
accept 0
)
%
@ -51,28 +52,28 @@ A(1,a)
EOF
run 1 ../acc input || exit 1
cat >input <<EOF
cat >input <<'EOF'
X=(
0 1 true
1 2 \$0
1 2 $0
accept 2
)
U=(
0 0 \$0
0 1 \$1
0 0 $0
0 1 $1
accept 1
)
F=U(true, \$0)
R=!U(!\$0, !\$1)
F=U(true, $0)
R=!U(!$0, !$1)
%
a U b | a R b | F(true) | U(a,b) -> R(a,b)
EOF
run 0 ../acc input || exit 1
cat >input <<EOF
cat >input <<'EOF'
U=(
0 0 \$0
0 1 \$1
0 0 $0
0 1 $1
accept 1
)
T=U(true,true)

52
src/tgbatest/eltl2tgba.test
View file

@ -1,6 +1,7 @@
#!/bin/sh
# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# -*- coding: utf-8 -*-
# Copyright (C) 2009, 2010, 2013 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@ -38,24 +39,29 @@ check_false()
run 1 ../ltl2tgba -CR -e -Poutput -f "$1"
}
for f in 'GFa' 'FGb' 'GFa->GFb'; do
run 0 ../ltl2tgba -lo -b "$f" > output
check_false "!($f)"
done
# Create the prelude file.
cat >input1 <<EOF
cat >input1 <<'EOF'
X=(
0 1 true
1 2 \$0
1 2 $0
accept 2
)
U=(
0 0 \$0
0 1 \$1
0 0 $0
0 1 $1
accept 1
)
G=(
0 0 \$0
0 0 $0
)
F=U(true, \$0)
Strong=G(F(\$0))->G(F(\$1))
R=!U(!\$0, !\$1)
F=U(true, $0)
Strong=G(F($0))->G(F($1))
R=!U(!$0, !$1)
EOF
cat >input <<EOF
@ -152,10 +158,10 @@ check_construct input
check_true 'a R b'
check_false '!(a R b)'
cat >input <<EOF
cat >input <<'EOF'
T=(
0 1 true
1 0 \$0
1 0 $0
)
%
T(f)
@ -163,14 +169,14 @@ EOF
check_construct input
cat >input <<EOF
cat >input <<'EOF'
include input1
Fusion=
(
0 1 \$0 & !finish(\$0)
1 1 !finish(\$0)
1 2 \$1 & finish(\$0)
0 2 \$0 & \$1 & finish(\$0)
0 1 $0 & !finish($0)
1 1 !finish($0)
1 2 $1 & finish($0)
0 2 $0 & $1 & finish($0)
accept 2
)
%
@ -179,14 +185,14 @@ EOF
check_construct input
cat >input <<EOF
cat >input <<'EOF'
Concat=
(
0 1 \$0 & !finish(\$0)
1 1 !finish(\$0)
1 2 finish(\$0)
0 2 \$0 & finish(\$0)
2 3 \$1
0 1 $0 & !finish($0)
1 1 !finish($0)
1 2 finish($0)
0 2 $0 & finish($0)
2 3 $1
accept 3
)
%