From 0c3d4fef9f53ecf1d9682f57fb49d62d96c58b23 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 21 Apr 2004 19:02:31 +0000
Subject: [PATCH] * wrap/python/spot.i: Process tgbaalgos/neverclaim.hh. *
 wrap/python/cgi/ltl2tgba.in: Display the never claim on demand.

---
 ChangeLog                   |  5 +++++
 wrap/python/cgi/ltl2tgba.in | 18 ++++++++++++++----
 wrap/python/spot.i          |  2 ++
 3 files changed, 21 insertions(+), 4 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 5b235e005..38d101a4c 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,8 @@
+2004-04-21  Alexandre Duret-Lutz  <adl@gnu.org>
+
+	* wrap/python/spot.i: Process tgbaalgos/neverclaim.hh.
+	* wrap/python/cgi/ltl2tgba.in: Display the never claim on demand.
+
 2004-04-21  Denis Poitrenaud  <dp@src.lip6.fr>
 
 	* src/ltlvisit/tostring.hh (to_spin_string): New function.
diff --git a/wrap/python/cgi/ltl2tgba.in b/wrap/python/cgi/ltl2tgba.in
index 7ee0eccee..31b2b22cb 100644
--- a/wrap/python/cgi/ltl2tgba.in
+++ b/wrap/python/cgi/ltl2tgba.in
@@ -199,6 +199,7 @@ options = [(
     ('show_formula_png',    'draw the formula',                            0),
     ('show_automaton_png',  'draw Büchi automaton',                        1),
     ('show_degen_png',      'draw degeneralized Büchi automaton',          0),
+    ('show_never_claim',    'output Spin never claim',                     0),
     ('show_lbtt',           'convert automaton for LBTT',                  0),
     ]), (
     'Debugging options', 0, '', [
@@ -411,14 +412,23 @@ dont_run_dot = print_stats(automaton)
 if show_automaton_png:
     render_automaton(imgprefix + '-a', automaton, dont_run_dot)
 
-if show_degen_png:
-    print '<H3>Degeneralized automaton</H3>'
+if show_degen_png or show_never_claim:
     degen = spot.tgba_tba_proxy(automaton)
-    dont_run_dot = print_stats(degen)
-    render_automaton(imgprefix + '-d', degen, dont_run_dot)
 else:
     degen = 0
 
+if show_degen_png:
+    print '<H3>Degeneralized automaton</H3>'
+    dont_run_dot = print_stats(degen)
+    render_automaton(imgprefix + '-d', degen, dont_run_dot)
+
+if show_never_claim:
+    print '<H3>Never claim (for degeneralized automaton)</H3>'
+    print '<PRE>'
+    spot.never_claim_reachable(spot.get_cout(), degen)
+    print '</PRE>'
+    sys.stdout.flush()
+
 if show_dictionnay:
     print '<H3>BDD dictionary</H3>'
     print '<pre>'
diff --git a/wrap/python/spot.i b/wrap/python/spot.i
index 1864a9ac0..1db599025 100644
--- a/wrap/python/spot.i
+++ b/wrap/python/spot.i
@@ -78,6 +78,7 @@
 #include "tgbaalgos/dupexp.hh"
 #include "tgbaalgos/lbtt.hh"
 #include "tgbaalgos/magic.hh"
+#include "tgbaalgos/neverclaim.hh"
 #include "tgbaalgos/save.hh"
 #include "tgbaalgos/stats.hh"
 
@@ -141,6 +142,7 @@ using namespace spot;
 %include "tgbaalgos/dupexp.hh"
 %include "tgbaalgos/lbtt.hh"
 %include "tgbaalgos/magic.hh"
+%include "tgbaalgos/neverclaim.hh"
 %include "tgbaalgos/save.hh"
 %include "tgbaalgos/stats.hh"
 #undef ltl