relabel: introduce an overlapping relabeling version

Related to issue #500 and issue #536.

* spot/tl/relabel.hh (relabel_overlapping_bse): New function.
* spot/tl/relabel.cc: Implement it.
* bin/ltlfilt.cc: Add a --relabel-overlapping-bool option.
* tests/core/ltlfilt.test: Test it.
* NEWS: Mention it.

NEWS

@@ -12,6 +12,10 @@ New in spot 2.11.6.dev  (not yet released)
 
         autfilt input.hoa -o output-%l.hoa
 
+  - ltlfilt has a new option --relabel-overlapping-bool=abc|pnn that
+    will replace boolean subformulas by fresh atomic propositions even
+    if those subformulas share atomic propositions.
+
   Library:
 
   - The following new trivial simplifications have been implemented for SEREs:
@@ -29,6 +33,10 @@ New in spot 2.11.6.dev  (not yet released)
   - spot::bdd_to_cnf_formula() is a new variant of spot::bdd_to_formula()
     that converts a BDD into a CNF instead of a DNF.
 
+  - spot::relabel_overlapping_bse() is a new function that will
+    replace boolean subformulas by fresh atomic propositions even if
+    those subformulas share atomic propositions.
+
 New in spot 2.11.6  (2023-08-01)
 
   Bug fixes:

bin/ltlfilt.cc

@@ -94,6 +94,7 @@ enum {
   OPT_REJECT_WORD,
   OPT_RELABEL,
   OPT_RELABEL_BOOL,
+  OPT_RELABEL_OVERLAP,
   OPT_REMOVE_WM,
   OPT_REMOVE_X,
   OPT_SAFETY,
@@ -139,8 +140,12 @@ static const argp_option options[] =
       "relabel all atomic propositions, alphabetically unless " \
       "specified otherwise", 0 },
     { "relabel-bool", OPT_RELABEL_BOOL, "abc|pnn", OPTION_ARG_OPTIONAL,
-      "relabel Boolean subexpressions, alphabetically unless " \
+      "relabel Boolean subexpressions that do not share atomic propositions,"
-      "specified otherwise", 0 },
+      " relabel alphabetically unless specified otherwise", 0 },
+    { "relabel-overlapping-bool", OPT_RELABEL_OVERLAP, "abc|pnn",
+      OPTION_ARG_OPTIONAL,
+      "relabel Boolean subexpressions even if they share atomic propositions,"
+      " relabel alphabetically unless specified otherwise", 0 },
     { "define", OPT_DEFINE, "FILENAME", OPTION_ARG_OPTIONAL,
       "when used with --relabel or --relabel-bool, output the relabeling map "
       "using #define statements", 0 },
@@ -316,7 +321,10 @@ static bool recurrence = false;
 static bool persistence = false;
 static range size = { -1, -1 };
 static range bsize = { -1, -1 };
-enum relabeling_mode { NoRelabeling = 0, ApRelabeling, BseRelabeling };
+enum relabeling_mode { NoRelabeling = 0,
+                       ApRelabeling,
+                       BseRelabeling,
+                       OverlappingRelabeling };
 static relabeling_mode relabeling = NoRelabeling;
 static spot::relabeling_style style = spot::Abc;
 static bool remove_x = false;
@@ -358,6 +366,19 @@ parse_formula_arg(const std::string& input)
   return pf.f;
 }
 
+static void
+parse_relabeling_style(const char* arg, const char* optname)
+{
+  if (!arg || !strncasecmp(arg, "abc", 6))
+    style = spot::Abc;
+  else if (!strncasecmp(arg, "pnn", 4))
+    style = spot::Pnn;
+  else
+    error(2, 0, "invalid argument for --relabel%s: '%s'\n"
+          "expecting 'abc' or 'pnn'", optname, arg);
+}
+
+
 static int
 parse_opt(int key, char* arg, struct argp_state*)
 {
@@ -500,16 +521,16 @@ parse_opt(int key, char* arg, struct argp_state*)
         }
       break;
     case OPT_RELABEL:
+      relabeling = ApRelabeling;
+      parse_relabeling_style(arg, "");
+      break;
     case OPT_RELABEL_BOOL:
-      relabeling = (key == OPT_RELABEL_BOOL ? BseRelabeling : ApRelabeling);
+      relabeling = BseRelabeling;
-      if (!arg || !strncasecmp(arg, "abc", 6))
+      parse_relabeling_style(arg, "-bool");
-        style = spot::Abc;
+      break;
-      else if (!strncasecmp(arg, "pnn", 4))
+    case OPT_RELABEL_OVERLAP:
-        style = spot::Pnn;
+      relabeling = OverlappingRelabeling;
-      else
+      parse_relabeling_style(arg, "-overlapping-bool");
-        error(2, 0, "invalid argument for --relabel%s: '%s'",
-              (key == OPT_RELABEL_BOOL ? "-bool" : ""),
-              arg);
       break;
     case OPT_REMOVE_WM:
       unabbreviate += "MW";
@@ -701,6 +722,12 @@ namespace
             f = spot::relabel_bse(f, style, &relmap);
             break;
           }
