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

tests: git rid of all the tool=tool assignents

Browse source 
Our use of
  ltl2tgba=ltl2tgba
  autfilt=autfilt
  ...
all over the test cases comes from the time where those tools were not
in PATH and we actually had something like
  ltl2tgba=../../bin/ltl2tgba
  autfilt=../../bin/autfilt

But today that is useless, and we prefer to write ltl2tgba rather than
$ltl2tgba, so let's remove this old cruft.

* tests/core/basimul.test, tests/core/det.test, tests/core/lbt.test,
tests/core/lenient.test, tests/core/ltl2dstar.test,
tests/core/ltl2dstar2.test, tests/core/ltl2dstar3.test,
tests/core/ltl2dstar4.test, tests/core/ltlcross2.test,
tests/core/ltlcross3.test, tests/core/ltlcross4.test,
tests/core/ltlcrossce2.test, tests/core/ltldo.test,
tests/core/ltlfilt.test, tests/core/optba.test,
tests/core/prodor.test, tests/core/rand.test,
tests/core/randomize.test, tests/core/remfin.test,
tests/core/satmin.test, tests/core/sbacc.test,
tests/core/strength.test, tests/core/stutter-ltl.test,
tests/core/stutter-tgba.test, tests/core/unabbrevwm.test,
tests/core/unambig.test: Get rid of all tool=tool assignments.
This commit is contained in:
Alexandre Duret-Lutz 2017-11-24 16:44:26 +01:00
parent a31ba7ff80
commit a9a375ccd8
26 changed files with 290 additions and 374 deletions
Download patch file Download diff file Expand all files Collapse all files

31
tests/core/basimul.test
View file

@ -1,7 +1,7 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement de # Copyright (C) 2013, 2014, 2017 Laboratoire de Recherche et
# l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -22,9 +22,6 @@
set -e set -e
ltl2tgba=ltl2tgba
# This bug was found while working on the state-based acceptance # This bug was found while working on the state-based acceptance
# output for the LBTT format. Using ba-simul=2 causes reverse # output for the LBTT format. Using ba-simul=2 causes reverse
# simulation to be applied to the BA automaton obtained after # simulation to be applied to the BA automaton obtained after
@ -60,15 +57,15 @@ ltlcross --seed=0 --products=5 --json=out.json \
-f '!p2 & (Fp5 R (((p0 U p1) & (p5 | p1)) | (!p5 & (!p0 R !p1))))' \ -f '!p2 & (Fp5 R (((p0 U p1) & (p5 | p1)) | (!p5 & (!p0 R !p1))))' \
-f '! ((p0 /\ p4) <-> ! ((! p0 U (p0 W p4)) /\ (X p5 -> ([] p3 /\ p5))))' \ -f '! ((p0 /\ p4) <-> ! ((! p0 U (p0 W p4)) /\ (X p5 -> ([] p3 /\ p5))))' \
-f '(X <> (<> X p0 /\ X (p5 <-> p0)) W (p3 W p0))' \ -f '(X <> (<> X p0 /\ X (p5 <-> p0)) W (p3 W p0))' \
"$ltl2tgba --ba --high --lbtt=t -x ba-simul=0 %f >%T" \ "ltl2tgba --ba --high --lbtt=t -x ba-simul=0 %f >%T" \
"$ltl2tgba --ba --high --lbtt=t -x ba-simul=1 %f >%T" \ "ltl2tgba --ba --high --lbtt=t -x ba-simul=1 %f >%T" \
"$ltl2tgba --ba --high --lbtt=t -x ba-simul=2 %f >%T" \ "ltl2tgba --ba --high --lbtt=t -x ba-simul=2 %f >%T" \
"$ltl2tgba --ba --high --lbtt=t -x ba-simul=3 %f >%T" \ "ltl2tgba --ba --high --lbtt=t -x ba-simul=3 %f >%T" \
"$ltl2tgba --ba --high --lbtt -x ba-simul=0 %f >%T" \ "ltl2tgba --ba --high --lbtt -x ba-simul=0 %f >%T" \
"$ltl2tgba --ba --high --lbtt -x ba-simul=1 %f >%T" \ "ltl2tgba --ba --high --lbtt -x ba-simul=1 %f >%T" \
"$ltl2tgba --ba --high --lbtt -x ba-simul=2 %f >%T" \ "ltl2tgba --ba --high --lbtt -x ba-simul=2 %f >%T" \
"$ltl2tgba --ba --high --lbtt -x ba-simul=3 %f >%T" \ "ltl2tgba --ba --high --lbtt -x ba-simul=3 %f >%T" \
"$ltl2tgba --ba --high --spin -x ba-simul=0 %f >%N" \ "ltl2tgba --ba --high --spin -x ba-simul=0 %f >%N" \
"$ltl2tgba --ba --high --spin -x ba-simul=1 %f >%N" \ "ltl2tgba --ba --high --spin -x ba-simul=1 %f >%N" \
"$ltl2tgba --ba --high --spin -x ba-simul=2 %f >%N" \ "ltl2tgba --ba --high --spin -x ba-simul=2 %f >%N" \
"$ltl2tgba --ba --high --spin -x ba-simul=3 %f >%N" "ltl2tgba --ba --high --spin -x ba-simul=3 %f >%N"

4
tests/core/det.test
View file

@ -21,8 +21,6 @@
. ./defs . ./defs
set -e set -e
ltl2tgba=ltl2tgba
cat >formulas <<'EOF' cat >formulas <<'EOF'
1,13,X((a M F((!b & !c) | (b & c))) W (G!c U b)) 1,13,X((a M F((!b & !c) | (b & c))) W (G!c U b))
1,5,X(((a & b) R (!a U !c)) R b) 1,5,X(((a & b) R (!a U !c)) R b)
@ -56,7 +54,7 @@ cat >formulas <<'EOF'
1,4,G(G!a | F!c | G!b) 1,4,G(G!a | F!c | G!b)
EOF EOF
$ltl2tgba -x tba-det --det --stats '%d,%s,%f' -F formulas/3 > out ltl2tgba -x tba-det --det --stats '%d,%s,%f' -F formulas/3 > out
diff formulas out diff formulas out
cat >in.hoa <<'EOF' cat >in.hoa <<'EOF'

28
tests/core/lbt.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2013, 2016 Laboratoire de Recherche et # Copyright (C) 2013, 2016, 2017 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -21,10 +21,6 @@
. ./defs . ./defs
set -e set -e
ltlfilt=ltlfilt
randltl=randltl
genltl=genltl
# Some example formulas taken from Ruediger Ehlers's dbaminimizer # Some example formulas taken from Ruediger Ehlers's dbaminimizer
# http://react.cs.uni-saarland.de/tools/dbaminimizer # http://react.cs.uni-saarland.de/tools/dbaminimizer
# which are expected to be processed by ltl2dstar. # which are expected to be processed by ltl2dstar.
@ -85,18 +81,18 @@ U p0 & | p0 p5 p1
EOF EOF
# More examples randomly generated # More examples randomly generated
$randltl -l -n 100 a p1 "X" "U" "U12" >> formulas randltl -l -n 100 a p1 "X" "U" "U12" >> formulas
# Some examples from scalables formulas # Some examples from scalables formulas
$genltl --rv-counter=1..10 --go-theta=1..10 -l >> formulas genltl --rv-counter=1..10 --go-theta=1..10 -l >> formulas
count=`wc -l < formulas` count=`wc -l < formulas`
test $count -eq 168 test $count -eq 168
run 0 $ltlfilt --lbt-input formulas > formulas.2 run 0 ltlfilt --lbt-input formulas > formulas.2
run 0 $ltlfilt -l formulas.2 > formulas.3 run 0 ltlfilt -l formulas.2 > formulas.3
run 0 $ltlfilt -l --lbt-input formulas > formulas.4 run 0 ltlfilt -l --lbt-input formulas > formulas.4
test `wc -l < formulas.2` -eq 168 test `wc -l < formulas.2` -eq 168
test `wc -l < formulas.3` -eq 168 test `wc -l < formulas.3` -eq 168
test `wc -l < formulas.4` -eq 168 test `wc -l < formulas.4` -eq 168
@ -104,15 +100,15 @@ test `wc -l < formulas.4` -eq 168
# The --csv-escape option is now obsolete and replaced by double # The --csv-escape option is now obsolete and replaced by double
# quotes in the format string. So eventually the first two lines # quotes in the format string. So eventually the first two lines
# should disappear. # should disappear.
run 0 $ltlfilt formulas.2 --csv-escape --format='%L,%f' > formulas.5 run 0 ltlfilt formulas.2 --csv-escape --format='%L,%f' > formulas.5
run 0 $ltlfilt formulas.5/2 --csv-escape --format='%L,%f' > formulas.6 run 0 ltlfilt formulas.5/2 --csv-escape --format='%L,%f' > formulas.6
run 0 $ltlfilt formulas.2 --format='%L,"%f"' > formulas.5a run 0 ltlfilt formulas.2 --format='%L,"%f"' > formulas.5a
run 0 $ltlfilt formulas.5/2 --format='%L,"%f"' > formulas.6a run 0 ltlfilt formulas.5/2 --format='%L,"%f"' > formulas.6a
cmp formulas.5 formulas.6 cmp formulas.5 formulas.6
cmp formulas.5 formulas.5a cmp formulas.5 formulas.5a
cmp formulas.5a formulas.6a cmp formulas.5a formulas.6a
# Make sure ltl2dstar-style litterals always get quoted. # Make sure ltl2dstar-style litterals always get quoted.
test "`$ltlfilt -l --lbt-input -f 'G F a'`" = 'G F "a"' test "`ltlfilt -l --lbt-input -f 'G F a'`" = 'G F "a"'
# Original lbt-style litterals are unquoted. # Original lbt-style litterals are unquoted.
test "`$ltlfilt -l --lbt-input -f 'G F p42'`" = 'G F p42' test "`ltlfilt -l --lbt-input -f 'G F p42'`" = 'G F p42'

