diff --git a/doc/org/ltlgrind.org b/doc/org/ltlgrind.org new file mode 100644 index 000000000..4eb85bcd5 --- /dev/null +++ b/doc/org/ltlgrind.org @@ -0,0 +1,82 @@ +#+TITLE: =ltlgrind= +#+EMAIL spot@lrde.epita.fr +#+OPTIONS: H:2 num:nil toc:t +#+LINK_UP: tools.html + +This tool lists formulas that are similar to but simpler than a given +formula by applying simple mutations to it, like removing operands or +operators. This is meant to be used with ltlcross to simplify a +formula that caused a problem before trying to debug it (see also +=ltlcross --grind=FILENAME=). + +Here is a list of the different kind of mutations that can be applied: + +#+BEGIN_SRC sh :results verbatim :exports results +ltlgrind --help | sed -n '/Transformation rules:/,/^$/p' | sed '1d;$d' +#+END_SRC + +#+RESULTS: +#+begin_example + --ap-to-const atomic propositions are replaced with true/false + --remove-multop-operands remove one operand from multops + --remove-one-ap all occurrences of an atomic proposition are + replaced with another atomic proposition used in + the formula + --remove-ops replace unary/binary operators with one of their + operands + --rewrite-ops rewrite operators that have a semantically simpler + form: a U b becomes a W b, etc. + --simplify-bounds on a bounded unary operator, decrement one of the + bounds, or set min to 0 or max to unbounded. + --split-ops when an operator can be expressed as a + conjunction/disjunction using simpler operators, + each term of the conjunction/disjunction is a + mutation. e.g. a <-> b can be written as ((a & b) + | (!a & !b)) or as ((a -> b) & (b -> a)) so those + four terms can be a mutation of a <-> b +#+end_example + +By default, all rules are applied. But if one or more rules are +specified, only those will be applied. + +#+BEGIN_SRC sh :results verbatim :exports both +ltlgrind -f 'a U G(b <-> c)' --split-ops --rewrite-ops --remove-ops +#+END_SRC + +#+RESULTS: +#+begin_example +a +G(b <-> c) +a W G(b <-> c) +a U (b <-> c) +a U Gb +a U Gc +a U G(b -> c) +a U G(c -> b) +a U G(b & c) +a U G(!b & !c) +#+end_example + +The idea behind this tool is that when a bogus algorithm is found with +=ltlcross=, you probably want to debug it using a smaller formula than +the one found by =ltlcross=. So you would give the formula found by +=ltlcross= as an argument to =ltlgrind= and then use the resulting +mutations as an new input for =ltlcross=. It might report an error on +one of the mutation, which is guaranteed to be simpler than the +initial formula. The process can then be repeated until no error is +reported by =ltlcross=. + +Since the whole process can become quite tedious, it can be done +automatically by calling =ltlcross= with the =--grind=FILENAME= +argument. + +* Miscellaneous options +** =--sort= + Formulas are outputted 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. +** =-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. diff --git a/doc/org/tools.org b/doc/org/tools.org index 26dd29f2b..56963c9aa 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -43,6 +43,8 @@ corresponding commands are hidden. - [[file:ltlcross.org][=ltlcross=]] Cross-compare LTL/PSL-to-Büchi translators. - [[file:dstar2tgba.org][=dstar2tgba=]] Convert deterministic Rabin or Streett automata into Büchi automata. +- [[file:ltlgrind.org][=ltlgrind=]] List formulas similar to but simpler than a given LTL/PSL + formula * Advanced uses diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am index 97972dcf0..616cc0256 100644 --- a/src/bin/Makefile.am +++ b/src/bin/Makefile.am @@ -43,7 +43,7 @@ libcommon_a_SOURCES = \ common_sys.hh bin_PROGRAMS = ltlfilt genltl randltl ltl2tgba ltl2tgta ltlcross \ - dstar2tgba + dstar2tgba ltlgrind # Dummy program used just to generate man/spot-x.7 in a way that is # consistent with the other man pages (e.g., with a version number that @@ -56,6 +56,7 @@ randltl_SOURCES = randltl.cc ltl2tgba_SOURCES = ltl2tgba.cc ltl2tgta_SOURCES = ltl2tgta.cc ltlcross_SOURCES = ltlcross.cc +ltlgrind_SOURCES = ltlgrind.cc dstar2tgba_SOURCES = dstar2tgba.cc spot_x_SOURCES = spot-x.cc ltlcross_LDADD = $(LDADD) $(LIB_GETHRXTIME) diff --git a/src/bin/ltlgrind.cc b/src/bin/ltlgrind.cc new file mode 100644 index 000000000..10f800b33 --- /dev/null +++ b/src/bin/ltlgrind.cc @@ -0,0 +1,207 @@ +// -*- coding: utf-8 -*- +// 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. +// +// 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 . + + +#include "common_sys.hh" +#include +#include +#include "common_setup.hh" +#include "common_finput.hh" +#include "common_output.hh" +#include "error.h" +#include "ltlast/allnodes.hh" +#include "ltlvisit/clone.hh" +#include "ltlvisit/apcollect.hh" +#include "ltlvisit/length.hh" +#include "ltlvisit/mutation.hh" + +#define OPT_AP2CONST 1 +#define OPT_SIMPLIFY_BOUNDS 2 +#define OPT_REMOVE_MULTOP_OPERANDS 3 +#define OPT_REMOVE_OPS 4 +#define OPT_SPLIT_OPS 5 +#define OPT_REWRITE_OPS 6 +#define OPT_REMOVE_ONE_AP 7 +#define OPT_SORT 8 + +static unsigned mutation_nb = 1; +static int max_output = std::numeric_limits::max(); + +static unsigned opt_all = 0xfff; +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 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}, + {"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" \ + "atomic proposition used in the formula", 15}, + {"remove-multop-operands", OPT_REMOVE_MULTOP_OPERANDS, 0, 0, + "remove one operand from multops", 15}, + {"remove-ops", OPT_REMOVE_OPS, 0, 0, + "replace unary/binary operators with one of their operands", + 15}, + {"split-ops", OPT_SPLIT_OPS, 0, 0, + "when an operator can be expressed as a conjunction/disjunction using " \ + "simpler operators, each term of the conjunction/disjunction is a " \ + "mutation. e.g. a <-> b can be written as ((a & b) | (!a & !b)) or as " \ + "((a -> b) & (b -> a)) so those four terms can be a mutation of a <-> b", 0}, + {"rewrite-ops", OPT_REWRITE_OPS, 0, 0, + "rewrite operators that have a semantically simpler form: a U b becomes " \ + "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, 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}, + {0, 0, 0, 0, 0, 0} +}; + +static const argp_child children[] = { + {&finput_argp, 0, 0, 10}, + {&output_argp, 0, 0, 20}, + {&misc_argp, 0, 0, -1}, + {0, 0, 0, 0} +}; + +static int +to_int(const char *s) +{ + char* endptr; + unsigned res = strtol(s, &endptr, 10); + if (*endptr) + error(2, 0, "failed to parse '%s' as an unsigned integer.", s); + return res; +} + +static unsigned +to_unsigned (const char *s) +{ + char* endptr; + unsigned res = strtoul(s, &endptr, 10); + if (*endptr) + error(2, 0, "failed to parse '%s' as an unsigned integer.", s); + return res; +} + +namespace +{ + using namespace spot::ltl; + + class mutate_processor: + public job_processor + { + public: + int + process_formula(const formula* f, const char *filename = 0, + int linenum = 0) + { + std::vector mutations = + get_mutations(f, mut_opts, opt_sort, max_output, mutation_nb); + + f->destroy(); + std::vector::iterator it; + for (it = mutations.begin(); it != mutations.end(); ++it) + { + output_formula_checked(*it, filename, linenum); + (*it)->destroy(); + } + return 0; + } + }; +} + +int +parse_opt(int key, char* arg, struct argp_state*) +{ + switch (key) + { + case 'm': + mutation_nb = to_unsigned(arg); + break; + case 'n': + max_output = to_int(arg); + break; + case OPT_AP2CONST: + opt_all = 0; + mut_opts |= MUT_AP2CONST; + break; + case OPT_REMOVE_ONE_AP: + opt_all = 0; + mut_opts |= MUT_REMOVE_ONE_AP; + break; + case OPT_REMOVE_MULTOP_OPERANDS: + opt_all = 0; + mut_opts |= MUT_REMOVE_MULTOP_OPERANDS; + break; + case OPT_REMOVE_OPS: + opt_all = 0; + mut_opts |= MUT_REMOVE_OPS; + break; + case OPT_SPLIT_OPS: + opt_all = 0; + mut_opts |= MUT_SPLIT_OPS; + break; + case OPT_REWRITE_OPS: + opt_all = 0; + mut_opts |= MUT_REWRITE_OPS; + break; + case OPT_SIMPLIFY_BOUNDS: + opt_all = 0; + mut_opts |= MUT_SIMPLIFY_BOUNDS; + break; + case OPT_SORT: + opt_sort = true; + break; + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} + +int +main(int argc, char* argv[]) +{ + setup(argv); + + const argp ap = { options, parse_opt, 0, argp_program_doc, children, 0, 0 }; + + if (int err = argp_parse(&ap, argc, argv, 0, 0, 0)) + exit(err); + + mut_opts |= opt_all; + + if (jobs.empty()) + jobs.push_back(job("-", 1)); + + mutate_processor processor; + if (processor.run()) + return 2; + return 0; +} diff --git a/src/bin/man/Makefile.am b/src/bin/man/Makefile.am index 4ad43e7cd..c77d653ec 100644 --- a/src/bin/man/Makefile.am +++ b/src/bin/man/Makefile.am @@ -29,6 +29,7 @@ dist_man1_MANS = \ ltl2tgta.1 \ ltlcross.1 \ ltlfilt.1 \ + ltlgrind.1 \ randltl.1 dist_man7_MANS = \ spot-x.7 @@ -59,3 +60,6 @@ randltl.1: $(common_dep) $(srcdir)/randltl.x $(srcdir)/../randltl.cc spot-x.7: $(common_dep) $(srcdir)/spot-x.x $(srcdir)/../spot-x.cc $(convman) ../spot-x$(EXEEXT) $(srcdir)/spot-x.x $@ + +ltlgrind.1: $(common_dep) $(srcdir)/ltlgrind.x $(srcdir)/../ltlgrind.cc + $(convman) ../ltlgrind$(EXEEXT) $(srcdir)/ltlgrind.x $@ diff --git a/src/bin/man/ltlgrind.x b/src/bin/man/ltlgrind.x new file mode 100644 index 000000000..ef05873b1 --- /dev/null +++ b/src/bin/man/ltlgrind.x @@ -0,0 +1,6 @@ +[NAME] +ltlgrind \- list mutations of a formula. +[DESCRIPTION] +.\" Add any additional description here +[SEE ALSO] +.BR ltlcross (1), diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index e4c17523b..a0331659c 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -98,6 +98,7 @@ TESTS = \ kind.test \ remove_x.test \ ltlrel.test \ + ltlgrind.test \ ltlfilt.test \ latex.test \ lbt.test \ diff --git a/src/ltltest/ltlgrind.test b/src/ltltest/ltlgrind.test new file mode 100755 index 000000000..58644a5e1 --- /dev/null +++ b/src/ltltest/ltlgrind.test @@ -0,0 +1,166 @@ +#! /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 + +checkopt() +{ + cat >exp + run 0 ../../bin/ltlgrind "$@" > out + diff exp out +} + +checkopt -f 'Xp1 U (p4 | (p3 xor (p4 W p0)))' <-> G(d <-> e) xor f' --split-ops \ +<-> (f & !G(d <-> e)) +{{{a | b}}[*4] & {{{a | b}}[*];c}}<>-> (!f & G(d <-> e)) +{{{a | b}}[*4] & {{{a | b}}[*];c}}<>-> (f xor G(d -> e)) +{{{a | b}}[*4] & {{{a | b}}[*];c}}<>-> (f xor G(e -> d)) +{{{a | b}}[*4] & {{{a | b}}[*];c}}<>-> (f xor G(d & e)) +{{{a | b}}[*4] & {{{a | b}}[*];c}}<>-> (f xor G(!d & !e)) +{{{{a | b}}[*];c} && {{{a | b}}[*4];[*]}}<>-> (f xor G(d <-> e)) +{{{a | b}}[*4] && {{{a | b}}[*];c;[*]}}<>-> (f xor G(d <-> e)) +EOF + + +checkopt -f '!(!XXp1 M X(p4 U p2))' --rewrite-ops < 0' --simplify-bounds < 0 +{p2[*3..5] | p3[*6..] | p1[*]}[]-> 0 +{p1[*0..2] | p3[*6..] | p2[*2..5]}[]-> 0 +{p1[*0..2] | p3[*6..] | p2[*0..5]}[]-> 0 +{p1[*0..2] | p3[*6..] | p2[*3..4]}[]-> 0 +{p1[*0..2] | p3[*6..] | p2[*3..]}[]-> 0 +{p1[*0..2] | p2[*3..5] | p3[*5..]}[]-> 0 +{p1[*0..2] | p2[*3..5] | p3[*]}[]-> 0 +EOF + +checkopt -f '!F(!X(Xp1 R p2) -> p4)' --remove-one-ap < p4) +!F(!X(Xp4 R p2) -> p4) +!F(!X(Xp1 R p1) -> p4) +!F(!X(Xp1 R p4) -> p4) +!F(!X(Xp1 R p2) -> p1) +!F(!X(Xp1 R p2) -> p2) +EOF + +checkopt -f '!p4 & (p2 | {{!p1}[*]})' --ap-to-const < p4)' -m 2 < p4 +p4 -> p3 +p3 & p4 +!p4 +!p3 +!p3 & !p4 +1 U p3 +1 U p4 +1 U !p3 +1 U !p4 +1 U (p3 & !p4) +1 U (!p3 & p4) +EOF diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index 1e32b7c3d..e1417b284 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -34,6 +34,7 @@ ltlvisit_HEADERS = \ lbt.hh \ length.hh \ lunabbrev.hh \ + mutation.hh \ nenoform.hh \ postfix.hh \ randomltl.hh \ @@ -58,6 +59,7 @@ libltlvisit_la_SOURCES = \ lunabbrev.cc \ mark.cc \ mark.hh \ + mutation.cc \ nenoform.cc \ postfix.cc \ randomltl.cc \ diff --git a/src/ltlvisit/mutation.cc b/src/ltlvisit/mutation.cc new file mode 100644 index 000000000..d5a1e68f6 --- /dev/null +++ b/src/ltlvisit/mutation.cc @@ -0,0 +1,399 @@ +// Copyright (C) 2013 Laboratoire de Recherche et Developpement de +// 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 . + +#include +#include + +#include "ltlast/allnodes.hh" +#include "ltlvisit/apcollect.hh" +#include "ltlvisit/clone.hh" +#include "ltlvisit/mutation.hh" +#include "ltlvisit/length.hh" +#include "misc/hash.hh" + +#define Implies_(x, y) \ + spot::ltl::binop::instance(spot::ltl::binop::Implies, (x), (y)) +#define And_(x, y) \ + spot::ltl::multop::instance(spot::ltl::multop::And, (x), (y)) +#define AndRat_(x, y) \ + spot::ltl::multop::instance(spot::ltl::multop::AndRat, (x), (y)) +#define AndNLM_(x) \ + spot::ltl::multop::instance(spot::ltl::multop::AndNLM, (x)) +#define Concat_(x, y) \ + spot::ltl::multop::instance(spot::ltl::multop::Concat, (x), (y)) +#define Not_(x) \ + spot::ltl::unop::instance(spot::ltl::unop::Not, (x)) + +namespace spot +{ + namespace ltl + { + namespace + { + class replace_visitor : public clone_visitor + { + public: + void visit(const atomic_prop* ap) + { + 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) + { + ap1_ = ap1; + ap2_ = ap2; + return recurse(f); + } + + private: + atomic_prop_set::iterator ap1_; + atomic_prop_set::iterator ap2_; + }; + + typedef std::vector vec; + class mutation_visitor : public clone_visitor + { + public: + mutation_visitor(const formula* f, unsigned opts) : f_(f), opts_(opts) + { + } + + void visit(const atomic_prop* ap) + { + result_ = 0; + if (opts_ & MUT_AP2CONST) + { + if (mutation_counter_-- == 0) + result_ = constant::true_instance(); + if (mutation_counter_-- == 0) + result_ = constant::false_instance(); + } + if (!result_) + result_ = ap->clone(); + } + + void visit(const unop* uo) + { + result_ = 0; + if (opts_ & MUT_REMOVE_OPS) + { + if ((uo->op() == unop::G + || uo->op() == unop::F + || uo->op() == unop::X + || uo->op() == unop::Not) + && mutation_counter_-- == 0) + result_ = uo->child()->clone(); + } + if (!result_) + { + if (mutation_counter_ < 0) + result_ = uo->clone(); + else + { + result_ = unop::instance(uo->op(), recurse(uo->child())); + } + } + } + + void visit(const binop* bo) + { + const formula* first = bo->first(); + const formula* second = bo->second(); + result_ = 0; + + if (opts_ & MUT_REMOVE_OPS && mutation_counter_-- == 0) + result_ = first->clone(); + if (opts_ & MUT_REMOVE_OPS && mutation_counter_-- == 0) + result_ = second->clone(); + if (opts_ & MUT_REWRITE_OPS) + { + switch (bo->op()) + { + case binop::U: + if (mutation_counter_-- == 0) + result_ = binop::instance(binop::W, first->clone(), + second->clone()); + break; + case binop::M: + if (mutation_counter_-- == 0) + result_ = binop::instance(binop::R, first->clone(), + second->clone()); + if (mutation_counter_-- == 0) + result_ = binop::instance(binop::U, second->clone(), + first->clone()); + break; + case binop::R: + if (mutation_counter_-- == 0) + result_ = binop::instance(binop::W, second->clone(), + first->clone()); + break; + default: + break; + } + } + if (opts_ & MUT_SPLIT_OPS) + { + switch (bo->op()) + { + case binop::Equiv: + if (mutation_counter_-- == 0) + result_ = Implies_(first->clone(), second->clone()); + if (mutation_counter_-- == 0) + result_ = Implies_(second->clone(), first->clone()); + if (mutation_counter_-- == 0) + result_ = And_(first->clone(), second->clone()); + if (mutation_counter_-- == 0) + result_ = And_(Not_(first->clone()), + Not_(second->clone())); + break; + case binop::Xor: + if (mutation_counter_-- == 0) + result_ = And_(first->clone(), Not_(second->clone())); + if (mutation_counter_-- == 0) + result_ = And_(Not_(first->clone()), second->clone()); + break; + default: + break; + } + } + if (!result_) + { + if (mutation_counter_ < 0) + result_ = bo->clone(); + else + result_ = + binop::instance(bo->op(), recurse(first), recurse(second)); + } + } + + void visit(const bunop* bu) + { + const formula* c = bu->child()->clone(); + result_ = 0; + + if (opts_ & MUT_REMOVE_OPS && mutation_counter_-- == 0) + result_ = c->clone(); + if (opts_ & MUT_SIMPLIFY_BOUNDS) + { + if (bu->min() > 0 && mutation_counter_-- == 0) + result_ = + bunop::instance(bu->op(), c, bu->min() - 1, bu->max()); + if (bu->min() > 0 && mutation_counter_-- == 0) + result_ = bunop::instance(bu->op(), c, 0, bu->max()); + if (bu->max() != bunop::unbounded && bu->max() > bu->min() + && mutation_counter_-- == 0) + result_ = + bunop::instance(bu->op(), c, bu->min(), bu->max() - 1); + if (bu->max() != bunop::unbounded && mutation_counter_-- == 0) + result_ = bunop::instance(bu->op(), c, bu->min(), + bunop::unbounded); + } + if (!result_) + { + c->destroy(); + if (mutation_counter_ < 0) + result_ = bu->clone(); + else + result_ = bunop::instance(bu->op(), recurse(c), bu->min(), + bu->max()); + } + } + + void visit(const multop* mo) + { + int mos = mo->size(); + int i; + result_ = 0; + + 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 (mutation_counter_ >= 0 && mutation_counter_ < 2 * (mos - 1)) + { + vec* v1 = new vec(); + vec* v2 = new vec(); + v1->push_back(mo->nth(0)->clone()); + bool reverse = false; + i = 1; + while (i < mos) + { + if (mutation_counter_-- == 0) + break; + if (mutation_counter_-- == 0) + { + reverse = true; + break; + } + v1->push_back(mo->nth(i++)->clone()); + } + for (; i < mos; ++i) + v2->push_back(mo->nth(i)->clone()); + const formula* tstar = + bunop::instance(bunop::Star, constant::true_instance(), + 0, + bunop::unbounded); + const formula* first = AndNLM_(v1); + const formula* second = AndNLM_(v2); + if (!reverse) + result_ = AndRat_(Concat_(first, tstar), second); + else + result_ = AndRat_(Concat_(second, tstar), first); + } + else + mutation_counter_ -= 2 * (mos - 1); + } + + if (!result_) + { + if (mutation_counter_ < 0) + result_ = mo->clone(); + else + { + vec* v = new vec(); + for (i = 0; i < mos; ++i) + v->push_back(recurse(mo->nth(i))); + result_ = multop::instance(mo->op(), v); + } + } + } + + const formula* + recurse(const formula* f) + { + f->accept(*this); + return result_; + } + + const formula* + get_mutation(int n) + { + mutation_counter_ = n; + const formula* mut = recurse(f_); + if (mut == f_) + { + mut->destroy(); + return 0; + } + return mut; + } + + private: + const formula* f_; + int mutation_counter_ = 0; + unsigned opts_; + }; + + bool + formula_length_less_than(const formula* left, const formula* right) + { + assert(left); + assert(right); + if (left == right) + return false; + return length(left) < length(right); + } + + typedef std::set fset_t; + + void + single_mutation_rec(const formula* f, fset_t& mutations, unsigned opts, + int& n, unsigned m) + { + if (m == 0) + { + if (mutations.insert(f).second) + { + f->clone(); + --n; + } + } + else + { + const formula* mut(nullptr); + int i = 0; + mutation_visitor mv(f, opts); + while (n > 0 && (mut = mv.get_mutation(i++))) + { + single_mutation_rec(mut, mutations, opts, n, m - 1); + mut->destroy(); + } + } + } + + void + replace_ap_rec(const formula* f, fset_t& mutations, unsigned opts, + int& n, unsigned m) + { + if (m == 0) + { + if (mutations.insert(f).second) + { + f->clone(); + --n; + } + } + else + { + const formula* mut; + 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) + { + if (ap1 == ap2) + continue; + mut = rv.replace(f, ap1, ap2); + replace_ap_rec(mut, mutations, opts, n, m - 1); + mut->destroy(); + } + } + } + } + + vec get_mutations(const formula* f, + unsigned opts, + bool sort, + int n, + unsigned m) + { + 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); + + vec res(mutations.begin(), mutations.end()); + if (sort) + std::sort(res.begin(), res.end(), formula_length_less_than); + return res; + } + } +} diff --git a/src/ltlvisit/mutation.hh b/src/ltlvisit/mutation.hh new file mode 100644 index 000000000..f27cf4b86 --- /dev/null +++ b/src/ltlvisit/mutation.hh @@ -0,0 +1,52 @@ +// -*- 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. +// +// 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 . + +#ifndef SPOT_LTLVISIT_MUTATION_HH +# 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; + SPOT_API + vec get_mutations(const formula*, + unsigned opts = 0xfff, + bool sort = true, + int n = std::numeric_limits::max(), + unsigned m = 1); + } +} +#endif