From 0745e735bb8bf90610bc297009cd07fa78a51205 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 10 Mar 2022 10:53:18 +0100
Subject: [PATCH] fix typos and make formula_from_bdd more usable in Python

* python/spot/impl.i (formula_from_bdd): Instantiate for twa_graph.
* spot/twa/twa.hh (register_aps_from_dict): Typo in exception.
* tests/python/except.py: More tests for the above.
* tests/python/bdddict.py: Typo in comment.
---
 python/spot/impl.i      |  2 ++
 spot/twa/twa.hh         |  4 ++--
 tests/python/bdddict.py |  4 ++--
 tests/python/except.py  | 36 ++++++++++++++++++++++++++++++++++++
 4 files changed, 42 insertions(+), 4 deletions(-)

diff --git a/python/spot/impl.i b/python/spot/impl.i
index 7132a5cc6..b7f116201 100644
--- a/python/spot/impl.i
+++ b/python/spot/impl.i
@@ -533,6 +533,8 @@ namespace std {
 %include <spot/twa/bdddict.hh>
 %include <spot/twa/bddprint.hh>
 %include <spot/twa/formula2bdd.hh>
+%template(formula_to_bdd) spot::formula_to_bdd<spot::twa_graph>;
+
 %include <spot/twa/fwd.hh>
  /* These operators may raise exceptions, and we do not
     want Swig4 to convert those exceptions to NotImplemented. */
diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh
index cb1e208ec..819a90962 100644
--- a/spot/twa/twa.hh
+++ b/spot/twa/twa.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011, 2013-2021 Laboratoire de Recherche et
+// Copyright (C) 2009, 2011, 2013-2022 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -761,7 +761,7 @@ namespace spot
     void register_aps_from_dict()
     {
       if (!aps_.empty())
-        throw std::runtime_error("register_ap_from_dict() may not be"
+        throw std::runtime_error("register_aps_from_dict() may not be"
                                  " called on an automaton that has already"
                                  " registered some AP");
       auto& m = get_dict()->bdd_map;
diff --git a/tests/python/bdddict.py b/tests/python/bdddict.py
index 0172bd050..b7b442b1f 100644
--- a/tests/python/bdddict.py
+++ b/tests/python/bdddict.py
@@ -17,8 +17,8 @@
 # You should have received a copy of the GNU General Public License
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-# Make sure we can leep track of BDD association in Python using bdd_dict, as
-# discussed in issue #372.
+# Make sure we can keep track of BDD association in Python using bdd_dict, as
+# discussed in (deleted???) issue #372.
 
 # CPython use reference counting, so that automata are destructed
 # when we expect them to be.   However other implementations like
diff --git a/tests/python/except.py b/tests/python/except.py
index 76f17f76c..8674721c9 100644
--- a/tests/python/except.py
+++ b/tests/python/except.py
@@ -295,3 +295,39 @@ except RuntimeError as e:
     se = str(e)
     tc.assertIn("synthesis-outputs", se)
     tc.assertIn("unregistered proposition", se)
+else:
+    report_missing_exception()
+
+
+a = spot.make_twa_graph()
+s = a.new_state()
+b = spot.formula_to_bdd("a & b", a.get_dict(), a)
+a.new_edge(s, s, b, [])
+try:
+    print(a.to_str('hoa'))
+except RuntimeError as e:
+    tc.assertIn("unregistered atomic propositions", str(e))
+else:
+    report_missing_exception()
+
+a.register_aps_from_dict()
+tc.assertEqual(a.to_str('hoa'), """HOA: v1
+States: 1
+Start: 0
+AP: 2 "a" "b"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0
+[0&1] 0
+--END--""")
+
+try:
+    a.register_aps_from_dict()
+except RuntimeError as e:
+    se = str(e)
+    tc.assertIn("register_aps_from_dict", se)
+    tc.assertIn("already registered", se)
+else:
+    report_missing_exception()