ltlcross: implement a --save-bogus=FILENAME option

Suggested by Joachim Klein.

* src/bin/ltlcross.cc: Implement it.
* src/tgbatest/ltlcross3.test: Test it.
* doc/org/ltlcross.org, NEWS: Document it.

NEWS

@@ -14,6 +14,10 @@ New in spot 1.2.4a (not yet released)
 
     - 'randltl 4' is now a shorthand for 'randltl p0 p1 p2 p3'.
 
+    - ltlcross has a new option --save-bogus=FILENAME to save any
+      formula for which a problem (other than timeout) was detected
+      during translation or using the resulting automatas.
+
   * Documentation:
 
     - The man page for ltl2tgba has some new notes and references

doc/org/ltlcross.org

@@ -610,9 +610,9 @@ automaton as well.
 
 ** =--stop-on-error=
 
-The =--stop-on-error= will cause =ltlcross= to abort on the first
+The =--stop-on-error= option will cause =ltlcross= to abort on the
-detected error.  This include failure to start some translator, read
+first detected error.  This include failure to start some translator,
-its output, or failure to passe the sanity checks.  Timeouts are
+read its output, or failure to passe the sanity checks.  Timeouts are
 allowed.
 
 One use for this option is when =ltlcross= is used in combination with
@@ -627,6 +627,30 @@ to remove duplicate formulas will keep growing).
 randltl -n -1 --tree-size 10..25 a b c | ltlcross --stop-on-error 'ltl2tgba --lbtt %f >%T' 'ltl3ba -f %s >%N'
 #+END_SRC
 
+** =--save-bogus=FILENAME=
+
+The =--save-bogus=FILENAME= will save any formula for which an error
+was detected (either some translation failed, or some problem was
+detected using the resulting automata) in =FILENAME=.  Again, timeouts
+are not considered to be errors, and therefore not reported in this
+file.
+
+The main use for this feature is in conjunction with =randltl='s
+generation of random formulas.  For instance the following command
+will run the translators on an infinite number of formulas, saving
+any problematic formula in =bugs.ltl=.
+
+#+BEGIN_SRC sh :export code :eval no
+randltl -n -1 --tree-size 10..25 a b c | ltlcross --save-bogus=bugs.ltl 'ltl2tgba --lbtt %f >%T' 'ltl3ba -f %s >%N'
+#+END_SRC
+
+You can periodically check the contents of =bugs.ltl=, and then run
+=ltlcross= only on those formulas to look at the problems:
+
+#+BEGIN_SRC sh :export code :eval no
+ltlcross -F bugs.ltl 'ltl2tgba --lbtt %f >%T' 'ltl3ba -f %s >%N'
+#+END_SRC
+
 ** =--no-check=
 
 The =--no-check= option disables all sanity checks, and only use the supplied

src/bin/ltlcross.cc

@@ -94,6 +94,7 @@ Exit status:\n\
 #define OPT_COLOR 10
 #define OPT_NOCOMP 11
 #define OPT_OMIT 12
+#define OPT_BOGUS 13
 
 static const argp_option options[] =
   {
@@ -159,6 +160,8 @@ static const argp_option options[] =
       "colorize output; WHEN can be 'never', 'always' (the default if "
       "--color is used without argument), or "
       "'auto' (the default if --color is not used)", 0 },
+    { "save-bogus", OPT_BOGUS, "FILENAME", 0,
+      "save formulas for which problems were detected in FILENAME", 0 },
     { 0, 0, 0, 0, 0, 0 }
   };
 
@@ -206,6 +209,8 @@ unsigned products = 1;
 bool products_avg = true;
 bool opt_omit = false;
 bool has_sr = false; // Has Streett or Rabin automata to process.
