diff --git a/tests/core/parse.test b/tests/core/parse.test index 2a17a0582..233d25d0f 100755 --- a/tests/core/parse.test +++ b/tests/core/parse.test @@ -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 < 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' diff --git a/tests/core/parseerr.test b/tests/core/parseerr.test index 2c138a2bb..e58a501e1 100755 --- a/tests/core/parseerr.test +++ b/tests/core/parseerr.test @@ -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 <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 <..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 -' diff --git a/tests/core/readltl.cc b/tests/core/readltl.cc index 9e3140c38..747c68fe6 100644 --- a/tests/core/readltl.cc +++ b/tests/core/readltl.cc @@ -21,6 +21,7 @@ // along with this program. If not, see . #include +#include #include #include #include @@ -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; } diff --git a/tests/core/utf8.test b/tests/core/utf8.test index aae837b3d..729d0872c 100755 --- a/tests/core/utf8.test +++ b/tests/core/utf8.test @@ -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 <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 <expected <>> □)◯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 <>> "αβγ"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