ltlcross: adding option --grind=FILENAME

Suggested by Joachim Klein.

When a bogus formula is found by ltlcross, the --grind=FILENAME option
tries to find a smaller formula for which the bug is still present, and
outputs it in FILENAME.

* src/bin/ltlcross.cc: Add the --grind option.
* doc/org/ltlcross.org: Document the --grind option.
* src/ltltest/ltlcrossgrind.test: Test it.
* src/ltltest/Makefile.am: Add test.

doc/org/ltlcross.org

@@ -668,3 +668,41 @@ be used to gather statistics about a specific set of formulas.
 #  LocalWords:  nxqfd hS vNItGg acc scc nondetstates nondeterministic
 #  LocalWords:  cvs LaTeX datacols len ith otimes ltlcheck eval setq
 #  LocalWords:  setenv concat getenv
+** =--grind=FILENAME=
+   This argument tells =ltlcross= that, when an error is detected, it
+   should try to find a smaller formula that still exhibit the
+   bug. This is the procedure used:
+     - Internally list the mutations of the bogus formula and sort
+       them by length (as =ltlgrind --sort= would do)
+     - Process every mutation until one is found that exhibit the bug
+     - Repeat the process with this formula, and again until a formula
+       is found for which no mutation exhibit the bug
+     - Output that last formula in FILENAME
+   Every bogus formula found during the process will be saved if
+   =--save-bogus=FILENAME= is provided.
+
+  Example:
+#+BEGIN_SRC sh :exports both :results verbatim
+ltlcross -f '(G!b & (!c | F!a)) | (c & Ga & Fb)' "modella %L %T" \
+  --save-bogus=bogus \
+  --grind=bogus-grind
+#+END_SRC
+
+#+RESULTS:
+
+#+BEGIN_SRC sh :exports both :results verbatim
+cat bogus
+#+END_SRC
+
+#+RESULTS:
+: (G!b & (!c | F!a)) | (c & Ga & Fb)
+: G!b | (c & Ga & Fb)
+: G!b | (c & Fb)
+: G!c | (c & Fc)
+
+#+BEGIN_SRC sh :exports both :results verbatim
+cat bogus-grind
+#+END_SRC
+
+#+RESULTS:
+: G!c | (c & Fc)

src/bin/ltlcross.cc

@@ -43,6 +43,7 @@
 #include "ltlvisit/tostring.hh"
 #include "ltlvisit/apcollect.hh"
 #include "ltlvisit/lbt.hh"
+#include "ltlvisit/mutation.hh"
 #include "ltlvisit/relabel.hh"
 #include "tgbaalgos/lbtt.hh"
 #include "tgba/tgbaproduct.hh"
@@ -97,6 +98,7 @@ Exit status:\n\
 #define OPT_OMIT 12
 #define OPT_BOGUS 13
 #define OPT_VERBOSE 14
+#define OPT_GRIND 15
 
 static const argp_option options[] =
   {
@@ -162,6 +164,9 @@ 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 },
+    { "grind", OPT_GRIND, "FILENAME", 0,
+      "for each formula for which a problem was detected, write a simpler " \
+      "formula that fails on the same test in FILENAME", 0 },
     { "save-bogus", OPT_BOGUS, "FILENAME", 0,
       "save formulas for which problems were detected in FILENAME", 0 },
     { "verbose", OPT_VERBOSE, 0, 0,
@@ -215,6 +220,7 @@ 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;
+std::ofstream* grind_output = 0;
 bool verbose = false;
 
 struct translator_spec
@@ -545,6 +551,11 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_DUPS:
       allow_dups = true;
       break;
+    case OPT_GRIND:
+      grind_output = new std::ofstream(arg);
+      if (!*grind_output)
+	error(2, errno, "cannot open '%s'", arg);
+      break;
     case OPT_JSON:
       want_stats = true;
       json_output = arg ? arg : "-";
@@ -1282,10 +1293,65 @@ namespace
 	    f->destroy();
 	  return 1;
 	}
+
+      f->clone();
       int res = process_formula(f, filename, linenum);
 
       if (res && bogus_output)
 	*bogus_output << input << std::endl;
+      if (res && grind_output)
+	{
+	  std::string bogus = input;
+	  std::vector<const spot::ltl::formula*> mutations;
+	  unsigned mutation_count;
+	  unsigned mutation_max;
+	  while	(res)
+	    {
+	      std::cerr << "Trying to find a bogus mutation of \"" << bogus <<
+		"\"" << std::endl;
+	      std::vector<const spot::ltl::formula*>::iterator it;
+
+	      mutations = get_mutations(f);
+	      mutation_count = 1;
+	      mutation_max = mutations.size();
+	      res = 0;
+	      for (it = mutations.begin(); it != mutations.end() && !res; ++it)
+		{
+		  std::cerr << "Mutation [" << mutation_count << '/'
+			    << mutation_max << ']' << std::endl;
+		  f->destroy();
+		  f = (*it)->clone();
+		  res = process_formula(*it);
+		  ++mutation_count;
+		}
+	      for (; it != mutations.end(); ++it)
+		(*it)->destroy();
+	      if (res)
+		{
+		  if (lbt_input)
+		    bogus = spot::ltl::to_lbt_string(f);
+		  else
+		    bogus = spot::ltl::to_string(f);
+		  if (bogus_output)
+		    *bogus_output << bogus << std::endl;
+		}
+	    }
+	  std::cerr << "The smallest bogus mutation found for ";
+	  if (color_opt)
+	    std::cerr << bright_blue;
+	  std::cerr << input;
+	  if (color_opt)
+	    std::cerr << reset_color;
+	  std::cerr << " was ";
+	  if (color_opt)
+	    std::cerr << bright_blue;
+	  std::cerr << bogus << std::endl << std::endl;
+	  if (color_opt)
+	    std::cerr << reset_color;
+	  *grind_output << bogus << std::endl;
+	}
+      f->destroy();
+
       return 0;
     }
 

src/ltltest/Makefile.am

@@ -99,6 +99,7 @@ TESTS = \
   remove_x.test \
   ltlrel.test \
   ltlgrind.test \
+  ltlcrossgrind.test \
   ltlfilt.test \
   latex.test \
   lbt.test \

src/ltltest/ltlcrossgrind.test

@@ -0,0 +1,35 @@
+#! /bin/sh
+# Copyright (C) 2013 Laboratoire de Recherche et Developement to
+# 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
+
+cat >fake <<EOF
+#!/bin/sh
+../../bin/ltl2tgba -s -f "\$1" | sed 's/p0/p1/g'
+EOF
+
+chmod +x fake
+
+run 1 ../../bin/ltlcross -f 'p0 U p1' "./fake %f >%N" \
+"../../bin/ltl2tgba -s -f %f >%N" --grind=bogus.grind
+
+echo p0 >exp
+diff bogus.grind exp