relabel: implement relabeling of Boolean subexpressions.

* src/ltlast/multop.cc, src/ltlast/multop.hh (multop::boolean_operands,
multop::boolean_count): New methods.
* src/ltlvisit/relabel.cc, src/ltlvisit/relabel.hh
(relabel): Take an optional relabeling_map as parameter.
(relabel_bse): New.
* src/ltltest/ltlrel.test, src/ltltest/ltlrel.cc: New files.
* src/ltltest/Makefile.am: Add them.
* src/bin/ltlfilt.cc: Add option --relabel-bool.
* src/ltltest/ltlfilt.test: Test it.
* NEWS: Mention it.
* doc/org/ltlfilt.org: Illustrate it.

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

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 <<EOF
+G (hfe_rdy -> 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:

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_SKIP_ERRORS 1
-#define OPT_DROP_ERRORS 3
+#define OPT_DROP_ERRORS 2
-#define OPT_NNF 4
+#define OPT_NNF 3
-#define OPT_LTL 5
+#define OPT_LTL 4
-#define OPT_NOX 7
+#define OPT_NOX 5
-#define OPT_BOOLEAN 8
+#define OPT_BOOLEAN 6
-#define OPT_EVENTUAL 9
+#define OPT_EVENTUAL 7
-#define OPT_UNIVERSAL 10
+#define OPT_UNIVERSAL 8
-#define OPT_SYNTACTIC_SAFETY 11
+#define OPT_SYNTACTIC_SAFETY 9
-#define OPT_SYNTACTIC_GUARANTEE 12
+#define OPT_SYNTACTIC_GUARANTEE 10
-#define OPT_SYNTACTIC_OBLIGATION 13
+#define OPT_SYNTACTIC_OBLIGATION 11
-#define OPT_SYNTACTIC_RECURRENCE 14
+#define OPT_SYNTACTIC_RECURRENCE 12
-#define OPT_SYNTACTIC_PERSISTENCE 15
+#define OPT_SYNTACTIC_PERSISTENCE 13
-#define OPT_SAFETY 16
+#define OPT_SAFETY 14
-#define OPT_GUARANTEE 17
+#define OPT_GUARANTEE 15
-#define OPT_OBLIGATION 18
+#define OPT_OBLIGATION 16
-#define OPT_SIZE_MIN 19
+#define OPT_SIZE_MIN 17
-#define OPT_SIZE_MAX 20
+#define OPT_SIZE_MAX 18
-#define OPT_BSIZE_MIN 21
+#define OPT_BSIZE_MIN 19
-#define OPT_BSIZE_MAX 22
+#define OPT_BSIZE_MAX 20
-#define OPT_IMPLIED_BY 23
+#define OPT_IMPLIED_BY 21
-#define OPT_IMPLY 24
+#define OPT_IMPLY 22
-#define OPT_EQUIVALENT_TO 25
+#define OPT_EQUIVALENT_TO 23
-#define OPT_RELABEL 26
+#define OPT_RELABEL 24
-#define OPT_REMOVE_WM 27
+#define OPT_RELABEL_BOOL 25
-#define OPT_BOOLEAN_TO_ISOP 28
+#define OPT_REMOVE_WM 26
-#define OPT_REMOVE_X 29
+#define OPT_BOOLEAN_TO_ISOP 27
-#define OPT_STUTTER_INSENSITIVE 30
+#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);
+	case ApRelabeling:
-	  f->destroy();
+	  {
-	  f = res;
+	    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)

src/ltlast/multop.cc

@@ -1,5 +1,5 @@
-// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
+// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
-// Développement de l'Epita (LRDE).
+// 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();

src/ltlast/multop.hh

@@ -138,6 +138,23 @@ namespace spot
       /// return a new formula <code>a|b|d</code>.
       const formula* all_but(unsigned n) const;
 
+      /// \brief return the number of Boolean operands in the binop.
+      ///
+      /// For instance if \c f <code>a|b|Xc|Gd</code>, this
+      /// returns 2.
+      unsigned boolean_count() const;
+
+      /// \brief return the Boolean part of the binop.
+      ///
+      /// For instance if \c f <code>a|b|Xc|Gd</code>, this
+      /// returns <code>a|b</code>.  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.

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 \

src/ltltest/ltlfilt.test

@@ -139,3 +139,23 @@ GFa | FGb
 F(GFa | Gb)
 F(b W GFa)
 EOF
+
+
+cat >in <<EOF
+a & Xb & c
+a & b & GF(a | c) & FG(a | c)
+b & GF(a | c) & FG(a | c)
+G(d & e) | FG(Xf| !c) | h | i
+b & !Xc & e & (f | g)
+b & GF(a | c) & !GF!(a | c)
+EOF
+
+cat >exp <<EOF
+p0 & Xp1
+p0 & p1 & GF(p0 | p2) & FG(p0 | p2)
+p0 & GFp1 & FGp1
+p0 | Gp1 | FG(p2 | Xp3)
+EOF
+
+run 0 ../../bin/ltlfilt -u --nnf --relabel-bool=pnn in >out
+diff exp out

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 <http://www.gnu.org/licenses/>.
+
+#include <iostream>
+#include <cassert>
+#include <cstdlib>
+#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<std::string, std::string> 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;
+}

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 <http://www.gnu.org/licenses/>.
+
+
+# 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 <<EOF
+a & Xb & c
+p0 & Xp1
+  p0   ->   a & c
+  p1   ->   b
+EOF
+
+t <<EOF
+a & b & GF(a | c) & FG(a | c)
+p0 & p1 & GF(p0 | p2) & FG(p0 | p2)
+  p0   ->   a
+  p1   ->   b
+  p2   ->   c
+EOF
+
+t <<EOF
+b & GF(a | c) & FG(a | c)
+p0 & GFp1 & FGp1
+  p0   ->   b
+  p1   ->   a | c
+EOF
+
+t <<EOF
+G(d & e) | FG(Xf| !c) | h | i
+p0 | Gp1 | FG(p2 | Xp3)
+  p0   ->   h | i
+  p1   ->   d & e
+  p2   ->   !c
+  p3   ->   f
+EOF
+
+t <<EOF
+a <-> b
+p0
+  p0   ->   a <-> b
+EOF
+
+t <<EOF
+(a <-> b) & X(b -> c)
+(p0 <-> p1) & X(p1 -> p2)
+  p0   ->   a
+  p1   ->   b
+  p2   ->   c
+EOF