+const char* bogus_output_filename = 0;
+std::ofstream* bogus_output = 0;
 
 struct translator_spec
 {
@@ -509,6 +514,14 @@ parse_opt(int key, char* arg, struct argp_state*)
 		<< "on your platform" << std::endl;
 #endif
       break;
+    case OPT_BOGUS:
+      {
+	bogus_output = new std::ofstream(arg);
+	if (!*bogus_output)
+	  error(2, errno, "cannot open '%s'", arg);
+	bogus_output_filename = arg;
+	break;
+      }
     case OPT_COLOR:
       {
 	if (arg)
@@ -849,7 +862,8 @@ namespace
     }
 
     const spot::tgba*
-    translate(unsigned int translator_num, char l, statistics_formula* fstats)
+    translate(unsigned int translator_num, char l, statistics_formula* fstats,
+	      bool& problem)
     {
       output.reset(translator_num);
 
@@ -874,11 +888,13 @@ namespace
 	  std::cerr << "warning: timeout during execution of command\n";
 	  ++timeout_count;
 	  status_str = "timeout";
+	  problem = false;	// A timeout is not a sign of a bug
 	  es = -1;
 	}
       else if (WIFSIGNALED(es))
 	{
 	  status_str = "signal";
+	  problem = true;
 	  es = WTERMSIG(es);
 	  global_error() << "error: execution terminated by signal "
 			 << es << ".\n";
@@ -888,6 +904,7 @@ namespace
 	{
 	  es = WEXITSTATUS(es);
 	  status_str = "exit code";
+	  problem = true;
 	  global_error() << "error: execution returned exit code "
 			 << es << ".\n";
 	  end_error();
@@ -895,6 +912,7 @@ namespace
       else
 	{
 	  status_str = "ok";
+	  problem = false;
 	  es = 0;
 	  switch (output.format)
 	    {
@@ -906,6 +924,7 @@ namespace
 		if (!pel.empty())
 		  {
 		    status_str = "parse error";
+		    problem = true;
 		    es = -1;
 		    std::ostream& err = global_error();
 		    err << "error: failed to parse the produced neverclaim.\n";
@@ -923,6 +942,7 @@ namespace
 		if (!f)
 		  {
 		    status_str = "no output";
+		    problem = true;
 		    es = -1;
 		    global_error() << "Cannot open " << output.val()
 				   << std::endl;
@@ -934,6 +954,7 @@ namespace
 		    if (!res)
 		      {
 			status_str = "parse error";
+			problem = true;
 			es = -1;
 			global_error() << ("error: failed to parse output in "
 					   "LBTT format: ")
@@ -952,6 +973,7 @@ namespace
 		if (!pel.empty())
 		  {
 		    status_str = "parse error";
+		    problem = true;
 		    es = -1;
 		    std::ostream& err = global_error();
 		    err << "error: failed to parse the produced DSTAR"
@@ -1048,7 +1070,7 @@ namespace
     }
   };
 
-  static void
+  static bool
   check_empty_prod(const spot::tgba* aut_i, const spot::tgba* aut_j,
 		   size_t i, size_t j, bool icomp, bool jcomp)
   {
@@ -1091,9 +1113,10 @@ namespace
     delete res;
     delete ec;
     delete prod;
+    return res;
   }
 
-  static void
+  static bool
   cross_check(const std::vector<spot::scc_map*>& maps, char l, unsigned p)
   {
     size_t m = maps.size();
@@ -1146,7 +1169,9 @@ namespace
 	else
 	  err << "the state-space\n";
 	end_error();
+	return true;
       }
+    return false;
   }
 
   typedef std::set<spot::state*, spot::state_ptr_less_than> state_set;
@@ -1212,12 +1237,35 @@ namespace
 	(*i++)->destroy();
     }
 
+    int
+    process_string(const std::string& input,
+		   const char* filename,
+		   int linenum)
+    {
+      spot::ltl::parse_error_list pel;
+      const spot::ltl::formula* f = parse_formula(input, pel);
+
+      if (!f || !pel.empty())
+	{
+	  if (filename)
+	    error_at_line(0, 0, filename, linenum, "parse error:");
+	  spot::ltl::format_parse_errors(std::cerr, input, pel);
+	  if (f)
+	    f->destroy();
+	  return 1;
+	}
+      int res = process_formula(f, filename, linenum);
+
+      if (res && bogus_output)
+	*bogus_output << input << std::endl;
+      return 0;
+    }
+
+
     int
     process_formula(const spot::ltl::formula* f,
 		    const char* filename = 0, int linenum = 0)
     {
-      (void) filename;
-      (void) linenum;
       static unsigned round = 0;
 
       // If we need LBT atomic proposition in any of the input or
@@ -1268,6 +1316,9 @@ namespace
 	    }
 	}
 
+
+      int problems = 0;
+
       // These store the result of the translation of the positive and
       // negative formulas.
       size_t m = translators.size();
@@ -1288,7 +1339,10 @@ namespace
 
       for (size_t n = 0; n < m; ++n)
 	{
-	  pos[n] = runner.translate(n, 'P', pstats);
+	  bool prob;
+	  pos[n] = runner.translate(n, 'P', pstats, prob);
+	  problems += prob;
+
 	  // If the automaton is deterministic, compute its complement
 	  // as well.  Note that if we have computed statistics
 	  // already, there is no need to call is_deterministic()
@@ -1326,7 +1380,10 @@ namespace
 
 	  for (size_t n = 0; n < m; ++n)
 	    {
-	      neg[n] = runner.translate(n, 'N', nstats);
+	      bool prob;
+	      neg[n] = runner.translate(n, 'N', nstats, prob);
+	      problems += prob;
+
 	      // If the automaton is deterministic, compute its
 	      // complement as well.  Note that if we have computed
 	      // statistics already, there is no need to call
@@ -1353,6 +1410,7 @@ namespace
 	      for (size_t j = 0; j < m; ++j)
 		if (neg[j])
 		  {
+		    problems +=
 		      check_empty_prod(pos[i], neg[j], i, j, false, false);
 
 		    // Deal with the extra complemented automata if we
@@ -1371,11 +1429,16 @@ namespace
 		    // translation was not deterministic.
 
 		    if (i != j && comp_pos[j] && !comp_neg[j])
-		      check_empty_prod(pos[i], comp_pos[j], i, j, false, true);
+		      problems +=
+			check_empty_prod(pos[i], comp_pos[j],
+					 i, j, false, true);
 		    if (i != j && comp_neg[i] && !comp_neg[i])
-		      check_empty_prod(comp_neg[i], neg[j], i, j, true, false);
+		      problems +=
+			check_empty_prod(comp_neg[i], neg[j],
+					 i, j, true, false);
 		    if (comp_pos[i] && comp_neg[j] &&
 			(i == j || (!comp_neg[i] && !comp_pos[j])))
+		      problems +=
 			check_empty_prod(comp_pos[i], comp_neg[j],
 					 i, j, true, true);
 		  }
@@ -1457,14 +1520,16 @@ namespace
 	  if (!no_checks)
 	    {
 	      // cross-comparison test
-	      cross_check(pos_map, 'P', p);
+	      problems += cross_check(pos_map, 'P', p);
-	      cross_check(neg_map, 'N', p);
+	      problems += cross_check(neg_map, 'N', p);
 
 	      // consistency check
 	      for (size_t i = 0; i < m; ++i)
 		if (pos_map[i] && neg_map[i] &&
 		    !(consistency_check(pos_map[i], neg_map[i], statespace)))
 		  {
+		    ++problems;
+
 		    std::ostream& err = global_error();
 		    err << "error: inconsistency between P" << i
 			<< " and N" << i;
@@ -1507,7 +1572,7 @@ namespace
 
       // Shall we stop processing formulas now?
       abort_run = global_error_flag && stop_on_error;
-      return 0;
+      return problems;
     }
   };
 }
@@ -1525,7 +1590,7 @@ print_stats_csv(const char* filename)
   else
     {
       out = outfile = new std::ofstream(filename);
-      if (!outfile)
+      if (!*outfile)
 	error(2, errno, "cannot open '%s'", filename);
     }
 
@@ -1563,7 +1628,7 @@ print_stats_json(const char* filename)
   else
     {
       out = outfile = new std::ofstream(filename);
-      if (!outfile)
+      if (!*outfile)
 	error(2, errno, "cannot open '%s'", filename);
     }
 
@@ -1642,10 +1707,16 @@ main(int argc, char** argv)
       if (global_error_flag)
 	{
 	  std::ostream& err = global_error();
+	  if (bogus_output)
+	    err << ("error: some error was detected during the above runs.\n"
+		    "       Check file ")
+		<< bogus_output_filename
+		<< " for problematic formulas.";
+	  else
 	    err << ("error: some error was detected during the above runs,\n"
 		    "       please search for 'error:' messages in the above"
-		  "trace.")
+		    " trace.");
-	      << std::endl;
+	  err << std::endl;
 	  if (timeout_count == 1)
 	    err << "Additionally, 1 timeout occurred." << std::endl;
 	  else if (timeout_count > 1)
@@ -1662,6 +1733,8 @@ main(int argc, char** argv)
 		  << " timeouts, but no other problem detected." << std::endl;
     }
 
+  delete bogus_output;
+
   if (json_output)
     print_stats_json(json_output);
   if (csv_output)

src/tgbatest/ltlcross3.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012, 2013 Laboratoire de Recherche et
+# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -55,13 +55,18 @@ test `grep '"exit code",1' out.csv | wc -l` -eq 0
 check_csv out.csv
 
 # Likewise for timeouts
+echo foo >bug
 run 0 ../../bin/ltlcross 'sleep 5; false %f >%N' \
-                         --timeout 2 -f a --csv=out.csv 2>stderr
+                         --timeout 2 -f a --csv=out.csv \
+                         --save-bogus=bug 2>stderr
 grep '"exit_status"' out.csv
 grep '"exit_code"' out.csv
 test `grep 'warning:.*timeout' stderr | wc -l` -eq 2
 test `grep '"timeout",-1' out.csv | wc -l` -eq 2
 check_csv out.csv
+# 'bug' should exist but be empty
+test -f bug
+test -s bug && exit 1
 
 run 0 ../../bin/ltlcross 'sleep 5; false %f >%N' \
                          --timeout 2 --omit-missing -f a --csv=out.csv 2>stderr
@@ -115,12 +120,13 @@ test $q -eq `expr $p + 12`
 
 # Check with Rabin/Streett output
 run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%D' \
-      -f a --csv=out.csv 2>stderr
+      -f 'X  a' --csv=out.csv --save-bogus=bug.txt 2>stderr
 q=`sed 's/[^,]//g;q' out.csv | wc -c`
 grep '"exit_status"' out.csv
 grep '"exit_code"' out.csv
 test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
 test `grep '"exit code",1' out.csv | wc -l` -eq 2
 check_csv out.csv
+grep 'X  a' bug.txt
 
 test $q -eq `expr $p + 6`