+        case OverlappingRelabeling:
+          {
+            relmap.clear();
+            f = spot::relabel_overlapping_bse(f, style, &relmap);
+            break;
+          }
         case NoRelabeling:
           break;
         }

spot/tl/relabel.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012-2016, 2018-2020, 2022 Laboratoire de Recherche et
+// Copyright (C) 2012-2016, 2018-2020, 2022, 2023 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -80,7 +80,9 @@ namespace spot
       }
     };
 
-
+    // if subexp == false, matches APs
+    // if subexp == true, matches boolean subexps
+    template <bool subexp>
     class relabeler
     {
     public:
@@ -101,54 +103,89 @@ namespace spot
 
       formula rename(formula old)
       {
+        if constexpr (subexp)
+          {
+            // have we given a name to the negation of this formula?
+            auto neg = newname.find(formula::Not(old));
+            if (neg != newname.end())
+              return formula::Not(neg->second);
+          }
+
         auto r = newname.emplace(old, nullptr);
         if (!r.second)
-          {
+          return r.first->second;
-            return r.first->second;
+
-          }
+        formula res = gen->next();
-        else
+        r.first->second = res;
-          {
+        if (oldnames)
-            formula res = gen->next();
+          (*oldnames)[res] = old;
-            r.first->second = res;
+        return res;
-            if (oldnames)
-              (*oldnames)[res] = old;
-            return res;
-          }
       }
 
       formula
       visit(formula f)
       {
-        if (f.is(op::ap))
+        if ((!subexp && f.is(op::ap))
-          return rename(f);
+            || (subexp && f.is_boolean()))
+          {
+            return rename(f);
+          }
+        if (subexp && f.is(op::Or, op::And) && f[0].is_boolean())
+          {
+            // Boolean terms are always beginning of And and Or, so
+            // the above test capture Or/And that some Boolean arguments
+            // and some non-Boolean arguments.
+            unsigned i = 0;
+            formula b = f.boolean_operands(&i);
+            unsigned sz = f.size();
+            std::vector<formula> res;
+            res.reserve(sz - i + 1);
+            res.emplace_back(visit(b));
+            for (; i < sz; ++i)
+              res.emplace_back(visit(f[i]));
+            return formula::multop(f.kind(), res);
+          }
         else
-          return f.map([this](formula f)
+          {
-                       {
+            return f.map([this](formula f)
-                         return this->visit(f);
+            {
-                       });
+              return this->visit(f);
+            });
+          }
       }
 
     };
 
-  }
+    template<bool subexp>
+    formula
+    relabel_do(formula f, relabeling_style style, relabeling_map* m)
+    {
+      ap_generator* gen = nullptr;
+      switch (style)
+        {
+        case Pnn:
+          gen = new pnn_generator;
+          break;
+        case Abc:
+          gen = new abc_generator;
+          break;
+        }
 
+      relabeler<subexp> r(gen, m);
+      return r.visit(f);
+    }
+  }
 
   formula
   relabel(formula f, relabeling_style style, relabeling_map* m)
   {
-    ap_generator* gen = nullptr;
+    return relabel_do<false>(f, style, m);
-    switch (style)
+  }
-      {
-      case Pnn:
-        gen = new pnn_generator;
-        break;
-      case Abc:
-        gen = new abc_generator;
-        break;
-      }
 
-    relabeler r(gen, m);
+  formula
-    return r.visit(f);
+  relabel_overlapping_bse(formula f, relabeling_style style, relabeling_map* m)
+  {
+    return relabel_do<true>(f, style, m);
   }
 
   namespace
@@ -502,7 +539,7 @@ namespace spot
     }
 
 
-    class bse_relabeler final: public relabeler
+    class bse_relabeler final: public relabeler<false>
     {
     public:
       const fset& c;

spot/tl/relabel.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2015, 2019 Laboratoire de Recherche et
+// Copyright (C) 2012, 2013, 2015, 2019, 2023 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -34,6 +34,9 @@ namespace spot
   ///
   /// If \a m is non-null, it is filled with correspondence
   /// between the new names (keys) and the old names (values).
+  ///
+  /// \see relabel_bse
+  /// \see relabel_overlaping_bse
   SPOT_API
   formula relabel(formula f, relabeling_style style,
                   relabeling_map* m = nullptr);
@@ -45,9 +48,27 @@ namespace spot
   ///
   /// If \a m is non-null, it is filled with correspondence
   /// between the new names (keys) and the old names (values).
+  ///
+  /// The relabel_overlapping_bse() will introduce a new atomic
+  /// proposition for each maximal Boolean subexpression encountered,
+  /// even if they overlap (i.e., share common atomic
+  /// propositions). For instance `(a & b & c) U (c & d & e)` will be
+  /// simply be relabeled as `p0 U p1`.  This kind of renaming to not
+  /// preserves the
+  ///
+  /// The relabel_bse() version will make sure that the replaced
+  /// subexpressions do not share atomic propositions.  For instance
+  /// `(a & b & c) U (c & d & e)` will be simply be relabeled as
+  /// `(p0 & p1) U (p1 & p2)`, were `p1` replaces `c` and the rest
+  /// is obvious.
+  ///
+  /// @{
   SPOT_API
   formula relabel_bse(formula f, relabeling_style style,
                       relabeling_map* m = nullptr);
+  SPOT_API formula
+  relabel_overlapping_bse(formula f, relabeling_style style, relabeling_map* m);
+  // @}
 
   /// \ingroup tl_rewriting
   /// \brief Replace atomic propositions of \a f by subformulas

tests/core/ltlfilt.test

@@ -1,7 +1,7 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013-2020, 2022 Laboratoire de Recherche et Développement de
+# Copyright (C) 2013-2020, 2022, 2023 Laboratoire de Recherche et
-# l'Epita (LRDE).
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -361,6 +361,8 @@ G(d & e) | FG(Xf| !c) | h | i
 b & !Xc & e & (f | g)
 b & GF(a | c) & !GF!(a | c)
 F(a <-> b) -> (c xor d)
+(a & b & c) U (c & d & e)
+(a & b & c) U !(a & b & c)
 EOF
 
 cat >exp <<EOF
@@ -369,6 +371,8 @@ p0 & p1 & GF(p0 | p2) & FG(p0 | p2)
 p0 & GFp1 & FGp1
 p0 | Gp1 | FG(p2 | Xp3)
 p0 | Gp1
+(p0 & p1) U (p1 & p2)
+(p0 & p1 & p2) U (!p0 | !p1 | !p2)
 EOF
 
 run 0 ltlfilt -u --nnf --relabel-bool=pnn in >out
@@ -393,6 +397,14 @@ p0 || []p1 || <>[](p2 || Xp3)
 #define p0 ((c && !d) || (!c && d))
 #define p1 ((a && !b) || (!a && b))
 p0 || []p1
+#define p0 (a && b)
+#define p1 (c)
+#define p2 (d && e)
+(p0 && p1) U (p1 && p2)
+#define p0 (a)
+#define p1 (b)
+#define p2 (c)
+(p0 && p1 && p2) U (!p0 || !p1 || !p2)
 EOF
 
 run 0 ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out
@@ -433,11 +445,53 @@ p0 && []<>(p1 || p2) && ![]<>!(p1 || p2)
 #define p2 (c)
 #define p3 (d)
 <>(p0 <-> p1) -> !(p2 <-> p3)
+#define p0 (a)
+#define p1 (b)
+#define p2 (c)
+#define p3 (d)
+#define p4 (e)
+(p0 && p1 && p2) U (p2 && p3 && p4)
+#define p0 (a)
+#define p1 (b)
+#define p2 (c)
+(p0 && p1 && p2) U !(p0 && p1 && p2)
 EOF
 
 run 0 ltlfilt -s -u --relabel=pnn --define in >out
 diff exp out
 
+cat >exp <<EOF
+#define p0 (a & c)
+#define p1 (b)
+p0 & Xp1
+#define p0 (a & b)
+#define p1 (a | c)
+p0 & GFp1 & FGp1
+#define p0 (h | i)
+#define p1 (d & e)
+#define p2 (!c)
+#define p3 (f)
+p0 | Gp1 | FG(p2 | Xp3)
+#define p0 (b & e & (f | g))
+#define p1 (c)
+p0 & !Xp1
+#define p0 (b)
+#define p1 (a | c)
+p0 & GFp1 & !GF!p1
+#define p0 (a <-> b)
+#define p1 (c xor d)
+Fp0 -> p1
+#define p0 (a & b & c)
+#define p1 (c & d & e)
+p0 U p1
+#define p0 (a & b & c)
+p0 U !p0
+EOF
+
+run 0 ltlfilt -u --relabel-over=pnn --define in >out
+diff exp out
+
+
 toolong='((p2=0) * (p3=1))' # work around the 80-col check
 cat >exp <<EOF
 #define p0 (a=1)
@@ -470,6 +524,16 @@ cat >exp <<EOF
 #define p2 (a=1)
 #define p3 (b=1)
 ((p0=1) * (p1=0)) + ((p0=0) * (p1=1)) + (G(((p2=1) * (p3=0)) + $toolong))
+#define p0 (a=1)
+#define p1 (b=1)
+#define p2 (c=1)
+#define p3 (d=1)
+#define p4 (e=1)
+((p0=1) * (p1=1) * (p2=1)) U ((p2=1) * (p3=1) * (p4=1))
+#define p0 (a=1)
+#define p1 (b=1)
+#define p2 (c=1)
+((p0=1) * (p1=1) * (p2=1)) U ((p0=0) + (p1=0) + (p2=0))
 EOF
 run 0 ltlfilt -p --wring -u --nnf --relabel=pnn --define in >out
 diff exp out
@@ -484,6 +548,8 @@ h | i | G(d & e) | FG(!c | Xf)@
 b & e & (f | g) & !Xc@
 b & GF(a | c) & !GF!(a | c)@
 F(a <-> b) -> (c xor d)@
+(a & b & c) U (c & d & e)@
+(a & b & c) U !(a & b & c)@
 EOF
 diff exp out