ltlfilt: add a --count option, like autfilt

* src/bin/common_output.cc, src/bin/common_output.hh:
Add count_output.
* src/bin/ltlfilt.cc: Add the --count option.
* src/ltltest/ltlfilt.test: Test it.
* NEWS: Mention it.

NEWS

@@ -41,6 +41,9 @@ New in spot 1.99a (not yet released)
       now.  The short '-n NUM' option is now the same as the new
       --max-count=N option, for consistency with other tools.
 
+    - ltlfilt has a new --count option to count the number of matching
+      automata.
+
     - ltlcross (and ltldo) have a list of hard-coded shorthands
       for some existing tools.  So for instance running
       'ltlcross spin ...' is the same as running

src/bin/common_output.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -104,6 +104,7 @@ stream_formula(std::ostream& out,
     case latex_output:
       spot::ltl::to_latex_string(f, out, full_parenth);
       break;
+    case count_output:
     case quiet_output:
       break;
     }
@@ -261,10 +262,10 @@ output_formula_checked(const spot::ltl::formula* f,
 		       const char* filename, int linenum,
 		       const char* prefix, const char* suffix)
 {
-  if (output_format == quiet_output)
+  if (output_format == quiet_output || output_format == count_output)
     return;
   output_formula(std::cout, f, filename, linenum, prefix, suffix);
-  std::cout << std::endl;
+  std::cout << '\n';
   // Make sure we abort if we can't write to std::cout anymore
   // (like disk full or broken pipe with SIGPIPE ignored).
   check_cout();

src/bin/common_output.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -29,7 +29,7 @@
 
 enum output_format_t { spot_output, spin_output, utf8_output,
 		       lbt_output, wring_output, latex_output,
-                       quiet_output };
+                       quiet_output, count_output };
 extern output_format_t output_format;
 extern bool full_parenth;
 extern bool escape_csv;

src/bin/ltlfilt.cc

@@ -168,6 +168,7 @@ static const argp_option options[] =
       "drop formulas that have already been output (not affected by -v)", 0 },
     /**************************************************/
     { 0, 0, 0, 0, "Output options:", -20 },
+    { "count", 'c', 0, 0, "print only a count of matched formulas", 0 },
     { "quiet", 'q', 0, 0, "suppress all normal output", 0 },
     { "max-count", 'n', "NUM", 0, "output at most NUM formulas", 0 },
     { 0, 0, 0, 0, "The FORMAT string passed to --format may use "\
@@ -235,6 +236,7 @@ static bool stutter_insensitive = false;
 static bool ap = false;
 static unsigned ap_n = 0;
 static int opt_max_count = -1;
+static long int match_count = 0;
 
 static const spot::ltl::formula* implied_by = 0;
 static const spot::ltl::formula* imply = 0;
@@ -258,6 +260,9 @@ parse_opt(int key, char* arg, struct argp_state*)
   // This switch is alphabetically-ordered.
   switch (key)
     {
+    case 'c':
+      output_format = count_output;
+      break;
     case 'n':
       opt_max_count = to_pos_int(arg);
       break;
@@ -472,7 +477,7 @@ namespace
     process_formula(const spot::ltl::formula* f,
 		    const char* filename = 0, int linenum = 0)
     {
-      if (opt_max_count == 0)
+      if (opt_max_count >= 0 && match_count >= opt_max_count)
 	{
 	  abort_run = true;
 	  f->destroy();
@@ -607,8 +612,7 @@ namespace
 	{
 	  one_match = true;
 	  output_formula_checked(f, filename, linenum, prefix, suffix);
-	  if (opt_max_count > 0)
-	    --opt_max_count;
+	  ++match_count;
 	}
       f->destroy();
       return 0;
@@ -635,8 +639,19 @@ main(int argc, char** argv)
   spot::ltl::ltl_simplifier_options opt = simplifier_options();
   opt.boolean_to_isop = boolean_to_isop;
   spot::ltl::ltl_simplifier simpl(opt);
-  ltl_processor processor(simpl);
-  if (processor.run())
-    return 2;
+  try
+    {
+      ltl_processor processor(simpl);
+      if (processor.run())
+	return 2;
+    }
+  catch (const std::runtime_error& e)
+    {
+      error(2, 0, "%s", e.what());
+    }
+
+  if (output_format == count_output)
+    std::cout << match_count << std::endl;
+
   return one_match ? 0 : 1;
 }

src/ltltest/ltlfilt.test

@@ -83,6 +83,10 @@ F(a & !Xa & Xb)
 a & (b | c)
 EOF
 
+checkopt -c --stutter-invariant <<EOF
+9
+EOF
+
 checkopt --simplify <<EOF
 F(GFa | Gb)
 F(GFa | Gb)