diff --git a/bin/common_post.cc b/bin/common_post.cc index 7bead8135..fdb1dc903 100644 --- a/bin/common_post.cc +++ b/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)) - // 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. + else type = spot::postprocessor::Parity; if (key == 'p') colored = spot::postprocessor::Colored; diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 1b741fa9a..4b5858c01 100644 --- a/bin/ltlsynt.cc +++ b/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" - " 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 }, + "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 }, { "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 a2630d2de..bd465fd62 100755 --- a/spot.spec.in +++ b/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 diff --git a/tests/core/parity2.test b/tests/core/parity2.test index b2b95f790..8fb35e365 100755 --- a/tests/core/parity2.test +++ b/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 - ( - ## --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 + autfilt -D --name=%M --high "-$x" >>res4 done cat >expected<expected5 < XXXb)' -f '(p0 W XXGp0) & GFp1 & FGp2' diff --git a/tests/sanity/bin.test b/tests/sanity/bin.test index 0ad836daa..6e9e5eafb 100644 --- a/tests/sanity/bin.test +++ b/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