merge

* flake.nix, flake.lock: here

bin/common_post.cc

@@ -231,7 +231,14 @@ parse_opt_post(int key, char* arg, struct argp_state*)
         if (arg)
           type = XARGMATCH(key == 'P' ? "--parity" : "--colored-parity",
                            arg, parity_args, parity_types);
-        else
+        else if (!(type & spot::postprocessor::Parity))
+          // If no argument was given, we just require Parity.
+          // However, if a Parity condition was already set before,
+          // don't overwrite it.  This way if someone mistakenly write
+          // `--parity='max even' --colored` without realizing that
+          // `--colored` is just the abbreviation for
+          // `--colored-parity=...` with the default argument, we
+          // won't reset the 'max even' setting.
           type = spot::postprocessor::Parity;
         if (key == 'p')
           colored = spot::postprocessor::Colored;

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:"
+      "choose the algorithm for synthesis:\n"
-      " \"sd\": translate to tgba, split, then determinize;"
+      "  sd: translate to TGBA, split, determinize\n"
-      " \"ds\": translate to tgba, determinize, then split;"
+      "  ds: translate to TGBA, determinize, split\n"
-      " \"ps\": translate to dpa, then split;"
+      "  ps: translate to DPA, split\n"
-      " \"lar\": translate to a deterministic automaton with arbitrary"
+      "  lar: translate to a deterministic TELA, convert to DPA"
-      " acceptance condition, then use LAR to turn to parity,"
+      " with LAR, split (default)\n"
-      " then split (default);"
+      "  lar.old: old version of LAR, for benchmarking;\n"
-      " \"lar.old\": old version of LAR, for benchmarking;"
+      "  acd: translate to a deterministic TELA, convert to DPA"
-      " \"acd\": translate to a deterministic automaton with arbitrary"
+      " with ACD, split", 0 },
-      " acceptance condition, then use ACD to turn to parity,"
-      " then split.\n", 0 },
     { "bypass", OPT_BYPASS, "yes|no", 0,
       "whether to try to avoid to construct a parity game "
       "(enabled by default)", 0},

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
 

tests/core/parity2.test

@@ -26,7 +26,19 @@ for x in P 'Pmin odd' 'Pmax even' p 'pmin odd' 'pmax even'; do
     autfilt --name=%M --high "-$x" >>res2
   ltl2tgba -D "-$x" FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' >>res3
   ltl2tgba FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' |
-    autfilt -D --name=%M --high "-$x" >>res4
+      autfilt -D --name=%M --high "-$x" >>res4
+  (
+      ## --colored is normally short for --colored-parity=any
+      ## But in case someone types something like
+      ##   --parity='max odd' --colored
+      ## let's make sure we handle it like --colored-parity='max odd'.
+      echo "=== -$x ==="
+      ltl2tgba FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' \
+               "-$x" --stats='%[]g'
+      echo "=== -$x --colored ==="
+      ltl2tgba FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' \
+               "-$x" --colored --stats='%[]g'
+  ) >> res5
 done
 
 cat >expected<<EOF
@@ -1423,6 +1435,58 @@ State: 4
 EOF
 diff expected4 res4
 
+cat >expected5 <<EOF
+=== -P ===
+co-Buchi
+Buchi
+Rabin 1
+=== -P --colored ===
+parity max even 2
+Streett 1
+parity min odd 3
+=== -Pmin odd ===
+co-Buchi
+Rabin 1
+Rabin 1
+=== -Pmin odd --colored ===
+Rabin 1
+parity min odd 3
+parity min odd 3
+=== -Pmax even ===
+parity max even 2
+Buchi
+parity max even 2
+=== -Pmax even --colored ===
+parity max even 2
+parity max even 3
+parity max even 4
+=== -p ===
+parity max even 2
+Streett 1
+parity min odd 3
+=== -p --colored ===
+parity max even 2
+Streett 1
+parity min odd 3
+=== -pmin odd ===
+Rabin 1
+parity min odd 3
+parity min odd 3
+=== -pmin odd --colored ===
+Rabin 1
+parity min odd 3
+parity min odd 3
+=== -pmax even ===
+parity max even 2
+parity max even 3
+parity max even 4
+=== -pmax even --colored ===
+parity max even 2
+parity max even 3
+parity max even 4
+EOF
+diff expected5 res5
+
 ltlcross 'ltl2tgba -P' 'ltl2tgba -P"odd max"' 'ltl2tgba -P"even min"' \
          'ltl2tgba -p' 'ltl2tgba -p"odd max"' 'ltl2tgba -p"even min"' \
          -f FGa -f 'GFa&GFb' -f 'GF(a <-> XXXb)' -f '(p0 W XXGp0) & GFp1 & FGp2'

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