8
tests/core/lenient.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2012 Laboratoire de Recherche et Développement de # Copyright (C) 2012, 2017 Laboratoire de Recherche et Développement de
# l'Epita (LRDE). # l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -22,8 +22,6 @@
set -e set -e
ltlfilt=ltlfilt
cat >input <<EOF cat >input <<EOF
(a < b) U (b == c - 1) (a < b) U (b == c - 1)
((a < b) U {b == c - 1}) ((a < b) U {b == c - 1})
@ -48,10 +46,10 @@ cat >expected <<EOF
Xa Xa
EOF EOF
run 0 $ltlfilt --lenient input > output run 0 ltlfilt --lenient input > output
cmp output expected cmp output expected
run 2 $ltlfilt --lenient -f 'F( )' 2> stderr run 2 ltlfilt --lenient -f 'F( )' 2> stderr
grep 'unexpected empty block' stderr grep 'unexpected empty block' stderr

49
tests/core/ltl2dstar.test
View file

@ -1,7 +1,7 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et # Copyright (C) 2013-2017 Laboratoire de Recherche et Développement de
# Développement de l'Epita (LRDE). # l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -28,16 +28,9 @@ set -e
# Skip this test if ltl2dstar is not installed. # Skip this test if ltl2dstar is not installed.
(ltl2dstar --version) || exit 77 (ltl2dstar --version) || exit 77
ltlfilt=ltlfilt ltlfilt -f 'a U b' -l |
ltl2tgba=ltl2tgba ltl2dstar --ltl2nba=spin:ltl2tgba@-s - - |
ltlcross=ltlcross dstar2tgba --stats '%s %e %t %a %d' |
randltl=randltl
ltlfilt=ltlfilt
dstar2tgba=dstar2tgba
$ltlfilt -f 'a U b' -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-s - - |
$dstar2tgba --stats '%s %e %t %a %d' |
tee out tee out
test "`cat out`" = '2 3 7 1 1' test "`cat out`" = '2 3 7 1 1'
@ -45,33 +38,33 @@ test "`cat out`" = '2 3 7 1 1'
RAB=--automata=rabin RAB=--automata=rabin
STR=--automata=streett STR=--automata=streett
$randltl -n 15 a b | $ltlfilt --nnf --remove-wm | randltl -n 15 a b | ltlfilt --nnf --remove-wm |
$ltlcross -F - -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \ ltlcross -F - -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \
--timeout=30 \ --timeout=30 \
"$ltl2tgba -s %f >%N" \ "ltl2tgba -s %f >%N" \
"ltl2dstar $RAB --output=nba --ltl2nba=spin:$ltl2tgba@-s %L %T" \ "ltl2dstar $RAB --output=nba --ltl2nba=spin:ltl2tgba@-s %L %T" \
"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \ "ltl2dstar $RAB --ltl2nba=spin:ltl2tgba@-s %L %D" \
"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L - | $dstar2tgba --low -s >%N" \ "ltl2dstar $RAB --ltl2nba=spin:ltl2tgba@-s %L - | dstar2tgba --low -s >%N" \
"ltl2dstar $STR --output=nba --ltl2nba=spin:$ltl2tgba@-s %L %T" \ "ltl2dstar $STR --output=nba --ltl2nba=spin:ltl2tgba@-s %L %T" \
"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" \ "ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L %D" \
"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L - | $dstar2tgba --low -s >%N" \ "ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L - | dstar2tgba --low -s >%N" \
--csv=out.csv --csv=out.csv
# A bug in ltlcross <=1.2.5 caused it to not use the complement of the # A bug in ltlcross <=1.2.5 caused it to not use the complement of the
# negative automaton. # negative automaton.
$ltlcross -f 'GFa' --verbose \ ltlcross -f 'GFa' --verbose \
"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \ "ltl2dstar $RAB --ltl2nba=spin:ltl2tgba@-s %L %D" \
"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" 2>err "ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L %D" 2>err
test `grep -c 'info: check_empty.*Comp' err` = 2 test `grep -c 'info: check_empty.*Comp' err` = 2
$ltlcross -f 'FGa' --verbose \ ltlcross -f 'FGa' --verbose \
"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \ "ltl2dstar $RAB --ltl2nba=spin:ltl2tgba@-s %L %D" \
"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" 2>err "ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L %D" 2>err
test `grep -c 'info: check_empty.*Comp' err` = 2 test `grep -c 'info: check_empty.*Comp' err` = 2
# Make sure ltldo preserve the Rabin acceptance by default # Make sure ltldo preserve the Rabin acceptance by default
ltldo \ ltldo \
"ltl2dstar --ltl2nba=spin:$ltl2tgba@-s --output-format=hoa %L %O" \ "ltl2dstar --ltl2nba=spin:ltl2tgba@-s --output-format=hoa %L %O" \
-f 'GFa -> GFb' -Hi > out.hoa -f 'GFa -> GFb' -Hi > out.hoa
cat >expected <<EOF cat >expected <<EOF
HOA: v1 HOA: v1

42
tests/core/ltl2dstar2.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2013, 2015, 2016 Laboratoire de Recherche et # Copyright (C) 2013, 2015-2017 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -28,33 +28,27 @@ set -e
# Skip this test if ltl2dstar is not installed. # Skip this test if ltl2dstar is not installed.
(ltl2dstar --version) || exit 77 (ltl2dstar --version) || exit 77
ltlfilt=ltlfilt
ltl2tgba=ltl2tgba
dstar2tgba=dstar2tgba
randltl=randltl
# Make sure all recurrence formulas are translated into deterministic # Make sure all recurrence formulas are translated into deterministic
# Büchi automata by the DRA->TGBA converter. # Büchi automata by the DRA->TGBA converter.
# (Note that ltl2tgba is not called with -D when want to make # (Note that ltl2tgba is not called with -D when want to make
# sure we get a deterministic output even if the automaton generated # sure we get a deterministic output even if the automaton generated
# by Spot initially was non-deterministic) # by Spot initially was non-deterministic)
$randltl -n -1 a b --tree-size=5..15 | randltl -n -1 a b --tree-size=5..15 |
$ltlfilt --syntactic-recurrence --remove-wm -r -u \ ltlfilt --syntactic-recurrence --remove-wm -r -u \
--size-min=4 --size-max=15 --relabel=abc | --size-min=4 --size-max=15 --relabel=abc |
head -n 20 > formulas head -n 20 > formulas
$randltl -n -1 a b --tree-size=5..15 | randltl -n -1 a b --tree-size=5..15 |
$ltlfilt -v --obligation | ltlfilt -v --obligation |
$ltlfilt --syntactic-recurrence --remove-wm -r -u --size=4..15 --relabel=abc | ltlfilt --syntactic-recurrence --remove-wm -r -u --size=4..15 --relabel=abc |
head -n 20 >> formulas head -n 20 >> formulas
while read f; do while read f; do
$ltlfilt -f "$f" -l | ltlfilt -f "$f" -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-s - foo ltl2dstar --ltl2nba=spin:ltl2tgba@-s - foo
echo "$f" echo "$f"
det=`$dstar2tgba foo --stats '%d'` det=`dstar2tgba foo --stats '%d'`
test $det -eq 1; test $det -eq 1;
done < formulas done < formulas
@ -62,16 +56,16 @@ echo ==========================
# For obligation formulas, the output of dstar2tgba should # For obligation formulas, the output of dstar2tgba should
# have the same size as the input when option -D is used. # have the same size as the input when option -D is used.
$randltl -n -1 a b --tree-size=5..15 | randltl -n -1 a b --tree-size=5..15 |
$ltlfilt --obligation --size=4..15 --relabel=abc --remove-wm -r -u | ltlfilt --obligation --size=4..15 --relabel=abc --remove-wm -r -u |
head -n 20 > formulas head -n 20 > formulas
while read f; do while read f; do
expected=`$ltl2tgba "$f" -BD --stats '%s %e 1 %d'` expected=`ltl2tgba "$f" -BD --stats '%s %e 1 %d'`
$ltlfilt -f "$f" -l | ltlfilt -f "$f" -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-Ds - foo ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - foo
echo "$f" echo "$f"
output=`$dstar2tgba foo -BD --stats '%s %e %d 1'` output=`dstar2tgba foo -BD --stats '%s %e %d 1'`
# the '1 %d' matching '%d 1' makes sure input and output are deterministic. # the '1 %d' matching '%d 1' makes sure input and output are deterministic.
test "$output" = "$expected"; test "$output" = "$expected";
done < formulas done < formulas
@ -90,9 +84,9 @@ FGa & FGb
EOF EOF
while read f; do while read f; do
$ltlfilt -f "$f" -l | ltlfilt -f "$f" -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-s - foo ltl2dstar --ltl2nba=spin:ltl2tgba@-s - foo
echo "$f" echo "$f"
det=`$dstar2tgba foo --stats '%d'` det=`dstar2tgba foo --stats '%d'`
test $det -eq 0; test $det -eq 0;
done < formulas done < formulas

19
tests/core/ltl2dstar3.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et # Copyright (C) 2015, 2017 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -26,23 +26,16 @@ set -e
# Skip this test if ltl2dstar is not installed. # Skip this test if ltl2dstar is not installed.
(ltl2dstar --version) || exit 77 (ltl2dstar --version) || exit 77
ltlfilt=ltlfilt
ltl2tgba=ltl2tgba
ltlcross=ltlcross
randltl=randltl
ltlfilt=ltlfilt
dstar2tgba=dstar2tgba
RAB='--automata=rabin --output-format=hoa' RAB='--automata=rabin --output-format=hoa'
STR='--automata=streett --output-format=hoa' STR='--automata=streett --output-format=hoa'
# Run ltlcross without product, because this requires too much memory. # Run ltlcross without product, because this requires too much memory.
$randltl -n 25 a b | $ltlfilt --remove-wm | randltl -n 25 a b | ltlfilt --remove-wm |
$ltlcross -F- -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \ ltlcross -F- -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \
--timeout=30 --verbose --csv=out.csv --products=0 \ --timeout=30 --verbose --csv=out.csv --products=0 \
"$ltl2tgba -s %f >%N" \ "ltl2tgba -s %f >%N" \
"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %H" \ "ltl2dstar $RAB --ltl2nba=spin:ltl2tgba@-s %L %H" \
"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %H" "ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L %H"
grep '"in_type"' out.csv && exit 1 grep '"in_type"' out.csv && exit 1
exit 0 exit 0

