From 926ffbf965efb7232569f59ffbdf1b3658817666 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 15 Aug 2016 15:45:26 +0200 Subject: [PATCH] bin: %a,%b,%s format specs for LTL output * NEWS: Mention those. * bin/common_output.cc, bin/common_output.hh: Implement them. * bin/genltl.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randltl.cc: Update --help. * tests/core/format.test: New file. * tests/Makefile.am: Add it. * doc/org/ioltl.org, doc/org/ltlfilt.org: Update documentation. --- NEWS | 10 ++++++ bin/common_output.cc | 20 +++++++++++ bin/common_output.hh | 9 +++++ bin/genltl.cc | 1 + bin/ltlfilt.cc | 1 + bin/ltlgrind.cc | 5 +-- bin/randltl.cc | 1 + doc/org/ioltl.org | 15 ++++---- doc/org/ltlfilt.org | 81 +++++++++++++++++++++++++++++++++++------- tests/Makefile.am | 3 +- tests/core/format.test | 52 +++++++++++++++++++++++++++ 11 files changed, 177 insertions(+), 21 deletions(-) create mode 100644 tests/core/format.test diff --git a/NEWS b/NEWS index f082b5087..d421d16ae 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,15 @@ New in spot 2.1.0a (not yet released) + Command-line tools: + + * ltlfilt, randltl, genltl, and ltlgrind learned to display the size + (%s), Boolean size (%b), and number of atomic propositions (%b) + with the --format and --output options. A typical use is to sort + formulas by size: + genltl --dac --format='%s,%f' | sort -n | cut -d, -f2 + or to group formulas by number of atomic propositions: + genltl --dac --output='ap-%a.ltl' + Bugs fixed: * Fix several cases where command-line tools would fail to diagnose diff --git a/bin/common_output.cc b/bin/common_output.cc index 6109b4e1e..f0a162a87 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -22,6 +22,8 @@ #include #include #include +#include +#include #include #include #include "common_cout.hh" @@ -179,12 +181,16 @@ namespace formula_printer(std::ostream& os, const char* format) : format_(format) { + declare('a', &ap_num_); + declare('b', &bool_size_); declare('f', &fl_); declare('F', &filename_); declare('L', &line_); + declare('s', &size_); declare('<', &prefix_); declare('>', &suffix_); set_output(os); + prime(format); } std::ostream& @@ -195,6 +201,17 @@ namespace line_ = fl.line; prefix_ = fl.prefix ? fl.prefix : ""; suffix_ = fl.suffix ? fl.suffix : ""; + auto f = fl_.val()->f; + if (has('a')) + { + auto s = spot::atomic_prop_collect(f); + ap_num_ = s->size(); + delete s; + } + if (has('b')) + bool_size_ = spot::length_boolone(f); + if (has('s')) + size_ = spot::length(f); return format(format_); } @@ -205,6 +222,9 @@ namespace spot::printable_value line_; spot::printable_value prefix_; spot::printable_value suffix_; + spot::printable_value size_; + spot::printable_value bool_size_; + spot::printable_value ap_num_; }; } diff --git a/bin/common_output.hh b/bin/common_output.hh index 4c1fc0b7b..fac994bbb 100644 --- a/bin/common_output.hh +++ b/bin/common_output.hh @@ -36,6 +36,15 @@ extern output_format_t output_format; extern bool full_parenth; extern bool escape_csv; +#define COMMON_LTL_OUTPUT_SPECS \ + { "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \ + "number of atomic propositions used in the formula", 0 }, \ + { "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \ + "the length (or size) of the formula", 0 }, \ + { "%b", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \ + "the Boolean-length of the formula (i.e., all Boolean " \ + "subformulas count as 1)", 0 } + extern const struct argp output_argp; int parse_opt_output(int key, char* arg, struct argp_state* state); diff --git a/bin/genltl.cc b/bin/genltl.cc index e0c6ccb8f..a7f2d61ea 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -270,6 +270,7 @@ static const argp_option options[] = "the argument of the pattern", 0 }, { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, + COMMON_LTL_OUTPUT_SPECS, { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, { nullptr, 0, nullptr, 0, nullptr, 0 } }; diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index e0e5d3534..c3da8fd8a 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -230,6 +230,7 @@ static const argp_option options[] = "comes from a column extracted from a CSV file", 0 }, { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, + COMMON_LTL_OUTPUT_SPECS, { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, { nullptr, 0, nullptr, 0, nullptr, 0 } }; diff --git a/bin/ltlgrind.cc b/bin/ltlgrind.cc index a67d52a36..6e112516f 100644 --- a/bin/ltlgrind.cc +++ b/bin/ltlgrind.cc @@ -96,8 +96,9 @@ static const argp_option options[] = { "comes from a column extracted from a CSV file", 0 }, { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, - {nullptr, 0, nullptr, 0, "Miscellaneous options:", -1}, - {nullptr, 0, nullptr, 0, nullptr, 0} + COMMON_LTL_OUTPUT_SPECS, + { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, + { nullptr, 0, nullptr, 0, nullptr, 0 } }; static const argp_child children[] = { diff --git a/bin/randltl.cc b/bin/randltl.cc index db183d3d4..fbff92935 100644 --- a/bin/randltl.cc +++ b/bin/randltl.cc @@ -119,6 +119,7 @@ static const argp_option options[] = "the (serial) number of the formula", 0 }, { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, + COMMON_LTL_OUTPUT_SPECS, { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, { nullptr, 0, nullptr, 0, nullptr, 0 } }; diff --git a/doc/org/ioltl.org b/doc/org/ioltl.org index be7d10695..91cf9227e 100644 --- a/doc/org/ioltl.org +++ b/doc/org/ioltl.org @@ -199,15 +199,18 @@ 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 | 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) | +| | =%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) | +| [[file:ltlfilt.org][=ltlgrind=]] | output formula | input filename | input line | leading text | trailing text | +Other =%=-sequences are supported by these tools, and documented in +the output of =--help=. 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 +redirect the output to a file, and pipe it to another tool. The =--output= (or =-o=) allows you to construct a filename using some of the above =%=-sequences. diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index d662b505c..0051caca9 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -49,9 +49,9 @@ ltlfilt --lbt-input -F scheck.ltl #+END_SRC #+RESULTS: : !(Gp0 | (Gp1 & Fp3)) -: Xp7 | Fp6 | p3 +: p3 | Xp7 | Fp6 : ((Xp0 & Xp4) U Fp1) & XX(XFp5 U (p0 U XXp3)) -: p0 U ((p0 | p5) & p1) +: p0 U (p1 & (p0 | p5)) * Altering the formula @@ -255,8 +255,9 @@ ltlfilt --help | sed -n '/Filtering options.*:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: #+begin_example - --ap=N match formulas which use exactly N atomic - propositions + --accept-word=WORD keep formulas that accept WORD + --ap=RANGE match formulas with a number of atomic + propositions in RANGE --boolean match Boolean formulas --bsize=RANGE match formulas with Boolean size in RANGE --equivalent-to=FORMULA match formulas equivalent to FORMULA @@ -266,6 +267,7 @@ ltlfilt --help | sed -n '/Filtering options.*:/,/^$/p' | sed '1d;$d' --imply=FORMULA match formulas implying FORMULA --ltl match only LTL formulas (no PSL operator) --obligation match obligation formulas (even pathological) + --reject-word=WORD keep formulas that reject WORD --safety match safety formulas (even pathological) --size=RANGE match formulas with size in RANGE --stutter-insensitive, --stutter-invariant @@ -447,16 +449,39 @@ GF(1 U b) (a U b) R b #+end_example +* Using =--format= and =--output= -* Using =--format= +The =--format= option can be used the alter the way formulas are output. +The list of supported =%=-escape sequences are recalled in the =--help= output: +#+BEGIN_SRC sh :results verbatim :exports results +ltlfilt --help | sed -n '/The FORMAT/,/^$/p' | sed '$d' +#+END_SRC +#+RESULTS: +#+begin_example + The FORMAT string passed to --format may use the following interpreted + sequences: + %< the part of the line before the formula if it + comes from a column extracted from a CSV file + %> the part of the line after the formula if it comes + from a column extracted from a CSV file + %% a single % + %a number of atomic propositions used in the formula + %b the Boolean-length of the formula (i.e., all + Boolean subformulas count as 1) + %f the formula (in the selected syntax) + %F the name of the input file + %L the original line number in the input file + %s the length (or size) of the formula +#+end_example -The =--format= option can be used the alter the way formulas are output (for instance use +As a trivial example, 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 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: +to enclose formula in LaTeX format with =$...$=. + +But =--format= can be useful in more complex scenarios. For instance +you could print 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 @@ -466,11 +491,43 @@ ltlfilt --lbt-input -F scheck.ltl --guarantee --format=%L : 3 : 4 +We could also prefix each formula by its size, in order to sort +the file by formula size: + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt --lbt-input scheck.ltl --format='%s,%f' | sort -n +#+END_SRC + +#+RESULTS: +: 7,p0 U (p1 & (p0 | p5)) +: 7,p3 | Xp7 | Fp6 +: 9,!(Gp0 | (Gp1 & Fp3)) +: 20,((Xp0 & Xp4) U Fp1) & XX(XFp5 U (p0 U XXp3)) + [[file:csv.org][More examples of how to use =--format= to create CSV files are on a separate page]] + +The =--output= option interprets its argument as an output filename, +but after evaluating the =%=-escape sequence for each formula. This +makes it very easy to partition a list of formulas in different files. +For instance here is how to split =scheck.ltl= according to formula +sizes. + #+BEGIN_SRC sh :results verbatim :exports both -rm -f ltlex.def ltlex.never +ltlfilt --lbt-input scheck.ltl --output='scheck-%s.ltl' +wc -l scheck*.ltl +#+END_SRC + +#+RESULTS: +: 1 scheck-20.ltl +: 2 scheck-7.ltl +: 1 scheck-9.ltl +: 4 scheck.ltl +: 8 total + +#+BEGIN_SRC sh :results verbatim :exports both +rm -f ltlex.def ltlex.never scheck.ltl #+END_SRC # LocalWords: ltlfilt num toc LTL PSL syntaxes LBT's SRC GFp scheck diff --git a/tests/Makefile.am b/tests/Makefile.am index 7cad228c9..dfe075640 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -177,7 +177,8 @@ TESTS_tl = \ core/reduccmp.test \ core/uwrm.test \ core/eventuniv.test \ - core/stutter-ltl.test + core/stutter-ltl.test \ + core/format.test TESTS_graph = \ core/graph.test \ diff --git a/tests/core/format.test b/tests/core/format.test new file mode 100644 index 000000000..157953e6c --- /dev/null +++ b/tests/core/format.test @@ -0,0 +1,52 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2016 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + + +. ./defs || exit 1 + +set -e + +genltl --dac=1..10 --format='%s,%b,%a,%f' > output +cat >expected < (!p1 U p0) +6,5,2,G(p0 -> G!p1) +13,9,3,G((p0 & !p1 & Fp1) -> (!p2 U p1)) +10,6,3,G((p0 & !p1) -> (!p2 W p1)) +2,2,1,Fp0 +7,3,2,!p0 W (!p0 & p1) +9,8,2,G!p0 | F(p0 & Fp1) +13,6,3,G((p0 & !p1) -> (!p1 W (!p1 & p2))) +13,6,3,G((p0 & !p1) -> (!p1 U (!p1 & p2))) +EOF +diff output expected + +genltl --dac | ltlfilt --output='ap-%a.ltl' +test 4 = `wc -l