From 846e33b9e5f3de97b8513abc9c8375c016b40bdd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 29 Nov 2013 18:46:02 +0100 Subject: [PATCH] ltl2tgba: Add a --csv-escape option and document CSV I/O. * src/bin/common_output.cc, src/bin/common_output.hh: (output_formula_checked, aut_stat_printer): New. * src/bin/genltl.cc, src/bin/randltl.cc, src/bin/ltlfilt.cc: Call output_formula_checked() instead of output_formula(). * src/bin/ltl2tgba.cc: Use aut_stat_printer and add option --csv-escape. * doc/org/csv.org: New file to document CSV I/O. * doc/Makefile.am: Add it. * doc/org/ioltl.org, doc/org/ltlfilt.org, doc/org/ltl2tgba.org, doc/org/tools.org: Link to csv.org --- NEWS | 5 + doc/Makefile.am | 1 + doc/org/csv.org | 238 +++++++++++++++++++++++++++++++++++++++ doc/org/ioltl.org | 51 ++++++--- doc/org/ltl2tgba.org | 25 ++-- doc/org/ltlfilt.org | 3 + doc/org/tools.org | 1 + src/bin/common_output.cc | 51 +++++++-- src/bin/common_output.hh | 47 +++++++- src/bin/genltl.cc | 2 +- src/bin/ltl2tgba.cc | 10 +- src/bin/ltlfilt.cc | 2 +- src/bin/randltl.cc | 2 +- 13 files changed, 399 insertions(+), 39 deletions(-) create mode 100644 doc/org/csv.org diff --git a/NEWS b/NEWS index ad4f3d206..147bc91da 100644 --- a/NEWS +++ b/NEWS @@ -31,6 +31,11 @@ New in spot 1.2a (not released) the rewriten formula. The new escape sequence %< (text in columns before the formula) and %> (text after) can be used with the --format option to alter this output. + - ltlfile, genltl, randltl, and ltl2tgba have a --csv-escape option + to help escape formulas in CSV files. + - Please check + http://spot.lip6.fr/userdoc/csv.html + for some discussion and examples of the last few features. * Bug fixes: - ltlcross' CSV output now stricly follows RFC 4180. - ltlcross failed to report missing input or output escape sequences diff --git a/doc/Makefile.am b/doc/Makefile.am index 9cb42479d..9219372e8 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -60,6 +60,7 @@ ORG_FILES = \ org/.dir-locals.el \ org/init.el.in \ org/syntax.css \ + org/csv.org \ org/dstar2tgba.org \ org/genltl.org \ org/ioltl.org \ diff --git a/doc/org/csv.org b/doc/org/csv.org new file mode 100644 index 000000000..adb85acb9 --- /dev/null +++ b/doc/org/csv.org @@ -0,0 +1,238 @@ +#+TITLE: Reading and writing CSV files +#+EMAIL spot@lrde.epita.fr +#+OPTIONS: H:2 num:nil toc:t +#+LINK_UP: file:tools.html + +This page discusses features available in Spot's command-line +tools to produce an consume CSV files. + +* Producing CSV files + +All the tools that normally produce formulas (like [[file:genltl.org][=genltl=]], [[file:randltl.org][=randltl=]], +and [[file:ltlfilt.org][=ltlfilt=]]) have a [[file:ioltl.org][=--format= option]]. That can be used to +customize the way output is formatted. + +For instance here is how we could use =genltl= to generate a CSV file +with three columns: the family name of the formula, its parameter, and +the formula itself. + +#+BEGIN_SRC sh :results verbatim :exports both +genltl --and-gf=1..5 --u-left=1..5 --format='%F,%L,%f' > gen.csv +cat gen.csv +#+END_SRC +#+RESULTS: +#+begin_example +and-gf,1,GFp1 +and-gf,2,GFp1 & GFp2 +and-gf,3,GFp1 & GFp2 & GFp3 +and-gf,4,GFp1 & GFp2 & GFp3 & GFp4 +and-gf,5,GFp1 & GFp2 & GFp3 & GFp4 & GFp5 +u-left,1,p1 +u-left,2,p1 U p2 +u-left,3,(p1 U p2) U p3 +u-left,4,((p1 U p2) U p3) U p4 +u-left,5,(((p1 U p2) U p3) U p4) U p5 +#+end_example + +Tools that produce automata (like [[file:ltl2tgba.org][=ltl2tgba=]], or [[file:dstar2tgba.org][=dstar2tgba=]]) have a +=--stats= option that can be used to output various statistics about +the constructed automaton (these statistics are shown *instead* of +printing the automaton). + +For instance, the following command will translate all the previous +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' +#+END_SRC +#+RESULTS: +#+begin_example +GFp1,1,2 +G(Fp1 & Fp2),1,4 +G(Fp1 & Fp2 & Fp3),1,8 +G(Fp1 & Fp2 & Fp3 & Fp4),1,16 +G(Fp1 & Fp2 & Fp3 & Fp4 & Fp5),1,32 +p1,2,2 +p1 U p2,2,3 +(p1 U p2) U p3,4,10 +((p1 U p2) U p3) U p4,8,34 +(((p1 U p2) U p3) U p4) U p5,16,116 +#+end_example + +If the translated formulas may contain commas, or double-quotes, this +simple output may prove difficult to process by other tools. For +instance consider the translation of the following two formulas: + +#+BEGIN_SRC sh :results verbatim :exports both +ltl2tgba -f Xa -f 'G("switch == on" -> F"tab[3,5] < 12")' --stats '%f,%s,%e' +#+END_SRC +#+RESULTS: +: Xa,3,3 +: G(!"switch == on" | F"tab[3,5] < 12"),2,4 + +The second line of this input does no conform to [[https://www.rfc-editor.org/rfc/rfc4180.txt][RFC 4180]] because +non-escaped fields are not allowed to contain comma or double-quotes. +To fix this, use =ltl2tgba='s =--csv-escape= option: this causes +"=%f=" to produce a double-quoted string properly escaped. + +#+BEGIN_SRC sh :results verbatim :exports both +ltl2tgba -f Xa -f 'G("switch == on" -> F"tab[3,5] < 12")' --stats '%f,%s,%e' --csv-escape +#+END_SRC + +#+RESULTS: +: "Xa",3,3 +: "G(!""switch == on"" | F""tab[3,5] < 12"")",2,4 + + +The tool [[file:ltlcross.org][=ltlcross=]] has its own =--csv=FILENAME= option to format the +statistics it gathers in a CSV file, but you have very little control +hover how this CSV file is formatted (it can only be changed +via option such as =--products= or =--omit-missing=). + +* Reading CSV files + +All the tools that read formulas from files extend the filename syntax +to support the specification of a CSV column. The notation +=filename/COL= denotes the column =COL= of that file. + +For instance let's consider the file =gen.csv= built with the first command of +this page. It contains: + +#+BEGIN_SRC sh :results verbatim :exports results +cat gen.csv +#+END_SRC +#+RESULTS: +#+begin_example +and-gf,1,GFp1 +and-gf,2,GFp1 & GFp2 +and-gf,3,GFp1 & GFp2 & GFp3 +and-gf,4,GFp1 & GFp2 & GFp3 & GFp4 +and-gf,5,GFp1 & GFp2 & GFp3 & GFp4 & GFp5 +u-left,1,p1 +u-left,2,p1 U p2 +u-left,3,(p1 U p2) U p3 +u-left,4,((p1 U p2) U p3) U p4 +u-left,5,(((p1 U p2) U p3) U p4) U p5 +#+end_example + +We can run =ltl2tgba= on the third column to produce +the same output as in a previous example: + +#+BEGIN_SRC sh :results verbatim :exports both +ltl2tgba -F gen.csv/3 --stats '%f,%s,%e' +#+END_SRC +#+RESULTS: +#+begin_example +GFp1,1,2 +G(Fp1 & Fp2),1,4 +G(Fp1 & Fp2 & Fp3),1,8 +G(Fp1 & Fp2 & Fp3 & Fp4),1,16 +G(Fp1 & Fp2 & Fp3 & Fp4 & Fp5),1,32 +p1,2,2 +p1 U p2,2,3 +(p1 U p2) U p3,4,10 +((p1 U p2) U p3) U p4,8,34 +(((p1 U p2) U p3) U p4) U p5,16,116 +#+end_example + +When =ltlfilt= is used on a CSV file, it will preserve the +text before and after the matched formula in the CSV file. +For instance: + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt -F gen.csv/3 --size-min=8 --relabel=abc +#+END_SRC +#+RESULTS: +: and-gf,3,GFa & GFb & GFc +: and-gf,4,GFa & GFb & GFc & GFd +: and-gf,5,GFa & GFb & GFc & GFd & GFe +: u-left,5,(((a U b) U c) U d) U e + +For security, in case a formula may contain double-quotes or +commas, you should use the =--csv-escape= option: + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt -F gen.csv/3 --size-min=8 --relabel=abc --csv-escape +#+END_SRC +#+RESULTS: +: and-gf,3,"GFa & GFb & GFc" +: and-gf,4,"GFa & GFb & GFc & GFd" +: and-gf,5,"GFa & GFb & GFc & GFd & GFe" +: u-left,5,"(((a U b) U c) U d) U e" + +The preservation in the output of the text before and after the +selected column can be altered using the =--format= option. The =%<= +escape sequence represent the (comma-separated) data of all the +columns before the selected column, and =%>= is the same for the +trailing data. Note that the comma that separate formulas' column +from the other column are excluded and should be added in the format +string. + +For instance this moves the first two columns after the formulas. + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt -F gen.csv/3 --size-min=8 --csv-escape --format='%f,%<' +#+END_SRC +#+RESULTS: +: "GFp1 & GFp2 & GFp3",and-gf,3 +: "GFp1 & GFp2 & GFp3 & GFp4",and-gf,4 +: "GFp1 & GFp2 & GFp3 & GFp4 & GFp5",and-gf,5 +: "(((p1 U p2) U p3) U p4) U p5",u-left,5 + + +Typical uses of =ltlfilt= on CSV file include: +- Filtering lines based on an LTL criterion, as above. +- Changing the syntax of LTL formulas. For instance =ltl2tgba='s + =--stats= option, and =ltlcross='s =--csv= option always output + formulas in Spot's format. If that is inappropriate, simply + use =ltlfilt= to rewrite the relevant column in your prefered + syntax. + +* Dealing with header lines + +Some CSV contain a header lines that should not be processed. +The CSV file produced by =ltlcross= have such a line: + +#+BEGIN_SRC sh :results verbatim :exports both +randltl -n 2 a b | ltlfilt --remove-wm | + ltlcross --csv=results.csv 'ltl2tgba -s %f >%N' 'ltl3ba -f %s >%N' +cat results.csv +#+END_SRC +#+RESULTS: +: "formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nonacc_scc","terminal_scc","weak_scc","strong_scc","nondet_states","nondet_aut","terminal_aut","weak_aut","strong_aut","product_states","product_transitions","product_scc" +: "(1)","ltl2tgba -s %f >%N","ok",0,0.0247303,1,1,1,1,1,0,1,0,0,0,0,1,0,0,200,3994,1 +: "(1)","ltl3ba -f %s >%N","ok",0,0.00314673,1,1,1,1,1,0,1,0,0,0,0,1,0,0,200,3994,1 +: "(0)","ltl2tgba -s %f >%N","ok",0,0.0246916,1,1,0,1,1,1,0,0,0,0,0,1,0,0,1,0,1 +: "(0)","ltl3ba -f %s >%N","ok",0,0.00343519,1,0,0,1,1,1,0,0,0,0,0,1,0,0,1,0,1 +: "(!(G((F(b)) | (F(!((b) | (G(b))))))))","ltl2tgba -s %f >%N","ok",0,0.0233752,1,1,0,1,1,1,0,0,0,0,0,1,0,0,1,0,1 +: "(!(G((F(b)) | (F(!((b) | (G(b))))))))","ltl3ba -f %s >%N","ok",0,0.00316933,1,0,0,1,1,1,0,0,0,0,0,1,0,0,1,0,1 +: "(G((F(b)) | (F(!((b) | (G(b)))))))","ltl2tgba -s %f >%N","ok",0,0.0238983,1,1,1,1,1,0,1,0,0,0,0,1,0,0,200,4083,1 +: "(G((F(b)) | (F(!((b) | (G(b)))))))","ltl3ba -f %s >%N","ok",0,0.00315896,1,1,1,1,1,0,1,0,0,0,0,1,0,0,200,4083,1 + +If we run =ltlfilt= on the first column, it will process the =formula= +header as if it was an LTL formula. + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt -F results.csv/1 --format='%f' --unique +#+END_SRC + +#+RESULTS: +: formula +: 1 +: 0 +: !G(Fb | F!(b | Gb)) +: G(Fb | F!(b | Gb)) + +In such case, the syntax =FILENAME/-COL= (with a minus sign before the +column number) can be used to discard the first line of a CSV file. + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt -F results.csv/-1 --format='%f' --unique +#+END_SRC + +#+RESULTS: +: 1 +: 0 +: !G(Fb | F!(b | Gb)) +: G(Fb | F!(b | Gb)) diff --git a/doc/org/ioltl.org b/doc/org/ioltl.org index 29901c65b..ccca280f5 100644 --- a/doc/org/ioltl.org +++ b/doc/org/ioltl.org @@ -16,7 +16,10 @@ ltl2tgba --help | sed -n '/Input options:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : -f, --formula=STRING process the formula STRING -: -F, --file=FILENAME process each line of FILENAME as a formula +: -F, --file=FILENAME[/COL] process each line of FILENAME as a formula; if COL +: is a positive integer, assume a CSV file and read +: column COL; usea negative COL to drop the first +: line of the CSV file : --lbt-input read all formulas using LBT's prefix syntax : --lenient parenthesized blocks that cannot be parsed as : subformulas are considered as atomic properties @@ -27,7 +30,12 @@ be repeated to pass multiple formulas. =-F= is used to read formulas from a file (one formula per line). This option can also be repeated to pass multiple files. If the filename specified is =-= (as in =-F-=), then formulas are read from -standard input. +standard input. If a filename is suffixed with =/COL=, where =COL= is +a positive integer, then the file is assumed to be a CSV file, and +formulas are read from its =COL=-th column. Use =/-COL= to read from +column =COL= and ignore the first line of the CSV file (which often +contains column headers). We have [[file:csv.org][examples of reading or writing CSV +files on a separate page]]. ** Default parser @@ -132,6 +140,7 @@ used by [[http://www.ltl2dstar.de][ltl2dstar]]. =--lbt-input= is a global option that affects *all* formulas that are read. + * Common output options All tools that output LTL/PSL formulas implement the following options: @@ -140,15 +149,18 @@ All tools that output LTL/PSL formulas implement the following options: ltlfilt --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: -: -8, --utf8 output using UTF-8 characters -: --format=FORMAT specify how each line should be output (default: -: "%f") -: -l, --lbt output in LBT's syntax -: --latex output using LaTeX macros -: -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 +#+begin_example + -8, --utf8 output using UTF-8 characters + --csv quote the formula for use in a CSV file + --format=FORMAT specify how each line should be output (default: + "%f") + -l, --lbt output in LBT's syntax + --latex output using LaTeX macros + -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 @@ -171,16 +183,23 @@ with read it as =(a U b) U c=. The =--lbt= option requests an output in LBT's prefix format, and in that case discussing associativity and parentheses makes no sense. +The =--csv= causes the formulas to be double-quoted (with inner +double-quotes doubled, as per RFC 4180), regardless of the selected +format. This is needed if the formula should appear in a CSV file, +and you want to be robust to formulas that contains commas or +double-quotes. We have [[file:csv.org][examples of reading or writing CSV files on a +separate page]]. + The =--format= option can be used to fine-tune the way the formula is output. Not using the =--format= option is equivalent to using =--format=%f=. The semantic of the available =%=-sequences differ from tool to tool: -| | =%f= | =%F= | =%L= | -|-----------+----------------+----------------+-------------------| -| [[file:ltlfilt.org][=ltlfilt=]] | output formula | input filename | input line | -| [[file:genltl.org][=genltl=]] | output formula | pattern name | pattern parameter | -| [[file:randltl.org][=randltl=]] | output formula | (empty) | formula number | +| | =%f= | =%F= | =%L= | =%<= | =%>= | +|-----------+----------------+----------------+-------------------+--------------+---------------| +| [[file:ltlfilt.org][=ltlfilt=]] | output formula | input filename | input line | leading text | trailing text | +| [[file:genltl.org][=genltl=]] | output formula | pattern name | pattern parameter | (empty) | (empty) | +| [[file:randltl.org][=randltl=]] | output formula | (empty) | formula number | (empty) | (empty) | # LocalWords: lbt LBT's filename UTF gfa GFa ltlfilt LBTT scheck # LocalWords: utf associativity diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 0eaf7aaae..76f87d99c 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -551,15 +551,19 @@ following sequence of characters (other characters are output as-is): ltl2tgba --help | sed -n '/^ *%/p' #+END_SRC #+RESULTS: -: %% a single % -: %a number of acceptance sets -: %c number of SCCs -: %d 1 if the automaton is deterministic, 0 otherwise -: %e number of edges -: %f the formula, in Spot's syntax -: %n number of nondeterministic states -: %s number of states -: %t number of transitions +#+begin_example + %% a single % + %a number of acceptance sets + %c number of SCCs + %d 1 if the automaton is deterministic, 0 otherwise + %e number of edges + %f the formula, in Spot's syntax + %n number of nondeterministic states + %p 1 if the automaton is complete, 0 otherwise + %r translation time (including pre- and + %s number of states + %t number of transitions +#+end_example For instance we can study the size of the automata generated for the right-nested =U= formulas as follows: @@ -592,6 +596,9 @@ Two automata with the same structures (states and edges) but differing labels, may have a different count of transitions, e.g., if one has more restricted labels. +[[file:csv.org][More examples of how to use =--stats= to create CSV +files are on a separate page]]. + * Building Monitors In addition to TGBA and BA, =ltl2tgba= can output /monitor/ using the diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index e3da1facf..e5b6ffbd1 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -351,6 +351,9 @@ ltlfilt --lbt-input -F scheck.ltl --guarantee --format=%L : 3 : 4 +[[file:csv.org][More examples of how to use =--format= to create CSV files are on a +separate page]] + # LocalWords: ltlfilt num toc LTL PSL syntaxes LBT's SRC GFp scheck # LocalWords: ltl EOF lbt Gp Fp Xp XFp XXp randltl ary nnf wm abc # LocalWords: pnn Xb Fc XFb XXd sed boolean bsize nox Gb Fb Xa XGb diff --git a/doc/org/tools.org b/doc/org/tools.org index a1cfae413..f1e127898 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -46,6 +46,7 @@ corresponding commands are hidden. * Advanced uses +- [[file:csv.org][Reading and writing CSV files]] - [[file:satmin.org][SAT-based minimization of Deterministic (Generalized) Büchi automata]] * Citing diff --git a/src/bin/common_output.cc b/src/bin/common_output.cc index 69aab4301..e97f46dde 100644 --- a/src/bin/common_output.cc +++ b/src/bin/common_output.cc @@ -24,6 +24,7 @@ #include "ltlvisit/tostring.hh" #include "ltlvisit/lbt.hh" #include "misc/formater.hh" +#include "misc/escape.hh" #include "common_cout.hh" #include "error.h" @@ -31,9 +32,11 @@ #define OPT_WRING 2 #define OPT_LATEX 3 #define OPT_FORMAT 4 +#define OPT_CSV 5 output_format_t output_format = spot_output; bool full_parenth = false; +bool escape_csv = false; static const argp_option options[] = { @@ -45,6 +48,8 @@ static const argp_option options[] = { "wring", OPT_WRING, 0, 0, "output in Wring's syntax", -20 }, { "utf8", '8', 0, 0, "output using UTF-8 characters", -20 }, { "latex", OPT_LATEX, 0, 0, "output using LaTeX macros", -20 }, + { "csv-escape", OPT_CSV, 0, 0, "quote the formula for use in a CSV file", + -20 }, { "format", OPT_FORMAT, "FORMAT", 0, "specify how each line should be output (default: \"%f\")", -20 }, { 0, 0, 0, 0, 0, 0 } @@ -102,6 +107,26 @@ stream_formula(std::ostream& out, } } +static void +stream_escapable_formula(std::ostream& os, + const spot::ltl::formula* f, + const char* filename, int linenum) +{ + if (escape_csv) + { + std::ostringstream out; + stream_formula(out, f, filename, linenum); + os << '"'; + spot::escape_rfc4180(os, out.str()); + os << '"'; + } + else + { + stream_formula(os, f, filename, linenum); + } +} + + namespace { struct formula_with_location @@ -127,10 +152,7 @@ namespace virtual void print(std::ostream& os, const char*) const { - stream_formula(os, - val_->f, - val_->filename, - val_->line); + stream_escapable_formula(os, val_->f, val_->filename, val_->line); } }; @@ -189,6 +211,9 @@ parse_opt_output(int key, char* arg, struct argp_state*) case 's': output_format = spin_output; break; + case OPT_CSV: + escape_csv = true; + break; case OPT_LATEX: output_format = latex_output; break; @@ -210,25 +235,33 @@ parse_opt_output(int key, char* arg, struct argp_state*) void -output_formula(const spot::ltl::formula* f, const char* filename, int linenum, +output_formula(std::ostream& out, + const spot::ltl::formula* f, const char* filename, int linenum, const char* prefix, const char* suffix) { if (!format) { if (prefix) - std::cout << prefix << ","; - stream_formula(std::cout, f, filename, linenum); + out << prefix << ","; + stream_escapable_formula(out, f, filename, linenum); if (suffix) - std::cout << "," << suffix; + out << "," << suffix; } else { formula_with_location fl = { f, filename, linenum, prefix, suffix }; format->print(fl); } +} +void +output_formula_checked(const spot::ltl::formula* f, + const char* filename, int linenum, + const char* prefix, const char* suffix) +{ + output_formula(std::cout, f, filename, linenum, prefix, suffix); + std::cout << std::endl; // Make sure we abort if we can't write to std::cout anymore // (like disk full or broken pipe with SIGPIPE ignored). - std::cout << std::endl; check_cout(); } diff --git a/src/bin/common_output.hh b/src/bin/common_output.hh index 1714cad6f..73bafb685 100644 --- a/src/bin/common_output.hh +++ b/src/bin/common_output.hh @@ -24,18 +24,63 @@ #include #include "ltlast/formula.hh" +#include "tgbaalgos/stats.hh" +#include "common_output.hh" enum output_format_t { spot_output, spin_output, utf8_output, lbt_output, wring_output, latex_output }; extern output_format_t output_format; extern bool full_parenth; +extern bool escape_csv; extern const struct argp output_argp; int parse_opt_output(int key, char* arg, struct argp_state* state); -void output_formula(const spot::ltl::formula* f, +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); + + +class printable_formula: + public spot::printable_value +{ +public: + printable_formula& + operator=(const spot::ltl::formula* new_val) + { + val_ = new_val; + return *this; + } + + virtual void + print(std::ostream& os, const char*) const + { + output_formula(os, val_); + } +}; + +class aut_stat_printer: protected spot::stat_printer +{ +public: + aut_stat_printer(std::ostream& os, const char* format) + : spot::stat_printer(os, format) + { + declare('f', &formula_); // Override the formula printer. + } + + std::ostream& + print(const spot::tgba* aut, const spot::ltl::formula* f = 0, + double run_time = -1.) + { + formula_ = f; + return this->spot::stat_printer::print(aut, f, run_time); + } + + printable_formula formula_; +}; #endif // SPOT_BIN_COMMON_OUTPUT_HH diff --git a/src/bin/genltl.cc b/src/bin/genltl.cc index 371b47cf0..9f36993b1 100644 --- a/src/bin/genltl.cc +++ b/src/bin/genltl.cc @@ -846,7 +846,7 @@ output_pattern(int pattern, int n) f = r; } - output_formula(f, class_name[pattern - 1], n); + output_formula_checked(f, class_name[pattern - 1], n); f->destroy(); } diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index 133843b8f..c81db4331 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -30,6 +30,7 @@ #include "common_r.hh" #include "common_cout.hh" #include "common_finput.hh" +#include "common_output.hh" #include "common_post.hh" #include "ltlast/formula.hh" @@ -55,6 +56,7 @@ If multiple formulas are supplied, several automata will be output."; #define OPT_LBTT 3 #define OPT_SPOT 4 #define OPT_STATS 5 +#define OPT_CSV 6 static const argp_option options[] = { @@ -67,6 +69,8 @@ static const argp_option options[] = "of the given formula)", 0 }, /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, + { "csv-escape", OPT_CSV, 0, 0, "quote formula output by %f in --format " + "for use in CSV file", 0 }, { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL, "LBTT's format (add =t to force transition-based acceptance even" @@ -127,6 +131,7 @@ parse_opt(int key, char* arg, struct argp_state*) { case '8': spot::enable_utf8(); + output_format = utf8_output; break; case 'B': type = spot::postprocessor::BA; @@ -146,6 +151,9 @@ parse_opt(int key, char* arg, struct argp_state*) error(2, 0, "failed to parse --options near '%s'", opt); } break; + case OPT_CSV: + escape_csv = true; + break; case OPT_DOT: format = Dot; break; @@ -194,7 +202,7 @@ namespace { public: spot::translator& trans; - spot::stat_printer statistics; + aut_stat_printer statistics; trans_processor(spot::translator& trans) : trans(trans), statistics(std::cout, stats) diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index 901521e31..5dfd27de7 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -577,7 +577,7 @@ namespace if (matched) { one_match = true; - output_formula(f, filename, linenum, prefix, suffix); + output_formula_checked(f, filename, linenum, prefix, suffix); } f->destroy(); return 0; diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc index d6ae4dd54..243bc7a1f 100644 --- a/src/bin/randltl.cc +++ b/src/bin/randltl.cc @@ -396,7 +396,7 @@ main(int argc, char** argv) error(2, 0, "failed to generate a new unique formula after %d trials", MAX_TRIALS); static int count = 0; - output_formula(f, 0, ++count); + output_formula_checked(f, 0, ++count); f->destroy(); };