40
tests/core/ltl2dstar4.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et # Copyright (C) 2013, 2014, 2015, 2017 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -28,42 +28,34 @@ set -e
# Skip this test if ltl2dstar is not installed. # Skip this test if ltl2dstar is not installed.
(ltl2dstar --version) || exit 77 (ltl2dstar --version) || exit 77
ltlfilt=ltlfilt
ltl2tgba=ltl2tgba
ltlcross=ltlcross
randltl=randltl
autfilt=autfilt
ltldo=ltldo
STR='--automata=streett --output-format=hoa' STR='--automata=streett --output-format=hoa'
$ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l | ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-s $STR - - | ltl2dstar --ltl2nba=spin:ltl2tgba@-s $STR - - |
$autfilt --tgba --stats '%S %E %A %s %e %t %a %d' | autfilt --tgba --stats '%S %E %A %s %e %t %a %d' |
tee out tee out
test "`cat out`" = '9 144 4 25 149 416 2 0' test "`cat out`" = '9 144 4 25 149 416 2 0'
$ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l | ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-s $STR - - | ltl2dstar --ltl2nba=spin:ltl2tgba@-s $STR - - |
SPOT_STREETT_CONV_MIN=1 $autfilt --tgba --stats '%S %E %A %s %e %t %a %d' | SPOT_STREETT_CONV_MIN=1 autfilt --tgba --stats '%S %E %A %s %e %t %a %d' |
tee out tee out
test "`cat out`" = '9 144 4 25 218 482 2 0' test "`cat out`" = '9 144 4 25 218 482 2 0'
LTL2DSTAR="ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L"
LTL2DSTAR="ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L"
# Generate 50 formulas for which the streett automaton has at least 3 # Generate 50 formulas for which the streett automaton has at least 3
# acceptance sets. # acceptance sets.
$randltl --ltl-priorities=W=0,M=0 -n 1000 3 | randltl --ltl-priorities=W=0,M=0 -n 1000 3 |
$ltldo "$LTL2DSTAR ->%O" -F- --name=%f -H | tee streett | ltldo "$LTL2DSTAR ->%O" -F- --name=%f -H | tee streett |
$autfilt --acc-set=3.. --stats=%M | head -n 50 > formulas autfilt --acc-set=3.. --stats=%M | head -n 50 > formulas
# Add 50 formulas that use less acceptance sets # Add 50 formulas that use less acceptance sets
$autfilt streett --acc-set=0..2 --stats=%M | head -n 50 >> formulas autfilt streett --acc-set=0..2 --stats=%M | head -n 50 >> formulas
$ltlcross -F formulas --timeout=30 \ ltlcross -F formulas --timeout=30 \
"$ltl2tgba -H %f >%O" \ "ltl2tgba -H %f >%O" \
"$LTL2DSTAR %O" \ "$LTL2DSTAR %O" \
"$LTL2DSTAR - | SPOT_STREETT_CONV_MIN=0 $autfilt --tgba -H >%O" \ "$LTL2DSTAR - | SPOT_STREETT_CONV_MIN=0 autfilt --tgba -H >%O" \
"$LTL2DSTAR - | SPOT_STREETT_CONV_MIN=1 $autfilt --tgba -H >%O" \ "$LTL2DSTAR - | SPOT_STREETT_CONV_MIN=1 autfilt --tgba -H >%O" \
--csv=out.csv --csv=out.csv

42
tests/core/ltlcross2.test
View file

@ -21,28 +21,26 @@
. ./defs . ./defs
set -e set -e
ltl2tgba=ltl2tgba
randltl -P -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 --seed=314 | randltl -P -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 --seed=314 |
ltlcross --products=3 --timeout=60 \ ltlcross --products=3 --timeout=60 \
"$ltl2tgba --lbtt --any --low %f > %T" \ "ltl2tgba --lbtt --any --low %f > %T" \
"$ltl2tgba --lbtt --any --medium %f > %T" \ "ltl2tgba --lbtt --any --medium %f > %T" \
"$ltl2tgba --hoa --any --high %f > %H" \ "ltl2tgba --hoa --any --high %f > %H" \
"$ltl2tgba --lbtt --deterministic --low %f > %T" \ "ltl2tgba --lbtt --deterministic --low %f > %T" \
"$ltl2tgba --lbtt --deterministic --medium %f > %T" \ "ltl2tgba --lbtt --deterministic --medium %f > %T" \
"$ltl2tgba --lbtt --deterministic --high %f > %T" \ "ltl2tgba --lbtt --deterministic --high %f > %T" \
"$ltl2tgba --lbtt --small --low %f > %T" \ "ltl2tgba --lbtt --small --low %f > %T" \
"$ltl2tgba --hoa --small --medium %f > %H" \ "ltl2tgba --hoa --small --medium %f > %H" \
"$ltl2tgba --lbtt --small --high %f > %T" \ "ltl2tgba --lbtt --small --high %f > %T" \
"$ltl2tgba --lbtt -x comp-susp --small %f >%T" \ "ltl2tgba --lbtt -x comp-susp --small %f >%T" \
"$ltl2tgba --lbtt -x comp-susp,!skel-wdba --small %f >%T" \ "ltl2tgba --lbtt -x comp-susp,!skel-wdba --small %f >%T" \
"$ltl2tgba --lbtt -x comp-susp,early-susp --small %f >%T" \ "ltl2tgba --lbtt -x comp-susp,early-susp --small %f >%T" \
"$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --small %f >%T" \ "ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --small %f >%T" \
"$ltl2tgba --spin --ba -x degen-lskip=0 %f >%N" \ "ltl2tgba --spin --ba -x degen-lskip=0 %f >%N" \
"$ltl2tgba --lbtt --ba --high %f > %T" \ "ltl2tgba --lbtt --ba --high %f > %T" \
"$ltl2tgba --spin=6 --ba -x degen-order,degen-lcache=2 --medium %f > %N" \ "ltl2tgba --spin=6 --ba -x degen-order,degen-lcache=2 --medium %f > %N" \
"$ltl2tgba --hoa -x degen-lcache=3 -BDC %f > %H" \ "ltl2tgba --hoa -x degen-lcache=3 -BDC %f > %H" \
"$ltl2tgba --lbtt -BC %f > %T" \ "ltl2tgba --lbtt -BC %f > %T" \
"$ltl2tgba --lbtt --unambiguous --low %f > %T" \ "ltl2tgba --lbtt --unambiguous --low %f > %T" \
"$ltl2tgba --lbtt --unambiguous --high %f > %T" \ "ltl2tgba --lbtt --unambiguous --high %f > %T" \
--json=output.json --csv=output.csv --json=output.json --csv=output.csv

44
tests/core/ltlcross3.test
View file

