From 26cf0145b723e084b3eb2d78e266f22ac9ca5323 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz
Date: Mon, 2 Feb 2004 19:29:56 +0000
Subject: [PATCH] * wrap/python/cgi/ltl2tgba.in (print_stats): New function.
Call it to display the size of the generalized and degeneralized automata.
---
ChangeLog | 6 ++++++
wrap/python/cgi/ltl2tgba.in | 20 +++++++++++++++++++-
2 files changed, 25 insertions(+), 1 deletion(-)
diff --git a/ChangeLog b/ChangeLog
index dcba7a52a..33500bd09 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,9 @@
+2004-02-02 Alexandre Duret-Lutz
+
+ * wrap/python/cgi/ltl2tgba.in (print_stats): New function. Call
+ it to display the size of the generalized and degeneralized
+ automata.
+
2004-02-02 Alexandre Duret-Lutz
* src/tgbalagos/stats.hh, src/tgbalagos/stats.cc: New files.
diff --git a/wrap/python/cgi/ltl2tgba.in b/wrap/python/cgi/ltl2tgba.in
index c5512426a..67e72f06f 100644
--- a/wrap/python/cgi/ltl2tgba.in
+++ b/wrap/python/cgi/ltl2tgba.in
@@ -1,6 +1,6 @@
#!@PYTHON@
# -*- python -*-
-# 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.
#
@@ -56,6 +56,21 @@ def escaped_print_set(dict, what):
del s
print ''; sys.stdout.flush()
+def print_stats(automaton):
+ stats = spot.stats_reachable(automaton)
+ print "", stats.states,
+ if stats.states == 1:
+ print " state,",
+ else:
+ print " states,",
+ print stats.transitions,
+ if stats.transitions == 1:
+ print " transition",
+ else:
+ print " transitions",
+ print "
"
+ sys.stdout.flush()
+
print "Content-Type: text/html"
print
@@ -188,6 +203,8 @@ elif trans_fm:
print 'done.
'
sys.stdout.flush()
+print_stats(automaton)
+
if show_automaton_dot:
print ''; sys.stdout.flush()
s = spot.ostringstream()
@@ -210,6 +227,7 @@ if show_automaton_gif:
if show_degen_dot or show_degen_gif:
print 'Degeneralized automaton
'
degen = spot.tgba_tba_proxy(automaton)
+ print_stats(degen)
if show_degen_dot:
print ''; sys.stdout.flush()
s = spot.ostringstream()