add options to %x to list atomic propositions

* bin/common_aoutput.cc, bin/common_aoutput.hh, bin/common_output.cc,
bin/common_output.hh: Add options to %x to list atomic propositions
with various quoting scheme.  Deprecate --format=%a in favor of the
new --format=%x for consistency with --stats=%x.
* tests/core/format.test, tests/core/remprop.test: Adjust and add more
tests.
* NEWS: Mention these changes.

NEWS

@@ -4,7 +4,9 @@ New in spot 2.3.1.dev (not yet released)
 
   - In tools that output automata the number of atomic propositions
     can be output using --stats=%x (output automaton) or --stats=%X
-    (input automaton).
+    (input automaton).  Additional options can be passed to list
+    atomic propositions instead of conting them.  Tools that output
+    formulas also support --format=%x for this purpose.
 
   Bugs fixed:
 
@@ -14,6 +16,14 @@ New in spot 2.3.1.dev (not yet released)
   - Because of a typo, the output of --stats='...%P...' was correct
     only if %p was used as well.
 
+  Deprecation notices:
+
+  - Using --format=%a to print the number of atomic propositions in
+    ltlfilt, genltl, and randltl still works, but it is not documented
+    anymore and should be replaced by the newly-introduced --format=%x
+    for consistency with tools producing automata.
+
+
 New in spot 2.3.1 (2017-02-20)
 
   Tools:

bin/common_aoutput.cc

@@ -20,12 +20,15 @@
 #include "common_sys.hh"
 #include "error.h"
 #include "argmatch.h"
+#include "common_output.hh"
 #include "common_aoutput.hh"
 #include "common_post.hh"
 #include "common_cout.hh"
 
 #include <unistd.h>
 #include <ctime>
+#include <ctype.h>
+#include <spot/misc/escape.hh>
 #include <spot/twa/bddprint.hh>
 #include <spot/twaalgos/dot.hh>
 #include <spot/twaalgos/hoa.hh>
@@ -193,8 +196,9 @@ static const argp_option io_options[] =
       "wall-clock time elapsed in seconds (excluding parsing)", 0 },
     { "%W, %w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
       "one word accepted by the automaton", 0 },
-    { "%X, %x", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
+    { "%X, %x, %[LETTERS]X, %[LETTERS]x", 0, nullptr,
-      "number of atomic propositions declared in the automaton", 0 },
+      OPTION_DOC | OPTION_NO_USAGE,
+      COMMON_X_OUTPUT_SPECS(declared in the automaton), 0 },
     { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
       "a single %", 0 },
     { "%<", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
@@ -254,8 +258,9 @@ static const argp_option o_options[] =
       "wall-clock time elapsed in seconds (excluding parsing)", 0 },
     { "%w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
       "one word accepted by the output automaton", 0 },
-    { "%x", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
+    { "%x, %[LETTERS]x", 0, nullptr,
-      "number of atomic propositions declared in the automaton", 0 },
+      OPTION_DOC | OPTION_NO_USAGE,
+      COMMON_X_OUTPUT_SPECS(declared in the automaton), 0 },
     { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
       "a single %", 0 },
     { nullptr, 0, nullptr, 0, nullptr, 0 }
@@ -367,7 +372,7 @@ hoa_stat_printer::hoa_stat_printer(std::ostream& os, const char* format,
       declare('S', &haut_states_);
       declare('T', &haut_trans_);
       declare('W', &haut_word_);
-      declare('X', &haut_ap_size_);
+      declare('X', &haut_ap_);
     }
   declare('<', &csv_prefix_);
   declare('>', &csv_suffix_);
@@ -379,7 +384,7 @@ hoa_stat_printer::hoa_stat_printer(std::ostream& os, const char* format,
   declare('h', &output_aut_);
   declare('m', &aut_name_);
   declare('w', &aut_word_);
-  declare('x', &aut_ap_size_);
+  declare('x', &aut_ap_);
 }
 
 std::ostream&
@@ -476,7 +481,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
             }
         }
       if (has('X'))
-        haut_ap_size_ = haut->aut->ap().size();
+        haut_ap_ = haut->aut->ap();
     }
 
   if (has('m'))
@@ -501,7 +506,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
         }
     }
   if (has('x'))
-    aut_ap_size_ = aut->ap().size();
+    aut_ap_ = aut->ap();
 
   auto& res = this->spot::stat_printer::print(aut, f, run_time);
   // Make sure we do not store the automaton until the next one is
@@ -625,6 +630,19 @@ void printable_automaton::print(std::ostream& os, const char* pos) const
   print_hoa(os, val_, options.c_str());
 }
 