@ -31,16 +31,14 @@ check_csv()
done) done)
} }
ltl2tgba=ltl2tgba
# Make sure ltlcross quotes formulas correctly # Make sure ltlcross quotes formulas correctly
cat >formula <<\EOF cat >formula <<\EOF
G"a'-'>'b" G"a'-'>'b"
FGa FGa
EOF EOF
run 0 ltlcross -F formula --csv=out.csv \ run 0 ltlcross -F formula --csv=out.csv \
"$ltl2tgba -s %f >%N" \ "ltl2tgba -s %f >%N" \
"$ltl2tgba --lenient -s %s >%N" \ "ltl2tgba --lenient -s %s >%N" \
--verbose 2> error --verbose 2> error
cat >ceplan <<EOF cat >ceplan <<EOF
info: check_empty P0*N0 info: check_empty P0*N0
@ -60,8 +58,8 @@ grep 'info: check_empty' error > ce
diff -u ce ceplan diff -u ce ceplan
ltlcross -F formula --csv=out.csv \ ltlcross -F formula --csv=out.csv \
--ref "$ltl2tgba -s %f >%N" \ --ref "ltl2tgba -s %f >%N" \
"$ltl2tgba --lenient -s %s >%N" \ "ltl2tgba --lenient -s %s >%N" \
--verbose 2> error --verbose 2> error
cat >ceplan <<EOF cat >ceplan <<EOF
info: check_empty P0*N1 info: check_empty P0*N1
@ -77,8 +75,8 @@ grep 'info: check_empty' error > ce
diff -u ce ceplan diff -u ce ceplan
ltlcross -F formula --csv=out.csv \ ltlcross -F formula --csv=out.csv \
-D "$ltl2tgba -s %f >%N" \ -D "ltl2tgba -s %f >%N" \
"$ltl2tgba --lenient -s %s >%N" \ "ltl2tgba --lenient -s %s >%N" \
--verbose 2> error --verbose 2> error
cat >ceplan <<EOF cat >ceplan <<EOF
info: check_empty P0*N0 info: check_empty P0*N0
@ -98,8 +96,8 @@ grep 'info: check_empty' error > ce
diff -u ce ceplan diff -u ce ceplan
ltlcross -F formula --csv=out.csv \ ltlcross -F formula --csv=out.csv \
-D --ref "$ltl2tgba -s %f >%N" \ -D --ref "ltl2tgba -s %f >%N" \
"$ltl2tgba --lenient -s %s >%N" \ "ltl2tgba --lenient -s %s >%N" \
--verbose 2> error --verbose 2> error
cat >ceplan <<EOF cat >ceplan <<EOF
@ -116,16 +114,16 @@ grep 'info: check_empty' error > ce
diff -u ce ceplan diff -u ce ceplan
ltlcross -F formula --csv=out.csv \ ltlcross -F formula --csv=out.csv \
--ref "$ltl2tgba -s %f >%N" \ --ref "ltl2tgba -s %f >%N" \
--ref "$ltl2tgba --lenient -s %s >%N" \ --ref "ltl2tgba --lenient -s %s >%N" \
--verbose 2> error --verbose 2> error
grep 'info: check_empty' error && exit 1 grep 'info: check_empty' error && exit 1
run 2 ltlcross "$ltl2tgba -s %f >%N" 'foo bar' 2>stderr -f a run 2 ltlcross "ltl2tgba -s %f >%N" 'foo bar' 2>stderr -f a
grep 'ltlcross.*no input.*in.*foo bar' stderr grep 'ltlcross.*no input.*in.*foo bar' stderr
# Make sure non-zero exit codes are reported... # Make sure non-zero exit codes are reported...
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
-f a --csv=out.csv 2>stderr -f a --csv=out.csv 2>stderr
grep '"exit_status"' out.csv grep '"exit_status"' out.csv
grep '"exit_code"' out.csv grep '"exit_code"' out.csv
@ -134,7 +132,7 @@ test `grep '"exit code",1' out.csv | wc -l` -eq 2
check_csv out.csv check_csv out.csv
# ... unless --omit-missing is supplied. # ... unless --omit-missing is supplied.
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
-f a --csv=out.csv --omit-missing 2>stderr -f a --csv=out.csv --omit-missing 2>stderr
grep '"exit_status"' out.csv && exit 1 grep '"exit_status"' out.csv && exit 1
grep '"exit_code"' out.csv && exit 1 grep '"exit_code"' out.csv && exit 1
@ -143,7 +141,7 @@ test `grep '"exit code",1' out.csv | wc -l` -eq 0
check_csv out.csv check_csv out.csv
# Additional columns should not be an issue # Additional columns should not be an issue
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
-f a --csv=out.csv --strength 2>stderr -f a --csv=out.csv --strength 2>stderr
grep '"exit_status"' out.csv grep '"exit_status"' out.csv
grep '"exit_code"' out.csv grep '"exit_code"' out.csv
@ -154,7 +152,7 @@ test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 2 test `grep '"exit code",1' out.csv | wc -l` -eq 2
check_csv out.csv check_csv out.csv
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
-f a --csv=out.csv --ambiguous 2>stderr -f a --csv=out.csv --ambiguous 2>stderr
grep '"exit_status"' out.csv grep '"exit_status"' out.csv
grep '"exit_code"' out.csv grep '"exit_code"' out.csv
@ -164,7 +162,7 @@ test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 2 test `grep '"exit code",1' out.csv | wc -l` -eq 2
check_csv out.csv check_csv out.csv
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
-f a --csv=out.csv --ambiguous --strength 2>stderr -f a --csv=out.csv --ambiguous --strength 2>stderr
grep '"exit_status"' out.csv grep '"exit_status"' out.csv
grep '"exit_code"' out.csv grep '"exit_code"' out.csv
@ -219,7 +217,7 @@ test `wc -l < bogous` -eq 1
check_csv out.csv check_csv out.csv
# Check with --products=5 --automata # Check with --products=5 --automata
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
-f a --csv=out.csv --products=5 --automata 2>stderr -f a --csv=out.csv --products=5 --automata 2>stderr
p=`sed 's/[^,]//g;q' out.csv | wc -c` p=`sed 's/[^,]//g;q' out.csv | wc -c`
grep '"exit_status"' out.csv grep '"exit_status"' out.csv
@ -230,7 +228,7 @@ test `grep '"HOA:.*--BODY--.*--END--"' out.csv | wc -l` -eq 2
check_csv out.csv check_csv out.csv
# ... unless --omit-missing is supplied. # ... unless --omit-missing is supplied.
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
-f a --csv=out.csv --omit-missing --products=5 2>stderr -f a --csv=out.csv --omit-missing --products=5 2>stderr
grep '"exit_status"' out.csv && exit 1 grep '"exit_status"' out.csv && exit 1
grep '"exit_code"' out.csv && exit 1 grep '"exit_code"' out.csv && exit 1
@ -240,7 +238,7 @@ check_csv out.csv
# Check with --products=+5 # Check with --products=+5
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
-f a --csv=out.csv --products=+5 --automata 2>stderr -f a --csv=out.csv --products=+5 --automata 2>stderr
q=`sed 's/[^,]//g;q' out.csv | wc -c` q=`sed 's/[^,]//g;q' out.csv | wc -c`
grep '"exit_status"' out.csv grep '"exit_status"' out.csv
@ -251,7 +249,7 @@ test `grep '"HOA:.*--BODY--.*--END--"' out.csv | wc -l` -eq 2
check_csv out.csv check_csv out.csv
# ... unless --omit-missing is supplied. # ... unless --omit-missing is supplied.
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
-f a --csv=out.csv --omit-missing --products=+5 2>stderr -f a --csv=out.csv --omit-missing --products=+5 2>stderr
grep '"exit_status"' out.csv && exit 1 grep '"exit_status"' out.csv && exit 1
grep '"exit_code"' out.csv && exit 1 grep '"exit_code"' out.csv && exit 1
@ -265,7 +263,7 @@ test $q -eq `expr $p + 12`
# Check with Rabin/Streett output # Check with Rabin/Streett output
first="should not be erased" first="should not be erased"
echo "$first" > bug.txt echo "$first" > bug.txt
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%D' \ run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%D' \
-f 'X a' --csv=out.csv --save-bogus='>>bug.txt' 2>stderr -f 'X a' --csv=out.csv --save-bogus='>>bug.txt' 2>stderr
q=`sed 's/[^,]//g;q' out.csv | wc -c` q=`sed 's/[^,]//g;q' out.csv | wc -c`
test $q -eq `expr $p - 1` test $q -eq `expr $p - 1`

8
tests/core/ltlcross4.test
View file

@ -23,17 +23,15 @@ set -e
test -z "$PYTHON" && exit 77 test -z "$PYTHON" && exit 77
ltl2tgba=ltl2tgba
cat >formulas.txt <<EOF cat >formulas.txt <<EOF
GFa & GFb GFa & GFb
GFa -> GFb GFa -> GFb
EOF EOF
ltlcross -F formulas.txt \ ltlcross -F formulas.txt \
"{ltl2tgba any} $ltl2tgba --lbtt --any %f > %T" \ "{ltl2tgba any} ltl2tgba --lbtt --any %f > %T" \
"{ltl2tgba det} $ltl2tgba --lbtt --deterministic %f > %T" \ "{ltl2tgba det} ltl2tgba --lbtt --deterministic %f > %T" \
"{ltl2tgba sma} $ltl2tgba --lbtt --small %f > %T" \ "{ltl2tgba sma} ltl2tgba --lbtt --small %f > %T" \
--csv=output.csv --csv=output.csv
cat >test.py <<EOF cat >test.py <<EOF

6
tests/core/ltlcrossce2.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2015, 2016 Laboratoire de Recherche et # Copyright (C) 2015-2017 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -21,8 +21,6 @@
. ./defs . ./defs
set -e set -e
ltl2tgba=ltl2tgba
cat >fake <<\EOF cat >fake <<\EOF
#!/bin/sh #!/bin/sh
case $1 in case $1 in
@ -63,7 +61,7 @@ EOF
chmod +x fake chmod +x fake
run 1 ltlcross -f 'G(a <-> Fb) U c' \ run 1 ltlcross -f 'G(a <-> Fb) U c' \
"$ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors "ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors
cat errors cat errors
grep 'error: P0\*N1 is nonempty' errors grep 'error: P0\*N1 is nonempty' errors
grep 'error: P1\*N1 is nonempty' errors grep 'error: P1\*N1 is nonempty' errors

30
tests/core/ltldo.test
View file

