diff --git a/bin/common_post.cc b/bin/common_post.cc index fdb1dc903..7bead8135 100644 --- a/bin/common_post.cc +++ b/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; 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/core/parity2.test b/tests/core/parity2.test index 8fb35e365..b2b95f790 100755 --- a/tests/core/parity2.test +++ b/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<expected5 < XXXb)' -f '(p0 W XXGp0) & GFp1 & FGp2' 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