From 1dd2ce3ae24d9324e1c521ff0e4fa020afc4c9be Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 11 Mar 2025 09:29:31 +0100
Subject: [PATCH] sanity: improve bin.test

* 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.
---
 bin/ltlsynt.cc        | 20 +++++++++-----------
 spot.spec.in          |  4 +++-
 tests/sanity/bin.test | 20 +++++++++++++++++++-
 3 files changed, 31 insertions(+), 13 deletions(-)

diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index 4b5858c01..1b741fa9a 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -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},
diff --git a/spot.spec.in b/spot.spec.in
index bd465fd62..a2630d2de 100755
--- a/spot.spec.in
+++ b/spot.spec.in
@@ -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
 
diff --git a/tests/sanity/bin.test b/tests/sanity/bin.test
index 6e9e5eafb..0ad836daa 100644
--- a/tests/sanity/bin.test
+++ b/tests/sanity/bin.test
@@ -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