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

genltl: improve coverage

Browse source 
* tests/core/genltl.test: here
* spot/gen/formulas.cc: typo
This commit is contained in:
Maximilien Colange 2018-05-23 16:56:29 +02:00
parent 321230f869
commit 61b2b9b140
2 changed files with 31 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
spot/gen/formulas.cc
View file

@ -1011,7 +1011,7 @@ namespace spot
int k = ceil(log2(n)) + (n == 1);
if (n <= 0)
bad_number("kr1-exp", n);
bad_number("kr-nlogn", n);
formula fa = formula::ap(a);
formula fb = formula::ap(b);

31
tests/core/genltl.test
View file

@ -87,7 +87,6 @@ diff expected output
genltl --dac=1..5 --eh=1..5 >output2
diff output output2
genltl --tv-f1=1:3 --tv-f2=1:3 --tv-g1=1:3 --tv-g2=1:3 --tv-uu=1:3 \
--format=%F,%L,%f >output
cat >expected <<EOF
@ -175,3 +174,33 @@ genltl --ms-example=0..4 --ms-phi-r=0..2 --ms-phi-s=0..2 --ms-phi-h=0..4 \
--gf-equiv=0..5 --gf-implies=0..5 --format=%F=%L,%f |
ltldo -F-/2 'ltl2tgba -G -D' --stats='%<,%s' > out
diff out exp
# Test out-of-range conditions
genltl --dac-patterns=0 2> err && exit 1
test $? = 2
test "`cat err`" = "genltl: no pattern dac-patterns=0, supported range is 1..55"
genltl --eh-patterns=0 2> err && exit 1
test $? = 2
test "`cat err`" = "genltl: no pattern eh-patterns=0, supported range is 1..12"
genltl --hkrss-patterns=0 2> err && exit 1
test $? = 2
test "`cat err`" = \
"genltl: no pattern hkrss-patterns=0, supported range is 1..55"
genltl --kr-n=0 2> err && exit 1
test $? = 2
test "`cat err`" = "genltl: no pattern kr-n=0, supported range is 1.."
genltl --kr-nlogn=0 2> err && exit 1
test $? = 2
test "`cat err`" = "genltl: no pattern kr-nlogn=0, supported range is 1.."
genltl --p-patterns=0 2> err && exit 1
test $? = 2
test "`cat err`" = "genltl: no pattern p-patterns=0, supported range is 1..20"
genltl --sb-patterns=0 2> err && exit 1
test $? = 2
test "`cat err`" = "genltl: no pattern sb-patterns=0, supported range is 1..27"