+
+namespace
+{
+  static void percent_error(const char* beg, const char* pos)
+  {
+    std::ostringstream tmp;
+    const char* end = std::strchr(pos, ']');
+    tmp << "unknown option '" << *pos << "' in '%"
+        << std::string(beg, end + 2) << '\'';
+    throw std::runtime_error(tmp.str());
+  }
+}
+
 void printable_timer::print(std::ostream& os, const char* pos) const
 {
   double res = 0;
@@ -652,20 +670,9 @@ void printable_timer::print(std::ostream& os, const char* pos) const
   bool children = false;
 
   const char* beg = pos;
-  auto error = [&](std::string str)
-  {
-    std::ostringstream tmp;
-    const char* end = std::strchr(pos, ']');
-    tmp << "unknown option '" << str << "' in '%" << std::string(beg, end + 2)
-      << '\'';
-    throw std::runtime_error(tmp.str());
-  };
-
   do
-  {
+    switch (*++pos)
-    ++pos;
+      {
-    switch (*pos)
-    {
       case 'u':
         user = true;
         break;
@@ -685,9 +692,9 @@ void printable_timer::print(std::ostream& os, const char* pos) const
       case ']':
         break;
       default:
-        error(std::string(pos, pos + 1));
+        percent_error(beg, pos);
-    }
+      }
-  } while (*pos != ']');
+  while (*pos != ']');
 
   if (!parent && !children)
     parent = children = true;
@@ -697,3 +704,68 @@ void printable_timer::print(std::ostream& os, const char* pos) const
   res = val_.get_uscp(user, system, children, parent);
   os << res / clocks_per_sec;
 }
+
+void printable_varset::print(std::ostream& os, const char* pos) const
+{
+  if (*pos != '[')
+    {
+      os << val_.size();
+      return;
+    }
+  char qstyle = 's';            // quote style
+  bool parent = false;
+  std::string sep;
+
+  const char* beg = pos;
+  do
+    switch (int c = *++pos)
+      {
+      case 'p':
+        parent = true;
+        break;
+      case 'c':
+      case 'd':
+      case 's':
+      case 'n':
+        qstyle = c;
+        break;
+      case ']':
+        break;
+      default:
+        if (isalnum(c))
+          percent_error(beg, pos);
+        sep += c;
+      }
+  while (*pos != ']');
+
+  if (sep.empty())
+    sep = " ";
+
+  bool first = true;
+  for (auto f: val_)
+    {
+      if (first)
+        first = false;
+      else
+        os << sep;
+      if (parent)
+        os << '(';
+      switch (qstyle)
+        {
+        case 's':
+          os << f;
+          break;
+        case 'n':
+          os << f.ap_name();
+          break;
+        case 'd':
+          spot::escape_str(os << '"', f.ap_name()) << '"';
+          break;
+        case 'c':
+          spot::escape_rfc4180(os << '"', f.ap_name()) << '"';
+          break;
+        }
+      if (parent)
+        os << ')';
+    }
+}

bin/common_aoutput.hh

@@ -31,6 +31,7 @@
 #include <spot/twaalgos/sccinfo.hh>
 #include <spot/twaalgos/stats.hh>
 #include <spot/twaalgos/word.hh>
+#include <spot/tl/formula.hh>
 
 
 // Format for automaton output
@@ -107,6 +108,38 @@ struct printable_timer final:
   void print(std::ostream& os, const char* pos) const override;
 };
 
+struct printable_varset final: public spot::printable
+{
+protected:
+  std::vector<spot::formula> val_;
+  void sort()
+  {
+    std::sort(val_.begin(), val_.end(),
+              [](spot::formula f, spot::formula g)
+              {
+                return strverscmp(f.ap_name().c_str(), g.ap_name().c_str()) < 0;
+              });
+  }
+public:
+
+  template<class T>
+  void set(T begin, T end)
+  {
+    val_.clear();
+    val_.insert(val_.end(), begin, end);
+    sort();
+  }
+
+  printable_varset& operator=(const std::vector<spot::formula>& val)
+  {
+    val_ = val;
+    sort();
+    return *this;
+  }
+
+  void print(std::ostream& os, const char* pos) const override;
+};
+
 /// \brief prints various statistics about a TGBA
 ///
 /// This object can be configured to display various statistics
@@ -144,8 +177,8 @@ private:
   spot::printable_value<unsigned> haut_edges_;
   spot::printable_value<unsigned> haut_trans_;
   spot::printable_value<unsigned> haut_acc_;
-  spot::printable_value<unsigned> haut_ap_size_;
+  printable_varset haut_ap_;
-  spot::printable_value<unsigned> aut_ap_size_;
+  printable_varset aut_ap_;
   spot::printable_scc_info haut_scc_;
   spot::printable_value<unsigned> haut_deterministic_;
   spot::printable_value<unsigned> haut_nondetstates_;

bin/common_output.cc

@@ -19,6 +19,7 @@
 
 #include "common_sys.hh"
 #include "common_output.hh"
+#include "common_aoutput.hh"
 #include <iostream>
 #include <sstream>
 #include <spot/tl/print.hh>
