diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 8c626e2e1..1249dbb6d 100644 --- a/doc/org/ltlcross.org +++ b/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) diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 61f93738e..540aee82a 100644 --- a/src/bin/ltlcross.cc +++ b/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 mutations; + unsigned mutation_count; + unsigned mutation_max; + while (res) + { + std::cerr << "Trying to find a bogus mutation of \"" << bogus << + "\"" << std::endl; + std::vector::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; } diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index a0331659c..eab5011e3 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -99,6 +99,7 @@ TESTS = \ remove_x.test \ ltlrel.test \ ltlgrind.test \ + ltlcrossgrind.test \ ltlfilt.test \ latex.test \ lbt.test \ diff --git a/src/ltltest/ltlcrossgrind.test b/src/ltltest/ltlcrossgrind.test new file mode 100755 index 000000000..5993da2d0 --- /dev/null +++ b/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 . + +. ./defs || exit 1 + +set -e + +cat >fake <%N" \ +"../../bin/ltl2tgba -s -f %f >%N" --grind=bogus.grind + +echo p0 >exp +diff bogus.grind exp