relabel_here: make it compatible with relabel_bse

* spot/twaalgos/relabel.cc: Deal with the cases where the substitution
value is a Boolean formula.
* spot/twaalgos/relabel.hh: Improve documentation.
* tests/python/relabel.py: Add more tests.
* python/spot/impl.i: Add bindings for are_isomorphic for the above
test.
* NEWS: Mention the news.

NEWS

@@ -114,15 +114,20 @@ New in spot 2.3.4.dev (not yet released)
   - The function spot::streett_to_generalized_buchi() is now able to
     work on automatons with Streett-like acceptance.
 
-  Python:
-
-  - The 'spot.gen' package exports the functions from libspotgen.
-    See https://spot.lrde.epita.fr/ipynb/gen.html for examples.
+  - spot::relabel_here() was used on automata to rename atomic
+    propositions, it can now replace atomic propositions by Boolean
+    subformula.  This makes it possible to use relabeling maps
+    produced by relabel_bse() on formulas.
 
   - twa_graph::copy_state_names_from() can be used to copy the state
     names from another automaton, honoring "original-states" if
     present.
 
+  Python:
+
+  - The 'spot.gen' package exports the functions from libspotgen.
+    See https://spot.lrde.epita.fr/ipynb/gen.html for examples.
+
   Bugs fixed:
 
   - We have fixed new cases where translating multiple formula in a

python/spot/impl.i

@@ -155,6 +155,7 @@
 #include <spot/twaalgos/dtwasat.hh>
 #include <spot/twaalgos/relabel.hh>
 #include <spot/twaalgos/word.hh>
+#include <spot/twaalgos/are_isomorphic.hh>
 
 #include <spot/parseaut/public.hh>
 
@@ -584,6 +585,7 @@ def state_is_accepting(self, src) -> "bool":
 %include <spot/twaalgos/relabel.hh>
 %include <spot/twaalgos/word.hh>
 %template(list_bdd) std::list<bdd>;
+%include <spot/twaalgos/are_isomorphic.hh>
 
 %pythonprepend spot::twa::dtwa_complement %{
   from warnings import warn

spot/twaalgos/relabel.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
+// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -18,6 +18,7 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #include <spot/twaalgos/relabel.hh>
+#include <spot/twa/formula2bdd.hh>
 
 namespace spot
 {
@@ -29,17 +30,46 @@ namespace spot
     std::vector<int> vars;
     std::set<int> newvars;
     vars.reserve(relmap->size());
+    bool bool_subst = false;
+
     for (auto& p: *relmap)
       {
+        if (!p.first.is(op::ap))
+          throw std::runtime_error
+            ("relabel_here: old labels should be atomic propositions");
+        if (!p.second.is_boolean())
+          throw std::runtime_error
+            ("relabel_here: new labels should be Boolean formulas");
+
         int oldv = aut->register_ap(p.first);
-        int newv = aut->register_ap(p.second);
-        bdd_setpair(pairs, oldv, newv);
         vars.emplace_back(oldv);
-        newvars.insert(newv);
+        if (p.second.is(op::ap))
+          {
+            int newv = aut->register_ap(p.second);
+            newvars.insert(newv);
+            bdd_setpair(pairs, oldv, newv);
+          }
+        else
+          {
+            p.second.traverse([&](const formula& f)
+                              {
+                                if (f.is(op::ap))
+                                  newvars.insert(aut->register_ap(f));
+                                return false;
+                              });
+            bdd newb = formula_to_bdd(p.second, d, aut);
+            bdd_setbddpair(pairs, oldv, newb);
+            bool_subst = true;
+          }
       }
-    for (auto& t: aut->edges())
-      t.cond = bdd_replace(t.cond, pairs);
-    // Erase all the old variable that are not reused in the new set.
+    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);
+
+    // 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
     // p0)
     for (auto v: vars)

spot/twaalgos/relabel.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015 Laboratoire de Recherche et Développement de
+// Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -24,8 +24,13 @@
 
 namespace spot
 {
-  /// replace atomic propositions in an automaton
+  /// \brief replace atomic propositions in an automaton
+  ///
+  /// The relabeling map \a relmap should have keys that are atomic
+  /// propositions, and values that are Boolean formulas.
+  ///
+  /// This function is typically used with maps produced by relabel()
+  /// or relabel_bse().
   SPOT_API void
-  relabel_here(twa_graph_ptr& aut,
-               relabeling_map* relmap);
+  relabel_here(twa_graph_ptr& aut, relabeling_map* relmap);
 }

tests/python/relabel.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015  Laboratoire de Recherche et Développement
+# Copyright (C) 2015, 2017  Laboratoire de Recherche et Développement
 # de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -30,3 +30,24 @@ print(res)
 assert(res == """#define p0 a & b
 #define p1 c
 GFp0 -> (FGp0 & Gp1)""")
+
+
+autg = g.translate()
+spot.relabel_here(autg, m)
+assert str(autg.ap()) == '(a, b, c)'
+assert spot.isomorphism_checker.are_isomorphic(autg, f.translate())
+
+a = spot.formula('a')
+u = spot.formula('a U b')
+m[a] = u
+try:
+    spot.relabel_here(autg, m)
+except RuntimeError as e:
+    assert "new labels" in str(e)
+
+m = spot.relabeling_map()
+m[u] = a
+try:
+    spot.relabel_here(autg, m)
+except RuntimeError as e:
+    assert "old labels" in str(e)