@ -21,11 +21,7 @@
. ./defs . ./defs
set -e set -e
ltldo=ltldo run 0 ltldo -f a -f 'a&b' -f 'a -> b' -t 'echo %f,%s,%[ei]w' >output
ltl2tgba=ltl2tgba
genltl=genltl
run 0 $ltldo -f a -f 'a&b' -f 'a -> b' -t 'echo %f,%s,%[ei]w' >output
cat >expected <<EOF cat >expected <<EOF
a,a,a=1 a,a,a=1
(a) & (b),(a) && (b),(a=1) * (b=1) (a) & (b),(a) && (b),(a=1) * (b=1)
@ -34,7 +30,7 @@ EOF
diff output expected diff output expected
# Renaming # Renaming
run 0 $ltldo -f a -f 'a&_b' -t 'echo %f,%s' >output run 0 ltldo -f a -f 'a&_b' -t 'echo %f,%s' >output
cat >expected <<EOF cat >expected <<EOF
a,a a,a
(p0) & (p1),(p0) && (p1) (p0) & (p1),(p0) && (p1)
@ -43,8 +39,8 @@ diff output expected
# Test timeouts. Each of these runs should take 2*2 seconds. # Test timeouts. Each of these runs should take 2*2 seconds.
$genltl --or-g=1..2 | genltl --or-g=1..2 |
run 0 $ltldo -t 'sleep 10; echo %f' -T1 -t 'sleep 10; echo %f' \ run 0 ltldo -t 'sleep 10; echo %f' -T1 -t 'sleep 10; echo %f' \
>output 2>stderr >output 2>stderr
test -z "`cat output`" test -z "`cat output`"
test 4 = `grep -c warning: stderr` test 4 = `grep -c warning: stderr`
@ -65,8 +61,8 @@ grep -q 'aborting here' stderr
test "`echo 1,a,3,4 | ltldo -F-/2 ltl2tgba --stats='%<,%s,%>'`" = '1,2,3,4' test "`echo 1,a,3,4 | ltldo -F-/2 ltl2tgba --stats='%<,%s,%>'`" = '1,2,3,4'
$genltl --and-gf=1..3 | genltl --and-gf=1..3 |
run 0 $ltldo "{tgba}$ltl2tgba %f -H >%H" "{ba}$ltl2tgba >%N %f -s" \ run 0 ltldo "{tgba}ltl2tgba %f -H >%H" "{ba}ltl2tgba >%N %f -s" \
--stats="%T,%#,%f,%s,%t,%e" >output --stats="%T,%#,%f,%s,%t,%e" >output
cat output cat output
cat >expected <<EOF cat >expected <<EOF
@ -80,7 +76,7 @@ EOF
diff output expected diff output expected
# Renaming # Renaming
run 0 $ltldo "$ltl2tgba -H %s>%H" -f GF_foo_ -H >output run 0 ltldo "ltl2tgba -H %s>%H" -f GF_foo_ -H >output
cat output cat output
# The HOA output uses _foo_ as atomic proposition, but the name shows # The HOA output uses _foo_ as atomic proposition, but the name shows
# that GFp0 was actually given to ltl2tgba. # that GFp0 was actually given to ltl2tgba.
@ -103,7 +99,7 @@ EOF
diff output expected diff output expected
# But we can force the name in the output: # But we can force the name in the output:
run 0 $ltldo "$ltl2tgba -H %s>%H" -f GF_foo_ -H --name=%f >output run 0 ltldo "ltl2tgba -H %s>%H" -f GF_foo_ -H --name=%f >output
cat output cat output
cat >expected <<EOF cat >expected <<EOF
HOA: v1 HOA: v1
@ -124,7 +120,7 @@ EOF
diff output expected diff output expected
# Not trusting properties # Not trusting properties
run 0 $ltldo "$ltl2tgba -H %s>%H" -f GF_foo_ -H --trust-hoa=no >output run 0 ltldo "ltl2tgba -H %s>%H" -f GF_foo_ -H --trust-hoa=no >output
cat output cat output
cat >expected <<EOF cat >expected <<EOF
HOA: v1 HOA: v1
@ -144,21 +140,21 @@ State: 0
EOF EOF
diff output expected diff output expected
$ltldo ': %s; true>%O' -f GFa 2>stderr && exit 1 ltldo ': %s; true>%O' -f GFa 2>stderr && exit 1
test $? = 2 test $? = 2
grep ':.*empty input' stderr grep ':.*empty input' stderr
grep 'ltldo: aborting' stderr grep 'ltldo: aborting' stderr
$ltldo ': %s; true>%O' --errors=ignore -f GFa 2>stderr ltldo ': %s; true>%O' --errors=ignore -f GFa 2>stderr
test $? = 0 test $? = 0
test -z "`cat stderr`" test -z "`cat stderr`"
$ltldo ': %s; true>%O' --errors=warn -f GFa 2>stderr ltldo ': %s; true>%O' --errors=warn -f GFa 2>stderr
test $? = 0 test $? = 0
grep ':.*empty input' stderr grep ':.*empty input' stderr
$ltldo '{name} foo/bar/ltl2baextended' -f GFa 2>stderr && exit 1 ltldo '{name} foo/bar/ltl2baextended' -f GFa 2>stderr && exit 1
grep 'error:.*foo/bar/ltl2baextended -f .*>.*' stderr grep 'error:.*foo/bar/ltl2baextended -f .*>.*' stderr

36
tests/core/ltlfilt.test
View file

@ -1,7 +1,7 @@
#! /bin/sh #! /bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et # Copyright (C) 2013-2017 Laboratoire de Recherche et Développement de
# Développement de l'Epita (LRDE). # l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -25,12 +25,10 @@
set -e set -e
ltlfilt=ltlfilt
checkopt() checkopt()
{ {
cat >exp cat >exp
run 0 $ltlfilt "$@" formulas > out run 0 ltlfilt "$@" formulas > out
diff exp out diff exp out
} }
@ -226,7 +224,7 @@ p0 | Gp1 | FG(p2 | Xp3)
p0 | Gp1 p0 | Gp1
EOF EOF
run 0 $ltlfilt -u --nnf --relabel-bool=pnn in >out run 0 ltlfilt -u --nnf --relabel-bool=pnn in >out
diff exp out diff exp out
cat >exp <<EOF cat >exp <<EOF
@ -250,7 +248,7 @@ p0 || []p1 || <>[](p2 || Xp3)
p0 || []p1 p0 || []p1
EOF EOF
run 0 $ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out run 0 ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out
diff exp out diff exp out
cat >exp <<EOF cat >exp <<EOF
@ -290,7 +288,7 @@ p0 && []<>(p1 || p2) && ![]<>!(p1 || p2)
<>(p0 <-> p1) -> !(p2 <-> p3) <>(p0 <-> p1) -> !(p2 <-> p3)
EOF EOF
run 0 $ltlfilt -s -u --relabel=pnn --define in >out run 0 ltlfilt -s -u --relabel=pnn --define in >out
diff exp out diff exp out
toolong='((p2=0) * (p3=1))' # work around the 80-col check toolong='((p2=0) * (p3=1))' # work around the 80-col check
@ -326,10 +324,10 @@ cat >exp <<EOF
#define p3 (b=1) #define p3 (b=1)
((p0=1) * (p1=0)) + ((p0=0) * (p1=1)) + (G(((p2=1) * (p3=0)) + $toolong)) ((p0=1) * (p1=0)) + ((p0=0) * (p1=1)) + (G(((p2=1) * (p3=0)) + $toolong))
EOF EOF
run 0 $ltlfilt -p --wring -u --nnf --relabel=pnn --define in >out run 0 ltlfilt -p --wring -u --nnf --relabel=pnn --define in >out
diff exp out diff exp out
run 0 $ltlfilt -0 in > out run 0 ltlfilt -0 in > out
perl -i -pe 's/\0/@\n/g' out perl -i -pe 's/\0/@\n/g' out
cat >exp <<EOF cat >exp <<EOF
a & c & Xb@ a & c & Xb@
@ -343,38 +341,38 @@ EOF
diff exp out diff exp out
SPOT_STUTTER_CHECK=0 \ SPOT_STUTTER_CHECK=0 \
$ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1 ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
test $? = 2 test $? = 2
grep 'non-LTL' stderr grep 'non-LTL' stderr
SPOT_STUTTER_CHECK=555 \ SPOT_STUTTER_CHECK=555 \
$ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1 ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
test $? = 2 test $? = 2
grep 'invalid' stderr grep 'invalid' stderr
SPOT_STUTTER_CHECK=5 \ SPOT_STUTTER_CHECK=5 \
$ltlfilt --stutter-invariant -f '!{a:b*:c}' ltlfilt --stutter-invariant -f '!{a:b*:c}'
# This one was incorrectly diagnosed as stutter invariant because of a # This one was incorrectly diagnosed as stutter invariant because of a
# bug in the bitvectors. # bug in the bitvectors.
$ltlfilt --stutter-invariant -f 'F(a & XXXXXX!a)' && exit 1 ltlfilt --stutter-invariant -f 'F(a & XXXXXX!a)' && exit 1
$ltlfilt -c -o 'foo' -f a 2>stderr && exit 1 ltlfilt -c -o 'foo' -f a 2>stderr && exit 1
grep 'ltlfilt: options --output and --count are incompatible' stderr grep 'ltlfilt: options --output and --count are incompatible' stderr
out=`$ltlfilt -f 'G(a xor b) -> F(c <-> Xd)' --unabbreviate='^iF'` out=`ltlfilt -f 'G(a xor b) -> F(c <-> Xd)' --unabbreviate='^iF'`
exp='(1 U (c <-> Xd)) | !G!(a <-> b)' exp='(1 U (c <-> Xd)) | !G!(a <-> b)'
test "$out" = "$exp" test "$out" = "$exp"
$ltlfilt -f 'GF"a\"\\b"' > out ltlfilt -f 'GF"a\"\\b"' > out
test "`cat out`" = 'GF"a\"\\b"' test "`cat out`" = 'GF"a\"\\b"'
$ltlfilt --lbt-input -f 'G F "a\"\\b"' -l > out ltlfilt --lbt-input -f 'G F "a\"\\b"' -l > out
test "`cat out`" = 'G F "a\"\\b"' test "`cat out`" = 'G F "a\"\\b"'
$ltlfilt --size=foo=2..3 2>stderr && exit 1 ltlfilt --size=foo=2..3 2>stderr && exit 1
grep 'invalid range.*should start with' stderr grep 'invalid range.*should start with' stderr

6
tests/core/optba.test
View file

