From bd69b16e464cde51950ac2ad84a464e0c2b52e3d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 23 Jun 2004 08:28:50 +0000
Subject: [PATCH] * wrap/python/cgi/ltl2tgba.in: Add "Formula Simplications"
 options. * wrap/python/spot.i: Wrap src/ltlvisite/reduce.hh.

---
 ChangeLog                   |  3 +++
 wrap/python/cgi/ltl2tgba.in | 27 +++++++++++++++++++++++++++
 wrap/python/spot.i          |  2 ++
 3 files changed, 32 insertions(+)

diff --git a/ChangeLog b/ChangeLog
index 9a30531e2..d8c858556 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,8 @@
 2004-06-23  Alexandre Duret-Lutz  <adl@gnu.org>
 
+	* wrap/python/cgi/ltl2tgba.in: Add "Formula Simplications" options.
+	* wrap/python/spot.i: Wrap src/ltlvisite/reduce.hh.
+
 	* src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh: New files,
 	extracted from ...
 	* src/ltlvisit/lunabbrev.cc: ... this one, which now work as documented
diff --git a/wrap/python/cgi/ltl2tgba.in b/wrap/python/cgi/ltl2tgba.in
index 0d9f31823..7544130a8 100644
--- a/wrap/python/cgi/ltl2tgba.in
+++ b/wrap/python/cgi/ltl2tgba.in
@@ -203,6 +203,11 @@ options_common = [
     ('show_never_claim',    'output Spin never claim',                     0),
     ('show_lbtt',           'convert automaton for LBTT',                  0),
     ]
+options_reduce = [
+    ('reduce_basics',       'basic rewritings',                            1),
+    ('reduce_syntimpl',     'syntactic implication',                       1),
+    ('reduce_eventuniv',    'eventuality and universality',                1),
+    ]
 options_debug = [
     ('show_parse',          'show traces during parsing',                  0),
     ('show_dictionnary',    'print BDD dictionary',                        0),
@@ -339,6 +344,7 @@ for opt, desc, color in translators:
     add_options('', 0, color, globals()['options_' + opt])
 
 add_options("Common Options", 1, '', options_common)
+add_options("Formula Simplications", 1, '', options_reduce)
 add_options("Debugging Options", 1, '', options_debug)
 
 print '<TABLE>'
@@ -351,6 +357,8 @@ for d in range(depth):
     for i in width:
         if d < len(column[i]):
             print column[i][d]
+        else:
+            print '<TD></TD>'
     print '</TR>'
 print '</TABLE>'
 
@@ -394,6 +402,25 @@ if show_formula_png:
     del outfile
     render_dot(imgprefix + '-f')
 
+opt = spot.Reduce_None
+if reduce_basics:
+    opt = opt + spot.Reduce_Basics
+if reduce_syntimpl:
+    opt = opt + spot.Reduce_Syntactic_Implications
+if reduce_eventuniv:
+    opt = opt + spot.Reduce_Eventuality_And_Universality
+if opt != spot.Reduce_None:
+    f2 = spot.reduce(f, opt)
+    spot.destroy(f)
+    f = f2
+    print "<p>Reduced formula is<code>", f, "</code></p>"
+
+    if show_formula_png:
+        outfile = spot.ofstream(imgprefix + '-f2.txt')
+        spot.dotty(outfile, f)
+        del outfile
+        render_dot(imgprefix + '-f2')
+
 print '<H2>Automaton</H2>'
 
 dict = spot.bdd_dict()
diff --git a/wrap/python/spot.i b/wrap/python/spot.i
index 1db599025..7e42cc47f 100644
--- a/wrap/python/spot.i
+++ b/wrap/python/spot.i
@@ -56,6 +56,7 @@
 #include "ltlvisit/dump.hh"
 #include "ltlvisit/lunabbrev.hh"
 #include "ltlvisit/nenoform.hh"
+#include "ltlvisit/reduce.hh"
 #include "ltlvisit/tostring.hh"
 #include "ltlvisit/tunabbrev.hh"
 
@@ -110,6 +111,7 @@ using namespace spot;
 %include "ltlvisit/dump.hh"
 %include "ltlvisit/lunabbrev.hh"
 %include "ltlvisit/nenoform.hh"
+%include "ltlvisit/reduce.hh"
 %include "ltlvisit/tostring.hh"
 %include "ltlvisit/tunabbrev.hh"