Commit e327f6ea authored by Thibaud Michaud's avatar Thibaud Michaud Committed by Alexandre Duret-Lutz
Browse files

Adding ltlgrind as a command-line tool

* src/bin/ltlgrind.cc: New file, command-line tool to get mutations of a
formula.
* src/bin/Makefile.am: Add it.
* src/ltlvisit/mutation.hh, src/ltlvisit/mutation.cc:
New files providing the get_mutations function.
* src/ltlvisit/Makefile.am: Add it.
* src/ltltest/ltlgrind.test: Test it.
* src/ltltest/Makefile.am: Add it.
* src/bin/man/ltlgrind.x: Document it.
* src/bin/man/Makefile.am: Add it.
* doc/org/ltlgrind.org: Document it.
* doc/org/tools.org: Add link to ltlgrind documentation page.
parent 51fe5108
#+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.
......@@ -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
......
......@@ -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)
// -*- 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 <http://www.gnu.org/licenses/>.
#include "common_sys.hh"
#include <argp.h>
#include <limits>
#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<int>::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<const formula*> mutations =
get_mutations(f, mut_opts, opt_sort, max_output, mutation_nb);
f->destroy();
std::vector<const formula*>::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;
}
......@@ -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 $@
[NAME]
ltlgrind \- list mutations of a formula.
[DESCRIPTION]
.\" Add any additional description here
[SEE ALSO]
.BR ltlcross (1),
......@@ -98,6 +98,7 @@ TESTS = \
kind.test \
remove_x.test \
ltlrel.test \
ltlgrind.test \
ltlfilt.test \
latex.test \
lbt.test \
......
#! /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
checkopt()
{
cat >exp
run 0 ../../bin/ltlgrind "$@" > out
diff exp out
}
checkopt -f 'Xp1 U (p4 | (p3 xor (p4 W p0)))' <<EOF
1
Xp1
p4 | (p3 xor (p4 W p0))
Xp1 W (p4 | (p3 xor (p4 W p0)))
Xp1 U (p3 xor (p4 W p0))
Xp1 U p4
Xp1 U (p3 | p4)
Xp1 U (p4 | (p4 W p0))
Xp1 U (p4 | (p3 & !(p4 W p0)))
Xp1 U (p4 | (!p3 & (p4 W p0)))
Xp1 U (p4 | (p3 xor p4))
Xp1 U (p4 | (p0 xor p3))
Xp1 U (!p3 | p4)
Xp1 U (p4 | (p3 xor (p4 W 0)))
Xp1 U (p4 | !(p4 W p0))
p1 U (p4 | (p3 xor (p4 W p0)))
1 U (p4 | (p3 xor (p4 W p0)))
Xp4 U (p4 | (p3 xor (p4 W p0)))
Xp3 U (p4 | (p3 xor (p4 W p0)))
Xp0 U (p4 | (p3 xor (p4 W p0)))
Xp1 U (p1 | (p3 xor (p1 W p0)))
Xp1 U (p3 | (p3 xor (p3 W p0)))
Xp1 U (p0 | (p0 xor p3))
Xp1 U (p4 | (p1 xor (p4 W p0)))
Xp1 U (p4 | (p4 xor (p4 W p0)))
Xp1 U (p4 | (p0 xor (p4 W p0)))
Xp1 U (p4 | (p3 xor (p4 W p1)))
Xp1 U (p4 | (p3 xor (p4 W p3)))
EOF
checkopt -f '(Xp4 R p3) W !p0' --sort <<EOF
1
!p0
Xp4 R p3
p3 W !p0
Xp4 W !p0
(Xp4 R p3) W p0
(Xp4 R p3) W 0
(p4 R p3) W !p0
(0 R p3) W !p0
(p3 W Xp4) W !p0
(Xp3 R p3) W !p0
(Xp0 R p3) W !p0
(Xp4 R p4) W !p0
(Xp4 R p0) W !p0
(Xp4 R p3) W !p4
(Xp4 R p3) W !p3
EOF
checkopt -f 'F(!p2 & p3) | Fp0' -n 4 <<EOF
F(!p2 & p3)
Fp0
(!p2 & p3) | Fp0
Fp0 | Fp3
EOF
checkopt -f '{(a | b)[*4] & ((a | b)*; c)} <>-> G(d <-> e) xor f' --split-ops \
<<EOF
{{{a | b}}[*4] & {{{a | b}}[*];c}}<>-> (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 <<EOF
!(!XXp1 R X(p4 U p2))
!(X(p4 U p2) U !XXp1)
!(!XXp1 M X(p4 W p2))
EOF
checkopt -f '!(p0 & !p2 & (p1 W 0))' --remove-multop-operands <<EOF
!(!p2 & (p1 W 0))
!(p0 & (p1 W 0))
!(p0 & !p2)
EOF
checkopt -f '{p1[*..2] | p2[*3..5] | p3[*6..]}[]-> 0' --simplify-bounds <<EOF
{p2[*3..5] | p3[*6..] | p1[*0..1]}[]-> 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 <<EOF
!F(!X(Xp2 R p2) -> 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 <<EOF
0
!p4
p2 | {{!p1}[*]}
!p4 & {{!p1}[*]}
p2 & !p4
!p4 & (p2 | {[*]})
EOF
checkopt -f 'F(XXp0 | (p4 & Gp0))' --remove-ops <<EOF
XXp0 | (p4 & Gp0)
F(Xp0 | (p4 & Gp0))
F((p0 & p4) | XXp0)
EOF
checkopt -f '1 U (p3 <-> p4)' -m 2 <<EOF
1
0
p3
p4
p3 -> 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
......@@ -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 \
......
// 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 <http://www.gnu.org/licenses/>.
#include <unordered_set>
#include <algorithm>
#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<const formula*> 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_)