From 179672fe3b920134d71287cec9cabb1b2ea0a30d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 13 Oct 2022 11:34:38 +0200
Subject: [PATCH] relabel: fix handling of concat and fusion

* spot/tl/relabel.cc (formula_to_fgraph): Do not assume that n-ary
operators are Boolean operators.
* tests/python/relabel.py: Add a test case found while discussing
some expression with Antoine Martin.
* NEWS: Mention it.
---
 NEWS                    |  3 +++
 spot/tl/relabel.cc      | 14 +++++++++++---
 tests/python/relabel.py |  4 ++++
 3 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/NEWS b/NEWS
index 805325fe6..3ad57d31d 100644
--- a/NEWS
+++ b/NEWS
@@ -3,6 +3,9 @@ New in spot 2.11.1.dev  (not yet released)
   Bugs fixed:
 
   - Fix pkg-config files containing @LIBSPOT_PTHREAD@ (issue #520)
+  - spot::relabel_bse() was incorrectly relabeling some dependent
+    Boolean subexpressions in SERE.  (Note that this had no
+    consequence on automata translated from those SERE.)
 
 New in spot 2.11.1  (2022-10-10)
 
diff --git a/spot/tl/relabel.cc b/spot/tl/relabel.cc
index 44d6577cb..26c7564c1 100644
--- a/spot/tl/relabel.cc
+++ b/spot/tl/relabel.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012-2016, 2018-2020 Laboratoire de Recherche et
+// Copyright (C) 2012-2016, 2018-2020, 2022 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -363,7 +363,7 @@ namespace spot
                 goto done;
               }
           }
-        if (sz > 2 && !f.is_boolean())
+        if (sz > 2 && !f.is_boolean() && f.is(op::And, op::Or))
           {
             /// If we have a formula like (a & b & Xc), consider
             /// it as ((a & b) & Xc) in the graph to isolate the
@@ -384,7 +384,7 @@ namespace spot
             for (i = 1; i < sz; ++i)
               {
                 formula next = f[i];
-                // Note that we only add an edge in both directions,
+                // Note that we add an edge in both directions,
                 // as the cut point algorithm really need undirected
                 // graphs.  (We used to do only one direction, and
                 // that turned out to be a bug.)
@@ -581,6 +581,14 @@ namespace spot
       conv.visit(f);
     }
 
+    //// Uncomment to print the graph.
+    // for (auto& [f, sv]: g)
+    //   {
+    //     std::cerr << f << ":\n";
+    //     for (auto& s: sv)
+    //       std::cerr << "  " << s << '\n';
+    //   }
+
     // Compute its cut-points
     fset c;
     cut_points(g, c, f);
diff --git a/tests/python/relabel.py b/tests/python/relabel.py
index 0de668b12..b32ebd752 100644
--- a/tests/python/relabel.py
+++ b/tests/python/relabel.py
@@ -55,3 +55,7 @@ try:
     spot.relabel_here(autg, m)
 except RuntimeError as e:
     tc.assertIn("old labels", str(e))
+
+f = spot.parse_infix_sere("(p9;p21|p22):(p1&p2;p11&p22;p1&p2)").f
+g = spot.relabel_bse(f, spot.Abc)
+tc.assertEqual(str(g), "(a;(b | c)):(d;(c & e);d)")