@ -24,8 +24,6 @@ set -x
# This is a case where autfilt is used to optimize BA, but used to # This is a case where autfilt is used to optimize BA, but used to
# produce a larger one. See issue #79. # produce a larger one. See issue #79.
autfilt=autfilt
# ltldo -s -f '!(((p1 W c1) U Gp2) || (GXc2 <-> F!F!c1))' 'ltl3ba -M0' # ltldo -s -f '!(((p1 W c1) U Gp2) || (GXc2 <-> F!F!c1))' 'ltl3ba -M0'
cat >input <<EOF cat >input <<EOF
never { never {
@ -158,7 +156,7 @@ T0_S18:
EOF EOF
# 18 states is fine for transition-based acceptance # 18 states is fine for transition-based acceptance
test `$autfilt --exclusive-ap=c1,c2 --high --small --stats=%s input` = 18 test `autfilt --exclusive-ap=c1,c2 --high --small --stats=%s input` = 18
# But we should have 19 with Büchi acceptance, not 20. # But we should have 19 with Büchi acceptance, not 20.
test `$autfilt --exclusive-ap=c1,c2 --high --small -B --stats=%s input` = 19 test `autfilt --exclusive-ap=c1,c2 --high --small -B --stats=%s input` = 19

29
tests/core/prodor.test
View file

@ -21,9 +21,6 @@
. ./defs . ./defs
set -e set -e
ltl2tgba=ltl2tgba
autfilt=autfilt
# Two empty automata # Two empty automata
cat >a1.hoa <<EOF cat >a1.hoa <<EOF
HOA: v1 HOA: v1
@ -48,11 +45,11 @@ State: 0
EOF EOF
# the OR product of two empty automata should be empty # the OR product of two empty automata should be empty
$autfilt --product-or a1.hoa a2.hoa -H | $autfilt --is-empty autfilt --product-or a1.hoa a2.hoa -H | autfilt --is-empty
$ltl2tgba -DH 'GFa' > gfa.hoa ltl2tgba -DH 'GFa' > gfa.hoa
$ltl2tgba -DH 'FGb' > fgb.hoa ltl2tgba -DH 'FGb' > fgb.hoa
$autfilt --product-or gfa.hoa fgb.hoa -H > por.hoa autfilt --product-or gfa.hoa fgb.hoa -H > por.hoa
cat por.hoa cat por.hoa
cat >exp <<EOF cat >exp <<EOF
@ -81,9 +78,9 @@ State: 2
EOF EOF
diff por.hoa exp diff por.hoa exp
test 2 = `$autfilt -c --intersect por.hoa gfa.hoa fgb.hoa` test 2 = `autfilt -c --intersect por.hoa gfa.hoa fgb.hoa`
$autfilt --product-and gfa.hoa fgb.hoa -H > pand.hoa autfilt --product-and gfa.hoa fgb.hoa -H > pand.hoa
cat pand.hoa cat pand.hoa
cat >exp <<EOF cat >exp <<EOF
@ -107,11 +104,11 @@ State: 1
EOF EOF
diff pand.hoa exp diff pand.hoa exp
test 2 = `$autfilt -c --intersect pand.hoa gfa.hoa fgb.hoa` test 2 = `autfilt -c --intersect pand.hoa gfa.hoa fgb.hoa`
$ltl2tgba -BDH 'GFa' > gfa.hoa ltl2tgba -BDH 'GFa' > gfa.hoa
$ltl2tgba -BDH 'Xb' > xb.hoa ltl2tgba -BDH 'Xb' > xb.hoa
$autfilt --product-or gfa.hoa xb.hoa -H > por.hoa autfilt --product-or gfa.hoa xb.hoa -H > por.hoa
cat por.hoa cat por.hoa
cat >exp <<EOF cat >exp <<EOF
@ -152,9 +149,9 @@ State: 6
EOF EOF
diff por.hoa exp diff por.hoa exp
$ltl2tgba -BDH 'GFa' > gfa.hoa ltl2tgba -BDH 'GFa' > gfa.hoa
$ltl2tgba -x '!wdba-minimize' -DH 'Xb' > xb.hoa ltl2tgba -x '!wdba-minimize' -DH 'Xb' > xb.hoa
$autfilt --product-or gfa.hoa xb.hoa -H > por.hoa autfilt --product-or gfa.hoa xb.hoa -H > por.hoa
cat por.hoa cat por.hoa
cat >exp <<EOF cat >exp <<EOF

26
tests/core/rand.test
View file

@ -1,7 +1,7 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement # Copyright (C) 2014, 2015, 2017 Laboratoire de Recherche et
# de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -21,9 +21,7 @@
. ./defs . ./defs
set -e set -e
randltl=randltl run 0 randltl -S -n 20 a b c --tree-size=10 \
run 0 $randltl -S -n 20 a b c --tree-size=10 \
--sere-priorities=and=0,andNLM=0 \ --sere-priorities=and=0,andNLM=0 \
--boolean-priorities=equiv=0,implies=0,xor=0,and=0,not=0 \ --boolean-priorities=equiv=0,implies=0,xor=0,and=0,not=0 \
--dump-priorities > stdout --dump-priorities > stdout
@ -58,7 +56,7 @@ diff stdout expected
sere='eword=0,and=0,andNLM=0,fusion=0,star=0,star_b=0' sere='eword=0,and=0,andNLM=0,fusion=0,star=0,star_b=0'
sere="$sere,or=0,concat=0,fstar=0,fstar_b=0" sere="$sere,or=0,concat=0,fstar=0,fstar_b=0"
run 0 $randltl -S -n 10000 a b c --tree-size=10..20 \ run 0 randltl -S -n 10000 a b c --tree-size=10..20 \
--sere-p=$sere \ --sere-p=$sere \
--boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 \ --boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 \
--dump-pr > stdout --dump-pr > stdout
@ -92,7 +90,7 @@ diff stdout expected
# Disabling all operators will prevent more formulas to be generated. # Disabling all operators will prevent more formulas to be generated.
$randltl -S -n 10000 a b c --tree-size=10..20 \ randltl -S -n 10000 a b c --tree-size=10..20 \
--sere-p=$sere \ --sere-p=$sere \
--boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 > out && --boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 > out &&
exit 1 exit 1
@ -107,7 +105,7 @@ diff expected out2
# atomic proposition can be implicitly specified using a number # atomic proposition can be implicitly specified using a number
$randltl -n 1000 3 --tree-size=10..20 > out randltl -n 1000 3 --tree-size=10..20 > out
grep -q p0 out grep -q p0 out
grep -q p1 out grep -q p1 out
grep -q p2 out grep -q p2 out
@ -116,7 +114,7 @@ grep p3 out && exit 1
# We should be able to generate exactly two formulas with 0 atomic # We should be able to generate exactly two formulas with 0 atomic
# propositions. # propositions.
run 0 $randltl -n2 0 | sort > out run 0 randltl -n2 0 | sort > out
cat >expected <<EOF cat >expected <<EOF
0 0
1 1
@ -124,19 +122,19 @@ EOF
diff out expected diff out expected
# requesting more formulas should fail # requesting more formulas should fail
run 2 $randltl -n3 0 run 2 randltl -n3 0
# If more numbers are given, there are interpreted as atomic propositions # If more numbers are given, there are interpreted as atomic propositions
run 0 $randltl -n1000 0 1 > out run 0 randltl -n1000 0 1 > out
grep -q '"0"' out grep -q '"0"' out
grep -q '"1"' out grep -q '"1"' out
run 0 $randltl -n5 2 -o test-all.ltl run 0 randltl -n5 2 -o test-all.ltl
run 0 $randltl -n5 2 -o test-%L.ltl run 0 randltl -n5 2 -o test-%L.ltl
cat test-1.ltl test-2.ltl test-3.ltl test-4.ltl test-5.ltl > test-cmp.ltl cat test-1.ltl test-2.ltl test-3.ltl test-4.ltl test-5.ltl > test-cmp.ltl
diff test-cmp.ltl test-all.ltl diff test-cmp.ltl test-all.ltl
$randltl 2 --ltl-prio=X 2>stderr && exit 1 randltl 2 --ltl-prio=X 2>stderr && exit 1
grep 'failed to parse LTL priorities near X' stderr grep 'failed to parse LTL priorities near X' stderr

29
tests/core/randomize.test
View file

@ -1,7 +1,7 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de # Copyright (C) 2014, 2015, 2017 Laboratoire de Recherche et
# l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -22,10 +22,7 @@
set -e set -e
ltl2tgba=ltl2tgba ltl2tgba --hoa 'Ga | Gb | Gc | Gd' > out
autfilt=autfilt
$ltl2tgba --hoa 'Ga | Gb | Gc | Gd' > out
cat >expected <<EOF cat >expected <<EOF
HOA: v1 HOA: v1
@ -58,10 +55,10 @@ diff out expected
# The seed and formula where chosen so that these four outputs are # The seed and formula where chosen so that these four outputs are
# different. # different.
run 0 $autfilt --seed=1 --dot out > 1.dot run 0 autfilt --seed=1 --dot out > 1.dot
run 0 $autfilt --seed=1 --dot --randomize=t out > 2.dot run 0 autfilt --seed=1 --dot --randomize=t out > 2.dot
run 0 $autfilt --seed=1 --dot --randomize=s out > 3.dot run 0 autfilt --seed=1 --dot --randomize=s out > 3.dot
run 0 $autfilt --seed=1 --dot --randomize=st out > 4.dot run 0 autfilt --seed=1 --dot --randomize=st out > 4.dot
cmp 1.dot 2.dot && exit 1 cmp 1.dot 2.dot && exit 1
cmp 1.dot 3.dot && exit 1 cmp 1.dot 3.dot && exit 1
@ -70,16 +67,16 @@ cmp 2.dot 4.dot && exit 1
cmp 3.dot 4.dot && exit 1 cmp 3.dot 4.dot && exit 1
# A second run should produce the same output # A second run should produce the same output
$autfilt --seed=1 --dot out > 1b.dot autfilt --seed=1 --dot out > 1b.dot
$autfilt --seed=1 --dot --randomize=t out > 2b.dot autfilt --seed=1 --dot --randomize=t out > 2b.dot
$autfilt --seed=1 --dot --randomize=s out > 3b.dot autfilt --seed=1 --dot --randomize=s out > 3b.dot
$autfilt --seed=1 --dot --randomize=st out > 4b.dot autfilt --seed=1 --dot --randomize=st out > 4b.dot
diff 1.dot 1b.dot diff 1.dot 1b.dot
diff 2.dot 2b.dot diff 2.dot 2b.dot
diff 3.dot 3b.dot diff 3.dot 3b.dot
diff 4.dot 4b.dot diff 4.dot 4b.dot
$autfilt --randomize=foo out 2>stderr && exit 1 autfilt --randomize=foo out 2>stderr && exit 1
grep "unknown argument for --randomize: 'f'" stderr grep "unknown argument for --randomize: 'f'" stderr
@ -108,7 +105,7 @@ State: 4 "s0"
[1] 2 [1] 2
--END-- --END--
EOF EOF
$autfilt --randomize --seed=1 input -H > output autfilt --randomize --seed=1 input -H > output
cat >expected <<EOF cat >expected <<EOF
HOA: v1 HOA: v1
States: 5 States: 5

6
tests/core/remfin.test
View file

@ -24,8 +24,6 @@
set -e set -e
autfilt=autfilt
cat >test1 <<EOF cat >test1 <<EOF
/* /*
** This was a TGBA for GFa & GFb, but ** This was a TGBA for GFa & GFb, but
@ -1412,11 +1410,11 @@ State: 3
--END-- --END--
EOF EOF
run 0 $autfilt -H --remove-fin test1 > output run 0 autfilt -H --remove-fin test1 > output
cat output cat output
diff -u output expected diff -u output expected
run 0 $autfilt -H --tgba test1 > output run 0 autfilt -H --tgba test1 > output
cat output cat output
diff -u output expected-tgba diff -u output expected-tgba

41
tests/core/satmin.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2013 Laboratoire de Recherche et Développement # Copyright (C) 2013, 2017 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.
@ -21,9 +21,6 @@
. ./defs . ./defs
set -e set -e
ltl2tgba=ltl2tgba
ltlcross=ltlcross
# The formulas below have been removed from the list to reduce the time # The formulas below have been removed from the list to reduce the time
# required to complete the test. In the future, we would like to respond # required to complete the test. In the future, we would like to respond
# quickly to them. # quickly to them.
@ -94,25 +91,25 @@ EOF
# The following tests are named from 1 to 11 in order to reduce the length of # The following tests are named from 1 to 11 in order to reduce the length of
# each line. If a test fails during the diff, it is easily identifiable. # each line. If a test fails during the diff, it is easily identifiable.
$ltlcross -F formulas \ ltlcross -F formulas \
--timeout=60 \ --timeout=60 \
"{1} $ltl2tgba --det --lbtt %f >%T" \ "{1} ltl2tgba --det --lbtt %f >%T" \
"{2} $ltl2tgba --det --lbtt -x tba-det %f >%T" \ "{2} ltl2tgba --det --lbtt -x tba-det %f >%T" \
"{3} $ltl2tgba --det --lbtt -x sat-acc=1 %f >%T" \ "{3} ltl2tgba --det --lbtt -x sat-acc=1 %f >%T" \
"{4} $ltl2tgba --det --lbtt -x sat-acc=3 %f >%T" \ "{4} ltl2tgba --det --lbtt -x sat-acc=3 %f >%T" \
"{5} $ltl2tgba --det --lbtt -x sat-states=3 %f >%T" \ "{5} ltl2tgba --det --lbtt -x sat-states=3 %f >%T" \
"{6} $ltl2tgba --det --lbtt -x sat-minimize %f >%T" \ "{6} ltl2tgba --det --lbtt -x sat-minimize %f >%T" \
"{7} $ltl2tgba --det --lbtt -x 'sat-minimize, sat-langmap' %f >%T" \ "{7} ltl2tgba --det --lbtt -x 'sat-minimize, sat-langmap' %f >%T" \
"{8} $ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=0' %f >%T" \ "{8} ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=0' %f >%T" \
"{9} $ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=1' %f >%T" \ "{9} ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=1' %f >%T" \
"{10} $ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=2' %f >%T" \ "{10} ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=2' %f >%T" \
"{11} $ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=50' %f >%T" \ "{11} ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=50' %f >%T" \
"{12} $ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=-1' %f >%T" \ "{12} ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=-1' %f >%T" \
"{13} $ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=0' %f >%T" \ "{13} ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=0' %f >%T" \
"{14} $ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=1' %f >%T" \ "{14} ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=1' %f >%T" \
"{15} $ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=2' %f >%T" \ "{15} ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=2' %f >%T" \
"{16} $ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=50' %f >%T" \ "{16} ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=50' %f >%T" \
"{17} $ltl2tgba --det --lbtt -x sat-minimize=4 %f >%T" \ "{17} ltl2tgba --det --lbtt -x sat-minimize=4 %f >%T" \
--csv=det.csv --csv=det.csv
grep -v ',\"5\",' det.csv | cut -d ',' -f '1,2,6' > output grep -v ',\"5\",' det.csv | cut -d ',' -f '1,2,6' > output

21
tests/core/sbacc.test
View file

@ -1,7 +1,7 @@
#! /bin/sh #! /bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement # Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
# de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -22,10 +22,7 @@
set -e set -e
ltl2tgba=ltl2tgba ltl2tgba 'GFa & GFb' -H | run 0 autfilt --sbacc -H > out.hoa
autfilt=autfilt
$ltl2tgba 'GFa & GFb' -H | run 0 $autfilt --sbacc -H > out.hoa
cat >expected<<EOF cat >expected<<EOF
HOA: v1 HOA: v1
@ -94,7 +91,7 @@ State: 1
EOF EOF
run 0 $autfilt --state-based-acceptance in.hoa -H > out.hoa run 0 autfilt --state-based-acceptance in.hoa -H > out.hoa
cat >expected <<EOF cat >expected <<EOF
HOA: v1 HOA: v1
@ -130,10 +127,10 @@ EOF
diff out.hoa expected diff out.hoa expected
$autfilt --sba -H expected > out.hoa autfilt --sba -H expected > out.hoa
diff out.hoa expected diff out.hoa expected
$autfilt --strip-acc -H expected -n1 > out.hoa autfilt --strip-acc -H expected -n1 > out.hoa
cat >expected <<EOF cat >expected <<EOF
HOA: v1 HOA: v1
States: 3 States: 3
@ -154,9 +151,9 @@ EOF
diff out.hoa expected diff out.hoa expected
randltl --weak-fairness -n 20 2 | randltl --weak-fairness -n 20 2 |
ltlcross "$ltl2tgba -DH %f >%O" \ ltlcross "ltl2tgba -DH %f >%O" \
"$ltl2tgba -S %f >%O" \ "ltl2tgba -S %f >%O" \
"$ltl2tgba -H %f | $autfilt -H >%O" "ltl2tgba -H %f | autfilt -H >%O"
test 4 = `ltl2tgba -S 'F(a & X(!a &Xb))' --any --stats=%s` test 4 = `ltl2tgba -S 'F(a & X(!a &Xb))' --any --stats=%s`

16
tests/core/strength.test
View file

@ -22,8 +22,6 @@
set -e set -e
autfilt=autfilt
cat >in <<EOF cat >in <<EOF
HOA: v1 HOA: v1
name: "a U b" name: "a U b"
@ -113,7 +111,7 @@ State: 4
--END-- --END--
EOF EOF
run 0 $autfilt -H --check=strength in | tee out run 0 autfilt -H --check=strength in | tee out
cat >expected <<EOF cat >expected <<EOF
HOA: v1 HOA: v1
@ -221,12 +219,12 @@ EOF
diff out expected diff out expected
run 0 $autfilt -H --decompose-strength=t in | tee out.t run 0 autfilt -H --decompose-strength=t in | tee out.t
run 0 $autfilt -H --decompose-strength=w in | tee out.w run 0 autfilt -H --decompose-strength=w in | tee out.w
run 0 $autfilt -H --decompose-strength=s in | tee out.s run 0 autfilt -H --decompose-strength=s in | tee out.s
run 0 $autfilt -H --decompose-strength=tw in | tee out.tw run 0 autfilt -H --decompose-strength=tw in | tee out.tw
run 0 $autfilt -H --decompose-strength=ws in | tee out.ws run 0 autfilt -H --decompose-strength=ws in | tee out.ws
run 0 $autfilt -H --decompose-strength=tws in | tee out.tws run 0 autfilt -H --decompose-strength=tws in | tee out.tws
echo '/******************************/' > sep echo '/******************************/' > sep
cat out.t sep out.w sep out.s sep out.tw sep out.ws sep out.tws > out cat out.t sep out.w sep out.s sep out.tw sep out.ws sep out.tws > out

13
tests/core/stutter-ltl.test
View file

@ -1,6 +1,6 @@
#! /bin/sh #! /bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et # Copyright (C) 2013, 2014, 2015, 2017 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -24,9 +24,6 @@
set -e set -e
randltl=randltl
ltlfilt=ltlfilt
# Use time only if it is available # Use time only if it is available
time=time time=time
if ($time ls) >/dev/null 2>&1; then if ($time ls) >/dev/null 2>&1; then
@ -38,15 +35,15 @@ fi
FILE=formulae FILE=formulae
rm -f $FILE rm -f $FILE
for i in 10 12 14 16 18 20; do for i in 10 12 14 16 18 20; do
$randltl --seed 0 --tree-size $i a b c -n 100 >> $FILE randltl --seed 0 --tree-size $i a b c -n 100 >> $FILE
$randltl --seed 100 --tree-size $i a b c d e f -n 100 >> $FILE randltl --seed 100 --tree-size $i a b c d e f -n 100 >> $FILE
done done
# We do not check i=0 and i=9, as they are too slow. # We do not check i=0 and i=9, as they are too slow.
for i in 1 2 3 4 5 6 7 8; do for i in 1 2 3 4 5 6 7 8; do
SPOT_STUTTER_CHECK=$i SPOT_STUTTER_CHECK=$i
export SPOT_STUTTER_CHECK export SPOT_STUTTER_CHECK
$time $ltlfilt --stutter-invariant -F $FILE > res.$i $time ltlfilt --stutter-invariant -F $FILE > res.$i
done done
# All results should be equal # All results should be equal
@ -69,7 +66,7 @@ EOF
for i in 0 1 2 3 4 5 6 7 8 9; do for i in 0 1 2 3 4 5 6 7 8 9; do
SPOT_STUTTER_CHECK=$i SPOT_STUTTER_CHECK=$i
export SPOT_STUTTER_CHECK export SPOT_STUTTER_CHECK
$time $ltlfilt --stutter-invariant -F $FILE > res.$i $time ltlfilt --stutter-invariant -F $FILE > res.$i
done done
# All results should be equal # All results should be equal

53
tests/core/stutter-tgba.test
View file

@ -22,32 +22,29 @@
set -e set -e
ltl2tgba=ltl2tgba ltl2tgba '!FG(a | Xa | G!a)' -H | autfilt -H --destut > pos.hoa
autfilt=autfilt ltl2tgba 'FG(a | Xa | G!a)' -H | autfilt -H --destut > neg.hoa
autfilt pos.hoa --product neg.hoa -H > prod.hoa
autfilt --is-empty prod.hoa -q && exit 1
autfilt --states=7 prod.hoa -q
$ltl2tgba '!FG(a | Xa | G!a)' -H | $autfilt -H --destut > pos.hoa ltl2tgba '!FG(a | Xa | G!a)' -H | autfilt -H --instut > pos.hoa
$ltl2tgba 'FG(a | Xa | G!a)' -H | $autfilt -H --destut > neg.hoa ltl2tgba 'FG(a | Xa | G!a)' -H | autfilt -H --instut > neg.hoa
$autfilt pos.hoa --product neg.hoa -H > prod.hoa autfilt pos.hoa --product neg.hoa -H > prod.hoa
$autfilt --is-empty prod.hoa -q && exit 1 autfilt --is-empty prod.hoa -q && exit 1
$autfilt --states=7 prod.hoa -q autfilt --states=9 prod.hoa -q
$ltl2tgba '!FG(a | Xa | G!a)' -H | $autfilt -H --instut > pos.hoa
$ltl2tgba 'FG(a | Xa | G!a)' -H | $autfilt -H --instut > neg.hoa
$autfilt pos.hoa --product neg.hoa -H > prod.hoa
$autfilt --is-empty prod.hoa -q && exit 1
$autfilt --states=9 prod.hoa -q
# Check for issue #7. # Check for issue #7.
# #
# We just run those without checking the output, it is enough to # We just run those without checking the output, it is enough to
# trigger assertions in the HOA output routines. # trigger assertions in the HOA output routines.
$ltl2tgba -H 'X(a U b)' > det.hoa ltl2tgba -H 'X(a U b)' > det.hoa
run 0 $autfilt --destut det.hoa -H run 0 autfilt --destut det.hoa -H
run 0 $autfilt --instut=1 det.hoa -H run 0 autfilt --instut=1 det.hoa -H
run 0 $autfilt --instut=2 det.hoa -H run 0 autfilt --instut=2 det.hoa -H
$ltl2tgba -H 'a & Fb' | $autfilt --destut -H > output ltl2tgba -H 'a & Fb' | autfilt --destut -H > output
cat >expected <<EOF cat >expected <<EOF
HOA: v1 HOA: v1
@ -72,36 +69,36 @@ EOF
diff output expected diff output expected
$ltl2tgba -H 'F(a & X(!a & b))' > input ltl2tgba -H 'F(a & X(!a & b))' > input
grep ' stutter-invariant' input && exit 1 grep ' stutter-invariant' input && exit 1
run 0 $ltl2tgba --check=stutter 'F(a & X(!a & b))' > input.2 run 0 ltl2tgba --check=stutter 'F(a & X(!a & b))' > input.2
grep ' stutter-invariant' input.2 grep ' stutter-invariant' input.2
run 0 $autfilt --check=stutter input > input.2 run 0 autfilt --check=stutter input > input.2
grep ' stutter-invariant' input.2 grep ' stutter-invariant' input.2
$ltl2tgba 'F(a & X(a & b))' > input ltl2tgba 'F(a & X(a & b))' > input
grep stutter-invariant input && exit 1 grep stutter-invariant input && exit 1
# HOA v1.1 calls it "!stutter-invariant" # HOA v1.1 calls it "!stutter-invariant"
run 0 $ltl2tgba -H1.1 --check=stutter 'F(a & X(a & b))' > input.2 run 0 ltl2tgba -H1.1 --check=stutter 'F(a & X(a & b))' > input.2
grep '!stutter-invariant' input.2 grep '!stutter-invariant' input.2
# HOA v1 has no name, so we use "stutter-sensitive" # HOA v1 has no name, so we use "stutter-sensitive"
run 0 $autfilt --check=stutter input > input.2 run 0 autfilt --check=stutter input > input.2
test `autfilt -c -v --is-stutter-invariant input` = 1 test `autfilt -c -v --is-stutter-invariant input` = 1
grep stutter-sensitive input.2 grep stutter-sensitive input.2
$ltl2tgba 'F(a & X(!a & Gb))' > input ltl2tgba 'F(a & X(!a & Gb))' > input
grep stutter-invariant input && exit 1 grep stutter-invariant input && exit 1
grep deterministic input && exit 1 grep deterministic input && exit 1
# This will involve a complementation # This will involve a complementation
run 0 $autfilt --check=stutter input > input.2 run 0 autfilt --check=stutter input > input.2
test `autfilt -c --is-stutter-invariant input` = 1 test `autfilt -c --is-stutter-invariant input` = 1
grep ' stutter-invariant' input.2 grep ' stutter-invariant' input.2
$ltl2tgba 'F(a & X(a & Gb))' > input ltl2tgba 'F(a & X(a & Gb))' > input
grep stutter input && exit 1 grep stutter input && exit 1
grep deterministic input && exit 1 grep deterministic input && exit 1
# This will involve a complementation # This will involve a complementation
run 0 $autfilt -H1.1 --check=stutter input > input.2 run 0 autfilt -H1.1 --check=stutter input > input.2
test `autfilt -c --is-stutter-invariant input` = 0 test `autfilt -c --is-stutter-invariant input` = 0
grep '!deterministic' input.2 grep '!deterministic' input.2
grep '!stutter-invariant' input.2 grep '!stutter-invariant' input.2

8
tests/core/unabbrevwm.test
View file

@ -1,6 +1,6 @@
#! /bin/sh #! /bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2012, 2015 Laboratoire de Recherche et Développement # Copyright (C) 2012, 2015, 2017 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.
@ -25,10 +25,8 @@
set -e set -e
ltlfilt=ltlfilt
# Removing W,M in this formula caused a segfault at some point. # Removing W,M in this formula caused a segfault at some point.
run 0 $ltlfilt --remove-wm >out <<EOF run 0 ltlfilt --remove-wm >out <<EOF
(!((G(p0)) U ((F(p0)) M ((F(X(p1))) & ((p2) W (G(p2))))))) M (F(p0)) (!((G(p0)) U ((F(p0)) M ((F(X(p1))) & ((p2) W (G(p2))))))) M (F(p0))
(Fp0 U(Fp0&!(Gp0 U((FXp1 &(Gp2 R(p2|Gp2))) U(Fp0&FXp1&(Gp2 R(p2|Gp2))))))) (Fp0 U(Fp0&!(Gp0 U((FXp1 &(Gp2 R(p2|Gp2))) U(Fp0&FXp1&(Gp2 R(p2|Gp2)))))))
EOF EOF
@ -40,7 +38,7 @@ test `uniq out | wc -l` = 1
for i in 'GFa' 'a R b' 'a W b' 'a M b'; do for i in 'GFa' 'a R b' 'a W b' 'a M b'; do
for fg in '' F G GF; do for fg in '' F G GF; do
for rwm in '' R W M RW RM WM RWM; do for rwm in '' R W M RW RM WM RWM; do
$ltlfilt -f "$i" --unabbrev=$fg$rwm --equivalent-to "$i" >out ltlfilt -f "$i" --unabbrev=$fg$rwm --equivalent-to "$i" >out
test -n "$rwm" && grep "[$rwm]" out && exit 1 test -n "$rwm" && grep "[$rwm]" out && exit 1
done done
done done

27
tests/core/unambig.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2013, 2015, 2016 Laboratoire de Recherche et # Copyright (C) 2013, 2015-2017 Laboratoire de Recherche et
# Developpement de l'Epita # Developpement de l'Epita
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -22,9 +22,6 @@
set -e set -e
ltl2tgba=ltl2tgba
autfilt=autfilt
for f in 'Ga' \ for f in 'Ga' \
'Ga | Gb' \ 'Ga | Gb' \
'Ga | GFb' \ 'Ga | GFb' \
@ -34,18 +31,18 @@ for f in 'Ga' \
'F(a & !b & (!c W b))' \ 'F(a & !b & (!c W b))' \
'G({{1;1}*}<>->a)' 'G({{1;1}*}<>->a)'
do do
$ltl2tgba -UH "$f" | $autfilt -q --is-unambiguous ltl2tgba -UH "$f" | autfilt -q --is-unambiguous
$ltl2tgba -UH "!($f)" | $autfilt -q --is-unambiguous ltl2tgba -UH "!($f)" | autfilt -q --is-unambiguous
$ltl2tgba -UH "$f" | $autfilt --check | ltl2tgba -UH "$f" | autfilt --check |
grep -E 'properties:.* (unambiguous|deterministic)' grep -E 'properties:.* (unambiguous|deterministic)'
$ltl2tgba -UH "!($f)" | $autfilt --check | ltl2tgba -UH "!($f)" | autfilt --check |
grep -E 'properties:.* (unambiguous|deterministic)' grep -E 'properties:.* (unambiguous|deterministic)'
done done
for f in FGa '{[*1..4]}<>-> (p1 & (p1 U p0))' for f in FGa '{[*1..4]}<>-> (p1 & (p1 U p0))'
do do
$ltl2tgba -H "$f" | $autfilt -qv --is-unambiguous ltl2tgba -H "$f" | autfilt -qv --is-unambiguous
$ltl2tgba -UH "$f" | $autfilt -q --is-unambiguous ltl2tgba -UH "$f" | autfilt -q --is-unambiguous
done done
# All these should be detected as ambiguous automata # All these should be detected as ambiguous automata
@ -147,13 +144,13 @@ State: 2
--END-- --END--
EOF EOF
run 1 $autfilt -q --is-unambiguous input run 1 autfilt -q --is-unambiguous input
run 0 $autfilt --check input > output run 0 autfilt --check input > output
test `grep -c unambiguous output` = 0 test `grep -c unambiguous output` = 0
# Check 1000 random PSL formulas # Check 1000 random PSL formulas
randltl --psl -n 1000 3 | $ltl2tgba -U -H | randltl --psl -n 1000 3 | ltl2tgba -U -H |
$autfilt -v --is-unamb --stats=%M && exit 1 autfilt -v --is-unamb --stats=%M && exit 1
cat >input <<EOF cat >input <<EOF
HOA: v1 HOA: v1
@ -194,7 +191,7 @@ ltl2tgba --lbt-input -B -U -x wdba-minimize=0 "U p0 & p1 X ! p0" |
# Make sure we preserve the "unambiguous" property if it is given. # Make sure we preserve the "unambiguous" property if it is given.
run 0 $autfilt -H --is-unambiguous input >output run 0 autfilt -H --is-unambiguous input >output
cat >expected <<EOF cat >expected <<EOF
HOA: v1 HOA: v1