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

sanity: improve bin.test

Browse source 
* tests/sanity/bin.test: Add missing exit status on error,
and report manpage and binaries missing from spot.spec.in.
* spot.spec.in: Add ltlmix and ltlmix.1.
* bin/ltlsynt.cc: Fix formating for --algo.
This commit is contained in:
Alexandre Duret-Lutz 2025-03-11 09:29:31 +01:00
parent c4e3509d18
commit 1dd2ce3ae2
3 changed files with 31 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

20
bin/ltlsynt.cc
View file

@ -91,17 +91,15 @@ static const argp_option options[] =
/**************************************************/
{ nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
{ "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old|acd", 0,
"choose the algorithm for synthesis:"
" \"sd\": translate to tgba, split, then determinize;"
" \"ds\": translate to tgba, determinize, then split;"
" \"ps\": translate to dpa, then split;"
" \"lar\": translate to a deterministic automaton with arbitrary"
" acceptance condition, then use LAR to turn to parity,"
" then split (default);"
" \"lar.old\": old version of LAR, for benchmarking;"
" \"acd\": translate to a deterministic automaton with arbitrary"
" acceptance condition, then use ACD to turn to parity,"
" then split.\n", 0 },
"choose the algorithm for synthesis:\n"
" sd: translate to TGBA, split, determinize\n"
" ds: translate to TGBA, determinize, split\n"
" ps: translate to DPA, split\n"
" lar: translate to a deterministic TELA, convert to DPA"
" with LAR, split (default)\n"
" lar.old: old version of LAR, for benchmarking;\n"
" acd: translate to a deterministic TELA, convert to DPA"
" with ACD, split", 0 },
{ "bypass", OPT_BYPASS, "yes|no", 0,
"whether to try to avoid to construct a parity game "
"(enabled by default)", 0},

4
spot.spec.in
View file

@ -38,6 +38,7 @@ logic (LTL & PSL).
%{_bindir}/ltldo
%{_bindir}/ltlfilt
%{_bindir}/ltlgrind
%{_bindir}/ltlmix
%{_bindir}/ltlsynt
%{_bindir}/randaut
%{_bindir}/randltl
@ -52,11 +53,12 @@ logic (LTL & PSL).
%{_mandir}/man1/ltldo.1*
%{_mandir}/man1/ltlfilt.1*
%{_mandir}/man1/ltlgrind.1*
%{_mandir}/man1/ltlmix.1*
%{_mandir}/man1/ltlsynt.1*
%{_mandir}/man1/randaut.1*
%{_mandir}/man1/randltl.1*
%{_mandir}/man7/spot-x.7*
%{_mandir}/man7/spot.7*
%{_mandir}/man7/spot-x.7*
%license COPYING
%doc AUTHORS COPYING NEWS README THANKS

20
tests/sanity/bin.test
View file

@ -52,6 +52,11 @@ do
echo "bin/man/$manpage is not listed in man/Makefile.am"
exit_status=2
fi
if ! grep -q "%{_mandir}/man./$manpage\*\$" $top_srcdir/spot.spec.in;
then
echo "$manpage is not listed in spot.spec.in"
exit_status=2
fi
fi
case $binary in
@ -74,7 +79,7 @@ do
;;
esac
# All man pages
# All tools
case $manpage in
*.1)
if ! test -f $top_srcdir/doc/org/$binary.org; then
@ -94,8 +99,20 @@ do
echo "$binary does not occur in doc/org/arch.tex"
exit_status=2
fi
if ! grep -q "%{_bindir}/$binary\$" $top_srcdir/spot.spec.in; then
echo "$binary does is not listed in spot.spec.in";
exit_status=2
fi
esac
if test -f $top_srcdir/bin/.gitignore; then
if ! grep -q "^$binary\$" $top_srcdir/bin/.gitignore; then
echo "$binary is not listed in bin/.gitignore"
exit_status=2
fi
fi
# Check --help text. Set a high rmargin to workaround some
# bug in argp where an extra line it sometimes added if the end
# of the document string fall right into the rmargin.
@ -107,6 +124,7 @@ do
echo "bin/$binary --help has options after blank line;" \
"missing section header?"
cat help-err
exit_status=2
fi
rm -f help-$binary.tmp help-err