merge

The previous implementation was wrong and led to segfaults when sorting
large expansions

bin/common_post.cc

@@ -231,14 +231,7 @@ 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 if (!(type & spot::postprocessor::Parity))
+        else
-          // 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,15 +91,17 @@ 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:\n"
+      "choose the algorithm for synthesis:"
-      "  sd: translate to TGBA, split, determinize\n"
+      " \"sd\": translate to tgba, split, then determinize;"
-      "  ds: translate to TGBA, determinize, split\n"
+      " \"ds\": translate to tgba, determinize, then split;"
-      "  ps: translate to DPA, split\n"
+      " \"ps\": translate to dpa, then split;"
-      "  lar: translate to a deterministic TELA, convert to DPA"
+      " \"lar\": translate to a deterministic automaton with arbitrary"
-      " with LAR, split (default)\n"
+      " acceptance condition, then use LAR to turn to parity,"
-      "  lar.old: old version of LAR, for benchmarking;\n"
+      " then split (default);"
-      "  acd: translate to a deterministic TELA, convert to DPA"
+      " \"lar.old\": old version of LAR, for benchmarking;"
-      " with ACD, split", 0 },
+      " \"acd\": translate to a deterministic automaton with arbitrary"
+      " 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,7 +38,6 @@ logic (LTL & PSL).
 %{_bindir}/ltldo
 %{_bindir}/ltlfilt
 %{_bindir}/ltlgrind
-%{_bindir}/ltlmix
 %{_bindir}/ltlsynt
 %{_bindir}/randaut
 %{_bindir}/randltl
@@ -53,12 +52,11 @@ 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.7*
 %{_mandir}/man7/spot-x.7*
+%{_mandir}/man7/spot.7*
 %license COPYING
 %doc AUTHORS COPYING NEWS README THANKS
 

tests/core/parity2.test

@@ -26,19 +26,7 @@ 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
@@ -1435,58 +1423,6 @@ 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,11 +52,6 @@ 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
@@ -79,7 +74,7 @@ do
             ;;
     esac
 
-    # All tools
+    # All man pages
     case $manpage in
         *.1)
             if ! test -f $top_srcdir/doc/org/$binary.org; then
@@ -99,20 +94,8 @@ 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.
@@ -124,7 +107,6 @@ 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