diff --git a/NEWS b/NEWS index 7d4077c5c..3f3d70560 100644 --- a/NEWS +++ b/NEWS @@ -76,6 +76,10 @@ New in spot 1.1.4a (not relased) Each operator is output as a command such as \U, \F, etc. doc/tl/spotltl.sty gives one possible definition for each macro. + - ltlfilt, genltl, and randltl have a new --format option to + indicate how to present the output formula, possibly with + information about the input. + * New functions and classes in the library: - dtba_sat_synthetize(): Use a SAT-solver to build an equivalent diff --git a/doc/org/genltl.org b/doc/org/genltl.org index 909058e9e..9e1ff925a 100644 --- a/doc/org/genltl.org +++ b/doc/org/genltl.org @@ -47,7 +47,7 @@ genltl --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d' (p1 U (p2 U (... U pn))) #+end_example -An example is probably all it takes to explain how this tool works: +An example is probably all it takes to understand how this tool works: #+BEGIN_SRC sh :results verbatim :exports both genltl --and-gf=1..5 --u-left=1..5 @@ -69,9 +69,47 @@ p1 U p2 =genltl= supports the [[file:ioltl.org][common option for output of LTL formulas]], so you may output these pattern for various tools. -Note that for the =--lbt= output, each formula is relabeled using +For instance here is the same formulas, but formatted in a way that is +suitable for being included in a LaTeX table. + + +#+BEGIN_SRC sh :results verbatim :exports both +genltl --and-gf=1..5 --u-left=1..5 --latex --format='%F & %L & $%f$ \\' +#+END_SRC +#+RESULTS: +#+begin_example +and-gf & 1 & $\G \F p_{1}$ \\ +and-gf & 2 & $\G \F p_{1} \land \G \F p_{2}$ \\ +and-gf & 3 & $\G \F p_{1} \land \G \F p_{2} \land \G \F p_{3}$ \\ +and-gf & 4 & $\G \F p_{1} \land \G \F p_{2} \land \G \F p_{3} \land \G \F p_{4}$ \\ +and-gf & 5 & $\G \F p_{1} \land \G \F p_{2} \land \G \F p_{3} \land \G \F p_{4} \land \G \F p_{5}$ \\ +u-left & 1 & $p_{1}$ \\ +u-left & 2 & $p_{1} \U p_{2}$ \\ +u-left & 3 & $(p_{1} \U p_{2}) \U p_{3}$ \\ +u-left & 4 & $((p_{1} \U p_{2}) \U p_{3}) \U p_{4}$ \\ +u-left & 5 & $(((p_{1} \U p_{2}) \U p_{3}) \U p_{4}) \U p_{5}$ \\ +#+end_example + +Note that for the =--lbt= syntax, each formula is relabeled using =p0=, =p1=, ... before it is output, when the pattern (like -=--ccj-alpha=) use different names. +=--ccj-alpha=) use different names. Compare: + +#+BEGIN_SRC sh :results verbatim :exports both +genltl --ccj-alpha=3 +#+END_SRC +#+RESULTS: +: F(F(Fq3 & q2) & q1) & F(F(Fp3 & p2) & p1) + +with + +#+BEGIN_SRC sh :results verbatim :exports both +genltl --ccj-alpha=3 --lbt +#+END_SRC +#+RESULTS: +: & F & p2 F & p1 F p0 F & F & F p3 p4 p5 + +This is because most tools using =lbt='s syntax require atomic +propositions to have the form =pNN=. # LocalWords: genltl num toc LTL scalable SRC sed gh pn fg FG gf qn # LocalWords: ccj Xp XXp Xq XXq rv GFp lbt diff --git a/doc/org/ioltl.org b/doc/org/ioltl.org index 4f550d169..29901c65b 100644 --- a/doc/org/ioltl.org +++ b/doc/org/ioltl.org @@ -141,7 +141,10 @@ 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) @@ -150,8 +153,14 @@ ltlfilt --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d' # 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]]. The =-p= option can -be used to request that parentheses be used at all levels. +output syntaxes as seen in [[tab:formula-syntaxes][the above table]]. + +Option =--latex= causes formulas to be output using LaTeX macros for +each operator. You may define these macros as you wish, and some +example definitions are in =doc/tl/spotltl.sty=. + +The =-p= option can be used to request that parentheses be used at all +levels. Note that by default Spot always outputs parentheses around operators such as =U=, because not all tools agree on their associativity. For @@ -162,5 +171,16 @@ 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 =--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 | + # LocalWords: lbt LBT's filename UTF gfa GFa ltlfilt LBTT scheck # LocalWords: utf associativity diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index 03a7be78e..26d09db46 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -253,6 +253,23 @@ It is therefore equivalent, but that is not a surprise since the [[http://homepages.inf.ed.ac.uk/kousha/note_on_stut_tl_lpi.ps][this procedure]] (calling the =remove_x()= function, and building automata to check the equivalence of the resulting formula with the original one). +* Using =--format= + +The =--format= option can be used the alter the way formulas are output (for instance use +#+HTML: --latex --format='$%f$' +to enclose formula in LaTeX format with =$...$=). You may also find +=--format= useful in more complex scenarios. For instance you could +print the only the line numbers containing formulas matching some +criterion. In the following, we print only the numbers of the lines +of =scheck.ltl= that contain guarantee formulas: + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt --lbt-input -F scheck.ltl --guarantee --format=%L +#+END_SRC +#+RESULTS: +: 2 +: 3 +: 4 # 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 diff --git a/src/bin/common_output.cc b/src/bin/common_output.cc index 8fb84f89c..fa7718cd8 100644 --- a/src/bin/common_output.cc +++ b/src/bin/common_output.cc @@ -20,14 +20,17 @@ #include "common_sys.hh" #include "common_output.hh" #include +#include #include "ltlvisit/tostring.hh" #include "ltlvisit/lbt.hh" +#include "misc/formater.hh" #include "common_cout.hh" #include "error.h" #define OPT_SPOT 1 #define OPT_WRING 2 #define OPT_LATEX 3 +#define OPT_FORMAT 4 output_format_t output_format = spot_output; bool full_parenth = false; @@ -42,13 +45,126 @@ 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 }, + { "format", OPT_FORMAT, "FORMAT", 0, + "specify how each line should be output (default: \"%f\")", -20 }, { 0, 0, 0, 0, 0, 0 } }; const struct argp output_argp = { options, parse_opt_output, 0, 0, 0, 0, 0 }; +static +void +report_not_ltl(const spot::ltl::formula* f, + const char* filename, int linenum, const char* syn) +{ + std::string s = spot::ltl::to_string(f); + static const char msg[] = + "formula '%s' cannot be written %s's syntax because it is not LTL"; + if (filename) + error_at_line(2, 0, filename, linenum, msg, s.c_str(), syn); + else + error(2, 0, msg, s.c_str(), syn); +} + +static void +stream_formula(std::ostream& out, + const spot::ltl::formula* f, const char* filename, int linenum) +{ + switch (output_format) + { + case lbt_output: + if (f->is_ltl_formula()) + spot::ltl::to_lbt_string(f, out); + else + report_not_ltl(f, filename, linenum, "LBT"); + break; + case spot_output: + spot::ltl::to_string(f, out, full_parenth); + break; + case spin_output: + if (f->is_ltl_formula()) + spot::ltl::to_spin_string(f, out, full_parenth); + else + report_not_ltl(f, filename, linenum, "Spin"); + break; + case wring_output: + if (f->is_ltl_formula()) + spot::ltl::to_wring_string(f, out); + else + report_not_ltl(f, filename, linenum, "Wring"); + break; + case utf8_output: + spot::ltl::to_utf8_string(f, out, full_parenth); + break; + case latex_output: + spot::ltl::to_latex_string(f, out, full_parenth); + break; + } +} + +namespace +{ + struct formula_with_location + { + const spot::ltl::formula* f; + const char* filename; + int line; + }; + + class printable_formula: + public spot::printable_value + { + public: + printable_formula& + operator=(const formula_with_location* new_val) + { + val_ = new_val; + return *this; + } + + virtual void + print(std::ostream& os, const char*) const + { + stream_formula(os, + val_->f, + val_->filename, + val_->line); + } + }; + + class formula_printer: protected spot::formater + { + public: + formula_printer(std::ostream& os, const char* format) + : format_(format) + { + declare('f', &fl_); + declare('F', &filename_); + declare('L', &line_); + set_output(os); + } + + std::ostream& + print(const formula_with_location& fl) + { + fl_ = &fl; + filename_ = fl.filename ? fl.filename : ""; + line_ = fl.line; + return format(format_); + } + + private: + const char* format_; + printable_formula fl_; + spot::printable_value filename_; + spot::printable_value line_; + }; +} + +static formula_printer* format = 0; + int -parse_opt_output(int key, char*, struct argp_state*) +parse_opt_output(int key, char* arg, struct argp_state*) { // This switch is alphabetically-ordered. switch (key) @@ -74,60 +190,30 @@ parse_opt_output(int key, char*, struct argp_state*) case OPT_WRING: output_format = wring_output; break; + case OPT_FORMAT: + delete format; + format = new formula_printer(std::cout, arg); + break; default: return ARGP_ERR_UNKNOWN; } return 0; } -static -void -report_not_ltl(const spot::ltl::formula* f, - const char* filename, int linenum, const char* syn) -{ - std::string s = spot::ltl::to_string(f); - static const char msg[] = - "formula '%s' cannot be written %s's syntax because it is not LTL"; - if (filename) - error_at_line(2, 0, filename, linenum, msg, s.c_str(), syn); - else - error(2, 0, msg, s.c_str(), syn); -} - void output_formula(const spot::ltl::formula* f, const char* filename, int linenum) { - switch (output_format) + if (!format) { - case lbt_output: - if (f->is_ltl_formula()) - spot::ltl::to_lbt_string(f, std::cout); - else - report_not_ltl(f, filename, linenum, "LBT"); - break; - case spot_output: - spot::ltl::to_string(f, std::cout, full_parenth); - break; - case spin_output: - if (f->is_ltl_formula()) - spot::ltl::to_spin_string(f, std::cout, full_parenth); - else - report_not_ltl(f, filename, linenum, "Spin"); - break; - case wring_output: - if (f->is_ltl_formula()) - spot::ltl::to_wring_string(f, std::cout); - else - report_not_ltl(f, filename, linenum, "Wring"); - break; - case utf8_output: - spot::ltl::to_utf8_string(f, std::cout, full_parenth); - break; - case latex_output: - spot::ltl::to_latex_string(f, std::cout, full_parenth); - break; + stream_formula(std::cout, f, filename, linenum); } + else + { + formula_with_location fl = { f, filename, linenum }; + format->print(fl); + } + // 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; diff --git a/src/bin/genltl.cc b/src/bin/genltl.cc index 678f396a5..371b47cf0 100644 --- a/src/bin/genltl.cc +++ b/src/bin/genltl.cc @@ -96,26 +96,52 @@ using namespace spot::ltl; const char argp_program_doc[] ="\ Generate temporal logic formulas from predefined scalable patterns."; -#define OPT_AND_F 2 -#define OPT_AND_FG 3 -#define OPT_AND_GF 4 -#define OPT_CCJ_ALPHA 5 -#define OPT_CCJ_BETA 6 -#define OPT_CCJ_BETA_PRIME 7 -#define OPT_GH_Q 8 -#define OPT_GH_R 9 -#define OPT_GO_THETA 10 -#define OPT_OR_FG 11 -#define OPT_OR_G 12 -#define OPT_OR_GF 13 -#define OPT_R_LEFT 14 -#define OPT_R_RIGHT 15 -#define OPT_RV_COUNTER 16 -#define OPT_RV_COUNTER_CARRY 17 -#define OPT_RV_COUNTER_CARRY_LINEAR 18 -#define OPT_RV_COUNTER_LINEAR 19 -#define OPT_U_LEFT 20 -#define OPT_U_RIGHT 21 +#define OPT_AND_F 1 +#define OPT_AND_FG 2 +#define OPT_AND_GF 3 +#define OPT_CCJ_ALPHA 4 +#define OPT_CCJ_BETA 5 +#define OPT_CCJ_BETA_PRIME 6 +#define OPT_GH_Q 7 +#define OPT_GH_R 8 +#define OPT_GO_THETA 9 +#define OPT_OR_FG 10 +#define OPT_OR_G 11 +#define OPT_OR_GF 12 +#define OPT_R_LEFT 13 +#define OPT_R_RIGHT 14 +#define OPT_RV_COUNTER 15 +#define OPT_RV_COUNTER_CARRY 16 +#define OPT_RV_COUNTER_CARRY_LINEAR 17 +#define OPT_RV_COUNTER_LINEAR 18 +#define OPT_U_LEFT 19 +#define OPT_U_RIGHT 20 +#define LAST_CLASS 20 + +const char* const class_name[LAST_CLASS] = + { + "and-f", + "and-fg", + "and-gf", + "ccj-alpha", + "ccj-beta", + "ccj-beta-prime", + "gh-q", + "gh-r", + "go-theta", + "or-fg", + "or-g", + "or-gf", + "or-r-left", + "or-r-right", + "rv-counter", + "rv-counter-carry", + "rv-counter-carry-linear", + "rv-counter-linear", + "u-left", + "u-right", + }; + #define OPT_ALIAS(o) { #o, 0, 0, OPTION_ALIAS, 0, 0 } @@ -168,6 +194,16 @@ static const argp_option options[] = RANGE_DOC, /**************************************************/ { 0, 0, 0, 0, "Output options:", -20 }, + { 0, 0, 0, 0, "The FORMAT string passed to --format may use "\ + "the following interpreted sequences:", -19 }, + { "%f", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "the formula (in the selected syntax)", 0 }, + { "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "the name of the pattern", 0 }, + { "%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "the argument of the pattern", 0 }, + { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "a single %", 0 }, { 0, 0, 0, 0, "Miscellaneous options:", -1 }, { 0, 0, 0, 0, 0, 0 } }; @@ -810,7 +846,7 @@ output_pattern(int pattern, int n) f = r; } - output_formula(f); + output_formula(f, class_name[pattern - 1], n); f->destroy(); } diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index d610be2ec..5cb4a8616 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -153,6 +153,16 @@ static const argp_option options[] = "drop formulas that have already been output (not affected by -v)", 0 }, /**************************************************/ { 0, 0, 0, 0, "Output options:", -20 }, + { 0, 0, 0, 0, "The FORMAT string passed to --format may use "\ + "the following interpreted sequences:", -19 }, + { "%f", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "the formula (in the selected syntax)", 0 }, + { "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "the name of the input file", 0 }, + { "%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "the original line number in the input file", 0 }, + { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "a single %", 0 }, { 0, 0, 0, 0, "Miscellaneous options:", -1 }, { 0, 0, 0, 0, 0, 0 } }; diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc index 35fe9d1d0..d6ae4dd54 100644 --- a/src/bin/randltl.cc +++ b/src/bin/randltl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -107,6 +107,14 @@ static const argp_option options[] = "listed by --dump-priorities.", 0 }, /**************************************************/ { 0, 0, 0, 0, "Output options:", -20 }, + { 0, 0, 0, 0, "The FORMAT string passed to --format may use "\ + "the following interpreted sequences:", -19 }, + { "%f", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "the formula (in the selected syntax)", 0 }, + { "%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "the (serial) number of the formula", 0 }, + { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "a single %", 0 }, { 0, 0, 0, 0, "Miscellaneous options:", -1 }, { 0, 0, 0, 0, 0, 0 } }; @@ -387,7 +395,8 @@ main(int argc, char** argv) if (trials == 0) error(2, 0, "failed to generate a new unique formula after %d trials", MAX_TRIALS); - output_formula(f); + static int count = 0; + output_formula(f, 0, ++count); f->destroy(); }; diff --git a/src/ltltest/latex.test b/src/ltltest/latex.test index 8a8954216..b8309d747 100755 --- a/src/ltltest/latex.test +++ b/src/ltltest/latex.test @@ -44,13 +44,13 @@ cat <<\EOF \usepackage{amsmath} \usepackage{spotltl} \begin{document} -\begin{align} +\begin{tabular}{ll} EOF -( ../../bin/ltlfilt --latex input; - ../../bin/genltl --go-theta=1..3 --latex ) | sed 's/$/\\\\/' +( ../../bin/ltlfilt --latex input --format='\texttt{%F:%L} & $%f$ \\'; + ../../bin/genltl --go-theta=1..3 --latex \ + --format='\texttt{--%F:%L} & $%f$ \\') cat <<\EOF -\text{done} -\end{align} +\end{tabular} \end{document} EOF ) > output.tex