From 74f14567d11f9fe91cc64836138693c3b5ddb494 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 7 Jan 2011 23:21:04 +0100
Subject: [PATCH] Fix usage of minimize_obligation in the CGI script.

* wrap/python/cgi-bin/ltl2tgba.py (reduce_wdba): Use
minimize_obligation_new a pass the formula.
* wrap/python/spot.i (minimize_obligation_new): New function, to
cope with the strange specification of spot::minimize_obligation()
not always creating a new automaton.
---
 ChangeLog                       | 10 ++++++++++
 wrap/python/cgi-bin/ltl2tgba.in |  5 ++++-
 wrap/python/spot.i              | 16 +++++++++++++++-
 3 files changed, 29 insertions(+), 2 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 3bb154397..6e0295226 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,13 @@
+2011-01-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Fix usage of minimize_obligation in the CGI script.
+
+	* wrap/python/cgi-bin/ltl2tgba.py (reduce_wdba): Use
+	minimize_obligation_new a pass the formula.
+	* wrap/python/spot.i (minimize_obligation_new): New function, to
+	cope with the strange specification of spot::minimize_obligation()
+	not always creating a new automaton.
+
 2011-01-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* NEWS: Convert to utf-8 and fix a few typos.
diff --git a/wrap/python/cgi-bin/ltl2tgba.in b/wrap/python/cgi-bin/ltl2tgba.in
index 7241623ca..173665cc6 100755
--- a/wrap/python/cgi-bin/ltl2tgba.in
+++ b/wrap/python/cgi-bin/ltl2tgba.in
@@ -574,7 +574,10 @@ elif trans_taa:
 if reduce_dmonitor:
     automaton = spot.minimize_monitor(automaton)
 elif reduce_wdba:
-    automaton = spot.minimize_obligation(automaton)
+    minimized = spot.minimize_obligation_new(automaton, f)
+    if minimized:
+        automaton = minimized
+        minimized = 0
 elif reduce_scc:
     # Do not suppress all useless acceptance conditions if
     # degeneralization is requested: keeping those that lead to
diff --git a/wrap/python/spot.i b/wrap/python/spot.i
index 20d674506..5d44707e9 100644
--- a/wrap/python/spot.i
+++ b/wrap/python/spot.i
@@ -149,7 +149,6 @@ using namespace spot;
 %feature("new") spot::ltl_to_tgba_lacim;
 %feature("new") spot::minimize_wdba;
 %feature("new") spot::minimize_monitor;
-%feature("new") spot::minimize_obligation;
 %feature("new") spot::reduc_tgba_sim;
 %feature("new") spot::scc_filter;
 %feature("new") spot::tgba_dupexp_bfs;
@@ -229,8 +228,23 @@ namespace std {
   };
 }
 
+%feature("new") minimize_obligation_new;
+
 %inline %{
 
+// A variant of minimize_obligation() that always return a new object.
+const spot::tgba*
+minimize_obligation_new(const spot::tgba* a, const spot::ltl::formula* f)
+{
+  const tgba* res = spot::minimize_obligation(a, f);
+  // Return 0 if the output is the same as the input, otherwise
+  // it is hard for swig to know if the output is "new" or not.
+  if (res == a)
+    return 0;
+  else
+    return res;
+}
+
 spot::ltl::parse_error_list
 empty_parse_error_list()
 {