tests: divide the run time of parse.test by 20
* tests/core/readltl.cc: Process many formulas from a file instead of one arg at a time. * tests/core/parse.test, tests/core/parseerr.test, tests/core/utf8.test: Adjust to supply a file as input.
This commit is contained in:
Alexandre Duret-Lutz
parent
ad51525608
commit
7e5b336f16
4 changed files with 160 additions and 170 deletions
|
|
@ -28,82 +28,72 @@
|
|||
|
||||
. ./defs || exit 1
|
||||
|
||||
for f in \
|
||||
'0' \
|
||||
'1' \
|
||||
'true' \
|
||||
'false' \
|
||||
'a' \
|
||||
'p11011' \
|
||||
'(p11011)' \
|
||||
'a & b' \
|
||||
'a * _b12' \
|
||||
'a && .b.' \
|
||||
'a + b' \
|
||||
'a3214 | b' \
|
||||
'a /\ b' \
|
||||
'a || b' \
|
||||
'a \/ b' \
|
||||
'a | b' \
|
||||
'_a_ U b' \
|
||||
'a R b' \
|
||||
'a <=> b' \
|
||||
'a <-> b' \
|
||||
'a ^ b' \
|
||||
'a xor b' \
|
||||
'a => b' \
|
||||
'a -> b' \
|
||||
'F b' \
|
||||
'Gb' \
|
||||
'G(b)' \
|
||||
'!G(!b)' \
|
||||
'!b' \
|
||||
'[]b' \
|
||||
'<>b' \
|
||||
'X b' \
|
||||
'()b' \
|
||||
'X"X"' \
|
||||
'X"F"' \
|
||||
'X"G"' \
|
||||
'X"U"' \
|
||||
'X"W"' \
|
||||
'X"R"' \
|
||||
'X"M"' \
|
||||
'long_atomic_proposition_1 U long_atomic_proposition_2' \
|
||||
' ab & ac | ad ^ af' \
|
||||
'((b & a) + a) & d' \
|
||||
'(ab & ac | ad ) <=> af ' \
|
||||
'a U b U c U d U e U f U g U h U i U j U k U l U m' \
|
||||
'(ab & !Xad + ad U ab) & FG p12 /\ GF p13' \
|
||||
'((([]<>()p12)) )' \
|
||||
'a R ome V anille' \
|
||||
'p=0Uq=1' \
|
||||
'((p=1Rq=1)+p=0)UXq=0' \
|
||||
'((p=1Rq=1)*p=0)UXq=0' \
|
||||
'(Gq=1*Fp=0)UXq=0' \
|
||||
'((p=1Mq=1)Wx+p=0)RXq=0' \
|
||||
'((p=1Vq=1)Rx+p=0)WXq=0' \
|
||||
'((X(p2=0))U(X(p2=0)))+((Xp1=0)UFALSE)'
|
||||
set -e
|
||||
|
||||
do
|
||||
if ../ltl2text "$f"; then
|
||||
:
|
||||
else
|
||||
echo "ltl2text failed to parse '$f'"
|
||||
exit 1
|
||||
fi
|
||||
cat >input <<EOF
|
||||
0
|
||||
1
|
||||
true
|
||||
false
|
||||
a
|
||||
p11011
|
||||
(p11011)
|
||||
a & b
|
||||
a * _b12
|
||||
a && .b.
|
||||
a + b
|
||||
a3214 | b
|
||||
a /\ b
|
||||
a || b
|
||||
a \/ b
|
||||
a | b
|
||||
_a_ U b
|
||||
a R b
|
||||
a <=> b
|
||||
a <-> b
|
||||
a ^ b
|
||||
a xor b
|
||||
a => b
|
||||
a -> b
|
||||
F b
|
||||
Gb
|
||||
G(b)
|
||||
!G(!b)
|
||||
!b
|
||||
[]b
|
||||
<>b
|
||||
X b
|
||||
()b
|
||||
X"X"
|
||||
X"F"
|
||||
X"G"
|
||||
X"U"
|
||||
X"W"
|
||||
X"R"
|
||||
X"M"
|
||||
long_atomic_proposition_1 U long_atomic_proposition_2
|
||||
ab & ac | ad ^ af
|
||||
((b & a) + a) & d
|
||||
(ab & ac | ad ) <=> af
|
||||
a U b U c U d U e U f U g U h U i U j U k U l U m
|
||||
(ab & !Xad + ad U ab) & FG p12 /\ GF p13
|
||||
((([]<>()p12)) )
|
||||
a R ome V anille
|
||||
p=0Uq=1
|
||||
((p=1Rq=1)+p=0)UXq=0
|
||||
((p=1Rq=1)*p=0)UXq=0
|
||||
(Gq=1*Fp=0)UXq=0
|
||||
((p=1Mq=1)Wx+p=0)RXq=0
|
||||
((p=1Vq=1)Rx+p=0)WXq=0
|
||||
((X(p2=0))U(X(p2=0)))+((Xp1=0)UFALSE)
|
||||
EOF
|
||||
|
||||
if test -n "$DOT"; then
|
||||
run 0 ../ltl2dot "$f" > parse.dot
|
||||
if $DOT -o /dev/null parse.dot; then
|
||||
rm -f parse.dot
|
||||
else
|
||||
rm -f parse.dot
|
||||
echo "dot failed to parse ltl2dot output for '$f'"
|
||||
exit 1
|
||||
fi
|
||||
fi
|
||||
done
|
||||
run 0 ../ltl2text input
|
||||
|
||||
if test -n "$DOT"; then
|
||||
run 0 ../ltl2dot "input" > parse.dot
|
||||
$DOT -o /dev/null parse.dot
|
||||
fi
|
||||
|
||||
# Make sure running the parser in debug mode does not crash
|
||||
run 0 ../ikwiad -d 'a U b'
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2009, 2010, 2011, 2013, 2014, 2015 Laboratoire de
|
||||
# Recherche et Développement de l'Epita (LRDE).
|
||||
# Copyright (C) 2009, 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire
|
||||
# de Recherche et Développement de l'Epita (LRDE).
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
|
|
@ -28,42 +28,54 @@
|
|||
. ./defs || exit 1
|
||||
set -e
|
||||
|
||||
check()
|
||||
{
|
||||
set +x; run 1 ../ltl2text "$1" >stdout 2>stderr; set -x
|
||||
if test -n "$2"; then
|
||||
echo "$2" >expect
|
||||
else
|
||||
: >expect
|
||||
fi
|
||||
if cmp stdout expect; then
|
||||
:
|
||||
else
|
||||
echo "'$1' parsed as"
|
||||
cat stdout
|
||||
echo "instead of"
|
||||
cat expect
|
||||
exit 1
|
||||
fi
|
||||
cat >input <<EOF
|
||||
|
||||
if test -n "$3"; then
|
||||
echo "$3" >expect
|
||||
if cmp stderr expect; then
|
||||
:
|
||||
else
|
||||
echo "==== Error output was ===="
|
||||
cat stderr
|
||||
echo "==== instead of ===="
|
||||
cat expect
|
||||
exit 1
|
||||
fi
|
||||
fi
|
||||
}
|
||||
+
|
||||
/2/3/4/5 a + b /6/7/8/
|
||||
a - b
|
||||
{a[*9999999999]}
|
||||
EOF
|
||||
|
||||
# Empty or unparsable strings
|
||||
check '' ''
|
||||
check '+' ''
|
||||
check '/2/3/4/5 a + b /6/7/8/' ''
|
||||
run 1 ../ltl2text input >output
|
||||
|
||||
sed 's/$$//' >expected<<\EOF
|
||||
>>> $
|
||||
^
|
||||
empty input
|
||||
|
||||
>>> +
|
||||
^
|
||||
syntax error, unexpected or operator
|
||||
|
||||
>>> +
|
||||
^
|
||||
ignoring trailing garbage
|
||||
|
||||
>>> /2/3/4/5 a + b /6/7/8/
|
||||
^
|
||||
syntax error, unexpected $undefined
|
||||
|
||||
>>> /2/3/4/5 a + b /6/7/8/
|
||||
^^^^^^^^^^^^^^^^^^^^^^
|
||||
ignoring trailing garbage
|
||||
|
||||
>>> a - b
|
||||
^
|
||||
syntax error, unexpected $undefined
|
||||
|
||||
>>> a - b
|
||||
^^^
|
||||
ignoring trailing garbage
|
||||
|
||||
ap(@3 #0 "a")
|
||||
>>> {a[*9999999999]}
|
||||
^^^^^^^^^^
|
||||
value too large ignored
|
||||
|
||||
Closure(@6 #0 [Star(@5 #0 0.. [ap(@4 #0 "a")])])
|
||||
EOF
|
||||
|
||||
diff output expected
|
||||
|
||||
|
||||
cat >recover.txt <<EOF
|
||||
|
|
@ -95,18 +107,3 @@ a & (, a & 0
|
|||
{a[->..0];b}, {a[->0..1];b}
|
||||
EOF
|
||||
run 0 ../equals -E recover.txt
|
||||
|
||||
check 'a - b' 'ap(@3 #0 "a")' '>>> a - b
|
||||
^
|
||||
syntax error, unexpected $undefined
|
||||
|
||||
>>> a - b
|
||||
^^^
|
||||
ignoring trailing garbage
|
||||
'
|
||||
|
||||
check '{a[*9999999999]}' 'Closure(@5 #0 [Star(@4 #0 0.. [ap(@3 #0 "a")])])' \
|
||||
'>>> {a[*9999999999]}
|
||||
^^^^^^^^^^
|
||||
value too large ignored
|
||||
'
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@
|
|||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include <iostream>
|
||||
#include <fstream>
|
||||
#include <cassert>
|
||||
#include <cstdlib>
|
||||
#include <cstring>
|
||||
|
|
@ -30,7 +31,7 @@
|
|||
static void
|
||||
syntax(char* prog)
|
||||
{
|
||||
std::cerr << prog << " [-d] formula" << std::endl;
|
||||
std::cerr << prog << " [-d] filename\n";
|
||||
exit(2);
|
||||
}
|
||||
|
||||
|
|
@ -43,40 +44,52 @@ main(int argc, char** argv)
|
|||
syntax(argv[0]);
|
||||
|
||||
bool debug = false;
|
||||
int formula_index = 1;
|
||||
int filename_index = 1;
|
||||
|
||||
if (!strcmp(argv[1], "-d"))
|
||||
{
|
||||
debug = true;
|
||||
if (argc < 3)
|
||||
syntax(argv[0]);
|
||||
formula_index = 2;
|
||||
filename_index = 2;
|
||||
}
|
||||
|
||||
{
|
||||
spot::environment& env(spot::default_environment::instance());
|
||||
|
||||
auto f = [&]()
|
||||
std::ifstream fin(argv[filename_index]);
|
||||
if (!fin)
|
||||
{
|
||||
auto pf = spot::parse_infix_psl(argv[formula_index], env, debug);
|
||||
exit_code = pf.format_errors(std::cerr);
|
||||
return pf.f;
|
||||
}();
|
||||
std::cerr << "Cannot open " << argv[filename_index] << '\n';
|
||||
exit(2);
|
||||
}
|
||||
|
||||
if (f)
|
||||
std::string input;
|
||||
while (std::getline(fin, input))
|
||||
{
|
||||
{
|
||||
spot::environment& env(spot::default_environment::instance());
|
||||
|
||||
auto f = [&]()
|
||||
{
|
||||
auto pf = spot::parse_infix_psl(input, env, debug);
|
||||
// We want the errors on std::cout for the test suite.
|
||||
exit_code = pf.format_errors(std::cout);
|
||||
return pf.f;
|
||||
}();
|
||||
|
||||
if (f)
|
||||
{
|
||||
#ifdef DOTTY
|
||||
spot::print_dot_psl(std::cout, f);
|
||||
spot::print_dot_psl(std::cout, f);
|
||||
#else
|
||||
f.dump(std::cout) << std::endl;
|
||||
f.dump(std::cout) << '\n';
|
||||
#endif
|
||||
}
|
||||
else
|
||||
{
|
||||
exit_code = 1;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
exit_code = 1;
|
||||
}
|
||||
|
||||
}
|
||||
assert(spot::fnode::instances_check());
|
||||
}
|
||||
assert(spot::fnode::instances_check());
|
||||
}
|
||||
return exit_code;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2012, 2013, 2015 Laboratoire de Recherche et
|
||||
# Copyright (C) 2012, 2013, 2015, 2016 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -24,22 +24,18 @@
|
|||
. ./defs || exit 1
|
||||
set -e
|
||||
|
||||
# ----
|
||||
run 0 ../ltl2text '□◯a' >out
|
||||
echo 'G(@5 #0 [X(@4 #0 [ap(@3 #0 "a")])])' > exp
|
||||
cmp out exp
|
||||
cat >input <<EOF
|
||||
□◯a
|
||||
□◯"αβγ"
|
||||
□)◯a
|
||||
"αβγ"X
|
||||
EOF
|
||||
|
||||
# ----
|
||||
run 0 ../ltl2text '□◯"αβγ"' >out
|
||||
echo 'G(@5 #0 [X(@4 #0 [ap(@3 #0 "αβγ")])])' > exp
|
||||
cmp out exp
|
||||
run 1 ../ltl2text input >output
|
||||
|
||||
|
||||
# ----
|
||||
set +x
|
||||
run 1 ../ltl2text '□)◯a' 2>err
|
||||
set -x
|
||||
cat >exp <<EOF
|
||||
cat >expected <<EOF
|
||||
G(@5 #0 [X(@4 #0 [ap(@3 #0 "a")])])
|
||||
G(@8 #0 [X(@7 #0 [ap(@6 #0 "αβγ")])])
|
||||
>>> □)◯a
|
||||
^
|
||||
syntax error, unexpected closing parenthesis
|
||||
|
|
@ -52,14 +48,7 @@ missing right operand for "always operator"
|
|||
^^^
|
||||
ignoring trailing garbage
|
||||
|
||||
EOF
|
||||
cmp exp err
|
||||
|
||||
# ----
|
||||
set +x
|
||||
run 1 ../ltl2text '"αβγ"X' 2>err
|
||||
set -x
|
||||
cat >exp <<EOF
|
||||
ff(@0 #0)
|
||||
>>> "αβγ"X
|
||||
^
|
||||
syntax error, unexpected next operator
|
||||
|
|
@ -68,9 +57,10 @@ syntax error, unexpected next operator
|
|||
^
|
||||
ignoring trailing garbage
|
||||
|
||||
ap(@9 #0 "αβγ")
|
||||
EOF
|
||||
cmp exp err
|
||||
|
||||
diff expected output
|
||||
|
||||
randltl --psl -8 --seed 0 --tree-size 16 a b c -n 100 > formulae
|
||||
../reduc -f -h 0 formulae
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue