relabel: generalize 9365f8de1 to remove more false edges

* spot/twaalgos/relabel.cc: Detect false edges as they are created,
even as the result of multiple renamings.
* tests/core/ltl2tgba2.test: More test cases, reported by Jens Kreber.
* NEWS: Mention the bug.
* THANKS: Add Jens.

NEWS

@@ -114,6 +114,11 @@ New in spot 2.8.7.dev (not yet released)
   - The twa_graph::is_alternating() and digraph::is_alternating() methods,
     deprecated in Spot 2.3.1 (2017-02-20), have been removed.
 
+  Bugs fixed:
+
+  - Relabeling automata could introduce false edges.  Those are now
+    removed.
+
 New in spot 2.8.7 (2020-03-13)
 
   Bugs fixed:

THANKS

@@ -23,6 +23,7 @@ Henrich Lauko
 Jan Strejček
 Jean-Michel Couvreur
 Jean-Michel Ilié
+Jens Kreber
 Jeroen Meijer
 Jiraphapa Jiravaraphan
 Joachim Klein

spot/twaalgos/relabel.cc

@@ -32,7 +32,6 @@ namespace spot
     std::set<int> newvars;
     vars.reserve(relmap->size());
     bool bool_subst = false;
-    bool need_cleanup = false;
 
     for (auto& p: *relmap)
       {
@@ -62,16 +61,20 @@ namespace spot
             bdd newb = formula_to_bdd(p.second, d, aut);
             bdd_setbddpair(pairs, oldv, newb);
             bool_subst = true;
-            if (newb == bddtrue || newb == bddfalse)
-              need_cleanup = true;
           }
       }
-    if (!bool_subst)
-      for (auto& t: aut->edges())
-        t.cond = bdd_replace(t.cond, pairs);
-    else
-      for (auto& t: aut->edges())
-        t.cond = bdd_veccompose(t.cond, pairs);
+
+    bool need_cleanup = false;
+    typedef bdd (*op_t)(const bdd&, bddPair*);
+    op_t op = bool_subst ?
+      static_cast<op_t>(bdd_veccompose) : static_cast<op_t>(bdd_replace);
+    for (auto& t: aut->edges())
+      {
+        bdd c = (*op)(t.cond, pairs);
+        t.cond = c;
+        if (c == bddfalse)
+          need_cleanup = true;
+      }
 
     // Erase all the old variables that are not reused in the new set.
     // (E.g., if we relabel a&p0 into p0&p1 we should not unregister
@@ -80,8 +83,8 @@ namespace spot
       if (newvars.find(v) == newvars.end())
         aut->unregister_ap(v);
 
-    // If some of the proposition are equivalent to true or false,
-    // it's possible that we have introduced edges with false labels.
+    // If some of the edges were relabeled false, we need to clean the
+    // automaton.
     if (need_cleanup)
       {
         aut->merge_edges();     // remove any edge labeled by 0

tests/core/ltl2tgba2.test

@@ -432,7 +432,13 @@ cat >expected <<EOF
 8,(Fin(1) | Inf(0)) & (Fin(2) | Inf(1)) & (Fin(0) | Inf(2))
 EOF
 
-# This formula used to produce translation with false label.
-ltl2tgba -D -G 'F(G(a | !a) & ((b <-> c) W d))' | grep '\[f\]' && exit 1
+# This formulas used to produce translation with false label.
 
+# Reported by Florian Renkin
+ltl2tgba -D -G 'F(G(a | !a) & ((b <-> c) W d))' | grep '\[f\]' && exit 1
+# Reported by Jens Kreber
+ltl2tgba '!b & e U (a & b & c)' | grep '\[f\]' && exit 1
+ltl2tgba '!b & e U (a & b & c)' --stats=%w | grep 0 && exit 1
+ltl2tgba 'X!c & X(b & c & d & a U e)' | grep '\[f\]' && exit 1
+ltl2tgba 'X!c & X(b & c & d & a U e)' --stats=%w | grep 0 && exit 1
 :