src/ltlvisit/relabel.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et
+// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
-// Développement de l'Epita (LRDE).
+// 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 <http://www.gnu.org/licenses/>.
 
-#include <relabel.hh>
+#include "relabel.hh"
 #include <sstream>
 #include "clone.hh"
 #include "misc/hash.hh"
 #include "ltlenv/defaultenv.hh"
+#include "ltlast/allnodes.hh"
+#include <map>
+#include <stack>
+
+#include <iostream>
+#include "tostring.hh"
 
 namespace spot
 {
   namespace ltl
   {
+
+    //////////////////////////////////////////////////////////////////////
+    // Basic relabeler
+    //////////////////////////////////////////////////////////////////////
+
     namespace
     {
-      class relabeler: public clone_visitor
+      struct ap_generator
       {
-      public:
-	typedef Sgi::hash_map<const atomic_prop*, const formula*,
-			      ptr_hash<atomic_prop> > 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:
+	unsigned nn;
-	relabeler_pnn()
+	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<const formula*, const formula*,
+			      ptr_hash<formula> > 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<map::iterator, bool> 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);
+      relabeler rel(gen, m);
-      const formula* res = rel->result();
+      return rel.recurse(f);
-      delete rel;
+    }
-      return res;
+
+    //////////////////////////////////////////////////////////////////////
+    // 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<const formula*> succ_vec;
+      typedef std::map<const formula*, succ_vec> 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<const formula*> 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<fgraph::iterator, bool> 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<const formula*> 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<const formula*, data_entry,
+			    const formula_ptr_hash> 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_entry> 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<fmap_t::iterator, bool> 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;
     }
   }
 }

src/ltlvisit/relabel.hh

@@ -20,7 +20,8 @@
 #ifndef SPOT_LTLVISIT_RELABEL_HH
 # define SPOT_LTLVISIT_RELABEL_HH
 
-#include <ltlast/formula.hh>
+#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<const formula*,
+						const formula*,
+						ptr_hash<formula> >
+    {
+      ~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);
+
   }
 }