diff --git a/NEWS b/NEWS index e64d2eda9..ab3a26455 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,32 @@ New in spot 2.0.3a (not yet released) Command-line tools: + * All tools that input formulas or automata (i.e., autfilt, + dstar2tgba, ltl2tgba, ltl2tgta, ltlcross, ltldo, ltlfilt, + ltlgrind) now have a more homogeneous handling of the default + input. + + - If no formula/automaton have been specified, and the standard + input is a not a tty, then the default is to read that. This is a + change for ltl2tgba and ltl2tgta. In particular, it simplifies + + genltl --dac | ltl2tgba -F- | autfilt ... + + into + + genltl --dac | ltl2tgba | autfilt ... + + - If standard input is a tty and no other input has been + specified, then an error message is printed. This is a change for + autfilt, dstar2tgba, ltlcross, ltldo, ltlfilt, ltlgrind, that used + to expect the user to type formula or automata at the terminal, + confusing people. + + - All tools now accept - as a shorthand for -F-, to force reading + input from the standard input (regardless of whether it is a tty + or not). This is a change for ltl2tgba, ltl2tgta, ltlcross, and + ltldo. + * ltldo has a new option --errors=... to specify how to deal with errors from executed tools. diff --git a/bin/autfilt.cc b/bin/autfilt.cc index eb7f111e1..d18cd6b53 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -1116,8 +1116,7 @@ main(int argc, char** argv) if (pref_set && !level_set) level = spot::postprocessor::High; - if (jobs.empty()) - jobs.emplace_back("-", true); + check_no_automaton(); if (opt->are_isomorphic) { diff --git a/bin/common_finput.cc b/bin/common_finput.cc index 599d0c394..78f556e70 100644 --- a/bin/common_finput.cc +++ b/bin/common_finput.cc @@ -18,10 +18,12 @@ // along with this program. If not, see . #include "common_finput.hh" +#include "common_setup.hh" #include "error.h" #include #include +#include enum { OPT_LBT = 1, @@ -353,3 +355,25 @@ job_processor::run() } return error; } + +void check_no_formula() +{ + if (!jobs.empty()) + return; + if (isatty(STDIN_FILENO)) + error(2, 0, "No formula to translate? Run '%s --help' for help.\n" + "Use '%s -' to force reading formulas from the standard " + "input.", program_name, program_name); + jobs.emplace_back("-", true); +} + +void check_no_automaton() +{ + if (!jobs.empty()) + return; + if (isatty(STDIN_FILENO)) + error(2, 0, "No automaton to process? Run '%s --help' for help.\n" + "Use '%s -' to force reading automata from the standard " + "input.", program_name, program_name); + jobs.emplace_back("-", true); +} diff --git a/bin/common_finput.hh b/bin/common_finput.hh index 0c4b3d459..41eaa0216 100644 --- a/bin/common_finput.hh +++ b/bin/common_finput.hh @@ -77,3 +77,8 @@ public: char* prefix; char* suffix; }; + +// Report and error message or add a default job depending on whether +// the input is a tty. +void check_no_formula(); +void check_no_automaton(); diff --git a/bin/dstar2tgba.cc b/bin/dstar2tgba.cc index b0a3e066b..ec51b5743 100644 --- a/bin/dstar2tgba.cc +++ b/bin/dstar2tgba.cc @@ -180,8 +180,7 @@ main(int argc, char** argv) if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) exit(err); - if (jobs.empty()) - jobs.emplace_back("-", true); + check_no_automaton(); spot::postprocessor post(&extra_options); post.set_pref(pref | comp | sbacc); diff --git a/bin/ltl2tgba.cc b/bin/ltl2tgba.cc index da84dbb47..7096bbc35 100644 --- a/bin/ltl2tgba.cc +++ b/bin/ltl2tgba.cc @@ -97,7 +97,10 @@ parse_opt(int key, char* arg, struct argp_state*) break; case ARGP_KEY_ARG: // FIXME: use stat() to distinguish filename from string? - jobs.emplace_back(arg, false); + if (*arg == '-' && !arg[1]) + jobs.emplace_back(arg, true); + else + jobs.emplace_back(arg, false); break; default: @@ -164,9 +167,7 @@ main(int argc, char** argv) if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) exit(err); - if (jobs.empty()) - error(2, 0, "No formula to translate? Run '%s --help' for usage.", - program_name); + check_no_formula(); try { diff --git a/bin/ltl2tgta.cc b/bin/ltl2tgta.cc index 7b73e0668..68c3b934c 100644 --- a/bin/ltl2tgta.cc +++ b/bin/ltl2tgta.cc @@ -24,6 +24,7 @@ #include #include +#include #include "error.h" #include "common_setup.hh" @@ -147,7 +148,10 @@ parse_opt(int key, char* arg, struct argp_state*) break; case ARGP_KEY_ARG: // FIXME: use stat() to distinguish filename from string? - jobs.emplace_back(arg, false); + if (*arg == '-' && !arg[1]) + jobs.emplace_back(arg, true); + else + jobs.emplace_back(arg, false); break; default: @@ -226,9 +230,7 @@ main(int argc, char** argv) if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) exit(err); - if (jobs.empty()) - error(2, 0, "No formula to translate? Run '%s --help' for usage.", - program_name); + check_no_formula(); try { diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index dd5439b16..b9beaf8ad 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -408,7 +408,10 @@ parse_opt(int key, char* arg, struct argp_state*) products = 0; break; case ARGP_KEY_ARG: - translators.push_back(arg); + if (arg[0] == '-' && !arg[1]) + jobs.emplace_back(arg, true); + else + translators.push_back(arg); break; case OPT_AUTOMATA: opt_automata = true; @@ -1443,8 +1446,7 @@ main(int argc, char** argv) if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) exit(err); - if (jobs.empty()) - jobs.emplace_back("-", 1); + check_no_formula(); if (translators.empty()) error(2, 0, "No translator to run? Run '%s --help' for usage.", diff --git a/bin/ltldo.cc b/bin/ltldo.cc index c191ae9c2..313858ebb 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -146,7 +146,10 @@ parse_opt(int key, char* arg, struct argp_state*) errors_opt = XARGMATCH("--errors", arg, errors_args, errors_types); break; case ARGP_KEY_ARG: - translators.push_back(arg); + if (arg[0] == '-' && !arg[1]) + jobs.emplace_back(arg, true); + else + translators.push_back(arg); break; default: return ARGP_ERR_UNKNOWN; @@ -356,8 +359,7 @@ main(int argc, char** argv) if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) exit(err); - if (jobs.empty()) - jobs.emplace_back("-", 1); + check_no_formula(); if (translators.empty()) error(2, 0, "No translator to run? Run '%s --help' for usage.", diff --git a/bin/ltlgrind.cc b/bin/ltlgrind.cc index 84bac6665..978000125 100644 --- a/bin/ltlgrind.cc +++ b/bin/ltlgrind.cc @@ -189,8 +189,7 @@ main(int argc, char* argv[]) mut_opts |= opt_all; - if (jobs.empty()) - jobs.push_back(job("-", true)); + check_no_formula(); mutate_processor processor; if (processor.run()) diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 316ce6eed..4cd3e2f68 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -739,7 +739,7 @@ of the form =cycle{b}=, and display the associated formula (which was stored as the name of the automaton by =ltl2tgba=). #+BEGIN_SRC sh :results verbatim :exports both -randltl -n -1 a b | ltlfilt --simplify --uniq | ltl2tgba -F- | +randltl -n -1 a b | ltlfilt --simplify --uniq | ltl2tgba | autfilt --accept-word='a&!b;cycle{!a&!b}' --accept-word='!a&!b;cycle{a&b}' \ --reject-word='cycle{b}' --stats=%M -n 10 #+END_SRC diff --git a/doc/org/csv.org b/doc/org/csv.org index 4a4d6e37d..0cee75f18 100644 --- a/doc/org/csv.org +++ b/doc/org/csv.org @@ -45,7 +45,7 @@ formulas, and show the resulting number of states (=%s=) and edges (=%e=) of the automaton constructed for each formula. #+BEGIN_SRC sh :results verbatim :exports both -genltl --and-gf=1..5 --u-left=1..5 | ltl2tgba -F- --stats '%f,%s,%e' +genltl --and-gf=1..5 --u-left=1..5 | ltl2tgba --stats '%f,%s,%e' #+END_SRC #+RESULTS: #+begin_example diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index 7a64539e8..9c69cd49e 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -421,9 +421,9 @@ For instance here is a complex command that will 1. generate an infinite stream of random LTL formulas with [[file:randltl.org][=randltl=]], 2. use [[file:ltlfilt.org][=ltlfilt=]] to rewrite the W and M operators away (=--remove-wm=), simplify the formulas (=-r=), remove duplicates (=u=) as well as - formulas that have a size less then 3 (=--size-min=3=), -3. use =head= to keep only 10 of such formula -4. loop to process each of these formula: + formulas that have a size less then 3 (=--size-min=3=), and + keep only the 10 first formulas (=-n 10=) +3. loop to process each of these formula: - print it - then convert the formula into =ltl2dstar='s input format, process it with =ltl2dstar= (using =ltl2tgba= as the actual LTL->BA @@ -438,8 +438,7 @@ deterministic, and =%p= whether the automaton is complete. #+BEGIN_SRC sh :results verbatim :exports both randltl -n -1 --tree-size=10..14 a b c | -ltlfilt --remove-wm -r -u --size-min=3 | -head -n 10 | +ltlfilt --remove-wm -r -u --size-min=3 -n 10 | while read f; do echo "$f" ltlfilt -l -f "$f" | diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index d85e2cead..9552f7bc4 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -835,7 +835,7 @@ For instance we can study the size of the automata generated for the right-nested =U= formulas as follows: #+BEGIN_SRC sh :results verbatim :exports both -genltl --u-right=1..8 | ltl2tgba -F - --stats '%s states and %e edges for "%f"' +genltl --u-right=1..8 | ltl2tgba --stats '%s states and %e edges for "%f"' #+END_SRC #+RESULTS: : 2 states and 2 edges for "p1" @@ -847,7 +847,11 @@ genltl --u-right=1..8 | ltl2tgba -F - --stats '%s states and %e edges for "%f"' : 7 states and 28 edges for "p1 U (p2 U (p3 U (p4 U (p5 U (p6 U p7)))))" : 8 states and 36 edges for "p1 U (p2 U (p3 U (p4 U (p5 U (p6 U (p7 U p8))))))" -Here =-F -= means that formulas should be read from the standard input. +Note that because no formula have been passed as argument to +=ltl2tgba=, it defaulted to reading them from standard input. Such a +behaviour can be requested explicitly with =-F -= if needed (e.g., to +read from standard input in addition to processing other formula +supplied with =-f=). When computing the size of an automaton, we distinguish /transitions/ and /edges/. An edge between two states is labeled by a Boolean diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 22c716f24..50cafdeb6 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -44,8 +44,9 @@ The core of =ltlcross= is a loop that does the following steps: * Formula selection -Formulas to translate should be specified using the [[file:ioltl.org][common input options]]. -Standard input is read if no =-f= or =-F= option is given. +Formulas to translate should be specified using the [[file:ioltl.org][common input +options]]. Standard input is read if it is not connected to a terminal, +and no =-f= or =-F= options are given. * Configuring translators diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index cf5bca47d..d662b505c 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -15,8 +15,9 @@ formulas.) It can be used to perform a number of tasks. Essentially: Because it read and write formulas, =ltlfilt= accepts all the [[file:ioltl.org][common input and output options]]. -Additionally, if no =-f= or =-F= option is specified, =ltlfilt= -will read formulas from the standard input. +Additionally, if no =-f= or =-F= option is specified, and =ltlfilt= +will read formulas from the standard input if it is not connected to a +terminal. For instance the following will convert two LTL formulas expressed using infix notation (with different names supported for the same diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 9572ae377..6854b72dd 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -1015,18 +1015,18 @@ using =autfilt -n5=. #+BEGIN_SRC sh :results verbatim :exports both randltl -n -1 a b | -ltl2tgba -F- | +ltl2tgba | autfilt --states=3 --stats='!(%M)' | -ltl2tgba -F- | +ltl2tgba | autfilt --states=3 --stats=%M -n5 #+END_SRC #+RESULTS: -: G(F!a & XF(a | G!b)) -: GFb | G(!b & FG!b) -: !a & F((a | b) & (!a | !b)) -: !a | (b R a) -: !b & X(!b U a) +: G(b | F(b & Fa)) +: (!a | b | (!b & (b W Ga))) & (a | (!b & (b | (!b M F!a)))) +: (!a | (!a R b)) & (a | (a U !b)) +: !a & F((!a | FG!a) & (a | GFa)) +: X(!b W a) Note that the above result can also be obtained without using =autfilt= and automata names. We can use the fact that =ltl2tgba @@ -1045,13 +1045,15 @@ head -n5 | cut -d, -f2 # return the five first formulas #+END_SRC #+RESULTS: -: G(F!a & XF(a | G!b)) -: GFb | G(!b & FG!b) -: !a & F((!a | !b) & (a | b)) -: !a | (b R a) -: !b & X(!b U a) - +: G(b | F(b & Fa)) +: (!a | b | (!b & (b W Ga))) & (a | (!b & (b | (!b M F!a)))) +: (!a | (!a R b)) & (a | (a U !b)) +: !a & F((!a | FG!a) & (a | GFa)) +: X(!b W a) +Note that the =-F-= argument in the first call to =ltl2tgba= is +superfluous as the tool default to reading from its standard input. +But we put it there for symmetry with the second call. # LocalWords: num toc html syntaxes ltl tgba sed utf UTF lbtt SCCs # LocalWords: GraphViz's hoaf HOA LBTT's neverclaim ba SPOT's Gb cn diff --git a/tests/core/acc_word.test b/tests/core/acc_word.test index 8a9b195c3..01a61607c 100644 --- a/tests/core/acc_word.test +++ b/tests/core/acc_word.test @@ -34,7 +34,7 @@ ltl2tgba -f 'a U b' | ltl2tgba -f 'a U b' | autfilt --accept-word='cycle{!b}' -q && exit 1 # An example from the documentation: -randltl -n -1 a b | ltlfilt --simplify --uniq | ltl2tgba -F- | +randltl -n -1 a b | ltlfilt --simplify --uniq | ltl2tgba | autfilt --accept-word='a&!b;cycle{!a&!b}' --accept-word='!a&!b;cycle{a&b}' \ --reject-word='cycle{b}' --stats=%M -n 3 > out cat >expect <output 2>stderr test -z "`cat output`" test 4 = `grep -c warning: stderr` diff --git a/tests/core/minusx.test b/tests/core/minusx.test index 41829a2be..96a518034 100755 --- a/tests/core/minusx.test +++ b/tests/core/minusx.test @@ -22,7 +22,7 @@ set -e # make sure option -x reports unknown arguments -ltl2tgba -F- -x foo error && exit 1 +ltl2tgba - -x foo error && exit 1 grep "ltl2tgba: option 'foo' was not used" error ltl2tgba -F- -x ba-simul,foo,bar error && exit 1 grep -v 'ba-simul' error diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 567494549..25d7b4639 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -115,9 +115,8 @@ diff stdout stdout2 # exercise both %M and %m. The nonexistant file should never be # open, because the input stream is infinite and autfilt should # stop after 10 automata. -randltl -n -1 a b | - ltl2tgba -H -F - | - autfilt -F- -F nonexistant --states=3 --edges=..10 --acc-sets=1.. \ +randltl -n -1 a b | ltl2tgba | + autfilt -F - -F nonexistant --states=3 --edges=..10 --acc-sets=1.. \ --name='%M, %S states' --stats='<%m>, %e, %a' -n 10 > output cat >expected <, 5, 1 @@ -278,7 +277,7 @@ autfilt --merge -Hm input --name="%E->%e edges, %T->%t transitions" > output diff output expected -cat < tmp.hoa +ltl2tgba -x degen-lskip=1 --ba > tmp.hoa < output test `grep -c unambiguous output` = 0 # Check 1000 random PSL formulas -randltl --psl -n 1000 3 | $ltl2tgba -U -F- -H | +randltl --psl -n 1000 3 | $ltl2tgba -U -H | $autfilt -v --is-unamb --stats=%M && exit 1 cat >input <