diff --git a/AUTHORS b/AUTHORS index 6a485edb2..eaef29dd8 100644 --- a/AUTHORS +++ b/AUTHORS @@ -13,6 +13,7 @@ Heikki Tauriainen Pierre Parutto Rachid Rebiha Souheib Baarir +Thibaud Michaud Thomas Badie Thomas Martinez Tomáš Babiak diff --git a/NEWS b/NEWS index 6fbf74d19..ee88d7af1 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,15 @@ New in spot 1.99a (not yet released) * Major changes (including backward incompatible changes): + - ltlgrind is a new tool that mutates LTL or PSL formulas. If you + have a tool that is bogus on some formula that is tool large to + debug, you can use ltlgrind to generate smaller derived formulas + and see if you can reproduce the bug on those. + + - ltlcross has a new option --grind, that attempts to reduce the + size of any bogus formula it discovers, while still exhibiting + the bug. + - Spot is now compiling in C++11 mode. The set of features we use requires GCC >= 4.6 or Clang >= 3.1. These minimum versions are old enough that it should not be an issue to most people. diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 1249dbb6d..efb66370c 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -651,44 +651,190 @@ You can periodically check the contents of =bugs.ltl=, and then run 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 -formulas in their positive form. - -When checks are enabled, the negated formulas are intermixed with the -positives ones in the results. Therefore the =--no-check= option can -be used to gather statistics about a specific set of formulas. - -# LocalWords: ltlcross num toc LTL Büchi LBTT Testbench PSL SRC sed -# LocalWords: automata LBT LBTT's ltl tgba GFa lck iDGV sA FYp BYY -# LocalWords: ClVQg wyErP UNE dQ coM tH eHPoQy goto ba lbt modella -# LocalWords: lbtt csv json randltl ltlfilt wm eGEYaZ nYpFBX fGdZQ -# LocalWords: CPs kXiZZS ILLzR wU CcMCaQ IOckzW tsT RZ TJXmT jb XRO -# 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 +This option tells =ltlcross= that, when a problem is detected, it +should try to find a smaller formula that still exhibits the +problem. + +Here is the procedure used: + - internally list the mutations of the bogus formula and sort + them by length (as [[file:ltlgrind.org][=ltlgrind --sort=]] would do) + - process every mutation until one is found that exhibit the bug + - repeat the process with this new formula, and again until a formula + is found for which no mutation exhibit the bug + - output that last formula in =FILENAME= + +If =--save-bogus=OTHERFILENAME= is provided, every bogus formula found +during the process will be saved in =OTHERFILENAME=. + +Example: +#+BEGIN_SRC sh :exports code :results verbatim ltlcross -f '(G!b & (!c | F!a)) | (c & Ga & Fb)' "modella %L %T" \ --save-bogus=bogus \ --grind=bogus-grind #+END_SRC - +#+BEGIN_SRC sh :exports results :results verbatim +ltlcross -f '(G!b & (!c | F!a)) | (c & Ga & Fb)' "modella %L %T" \ + --save-bogus=bogus --grind=bogus-grind 2>&1 +true +#+END_SRC #+RESULTS: +#+begin_example +| & G ! p0 | ! p1 F ! p2 & & p1 G p2 F p0 +Running [P0]: modella 'lcr-i0-YBdcX8' 'lcr-o0-VWBBUF' +Running [N0]: modella 'lcr-i0-wteTSc' 'lcr-o0-pqlbRJ' +Performing sanity checks and gathering statistics... +error: P0*N0 is nonempty; both automata accept the infinite word + cycle{!p0 & !p1} + +Trying to find a bogus mutation of "(G!b & (!c | F!a)) | (c & Ga & Fb)" +Mutation [1/22] +& & p0 G p1 F p2 +Running [P0]: modella 'lcr-i1-Ursu0g' 'lcr-o0-Lm3N9N' +Running [N0]: modella 'lcr-i1-AkNujl' 'lcr-o0-VYRbtS' +Performing sanity checks and gathering statistics... + +Mutation [2/22] +& G ! p0 | ! p1 F ! p2 +Running [P0]: modella 'lcr-i2-uuBGGp' 'lcr-o0-eZLbUW' +Running [N0]: modella 'lcr-i2-qO717t' 'lcr-o0-evKSl1' +Performing sanity checks and gathering statistics... + +Mutation [3/22] +| G ! p0 & & p1 G p2 F p0 +Running [P0]: modella 'lcr-i3-hQAiDy' 'lcr-o0-PoKIU5' +Running [N0]: modella 'lcr-i3-Jl5vcD' 'lcr-o0-RtIjua' +Performing sanity checks and gathering statistics... +error: P0*N0 is nonempty; both automata accept the infinite word + cycle{!p0 & !p1} + +Trying to find a bogus mutation of "G!b | (c & Ga & Fb)" +Mutation [1/16] +t +Running [P0]: modella 'lcr-i4-HUTvSH' 'lcr-o0-XXrIgf' +Running [N0]: modella 'lcr-i4-MoZ9EM' 'lcr-o0-w2MB3j' +Performing sanity checks and gathering statistics... + +Mutation [2/16] +G ! p0 +Running [P0]: modella 'lcr-i5-ZjeLsR' 'lcr-o0-lT2URo' +Running [N0]: modella 'lcr-i5-ELzihW' 'lcr-o0-tljGGt' +Performing sanity checks and gathering statistics... + +Mutation [3/16] +& & p0 G p1 F p2 +warning: This formula or its negation has already been checked. + Use --allow-dups if it should not be ignored. + +Mutation [4/16] +| G ! p0 & p1 F p0 +Running [P0]: modella 'lcr-i6-VUy2yy' 'lcr-o0-44be05' +Running [N0]: modella 'lcr-i6-SBBHrD' 'lcr-o0-VAcbTa' +Performing sanity checks and gathering statistics... +error: P0*N0 is nonempty; both automata accept the infinite word + cycle{!p0 & !p1} + +Trying to find a bogus mutation of "G!b | (c & Fb)" +Mutation [1/10] +t +warning: This formula or its negation has already been checked. + Use --allow-dups if it should not be ignored. + +Mutation [2/10] +G ! p0 +warning: This formula or its negation has already been checked. + Use --allow-dups if it should not be ignored. + +Mutation [3/10] +& p0 F p1 +Running [P0]: modella 'lcr-i7-gBs0mN' 'lcr-o0-bgNCRk' +Running [N0]: modella 'lcr-i7-oAYtmS' 'lcr-o0-VvmlRp' +Performing sanity checks and gathering statistics... + +Mutation [4/10] +| p0 G ! p1 +Running [P0]: modella 'lcr-i8-wLstoX' 'lcr-o0-jZOBVu' +Running [N0]: modella 'lcr-i8-4hBZs2' 'lcr-o0-3Ezn0z' +Performing sanity checks and gathering statistics... + +Mutation [5/10] +| G ! p0 F p0 +Running [P0]: modella 'lcr-i9-mqY0z7' 'lcr-o0-hcDE9E' +Running [N0]: modella 'lcr-i9-MtDCJc' 'lcr-o0-5fRAjK' +Performing sanity checks and gathering statistics... + +Mutation [6/10] +| ! p0 & p1 F p0 +Running [P0]: modella 'lcr-i10-s5ZlUh' 'lcr-o0-fvp7uP' +Running [N0]: modella 'lcr-i10-4GWe6m' 'lcr-o0-LKFmHU' +Performing sanity checks and gathering statistics... + +Mutation [7/10] +| G p1 & p0 F p1 +Running [P0]: modella 'lcr-i11-wZJKjs' 'lcr-o0-D948VZ' +Running [N0]: modella 'lcr-i11-yVpOyx' 'lcr-o0-rjXtb5' +Performing sanity checks and gathering statistics... + +Mutation [8/10] +| & p0 p1 G ! p0 +Running [P0]: modella 'lcr-i12-g9bpRC' 'lcr-o0-RhIkxa' +Running [N0]: modella 'lcr-i12-rvWBdI' 'lcr-o0-DauTTf' +Performing sanity checks and gathering statistics... + +Mutation [9/10] +| G ! p0 & p0 F p0 +Running [P0]: modella 'lcr-i13-sXVtCN' 'lcr-o0-9WE4kl' +Running [N0]: modella 'lcr-i13-49803S' 'lcr-o0-BNXXMq' +Performing sanity checks and gathering statistics... +error: P0*N0 is nonempty; both automata accept the infinite word + cycle{!p0} + +Trying to find a bogus mutation of "G!c | (c & Fc)" +Mutation [1/7] +t +warning: This formula or its negation has already been checked. + Use --allow-dups if it should not be ignored. + +Mutation [2/7] +G ! p0 +warning: This formula or its negation has already been checked. + Use --allow-dups if it should not be ignored. + +Mutation [3/7] +& p0 F p0 +Running [P0]: modella 'lcr-i14-Ohct43' 'lcr-o0-vKfEPB' +Running [N0]: modella 'lcr-i14-aKk2A9' 'lcr-o0-RiFqmH' +Performing sanity checks and gathering statistics... + +Mutation [4/7] +| p0 G ! p0 +Running [P0]: modella 'lcr-i15-Oht38e' 'lcr-o0-bhxGVM' +Running [N0]: modella 'lcr-i15-iyrAIk' 'lcr-o0-nMFuvS' +Performing sanity checks and gathering statistics... + +Mutation [5/7] +| G ! p0 F p0 +warning: This formula or its negation has already been checked. + Use --allow-dups if it should not be ignored. + +Mutation [6/7] +| ! p0 & p0 F p0 +Running [P0]: modella 'lcr-i16-nZMD9X' 'lcr-o0-epKIYv' +Running [N0]: modella 'lcr-i16-DSW2N3' 'lcr-o0-6ElnDB' +Performing sanity checks and gathering statistics... + +Mutation [7/7] +| & p0 F p0 G p0 +Running [P0]: modella 'lcr-i17-Z6avt9' 'lcr-o0-QJhDjH' +Running [N0]: modella 'lcr-i17-hEo69e' 'lcr-o0-OBHz0M' +Performing sanity checks and gathering statistics... + +The smallest bogus mutation found for (G!b & (!c | F!a)) | (c & Ga & Fb) was G!c | (c & Fc) + +error: some error was detected during the above runs. + Check file bogus for problematic formulas. +#+end_example #+BEGIN_SRC sh :exports both :results verbatim cat bogus @@ -706,3 +852,22 @@ cat bogus-grind #+RESULTS: : G!c | (c & Fc) + +** =--no-check= + +The =--no-check= option disables all sanity checks, and only use the supplied +formulas in their positive form. + +When checks are enabled, the negated formulas are intermixed with the +positives ones in the results. Therefore the =--no-check= option can +be used to gather statistics about a specific set of formulas. + + +# LocalWords: ltlcross num toc LTL Büchi LBTT Testbench PSL SRC sed +# LocalWords: automata LBT LBTT's ltl tgba GFa lck iDGV sA FYp BYY +# LocalWords: ClVQg wyErP UNE dQ coM tH eHPoQy goto ba lbt modella +# LocalWords: lbtt csv json randltl ltlfilt wm eGEYaZ nYpFBX fGdZQ +# LocalWords: CPs kXiZZS ILLzR wU CcMCaQ IOckzW tsT RZ TJXmT jb XRO +# LocalWords: nxqfd hS vNItGg acc scc nondetstates nondeterministic +# LocalWords: cvs LaTeX datacols len ith otimes ltlcheck eval setq +# LocalWords: setenv concat getenv diff --git a/doc/org/ltlgrind.org b/doc/org/ltlgrind.org index 4eb85bcd5..843c01d6d 100644 --- a/doc/org/ltlgrind.org +++ b/doc/org/ltlgrind.org @@ -72,11 +72,16 @@ argument. * Miscellaneous options ** =--sort= - Formulas are outputted from the shortest to the longest one. The + Output formulas from the shortest to the longest one. The length of a formula is the number of atomic propositions, constants - and operators occuring in the formula. + and operators occurring in the formula. ** =-m N=, =--mutations=N= - This option is used to specify the number of mutations to be - applied to the formula. This is like calling ltlgrind on its own - output several times, except for the fact that, when called on - several formulas, ltlgrind doesn't handle duplicates. + Specify the number of mutations to be applied to the formula. By + default, =N=1=, so using this option is like calling ltlgrind on its + own output several times, except for the fact that, when called on + several formulas, ltlgrind doesn't handle duplicates. +** =-n N=, =--max-output=N= + Limit the number of mutated formulas output to =N=. + +# LocalWords: ltlgrind num toc html ltlcross FILENAME SRC sed ap Gb +# LocalWords: const multop multops unary decrement disjunction Gc diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 540aee82a..89d63649a 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -1307,25 +1307,31 @@ namespace unsigned mutation_max; while (res) { - std::cerr << "Trying to find a bogus mutation of \"" << bogus << - "\"" << std::endl; - std::vector::iterator it; + std::cerr << "Trying to find a bogus mutation of "; + if (color_opt) + std::cerr << bright_blue; + std::cerr << bogus; + if (color_opt) + std::cerr << reset_color; + std::cerr << "...\n"; - mutations = get_mutations(f); + mutations = mutate(f); mutation_count = 1; mutation_max = mutations.size(); res = 0; - for (it = mutations.begin(); it != mutations.end() && !res; ++it) + for (auto g: mutations) { - std::cerr << "Mutation [" << mutation_count << '/' - << mutation_max << ']' << std::endl; + std::cerr << "Mutation " << mutation_count << '/' + << mutation_max << ": "; f->destroy(); - f = (*it)->clone(); - res = process_formula(*it); + f = g->clone(); + res = process_formula(g->clone()); + if (res) + break; ++mutation_count; } - for (; it != mutations.end(); ++it) - (*it)->destroy(); + for (auto g: mutations) + g->destroy(); if (res) { if (lbt_input) @@ -1336,18 +1342,19 @@ namespace *bogus_output << bogus << std::endl; } } - std::cerr << "The smallest bogus mutation found for "; + std::cerr << "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 "; + std::cerr << " is "; if (color_opt) std::cerr << bright_blue; - std::cerr << bogus << std::endl << std::endl; + std::cerr << bogus; if (color_opt) std::cerr << reset_color; + std::cerr << ".\n\n"; *grind_output << bogus << std::endl; } f->destroy(); diff --git a/src/bin/ltlgrind.cc b/src/bin/ltlgrind.cc index 10f800b33..b1020049b 100644 --- a/src/bin/ltlgrind.cc +++ b/src/bin/ltlgrind.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2014 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -20,7 +20,6 @@ #include "common_sys.hh" #include -#include #include "common_setup.hh" #include "common_finput.hh" #include "common_output.hh" @@ -41,24 +40,25 @@ #define OPT_SORT 8 static unsigned mutation_nb = 1; -static int max_output = std::numeric_limits::max(); +static unsigned max_output = -1U; -static unsigned opt_all = 0xfff; +static unsigned opt_all = spot::ltl::Mut_All; static unsigned mut_opts = 0; static bool opt_sort = false; -const char * argp_program_doc = "List formulas that are similar to but " \ - "simpler than a given formula."; +static const char * argp_program_doc = + "List formulas that are similar to but simpler than a given formula."; static const argp_option options[] = { {"mutations", 'm', "N", 0, "number of mutations to apply to the " \ "formulae (default: 1)", -1}, {"sort", OPT_SORT, 0, 0, "sort the result by formula size", 0}, - {0, 0, 0, 0, "Transformation rules:", 15}, + {0, 0, 0, 0, "Mutation rules (all enabled unless those options are used):", + 15}, {"ap-to-const", OPT_AP2CONST, 0, 0, "atomic propositions are replaced with true/false", 15}, {"remove-one-ap", OPT_REMOVE_ONE_AP, 0, 0, - "all occurrences of an atomic proposition are replaced with another" \ + "all occurrences of an atomic proposition are replaced with another " \ "atomic proposition used in the formula", 15}, {"remove-multop-operands", OPT_REMOVE_MULTOP_OPERANDS, 0, 0, "remove one operand from multops", 15}, @@ -75,8 +75,7 @@ static const argp_option options[] = { "a W b, etc.", 0}, {"simplify-bounds", OPT_SIMPLIFY_BOUNDS, 0, 0, "on a bounded unary operator, decrement one of the bounds, or set min to " \ - "0 or max to " \ - "unbounded.", 15}, + "0 or max to unbounded", 15}, {0, 0, 0, 0, "Output options:", 20}, {"max-output", 'n', "N", 0, "maximum number of mutations to output", 20}, {0, 0, 0, 0, "Miscellaneous options:", -1}, @@ -112,25 +111,21 @@ to_unsigned (const char *s) namespace { - using namespace spot::ltl; - class mutate_processor: public job_processor { public: int - process_formula(const formula* f, const char *filename = 0, + process_formula(const spot::ltl::formula* f, const char *filename = 0, int linenum = 0) { - std::vector mutations = - get_mutations(f, mut_opts, opt_sort, max_output, mutation_nb); - + auto mutations = + spot::ltl::mutate(f, mut_opts, max_output, mutation_nb, opt_sort); f->destroy(); - std::vector::iterator it; - for (it = mutations.begin(); it != mutations.end(); ++it) + for (auto g: mutations) { - output_formula_checked(*it, filename, linenum); - (*it)->destroy(); + output_formula_checked(g, filename, linenum); + g->destroy(); } return 0; } @@ -150,31 +145,31 @@ parse_opt(int key, char* arg, struct argp_state*) break; case OPT_AP2CONST: opt_all = 0; - mut_opts |= MUT_AP2CONST; + mut_opts |= spot::ltl::Mut_Ap2Const; break; case OPT_REMOVE_ONE_AP: opt_all = 0; - mut_opts |= MUT_REMOVE_ONE_AP; + mut_opts |= spot::ltl::Mut_Remove_One_Ap; break; case OPT_REMOVE_MULTOP_OPERANDS: opt_all = 0; - mut_opts |= MUT_REMOVE_MULTOP_OPERANDS; + mut_opts |= spot::ltl::Mut_Remove_Multop_Operands; break; case OPT_REMOVE_OPS: opt_all = 0; - mut_opts |= MUT_REMOVE_OPS; + mut_opts |= spot::ltl::Mut_Remove_Ops; break; case OPT_SPLIT_OPS: opt_all = 0; - mut_opts |= MUT_SPLIT_OPS; + mut_opts |= spot::ltl::Mut_Split_Ops; break; case OPT_REWRITE_OPS: opt_all = 0; - mut_opts |= MUT_REWRITE_OPS; + mut_opts |= spot::ltl::Mut_Rewrite_Ops; break; case OPT_SIMPLIFY_BOUNDS: opt_all = 0; - mut_opts |= MUT_SIMPLIFY_BOUNDS; + mut_opts |= spot::ltl::Mut_Simplify_Bounds; break; case OPT_SORT: opt_sort = true; diff --git a/src/ltltest/ltlcrossgrind.test b/src/ltltest/ltlcrossgrind.test index 5993da2d0..8c9a974e4 100755 --- a/src/ltltest/ltlcrossgrind.test +++ b/src/ltltest/ltlcrossgrind.test @@ -1,5 +1,6 @@ #! /bin/sh -# Copyright (C) 2013 Laboratoire de Recherche et Developement to +# -*- coding: utf-8 -*- +# Copyright (C) 2014 Laboratoire de Recherche et Dévelopement to # l'Epita (LRDE). # # This file is part of Spot, a model checking library. diff --git a/src/ltltest/ltlgrind.test b/src/ltltest/ltlgrind.test index 58644a5e1..5e2ca9603 100755 --- a/src/ltltest/ltlgrind.test +++ b/src/ltltest/ltlgrind.test @@ -1,5 +1,6 @@ #! /bin/sh -# Copyright (C) 2013 Laboratoire de Recherche et Developement to +# -*- coding: utf-8 -*- +# Copyright (C) 2014 Laboratoire de Recherche et Dévelopement to # l'Epita (LRDE). # # This file is part of Spot, a model checking library. diff --git a/src/ltlvisit/mutation.cc b/src/ltlvisit/mutation.cc index d5a1e68f6..9d2e7f069 100644 --- a/src/ltlvisit/mutation.cc +++ b/src/ltlvisit/mutation.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2013 Laboratoire de Recherche et Developpement de +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et Developpement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -26,17 +27,17 @@ #include "ltlvisit/length.hh" #include "misc/hash.hh" -#define Implies_(x, y) \ +#define Implies_(x, y) \ spot::ltl::binop::instance(spot::ltl::binop::Implies, (x), (y)) -#define And_(x, y) \ +#define And_(x, y) \ spot::ltl::multop::instance(spot::ltl::multop::And, (x), (y)) -#define AndRat_(x, y) \ +#define AndRat_(x, y) \ spot::ltl::multop::instance(spot::ltl::multop::AndRat, (x), (y)) -#define AndNLM_(x) \ +#define AndNLM_(x) \ spot::ltl::multop::instance(spot::ltl::multop::AndNLM, (x)) -#define Concat_(x, y) \ +#define Concat_(x, y) \ spot::ltl::multop::instance(spot::ltl::multop::Concat, (x), (y)) -#define Not_(x) \ +#define Not_(x) \ spot::ltl::unop::instance(spot::ltl::unop::Not, (x)) namespace spot @@ -50,15 +51,16 @@ namespace spot public: void visit(const atomic_prop* ap) { - if (ap == (*ap1_)) - result_ = (*ap2_)->clone(); + if (ap == ap1_) + result_ = ap2_->clone(); else result_ = ap->clone(); } const formula* replace(const formula* f, - atomic_prop_set::iterator ap1, atomic_prop_set::iterator ap2) + const atomic_prop* ap1, + const atomic_prop* ap2) { ap1_ = ap1; ap2_ = ap2; @@ -66,8 +68,8 @@ namespace spot } private: - atomic_prop_set::iterator ap1_; - atomic_prop_set::iterator ap2_; + const atomic_prop* ap1_; + const atomic_prop* ap2_; }; typedef std::vector vec; @@ -81,7 +83,7 @@ namespace spot void visit(const atomic_prop* ap) { result_ = 0; - if (opts_ & MUT_AP2CONST) + if (opts_ & Mut_Ap2Const) { if (mutation_counter_-- == 0) result_ = constant::true_instance(); @@ -95,7 +97,7 @@ namespace spot void visit(const unop* uo) { result_ = 0; - if (opts_ & MUT_REMOVE_OPS) + if (opts_ & Mut_Remove_Ops) { if ((uo->op() == unop::G || uo->op() == unop::F @@ -121,11 +123,11 @@ namespace spot const formula* second = bo->second(); result_ = 0; - if (opts_ & MUT_REMOVE_OPS && mutation_counter_-- == 0) + if (opts_ & Mut_Remove_Ops && mutation_counter_-- == 0) result_ = first->clone(); - if (opts_ & MUT_REMOVE_OPS && mutation_counter_-- == 0) + if (opts_ & Mut_Remove_Ops && mutation_counter_-- == 0) result_ = second->clone(); - if (opts_ & MUT_REWRITE_OPS) + if (opts_ & Mut_Rewrite_Ops) { switch (bo->op()) { @@ -151,7 +153,7 @@ namespace spot break; } } - if (opts_ & MUT_SPLIT_OPS) + if (opts_ & Mut_Split_Ops) { switch (bo->op()) { @@ -191,9 +193,9 @@ namespace spot const formula* c = bu->child()->clone(); result_ = 0; - if (opts_ & MUT_REMOVE_OPS && mutation_counter_-- == 0) + if (opts_ & Mut_Remove_Ops && mutation_counter_-- == 0) result_ = c->clone(); - if (opts_ & MUT_SIMPLIFY_BOUNDS) + if (opts_ & Mut_Simplify_Bounds) { if (bu->min() > 0 && mutation_counter_-- == 0) result_ = @@ -225,14 +227,14 @@ namespace spot int i; result_ = 0; - if (opts_ & MUT_REMOVE_MULTOP_OPERANDS) + if (opts_ & Mut_Remove_Multop_Operands) { for (i = 0; i < mos; ++i) if (mutation_counter_-- == 0) result_ = mo->all_but(i); } - if (opts_ & MUT_SPLIT_OPS && mo->op() == multop::AndNLM) + if (opts_ & Mut_Split_Ops && mo->op() == multop::AndNLM) { if (mutation_counter_ >= 0 && mutation_counter_ < 2 * (mos - 1)) { @@ -323,7 +325,7 @@ namespace spot void single_mutation_rec(const formula* f, fset_t& mutations, unsigned opts, - int& n, unsigned m) + unsigned& n, unsigned m) { if (m == 0) { @@ -348,7 +350,7 @@ namespace spot void replace_ap_rec(const formula* f, fset_t& mutations, unsigned opts, - int& n, unsigned m) + unsigned& n, unsigned m) { if (m == 0) { @@ -360,35 +362,34 @@ namespace spot } else { - const formula* mut; + if (!n) + return; replace_visitor rv; - std::unique_ptr aps = - std::unique_ptr(atomic_prop_collect(f)); - atomic_prop_set::iterator ap1; - atomic_prop_set::iterator ap2; - for (ap1 = aps->begin(); ap1 != aps->end() && n > 0; ++ap1) - for (ap2 = aps->begin(); ap2 != aps->end() && n > 0; ++ap2) + auto aps = + std::unique_ptr(atomic_prop_collect(f)); + for (auto ap1: *aps) + for (auto ap2: *aps) { if (ap1 == ap2) continue; - mut = rv.replace(f, ap1, ap2); + auto mut = rv.replace(f, ap1, ap2); replace_ap_rec(mut, mutations, opts, n, m - 1); mut->destroy(); + if (!n) + return; } } } } - vec get_mutations(const formula* f, - unsigned opts, - bool sort, - int n, - unsigned m) + std::vector + mutate(const formula* f, unsigned opts, unsigned max_output, + unsigned mutation_count, bool sort) { fset_t mutations; - single_mutation_rec(f, mutations, opts, n, m); - if (opts & MUT_REMOVE_ONE_AP) - replace_ap_rec(f, mutations, opts, n, m); + single_mutation_rec(f, mutations, opts, max_output, mutation_count); + if (opts & Mut_Remove_One_Ap) + replace_ap_rec(f, mutations, opts, max_output, mutation_count); vec res(mutations.begin(), mutations.end()); if (sort) diff --git a/src/ltlvisit/mutation.hh b/src/ltlvisit/mutation.hh index f27cf4b86..469749840 100644 --- a/src/ltlvisit/mutation.hh +++ b/src/ltlvisit/mutation.hh @@ -1,9 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2014 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -24,29 +21,31 @@ # define SPOT_LTLVISIT_MUTATION_HH #include "ltlast/formula.hh" -#include #include #include -#define MUT_AP2CONST 0x1 -#define MUT_SIMPLIFY_BOUNDS 0x2 -#define MUT_REMOVE_MULTOP_OPERANDS 0x4 -#define MUT_REMOVE_OPS 0x8 -#define MUT_SPLIT_OPS 0x10 -#define MUT_REWRITE_OPS 0x20 -#define MUT_REMOVE_ONE_AP 0x40 - namespace spot { namespace ltl { - typedef std::vector vec; + enum mut_opts + { + Mut_Ap2Const = 1U<<0, + Mut_Simplify_Bounds = 1U<<1, + Mut_Remove_Multop_Operands = 1U<<2, + Mut_Remove_Ops = 1U<<3, + Mut_Split_Ops = 1U<<4, + Mut_Rewrite_Ops = 1U<<5, + Mut_Remove_One_Ap = 1U<<6, + Mut_All = -1U + }; + SPOT_API - vec get_mutations(const formula*, - unsigned opts = 0xfff, - bool sort = true, - int n = std::numeric_limits::max(), - unsigned m = 1); + std::vector mutate(const formula* f, + unsigned opts = Mut_All, + unsigned max_output = -1U, + unsigned mutation_count = 1, + bool sort = true); } } #endif