From c46204dfadec56f12f1a3676cecb488b68e7c16a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 2 Feb 2004 21:39:25 +0000
Subject: [PATCH] * src/misc/bddalloc.hh: Make all methods public. *
 wrap/python/spot.i: Include misc/bddalloc.hh and misc/minato.hh. *
 wrap/python/tests/minato.py: New file. * wrap/python/tests/Makefile.am
 (TESTS): Add minato.py.

---
 ChangeLog                     |  5 ++++
 src/misc/bddalloc.hh          |  6 ++---
 wrap/python/spot.i            |  4 +++
 wrap/python/tests/Makefile.am |  5 ++--
 wrap/python/tests/minato.py   | 48 +++++++++++++++++++++++++++++++++++
 5 files changed, 63 insertions(+), 5 deletions(-)
 create mode 100755 wrap/python/tests/minato.py

diff --git a/ChangeLog b/ChangeLog
index 83ccba305..a8224a9c9 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,10 @@
 2004-02-02  Alexandre Duret-Lutz  <adl@gnu.org>
 
+	* src/misc/bddalloc.hh: Make all methods public.
+	* wrap/python/spot.i: Include misc/bddalloc.hh and misc/minato.hh.
+	* wrap/python/tests/minato.py: New file.
+	* wrap/python/tests/Makefile.am (TESTS): Add minato.py.
+
 	* src/tgbatest/explicit.cc, src/tgbatest/explprod.cc,
 	src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
 	src/tgbatest/mixprod.cc, src/tgbatest/powerset.cc,
diff --git a/src/misc/bddalloc.hh b/src/misc/bddalloc.hh
index aae3db2b1..7e4500591 100644
--- a/src/misc/bddalloc.hh
+++ b/src/misc/bddalloc.hh
@@ -1,4 +1,4 @@
-// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -31,7 +31,7 @@ namespace spot
   /// Manage ranges of variables.
   class bdd_allocator
   {
-  protected:
+  public:
     /// Default constructor.
     bdd_allocator();
     /// Initialize the BDD library.
@@ -40,7 +40,7 @@ namespace spot
     int allocate_variables(int n);
     /// Release \a n BDD variables starting at \a base.
     void release_variables(int base, int n);
-
+  protected:
     static bool initialized; ///< Whether the BDD library has been initialized.
     static int varnum; ///< number of variables in use in the BDD library.
     int lvarnum; ///< number of variables in use in this allocator.
diff --git a/wrap/python/spot.i b/wrap/python/spot.i
index adbe3c73c..575f7b8f1 100644
--- a/wrap/python/spot.i
+++ b/wrap/python/spot.i
@@ -32,6 +32,8 @@
 #include <sstream>
 
 #include "misc/version.hh"
+#include "misc/bddalloc.hh"
+#include "misc/minato.hh"
 
 #include "ltlast/formula.hh"
 #include "ltlast/refformula.hh"
@@ -83,6 +85,8 @@ using namespace spot;
 %}
 
 %include "misc/version.hh"
+%include "misc/bddalloc.hh"
+%include "misc/minato.hh"
 
 %include "ltlast/formula.hh"
 %include "ltlast/refformula.hh"
diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am
index 5a71e5aee..09754ae0c 100644
--- a/wrap/python/tests/Makefile.am
+++ b/wrap/python/tests/Makefile.am
@@ -1,4 +1,4 @@
-## Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+## Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 ## département Systèmes Répartis Coopératifs (SRC), Université Pierre
 ## et Marie Curie.
 ##
@@ -32,4 +32,5 @@ TESTS = \
   ltlparse.py \
   bddnqueen.py \
   ltl2tgba.test \
-  interdep.py
+  interdep.py \
+  minato.py
diff --git a/wrap/python/tests/minato.py b/wrap/python/tests/minato.py
new file mode 100755
index 000000000..41705a1cc
--- /dev/null
+++ b/wrap/python/tests/minato.py
@@ -0,0 +1,48 @@
+# -*- mode: python; coding: iso-8859-1 -*-
+# Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# et Marie Curie.
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+import ltihooks
+import spot
+import buddy
+import sys
+
+alloc = spot.bdd_allocator()
+
+alloc.allocate_variables(3)
+
+a = buddy.bdd_ithvar(0)
+b = buddy.bdd_ithvar(1)
+c = buddy.bdd_ithvar(2)
+
+w = -a & -b | -c & b | a & -b
+
+isop = spot.minato_isop(w)
+
+i = isop.next()
+l = []
+while i != buddy.bddfalse:
+    buddy.bdd_printset(i)
+    print
+    l.append(i)
+    i = isop.next()
+
+sys.exit(l == [-a, -c])