From 78def4f8cad41d191f1e5447099b16cfdb9be83c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 15 Feb 2015 23:50:48 +0100 Subject: [PATCH] bin: add the --output to tools that output formulas * src/bin/common_output.cc, src/bin/common_output.hh: Add option --output. * src/ltltest/ltlfilt.test, src/ltltest/rand.test: Add tests. * NEWS, doc/org/ioltl.org: Document it. --- NEWS | 6 +++++ doc/org/ioltl.org | 34 ++++++++++++++++++++++++++-- src/bin/common_output.cc | 48 +++++++++++++++++++++++++++++++++++----- src/bin/common_output.hh | 13 +++++------ src/ltltest/ltlfilt.test | 4 ++++ src/ltltest/rand.test | 6 +++++ 6 files changed, 96 insertions(+), 15 deletions(-) diff --git a/NEWS b/NEWS index b914b9b2d..23366eb07 100644 --- a/NEWS +++ b/NEWS @@ -44,6 +44,12 @@ New in spot 1.99a (not yet released) - ltlfilt has a new --count option to count the number of matching automata. + - all tools that produce formulas or automata now have an --output + (a.k.a. -o) option to redirect that output to a file instead of + standard output. The name of this file can be constructed using + the same %-escape sequences that are available for --stats or + --format. + - ltlcross (and ltldo) have a list of hard-coded shorthands for some existing tools. So for instance running 'ltlcross spin ...' is the same as running diff --git a/doc/org/ioltl.org b/doc/org/ioltl.org index b9eacda6d..78cd19b45 100644 --- a/doc/org/ioltl.org +++ b/doc/org/ioltl.org @@ -150,6 +150,7 @@ ltlfilt --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: #+begin_example + -c, --count print only a count of matched formulas -n, --max-count=NUM output at most NUM formulas -q, --quiet suppress all normal output -8, --utf8 output using UTF-8 characters @@ -158,14 +159,15 @@ ltlfilt --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d' "%f") -l, --lbt output in LBT's syntax --latex output using LaTeX macros + -o, --output=FORMAT send output to a file named FORMAT instead of + standard output. The first formula sent to a file + truncates it unless FORMAT starts with '>>'. -p, --full-parentheses output fully-parenthesized formulas -s, --spin output in Spin's syntax --spot output in Spot's syntax (default) --wring output in Wring's syntax #+end_example -# LocalWords: syntaxes LTL PSL num toc SRC ltl tgba sed FILENAME - The =--spot=, =--utf-8=, =--spin=, =--wring= options select different output syntaxes as seen in [[tab:formula-syntaxes][the above table]]. @@ -203,5 +205,33 @@ from tool to tool: | [[file:genltl.org][=genltl=]] | output formula | pattern name | pattern parameter | (empty) | (empty) | | [[file:randltl.org][=randltl=]] | output formula | (empty) | formula number | (empty) | (empty) | + +By default everything is output to standard output, so that you can +redirect the output to a file, and pipe it to another tool. The the +=--output= (or =-o=) allows you to construct a filename using some of +the above =%=-sequences. + +For instance the following invocation of [[file:randltl.org][=randltl=]] will create 5 +random formulas, but in 5 different files: + +#+BEGIN_SRC sh :results verbatim :exports both +randltl -n5 a b -o example-%L.ltl +wc -l example-*.ltl +#+END_SRC +#+RESULTS: +: 1 example-1.ltl +: 1 example-2.ltl +: 1 example-3.ltl +: 1 example-4.ltl +: 1 example-5.ltl +: 5 total + +#+BEGIN_SRC sh :results verbatim :exports none +rm -f example-*.ltl +#+END_SRC +#+RESULTS: + + # LocalWords: lbt LBT's filename UTF gfa GFa ltlfilt LBTT scheck # LocalWords: utf associativity +# LocalWords: syntaxes LTL PSL num toc SRC ltl tgba sed FILENAME diff --git a/src/bin/common_output.cc b/src/bin/common_output.cc index 1d039d97e..40e2c7543 100644 --- a/src/bin/common_output.cc +++ b/src/bin/common_output.cc @@ -52,6 +52,10 @@ static const argp_option options[] = -20 }, { "format", OPT_FORMAT, "FORMAT", 0, "specify how each line should be output (default: \"%f\")", -20 }, + { "output", 'o', "FORMAT", 0, + "send output to a file named FORMAT instead of standard output. The" + " first formula sent to a file truncates it unless FORMAT starts" + " with '>>'.", 0 }, { 0, 0, 0, 0, 0, 0 } }; @@ -195,6 +199,9 @@ namespace } static formula_printer* format = 0; +static std::ostringstream outputname; +static formula_printer* outputnamer = 0; +static std::map> outputfiles; int parse_opt_output(int key, char* arg, struct argp_state*) @@ -208,6 +215,9 @@ parse_opt_output(int key, char* arg, struct argp_state*) case 'l': output_format = lbt_output; break; + case 'o': + outputnamer = new formula_printer(outputname, arg); + break; case 'p': full_parenth = true; break; @@ -237,10 +247,11 @@ parse_opt_output(int key, char* arg, struct argp_state*) } -void +static void output_formula(std::ostream& out, - const spot::ltl::formula* f, const char* filename, int linenum, - const char* prefix, const char* suffix) + const spot::ltl::formula* f, + const char* filename = nullptr, int linenum = 0, + const char* prefix = nullptr, const char* suffix = nullptr) { if (!format) { @@ -257,15 +268,40 @@ output_formula(std::ostream& out, } } +void +::printable_formula::print(std::ostream& os, const char*) const +{ + output_formula(os, val_); +} + void output_formula_checked(const spot::ltl::formula* f, const char* filename, int linenum, const char* prefix, const char* suffix) { - if (output_format == quiet_output || output_format == count_output) + if (output_format == count_output) + { + if (outputnamer) + throw std::runtime_error + ("options --output and --count are incompatible"); + return; + } + if (output_format == quiet_output) return; - output_formula(std::cout, f, filename, linenum, prefix, suffix); - std::cout << '\n'; + std::ostream* out = &std::cout; + if (outputnamer) + { + outputname.str(""); + formula_with_location fl = { f, filename, linenum, prefix, suffix }; + outputnamer->print(fl); + std::string fname = outputname.str(); + auto p = outputfiles.emplace(fname, nullptr); + if (p.second) + p.first->second.reset(new output_file(fname.c_str())); + out = &p.first->second->ostream(); + } + output_formula(*out, f, filename, linenum, prefix, suffix); + *out << '\n'; // Make sure we abort if we can't write to std::cout anymore // (like disk full or broken pipe with SIGPIPE ignored). check_cout(); diff --git a/src/bin/common_output.hh b/src/bin/common_output.hh index 5492c56c6..facdb0648 100644 --- a/src/bin/common_output.hh +++ b/src/bin/common_output.hh @@ -23,9 +23,12 @@ #include "common_sys.hh" #include +#include +#include #include "ltlast/formula.hh" #include "tgbaalgos/stats.hh" #include "common_output.hh" +#include "common_file.hh" enum output_format_t { spot_output, spin_output, utf8_output, lbt_output, wring_output, latex_output, @@ -38,9 +41,6 @@ extern const struct argp output_argp; int parse_opt_output(int key, char* arg, struct argp_state* state); -void output_formula(std::ostream& os, const spot::ltl::formula* f, - const char* filename = 0, int linenum = 0, - const char* prefix = 0, const char* suffix = 0); void output_formula_checked(const spot::ltl::formula* f, const char* filename = 0, int linenum = 0, const char* prefix = 0, const char* suffix = 0); @@ -58,10 +58,7 @@ public: } virtual void - print(std::ostream& os, const char*) const - { - output_formula(os, val_); - } + print(std::ostream& os, const char*) const; }; class aut_stat_printer: protected spot::stat_printer @@ -73,6 +70,8 @@ public: declare('f', &formula_); // Override the formula printer. } + using spot::formater::set_output; + std::ostream& print(const spot::const_tgba_digraph_ptr& aut, const spot::ltl::formula* f = 0, diff --git a/src/ltltest/ltlfilt.test b/src/ltltest/ltlfilt.test index 03616b843..f88ff036f 100755 --- a/src/ltltest/ltlfilt.test +++ b/src/ltltest/ltlfilt.test @@ -188,4 +188,8 @@ SPOT_STUTTER_CHECK=5 \ # bug in the bitvectors. ../../bin/ltlfilt --stutter-invariant -f 'F(a & XXXXXX!a)' && exit 1 + +../../bin/ltlfilt -c -o 'foo' -f a 2>stderr && exit 1 +grep 'ltlfilt: options --output and --count are incompatible' stderr + true diff --git a/src/ltltest/rand.test b/src/ltltest/rand.test index fa9095c85..bbf9b8ad6 100755 --- a/src/ltltest/rand.test +++ b/src/ltltest/rand.test @@ -130,3 +130,9 @@ run 2 $randltl -n3 0 run 0 $randltl -n1000 0 1 > out grep -q '"0"' out grep -q '"1"' out + + +run 0 $randltl -n5 2 -o test-all.ltl +run 0 $randltl -n5 2 -o test-%L.ltl +cat test-1.ltl test-2.ltl test-3.ltl test-4.ltl test-5.ltl > test-cmp.ltl +diff test-cmp.ltl test-all.ltl