@@ -203,13 +204,14 @@ namespace
     formula_printer(std::ostream& os, const char* format)
       : format_(format)
     {
-      declare('a', &ap_num_);
+      declare('a', &ap_);       // deprecated in 2.3.2
       declare('b', &bool_size_);
       declare('f', &fl_);
       declare('F', &filename_);
       declare('L', &line_);
       declare('s', &size_);
       declare('h', &class_);
+      declare('x', &ap_);
       declare('<', &prefix_);
       declare('>', &suffix_);
       set_output(os);
@@ -225,10 +227,10 @@ namespace
       prefix_ = fl.prefix ? fl.prefix : "";
       suffix_ = fl.suffix ? fl.suffix : "";
       auto f = fl_.val()->f;
-      if (has('a'))
+      if (has('a') || has('x'))
         {
           auto s = spot::atomic_prop_collect(f);
-          ap_num_ = s->size();
+          ap_.set(s->begin(), s->end());
           delete s;
         }
       if (has('b'))
@@ -250,7 +252,7 @@ namespace
     spot::printable_value<int> size_;
     printable_formula_class class_;
     spot::printable_value<int> bool_size_;
-    spot::printable_value<int> ap_num_;
+    printable_varset ap_;
   };
 }
 

bin/common_output.hh

@@ -36,9 +36,18 @@ extern output_format_t output_format;
 extern bool full_parenth;
 extern bool escape_csv;
 
+#define COMMON_X_OUTPUT_SPECS(where)                                    \
+      "number of atomic propositions " #where "; "      \
+      " add LETTERS to list atomic propositions with "                  \
+      "(n) no quoting, "                                                \
+      "(s) occasional double-quotes with C-style escape, "              \
+      "(d) double-quotes with C-style escape, "                         \
+      "(c) double-quotes with CSV-style escape, "                       \
+      "(p) between parentheses, "                                       \
+      "any extra non-alphanumeric character will be used to "           \
+      "separate propositions"
+
 #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,                   \
@@ -47,7 +56,10 @@ extern bool escape_csv;
     { "%h, %[vw]h", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,           \
         "the class of the formula is the Manna-Pnueli hierarchy "       \
         "([v] replaces abbreviations by class names, [w] for all "      \
-        "compatible classes)", 0 }
+        "compatible classes)", 0 },                                     \
+    { "%x, %[LETTERS]X, %[LETTERS]x", 0, nullptr,                       \
+        OPTION_DOC | OPTION_NO_USAGE,                                   \
+        COMMON_X_OUTPUT_SPECS(used in the formula), 0 }
 
 extern const struct argp output_argp;
 

tests/core/format.test

@@ -23,7 +23,7 @@
 
 set -e
 
-genltl --dac=1..10 --format='%s,%b,%a,%f' > output
+genltl --dac=1..10 --format='%s,%b,%x,%f' > output
 cat >expected <<EOF
 3,2,1,G!p0
 7,6,2,Fp0 -> (!p1 U p0)
@@ -38,7 +38,7 @@ cat >expected <<EOF
 EOF
 diff output expected
 
-genltl --dac | ltlfilt --output='ap-%a.ltl'
+genltl --dac | ltlfilt --output='ap-%x.ltl'
 test 4 = `wc -l<ap-1.ltl`
 test 10 = `wc -l<ap-2.ltl`
 test 16 = `wc -l<ap-3.ltl`
@@ -46,7 +46,7 @@ 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'
+genltl --dac --output='ap-%x.ltl2'
 for i in 1 2 3 4 5 6; do
   cmp ap-$i.ltl ap-$i.ltl2 || exit 1
 done
@@ -56,7 +56,7 @@ out=`<GFa autfilt --stats='%W,%w' --complement`
 test "$out" = "cycle{a},cycle{!a}"
 ltl2tgba FGa > FGa
 test "0,1,0,1" = "`<FGa autfilt -D --stats='%D,%d,%P,%p'`"
-test "0,0,0,1" = "`<FGa autfilt -C --stats='%D,%d,%P,%p'`"
+test '0,0,0,1,"a"' = "`<FGa autfilt -C --stats='%D,%d,%P,%p,%[d]x'`"
 # We had some issues in the pase where %P was set only if %p was used
 # as well.  So we make separate tests for this.
 test "0,0" = "`<FGa autfilt -C --stats='%D,%P'`"

tests/core/remprop.test

@@ -75,6 +75,7 @@ diff out expected
 
 cat >expected <<EOF
 HOA: v1
+name: "\"a\", \"b\", \"c\"->(c)"
 States: 3
 Start: 0
 AP: 1 "c"
@@ -90,7 +91,7 @@ State: 2
 --END--
 EOF
 
-run 0 autfilt -H --remove-ap=a=1,b=0 automaton >out
+run 0 autfilt -H --remove-ap=a=1,b=0 --name='%[d, ]X->%[p]x' automaton >out
 cat out
 diff out expected