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

 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

bin/common_output.cc

@@ -22,6 +22,8 @@
 #include <iostream>
 #include <sstream>
 #include <spot/tl/print.hh>
+#include <spot/tl/length.hh>
+#include <spot/tl/apcollect.hh>
 #include <spot/misc/formater.hh>
 #include <spot/misc/escape.hh>
 #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<int> line_;
     spot::printable_value<const char*> prefix_;
     spot::printable_value<const char*> suffix_;
+    spot::printable_value<int> size_;
+    spot::printable_value<int> bool_size_;
+    spot::printable_value<int> ap_num_;
   };
 }
 

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);

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 }
   };

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 }
   };

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[] = {

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 }
   };

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.
 

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: <code>--latex --format='$%f$'</code>
-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
+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
+rm -f ltlex.def ltlex.never scheck.ltl
 #+END_SRC
 
 #  LocalWords:  ltlfilt num toc LTL PSL syntaxes LBT's SRC GFp scheck

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 \

tests/core/format.test

+#! /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 <http://www.gnu.org/licenses/>.
+
+
+. ./defs || exit 1
+
+set -e
+
+genltl --dac=1..10 --format='%s,%b,%a,%f' > output
+cat >expected <<EOF
+3,2,1,G!p0
+7,6,2,Fp0 -> (!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<ap-1.ltl`
+test 10 = `wc -l<ap-2.ltl`
+test 16 = `wc -l<ap-3.ltl`
+test 13 = `wc -l<ap-4.ltl`
+test 10 = `wc -l<ap-5.ltl`
+test 2 = `wc -l<ap-6.ltl`
+
+genltl --dac --output='ap-%a.ltl2'
+for i in 1 2 3 4 5 6; do
+  cmp ap-$i.ltl ap-$i.ltl2 || exit 1
+done