diff --git a/NEWS b/NEWS index 6db246f97..497852728 100644 --- a/NEWS +++ b/NEWS @@ -80,6 +80,11 @@ New in spot 1.1.4a (not relased) indicate how to present the output formula, possibly with information about the input. + - ltlfilt as a new option, --relabel-bool, to abstract independent + Boolean subformulae as if they were atomic propositions. + For instance "a & GF(c | d) & b & X(c | d)" would be rewritten + as "p0 & GF(p1) & Xp1". + * New functions and classes in the library: - dtba_sat_synthetize(): Use a SAT-solver to build an equivalent @@ -143,6 +148,9 @@ New in spot 1.1.4a (not relased) - to_latex_string(): Output a formula using LaTeX syntax. + - relabel_bse(): Relabeling of Boolean Sub-Expressions. + Implements ltlfilt's --relabel-bool option describe above. + * Noteworthy internal changes: - When minimize_obligation() is not given the formula associated diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index 26d09db46..e9bc006cc 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -104,6 +104,86 @@ ltlfilt --lenient --relabel=pnn -f '(a < b) U (process[2]@ok)' #+RESULTS: : p0 U p1 + +Finally, there is a second variant of the relabeling procedure that is +enabled by =--relabel-bool=abc= or =--relabel-book=pnn=. With this +option, Boolean subformulas that do not interfere with other +subformulas will be changed into atomic propositions. For instance: + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt -f '(a & !b) & GF(a & !b) & FG(!c)' --relabel-bool=pnn +ltlfilt -f '(a & !b) & GF(a & !b) & FG(!c & a)' --relabel-bool=pnn +#+END_SRC +#+RESULTS: +: p0 & GFp0 & FGp1 +: p0 & p1 & GF(p0 & p1) & FG(p0 & p2) + +In the first formula, the independent =a & !b= and =!c= subformulae +were respectively renamed =p0= and =p1=. In the second formula, =a & +!b= and =!c & a= are dependent so they could not be renamed; instead +=a=, =!b= and =c= were renamed as =p0=, =p1= and =p2=. + +This option was originally developed to remove superfluous formulas +from benchmarks of LTL translators. For instance the automata +generated for =GF(a|b)= and =GF(p0)= should be structurally +equivalent: replacing =p0= by =a|b= in the second automaton should +turn in into the first automaton, and vice-versa. (However algorithms +dealing with =GF(a|b)= might be slower because they have to deal with +more atomic propositions.) So given a long list of LTL formulas, we +can combine =--relabel-bool= and =-u= to keep only one instance of +formulas that are equivalent after such relabeling. We also suggest +to use =--nnf= so that =!FG(a -> b)= would become =GF(p0)= +as well. For instance here are some LTL formulas extracted from an +[[http://www.fi.muni.cz/~xrehak/publications/verificationresults.ps.gz][industrial project]]: + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt --nnf -u --relabel-bool < F !hfe_req) +G (lup_sr_valid -> F lup_sr_clean ) +G F (hfe_req) +reset && X G (!reset) +G ( (F hfe_clk) && (F ! hfe_clk) ) +G ( (F lup_clk) && (F ! lup_clk) ) +G F (lup_sr_clean) +G ( ( !(lup_addr_5_ <-> (X lup_addr_5_)) || !(lup_addr_6_ <-> (X lup_addr_6_)) || !(lup_addr_7_ <-> (X lup_addr_7_)) || !(lup_addr_8_ <-> (X lup_addr_8_)) ) -> ( (X !lup_sr_clean) && X ( (!( !(lup_addr_5_ <-> (X lup_addr_5_)) || !(lup_addr_6_ <-> (X lup_addr_6_)) || !(lup_addr_7_ <-> (X lup_addr_7_)) || !(lup_addr_8_ <-> (X lup_addr_8_)) )) U lup_sr_clean ) ) ) +G F ( !(lup_addr_5_ <-> (X lup_addr_5_)) || !(lup_addr_6_ <-> (X lup_addr_6_)) || !(lup_addr_7_ <-> (X lup_addr_7_)) || !(lup_addr_8_ <-> (X lup_addr_8_)) ) +(lup_addr_8__5__eq_0) +((hfe_block_0__eq_0)&&(hfe_block_1__eq_0)&&(hfe_block_2__eq_0)&&(hfe_block_3__eq_0)) +G ((lup_addr_8__5__eq_0) -> X( (lup_addr_8__5__eq_0) || (lup_addr_8__5__eq_1) ) ) +G ((lup_addr_8__5__eq_1) -> X( (lup_addr_8__5__eq_1) || (lup_addr_8__5__eq_2) ) ) +G ((lup_addr_8__5__eq_2) -> X( (lup_addr_8__5__eq_2) || (lup_addr_8__5__eq_3) ) ) +G ((lup_addr_8__5__eq_3) -> X( (lup_addr_8__5__eq_3) || (lup_addr_8__5__eq_4) ) ) +G ((lup_addr_8__5__eq_4) -> X( (lup_addr_8__5__eq_4) || (lup_addr_8__5__eq_5) ) ) +G ((lup_addr_8__5__eq_5) -> X( (lup_addr_8__5__eq_5) || (lup_addr_8__5__eq_6) ) ) +G ((lup_addr_8__5__eq_6) -> X( (lup_addr_8__5__eq_6) || (lup_addr_8__5__eq_7) ) ) +G ((lup_addr_8__5__eq_7) -> X( (lup_addr_8__5__eq_7) || (lup_addr_8__5__eq_8) ) ) +G ((lup_addr_8__5__eq_8) -> X( (lup_addr_8__5__eq_8) || (lup_addr_8__5__eq_9) ) ) +G ((lup_addr_8__5__eq_9) -> X( (lup_addr_8__5__eq_9) || (lup_addr_8__5__eq_10) ) ) +G ((lup_addr_8__5__eq_10) -> X( (lup_addr_8__5__eq_10) || (lup_addr_8__5__eq_11) ) ) +G ((lup_addr_8__5__eq_11) -> X( (lup_addr_8__5__eq_11) || (lup_addr_8__5__eq_12) ) ) +G ((lup_addr_8__5__eq_12) -> X( (lup_addr_8__5__eq_12) || (lup_addr_8__5__eq_13) ) ) +G ((lup_addr_8__5__eq_13) -> X( (lup_addr_8__5__eq_13) || (lup_addr_8__5__eq_14) ) ) +G ((lup_addr_8__5__eq_14) -> X( (lup_addr_8__5__eq_14) || (lup_addr_8__5__eq_15) ) ) +G ((lup_addr_8__5__eq_15) -> X( (lup_addr_8__5__eq_15) || (lup_addr_8__5__eq_0) ) ) +G (((X hfe_clk) -> hfe_clk)->((hfe_req->X hfe_req)&&((!hfe_req) -> (X !hfe_req)))) +G (((X lup_clk) -> lup_clk)->((lup_sr_clean->X lup_sr_clean)&&((!lup_sr_clean) -> (X !lup_sr_clean)))) +EOF +#+END_SRC +#+RESULTS: +: G(a | Fb) +: GFa +: a & XG!a +: G(Fa & F!a) +: G((((!a & X!a) | (a & Xa)) & ((!b & X!b) | (b & Xb)) & ((!c & X!c) | (c & Xc)) & ((!d & X!d) | (d & Xd))) | (X!e & X((((!a & X!a) | (a & Xa)) & ((!b & X!b) | (b & Xb)) & ((!c & X!c) | (c & Xc)) & ((!d & X!d) | (d & Xd))) U e))) +: GF((!a & Xa) | (a & X!a) | (!b & Xb) | (b & X!b) | (!c & Xc) | (c & X!c) | (!d & Xd) | (d & X!d)) +: a +: G(!a | X(a | b)) +: G((!b & Xb) | ((!a | Xa) & (a | X!a))) + +Here 29 formulas were reduced into 9 formulas after relabeling of +Boolean subexpression and removing of duplicate formulas. In other +words the original set of formulas contains 9 different patterns. + * Filtering =ltlfilt= supports many ways to filter formulas: diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index 5cb4a8616..9d9bdd5d0 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -52,34 +52,35 @@ Exit status:\n\ 1 if no formulas were output (no match)\n\ 2 if any error has been reported"; -#define OPT_SKIP_ERRORS 2 -#define OPT_DROP_ERRORS 3 -#define OPT_NNF 4 -#define OPT_LTL 5 -#define OPT_NOX 7 -#define OPT_BOOLEAN 8 -#define OPT_EVENTUAL 9 -#define OPT_UNIVERSAL 10 -#define OPT_SYNTACTIC_SAFETY 11 -#define OPT_SYNTACTIC_GUARANTEE 12 -#define OPT_SYNTACTIC_OBLIGATION 13 -#define OPT_SYNTACTIC_RECURRENCE 14 -#define OPT_SYNTACTIC_PERSISTENCE 15 -#define OPT_SAFETY 16 -#define OPT_GUARANTEE 17 -#define OPT_OBLIGATION 18 -#define OPT_SIZE_MIN 19 -#define OPT_SIZE_MAX 20 -#define OPT_BSIZE_MIN 21 -#define OPT_BSIZE_MAX 22 -#define OPT_IMPLIED_BY 23 -#define OPT_IMPLY 24 -#define OPT_EQUIVALENT_TO 25 -#define OPT_RELABEL 26 -#define OPT_REMOVE_WM 27 -#define OPT_BOOLEAN_TO_ISOP 28 -#define OPT_REMOVE_X 29 -#define OPT_STUTTER_INSENSITIVE 30 +#define OPT_SKIP_ERRORS 1 +#define OPT_DROP_ERRORS 2 +#define OPT_NNF 3 +#define OPT_LTL 4 +#define OPT_NOX 5 +#define OPT_BOOLEAN 6 +#define OPT_EVENTUAL 7 +#define OPT_UNIVERSAL 8 +#define OPT_SYNTACTIC_SAFETY 9 +#define OPT_SYNTACTIC_GUARANTEE 10 +#define OPT_SYNTACTIC_OBLIGATION 11 +#define OPT_SYNTACTIC_RECURRENCE 12 +#define OPT_SYNTACTIC_PERSISTENCE 13 +#define OPT_SAFETY 14 +#define OPT_GUARANTEE 15 +#define OPT_OBLIGATION 16 +#define OPT_SIZE_MIN 17 +#define OPT_SIZE_MAX 18 +#define OPT_BSIZE_MIN 19 +#define OPT_BSIZE_MAX 20 +#define OPT_IMPLIED_BY 21 +#define OPT_IMPLY 22 +#define OPT_EQUIVALENT_TO 23 +#define OPT_RELABEL 24 +#define OPT_RELABEL_BOOL 25 +#define OPT_REMOVE_WM 26 +#define OPT_BOOLEAN_TO_ISOP 27 +#define OPT_REMOVE_X 28 +#define OPT_STUTTER_INSENSITIVE 29 static const argp_option options[] = { @@ -97,6 +98,9 @@ static const argp_option options[] = { "relabel", OPT_RELABEL, "abc|pnn", OPTION_ARG_OPTIONAL, "relabel all atomic propositions, alphabetically unless " \ "specified otherwise", 0 }, + { "relabel-bool", OPT_RELABEL_BOOL, "abc|pnn", OPTION_ARG_OPTIONAL, + "relabel Boolean subexpressions, alphabetically unless " \ + "specified otherwise", 0 }, { "remove-wm", OPT_REMOVE_WM, 0, 0, "rewrite operators W and M using U and R", 0 }, { "boolean-to-isop", OPT_BOOLEAN_TO_ISOP, 0, 0, @@ -203,7 +207,8 @@ static int size_min = -1; static int size_max = -1; static int bsize_min = -1; static int bsize_max = -1; -static bool relabeling = false; +enum relabeling_mode { NoRelabeling = 0, ApRelabeling, BseRelabeling }; +static relabeling_mode relabeling = NoRelabeling; static spot::ltl::relabeling_style style = spot::ltl::Abc; static bool remove_wm = false; static bool remove_x = false; @@ -318,13 +323,16 @@ parse_opt(int key, char* arg, struct argp_state*) obligation = true; break; case OPT_RELABEL: - relabeling = true; + case OPT_RELABEL_BOOL: + relabeling = (key == OPT_RELABEL_BOOL ? BseRelabeling : ApRelabeling); if (!arg || !strncasecmp(arg, "abc", 6)) style = spot::ltl::Abc; else if (!strncasecmp(arg, "pnn", 4)) style = spot::ltl::Pnn; else - error(2, 0, "invalid argument for --relabel: '%s'", arg); + error(2, 0, "invalid argument for --relabel%s: '%s'", + (key == OPT_RELABEL_BOOL ? "-bool" : ""), + arg); break; case OPT_REMOVE_WM: remove_wm = true; @@ -466,11 +474,24 @@ namespace f = res; } - if (relabeling) + switch (relabeling) { - const spot::ltl::formula* res = spot::ltl::relabel(f, style); - f->destroy(); - f = res; + case ApRelabeling: + { + const spot::ltl::formula* res = spot::ltl::relabel(f, style); + f->destroy(); + f = res; + break; + } + case BseRelabeling: + { + const spot::ltl::formula* res = spot::ltl::relabel_bse(f, style); + f->destroy(); + f = res; + break; + } + case NoRelabeling: + break; } if (remove_wm) diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index aa07f9582..9eb4a5207 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -147,6 +147,31 @@ namespace spot return instance(op_, v); } + unsigned + multop::boolean_count() const + { + unsigned pos = 0; + unsigned s = size(); + while (pos < s && nth(pos)->is_boolean()) + ++pos; + return pos; + } + + const formula* + multop::boolean_operands(unsigned* width) const + { + unsigned s = boolean_count(); + if (width) + *width = s; + if (!s) + return 0; + vec* v = new vec(children_->begin(), + children_->begin() + s); + for (unsigned n = 0; n < s; ++n) + (*v)[n]->clone(); + return instance(op_, v); + } + multop::type multop::op() const { @@ -599,7 +624,7 @@ namespace spot } else { - // The instance did not already exist. + // The instance did not already exist. res = ires.first->second = new multop(op, v); } res->clone(); diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 4750e3e65..550fedd87 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -138,6 +138,23 @@ namespace spot /// return a new formula a|b|d. const formula* all_but(unsigned n) const; + /// \brief return the number of Boolean operands in the binop. + /// + /// For instance if \c f a|b|Xc|Gd, this + /// returns 2. + unsigned boolean_count() const; + + /// \brief return the Boolean part of the binop. + /// + /// For instance if \c f a|b|Xc|Gd, this + /// returns a|b. Return 0 if there is no + /// Boolean operand. + /// + /// If \a width is not null, it is filled with the number + /// of Boolean operands extracted (i.e., the result + /// of boolean_count()) + const formula* boolean_operands(unsigned* width = 0) const; + /// Get the type of this operator. type op() const; /// Get the type of this operator, as a string. diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index fdeafe168..887530240 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -32,6 +32,7 @@ check_PROGRAMS = \ length \ ltl2dot \ ltl2text \ + ltlrel \ lunabbrev \ nenoform \ reduc \ @@ -52,6 +53,7 @@ length_SOURCES = length.cc ltl2dot_SOURCES = readltl.cc ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY ltl2text_SOURCES = readltl.cc +ltlrel_SOURCES = ltlrel.cc lunabbrev_SOURCES = equals.cc lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DLUNABBREV nenoform_SOURCES = equals.cc @@ -94,6 +96,7 @@ TESTS = \ consterm.test \ kind.test \ remove_x.test \ + ltlrel.test \ ltlfilt.test \ latex.test \ lbt.test \ diff --git a/src/ltltest/ltlfilt.test b/src/ltltest/ltlfilt.test index c1640e1ad..1e2f11c4c 100755 --- a/src/ltltest/ltlfilt.test +++ b/src/ltltest/ltlfilt.test @@ -139,3 +139,23 @@ GFa | FGb F(GFa | Gb) F(b W GFa) EOF + + +cat >in <exp <out +diff exp out diff --git a/src/ltltest/ltlrel.cc b/src/ltltest/ltlrel.cc new file mode 100644 index 000000000..45dd68df6 --- /dev/null +++ b/src/ltltest/ltlrel.cc @@ -0,0 +1,77 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013 Laboratoire de Recherche et Developement 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 +#include "ltlparse/public.hh" +#include "ltlvisit/relabel.hh" +#include "ltlast/allnodes.hh" +#include "ltlvisit/tostring.hh" + +void +syntax(char *prog) +{ + std::cerr << prog << " formula" << std::endl; + exit(2); +} + +int +main(int argc, char **argv) +{ + if (argc != 2) + syntax(argv[0]); + + spot::ltl::parse_error_list p1; + const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); + + if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) + return 2; + + spot::ltl::relabeling_map* m = new spot::ltl::relabeling_map; + const spot::ltl::formula* f2 = spot::ltl::relabel_bse(f1, spot::ltl::Pnn, m); + f1->destroy(); + spot::ltl::to_string(f2, std::cout) << "\n"; + + + typedef std::map map_t; + map_t sorted_map; + for (spot::ltl::relabeling_map::const_iterator i = m->begin(); + i != m->end(); ++i) + sorted_map[spot::ltl::to_string(i->first)] = + spot::ltl::to_string(i->second); + for (map_t::const_iterator i = sorted_map.begin(); + i != sorted_map.end(); ++i) + std::cout << " " << i->first << " -> " + << i->second << "\n"; + f2->destroy(); + delete m; + + spot::ltl::atomic_prop::dump_instances(std::cerr); + spot::ltl::unop::dump_instances(std::cerr); + spot::ltl::binop::dump_instances(std::cerr); + spot::ltl::multop::dump_instances(std::cerr); + spot::ltl::automatop::dump_instances(std::cerr); + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + assert(spot::ltl::automatop::instance_count() == 0); + return 0; +} diff --git a/src/ltltest/ltlrel.test b/src/ltltest/ltlrel.test new file mode 100755 index 000000000..13c4de3a0 --- /dev/null +++ b/src/ltltest/ltlrel.test @@ -0,0 +1,79 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2013 Laboratoire de Recherche et Dévelopement 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 . + + +# Check for the constant_term visitor + +. ./defs || exit 1 + +set -e + +t() +{ + cat > tmp.$$ + run 0 ../ltlrel "`head -n 1 tmp.$$`" > out.$$ + sed 1d tmp.$$ > exp.$$ + diff out.$$ exp.$$ +} + +t < a & c + p1 -> b +EOF + +t < a + p1 -> b + p2 -> c +EOF + +t < b + p1 -> a | c +EOF + +t < h | i + p1 -> d & e + p2 -> !c + p3 -> f +EOF + +t < b +p0 + p0 -> a <-> b +EOF + +t < b) & X(b -> c) +(p0 <-> p1) & X(p1 -> p2) + p0 -> a + p1 -> b + p2 -> c +EOF diff --git a/src/ltlvisit/relabel.cc b/src/ltlvisit/relabel.cc index 9236c283b..903ddc717 100644 --- a/src/ltlvisit/relabel.cc +++ b/src/ltlvisit/relabel.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,48 +17,43 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include +#include "relabel.hh" #include #include "clone.hh" #include "misc/hash.hh" #include "ltlenv/defaultenv.hh" +#include "ltlast/allnodes.hh" +#include +#include + +#include +#include "tostring.hh" namespace spot { namespace ltl { + + ////////////////////////////////////////////////////////////////////// + // Basic relabeler + ////////////////////////////////////////////////////////////////////// + namespace { - class relabeler: public clone_visitor + struct ap_generator { - public: - typedef Sgi::hash_map > map; - map newname; - - void - visit(const atomic_prop* ap) - { - map::const_iterator it = newname.find(ap); - if (it != newname.end()) - result_ = it->second->clone(); - else - newname[ap] = result_ = next(); - } - virtual const formula* next() = 0; + virtual ~ap_generator() {} }; - class relabeler_pnn: public relabeler + struct pnn_generator: ap_generator { - public: - relabeler_pnn() + unsigned nn; + pnn_generator() : nn(0) { } - unsigned nn; - const formula* next() { std::ostringstream s; @@ -67,10 +62,10 @@ namespace spot } }; - class relabeler_abc: public relabeler + struct abc_generator: ap_generator { public: - relabeler_abc() + abc_generator() : nn(0) { } @@ -91,26 +86,467 @@ namespace spot return default_environment::instance().require(s); } }; + + + class relabeler: public clone_visitor + { + public: + typedef Sgi::hash_map > map; + map newname; + ap_generator* gen; + relabeling_map* oldnames; + + relabeler(ap_generator* gen, relabeling_map* m) + : gen(gen), oldnames(m) + { + } + + ~relabeler() + { + delete gen; + } + + const formula* rename(const formula* old) + { + std::pair r = + newname.insert(map::value_type(old, 0)); + if (!r.second) + { + return r.first->second->clone(); + } + else + { + const formula* res; + r.first->second = res = gen->next(); + if (oldnames) + (*oldnames)[res] = old->clone(); + return res; + } + } + + using clone_visitor::visit; + + void + visit(const atomic_prop* ap) + { + result_ = rename(ap); + } + + }; + } const formula* - relabel(const formula* f, relabeling_style style) + relabel(const formula* f, relabeling_style style, + relabeling_map* m) { - relabeler* rel = 0; + ap_generator* gen = 0; switch (style) { case Pnn: - rel = new relabeler_pnn; + gen = new pnn_generator; break; case Abc: - rel = new relabeler_abc; + gen = new abc_generator; break; } - f->accept(*rel); - const formula* res = rel->result(); - delete rel; - return res; + relabeler rel(gen, m); + return rel.recurse(f); + } + + ////////////////////////////////////////////////////////////////////// + // Boolean-subexpression relabeler + ////////////////////////////////////////////////////////////////////// + + // Detecting Boolean subexpression is not a problem. Further more + // because we are already representing LTL formulas with + // sharing of identical sub-expressions we can easily rename a + // subexpression only once. However this scheme fails has two + // problems: + // + // 1. It will not detect inter-dependent Boolean subexpressions. + // For instance it will mistakenly relabel "(a & b) U (a & !b)" + // as "p0 U p1", hiding the dependency between a&b and a&!b. + // + // 2. Because of our n-ary operators, it will fail to + // notice that (a & b) is a sub-expression of (a & b & c). + // + // The code below only addresses point 1 so that interdependent + // subexpressions are not relabeled. Point 2 could be improved in + // a future version of somebody feels inclined to do so. + // + // The way we compute the subexpressions that can be relabeled is + // by transforming the formula syntax tree into an undirected + // graph, and computing the cut points of this graph. The cut + // points (or articulation points) are the node whose removal + // would split the graph in two components. To ensure that a + // Boolean operator is only considered as a cut-point if it would + // separate all of its children from the rest of the graph, we + // connect all the children of Boolean operators. + // + // For instance (a & b) U (c & d) has two (Boolean) cut-points + // corresponding to the two AND operators: + // + // (a&b)U(c&d) + // ╱ ╲ + // a&b c&d + // ╱ ╲ ╱ ╲ + // a─────b c─────d + // + // (The root node is also a cut-point, but we only consider Boolean + // cut-points for relabeling.) + // + // On the other hand, (a & b) U (b & !c) has only one Boolean + // cut-point which corresponds to the NOT operator: + // + // (a&b)U(b&!c) + // ╱ ╲ + // a&b b&c + // ╱ ╲ ╱ ╲ + // a─────b────!c + // │ + // c + // + // Note that if the children of a&b and b&c were not connected, + // a&b and b&c would be considered as cut-points because they + // separate "a" or "!c" from the rest of the graph. + namespace + { + typedef std::vector succ_vec; + typedef std::map fgraph; + + // Convert the formula's syntax tree into an undirected graph + // labeled by subformulas. + class formula_to_fgraph: public visitor + { + public: + fgraph& g; + std::stack s; + + formula_to_fgraph(fgraph& g): + g(g) + { + } + + ~formula_to_fgraph() + { + } + + void + visit(const atomic_prop*) + { + } + + void + visit(const constant*) + { + } + + void + visit(const bunop* bo) + { + recurse(bo->child()); + } + + void + visit(const unop* uo) + { + recurse(uo->child()); + } + + void + visit(const binop* bo) + { + const formula* l = bo->first(); + recurse(l); + const formula* r = bo->second(); + recurse(r); + // Link operands of Boolean operators. + if (bo->is_boolean()) + { + g[l].push_back(r); + g[r].push_back(l); + } + } + + void + visit(const automatop* ao) + { + for (unsigned i = 0; i < ao->size(); ++i) + recurse(ao->nth(i)); + } + + void + visit(const multop* mo) + { + unsigned mos = mo->size(); + + /// If we have a formula like (a & b & Xc), consider + /// it as ((a & b) & Xc) in the graph to isolate the + /// Boolean operands as a single node. + unsigned i = 0; + const formula* b = mo->is_boolean() ? 0 : mo->boolean_operands(&i); + if (b) + { + recurse(b); + b->destroy(); + } + for (; i < mos; ++i) + recurse(mo->nth(i)); + // For Boolean nodes, connect all children in a loop. This + // way the node can only be a cut-point if it separates all + // children from the reset of the graph (not only one). + if (mo->is_boolean()) + { + const formula* pred = mo->nth(0); + for (i = 1; i < mos; ++i) + { + const formula* next = mo->nth(i); + // Note that we only add an edge in one direction, + // because we are building a cycle between all + // children anyway. + g[pred].push_back(next); + pred = next; + } + g[pred].push_back(mo->nth(0)); + } + } + + void + recurse(const formula* f) + { + std::pair i = + g.insert(fgraph::value_type(f, succ_vec())); + + if (!s.empty()) + { + const formula* top = s.top(); + i.first->second.push_back(top); + g[top].push_back(f); + if (!i.second) + return; + } + else + { + assert(i.second); + } + f->clone(); + s.push(f); + f->accept(*this); + s.pop(); + } + + }; + + + typedef std::set fset; + struct data_entry // for each node of the graph + { + unsigned num; // serial number, in pre-order + unsigned low; // lowest number accessible via unstacked descendants + }; + typedef Sgi::hash_map fmap_t; + struct stack_entry + { + const formula* grand_parent; + const formula* parent; // current node + succ_vec::const_iterator current_child; + succ_vec::const_iterator last_child; + }; + typedef std::stack stack_t; + + // Fill c with the Boolean cutpoints of g, starting from start. + // + // This is based no "Efficient Algorithms for Graph + // Manipulation", J. Hopcroft & R. Tarjan, in Communications of + // the ACM, 16 (6), June 1973. + // + // It differs from the original algorithm by returning only the + // Boolean cutpoints, and not dealing with the initial state + // properly (our initial state will always be considered as a + // cut-point, but since we only return Boolean cut-points it's + // OK: if the top-most formula is Boolean we want to replace it + // as a whole). + void cut_points(const fgraph& g, fset& c, const formula* start) + { + stack_t s; + + unsigned num = 0; + fmap_t data; + data_entry d = { num, num }; + data[start] = d; + ++num; + const succ_vec& children = g.find(start)->second; + stack_entry e = { start, start, children.begin(), children.end() }; + s.push(e); + + while (!s.empty()) + { + // std::cerr << "-- visiting " << to_string(s.top().parent) << "\n"; + stack_entry& e = s.top(); + if (e.current_child != e.last_child) + { + // Skip the edge if it is just the reverse of the one + // we took. + const formula* child = *e.current_child; + if (child == e.grand_parent) + { + ++e.current_child; + continue; + } + // std::cerr << " grand parent is " + // << to_string(e.grand_parent) << "\n" + // << " child is " << to_string(child) << "\n"; + data_entry d = { num, num }; + std::pair i = + data.insert(fmap_t::value_type(child, d)); + if (i.second) // New destination. + { + ++num; + const succ_vec& children = g.find(child)->second; + stack_entry newe = { e.parent, child, + children.begin(), children.end() }; + s.push(newe); + } + else // Destination exists. + { + data_entry& dparent = data[e.parent]; + data_entry& dchild = i.first->second; + // If this is a back-edge, update + // the low field of the parent. + if (dchild.num <= dparent.num) + if (dparent.low > dchild.num) + dparent.low = dchild.num; + } + ++e.current_child; + } + else + { + const formula* grand_parent = e.grand_parent; + const formula* parent = e.parent; + s.pop(); + if (!s.empty()) + { + data_entry& dparent = data[parent]; + data_entry& dgrand_parent = data[grand_parent]; + if (dparent.low >= dgrand_parent.num // cut-point + && grand_parent->is_boolean()) + c.insert(grand_parent); + if (dparent.low < dgrand_parent.low) + dgrand_parent.low = dparent.low; + } + } + //std::cerr << " state of data:\n"; + //for (fmap_t::const_iterator i = data.begin(); + // i != data.end(); ++i) + // { + // std::cerr << " " << to_string(i->first) + // << " = { num=" << i->second.num + // << ", low=" << i->second.low + // << " }\n"; + // } + } + } + + + class bse_relabeler: public relabeler + { + public: + fset& c; + + bse_relabeler(ap_generator* gen, fset& c, + relabeling_map* m) + : relabeler(gen, m), c(c) + { + } + + using relabeler::visit; + + void + visit(const multop* mo) + { + unsigned mos = mo->size(); + + /// If we have a formula like (a & b & Xc), consider + /// it as ((a & b) & Xc) in the graph to isolate the + /// Boolean operands as a single node. + unsigned i = 0; + const formula* b = mo->is_boolean() ? 0 : mo->boolean_operands(&i); + multop::vec* res = new multop::vec; + if (b) + { + res->reserve(mos - i + 1); + res->push_back(recurse(b)); + b->destroy(); + } + else + { + res->reserve(mos); + } + for (; i < mos; ++i) + res->push_back(recurse(mo->nth(i))); + result_ = multop::instance(mo->op(), res); + } + + const formula* + recurse(const formula* f) + { + fset::const_iterator it = c.find(f); + if (it != c.end()) + result_ = rename(f); + else + f->accept(*this); + return result_; + } + }; + + } + + + const formula* + relabel_bse(const formula* f, relabeling_style style, + relabeling_map* m) + { + fgraph g; + + // Build the graph g from the formula f. + { + formula_to_fgraph conv(g); + conv.recurse(f); + } + + // Compute its cut-points + fset c; + cut_points(g, c, f); + + // Relabel the formula recursively, stopping + // at cut-points or atomic propositions. + ap_generator* gen = 0; + switch (style) + { + case Pnn: + gen = new pnn_generator; + break; + case Abc: + gen = new abc_generator; + break; + } + bse_relabeler rel(gen, c, m); + f = rel.recurse(f); + + // Cleanup. + fgraph::const_iterator i = g.begin(); + while (i != g.end()) + { + const formula* f = i->first; + ++i; + f->destroy(); + } + + return f; } } } diff --git a/src/ltlvisit/relabel.hh b/src/ltlvisit/relabel.hh index 34030c105..75cc7bef7 100644 --- a/src/ltlvisit/relabel.hh +++ b/src/ltlvisit/relabel.hh @@ -20,7 +20,8 @@ #ifndef SPOT_LTLVISIT_RELABEL_HH # define SPOT_LTLVISIT_RELABEL_HH -#include +#include "ltlast/formula.hh" +#include "misc/hash.hh" namespace spot { @@ -28,10 +29,38 @@ namespace spot { enum relabeling_style { Abc, Pnn }; + + struct relabeling_map: public Sgi::hash_map > + { + ~relabeling_map() + { + for (iterator i = begin(); i != end(); ++i) + i->second->destroy(); + } + }; + /// \ingroup ltl_rewriting /// \brief Relabel the atomic propositions in a formula. + /// + /// If \a m is non-null, it is filled with correspondence + /// between the new names (keys) and the old names (values). SPOT_API - const formula* relabel(const formula* f, relabeling_style style); + const formula* relabel(const formula* f, relabeling_style style, + relabeling_map* m = 0); + + + /// \ingroup ltl_rewriting + /// \brief Relabel Boolean subexpressions in a formula using + /// atomic propositions. + /// + /// If \a m is non-null, it is filled with correspondence + /// between the new names (keys) and the old names (values). + SPOT_API + const formula* relabel_bse(const formula* f, relabeling_style style, + relabeling_map* m = 0); + } }