From 649793df751d3b3de44bfabf31405d516d4734ff Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 27 Apr 2017 18:00:51 +0200
Subject: [PATCH] gen: pass the bdd_dict to aut_pattern()

* spot/gen/automata.hh (aut_pattern): Add the dict argument.
* spot/gen/automata.cc, python/spot/gen.i: Adjust.
* tests/python/gen.py: Make sure two automata built without
specifying any dictionary share the same one.
---
 python/spot/gen.i    | 10 ++++++++++
 spot/gen/automata.cc |  7 +++----
 spot/gen/automata.hh |  9 ++++++++-
 tests/python/gen.py  |  3 +++
 4 files changed, 24 insertions(+), 5 deletions(-)

diff --git a/python/spot/gen.i b/python/spot/gen.i
index f64874f76..b2fa5057f 100644
--- a/python/spot/gen.i
+++ b/python/spot/gen.i
@@ -30,6 +30,7 @@
 %include "std_shared_ptr.i"
 
 %shared_ptr(spot::twa_graph)
+%shared_ptr(spot::bdd_dict)
 
 %{
 #include <spot/gen/automata.hh>
@@ -40,6 +41,7 @@ using namespace spot;
 %import(module="spot.impl") <spot/misc/common.hh>
 %import(module="spot.impl") <spot/tl/formula.hh>
 %import(module="spot.impl") <spot/twa/fwd.hh>
+%import(module="spot.impl") <spot/twa/bdddict.hh>
 
 %exception {
   try {
@@ -86,6 +88,14 @@ def ltl_patterns(*args):
     for n in range(min, max + 1):
       yield ltl_pattern(pat, n)
 
+
+# Override aut_pattern now(), because %feature("shadow") does not
+# seem to work correctly.  See https://github.com/swig/swig/issues/980
+def aut_pattern(pattern: 'spot::gen::aut_pattern_id', n: 'int',
+                dict: 'spot::bdd_dict_ptr' = None) -> "spot::twa_graph_ptr":
+  return _gen.aut_pattern(pattern, n, dict or spot._bdd_dict)
+
+
 def aut_patterns(*args):
   """
   Generate automata patterns.
diff --git a/spot/gen/automata.cc b/spot/gen/automata.cc
index 67374bce6..dee729b4d 100644
--- a/spot/gen/automata.cc
+++ b/spot/gen/automata.cc
@@ -28,7 +28,7 @@ namespace spot
     namespace
     {
       static twa_graph_ptr
-      ks_cobuchi(unsigned n)
+      ks_cobuchi(unsigned n, bdd_dict_ptr dict)
       {
         if (n == 0)
           throw std::runtime_error("ks_cobuchi expects a positive argument");
@@ -45,7 +45,6 @@ namespace spot
         // the automaton has 2n+1 states, numbered from 0 to 2n
         // 0 is the initial state and the only non-deterministic state
 
-        auto dict = make_bdd_dict();
         auto aut = make_twa_graph(dict);
 
         // register aps
@@ -91,7 +90,7 @@ namespace spot
       }
     }
 
-    twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n)
+    twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n, bdd_dict_ptr dict)
     {
       if (n < 0)
         {
@@ -105,7 +104,7 @@ namespace spot
         {
           // Keep this alphabetically-ordered!
         case AUT_KS_COBUCHI:
-          return ks_cobuchi(n);
+          return ks_cobuchi(n, dict);
         case AUT_END:
           break;
         }
diff --git a/spot/gen/automata.hh b/spot/gen/automata.hh
index 9da6d0a5b..182906968 100644
--- a/spot/gen/automata.hh
+++ b/spot/gen/automata.hh
@@ -21,6 +21,7 @@
 
 #include <spot/misc/common.hh>
 #include <spot/twa/fwd.hh>
+#include <spot/twa/bdddict.hh>
 
 namespace spot
 {
@@ -55,7 +56,13 @@ namespace spot
     /// The pattern is specified using one value from the aut_pattern_id
     /// enum.  See the man page of the `genaut` binary for a
     /// description of those patterns, and bibliographic references.
-    SPOT_API twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n);
+    ///
+    /// In case you want to combine this automaton with other
+    /// automata, pass the bdd_dict to use to make sure that all share
+    /// the same.
+    SPOT_API twa_graph_ptr
+    aut_pattern(aut_pattern_id pattern, int n,
+                spot::bdd_dict_ptr dict = make_bdd_dict());
 
     /// \brief convert an aut_pattern_it value into a name
     ///
diff --git a/tests/python/gen.py b/tests/python/gen.py
index 3fc1d7cf4..2b74f3ec3 100644
--- a/tests/python/gen.py
+++ b/tests/python/gen.py
@@ -31,6 +31,9 @@ assert k2.num_states() == 5
 # the type returned by spot.gen.ks_cobuchi() is the correct one.
 assert 'to_str' in dir(k2)
 
+k3 = gen.aut_pattern(gen.AUT_KS_COBUCHI, 3)
+assert k2.get_dict() == k3.get_dict()
+
 try:
     gen.aut_pattern(gen.AUT_KS_COBUCHI, 0)
 except RuntimeError as e: