alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* wrap/python/cgi/ltl2tgba.in (print_stats): New function. Call

Browse source 
it to display the size of the generalized and degeneralized
automata.
This commit is contained in:
Alexandre Duret-Lutz 2004-02-02 19:29:56 +00:00
parent 834ce05235
commit 26cf0145b7
2 changed files with 25 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
ChangeLog
View file

@ -1,3 +1,9 @@
2004-02-02 Alexandre Duret-Lutz <adl@gnu.org>
* 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 <adl@src.lip6.fr> 2004-02-02 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbalagos/stats.hh, src/tgbalagos/stats.cc: New files. * src/tgbalagos/stats.hh, src/tgbalagos/stats.cc: New files.

20
wrap/python/cgi/ltl2tgba.in
View file

@ -1,6 +1,6 @@
#!@PYTHON@ #!@PYTHON@
# -*- 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 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie. # et Marie Curie.
# #
@ -56,6 +56,21 @@ def escaped_print_set(dict, what):
del s del s
print '</pre>'; sys.stdout.flush() print '</pre>'; sys.stdout.flush()
def print_stats(automaton):
stats = spot.stats_reachable(automaton)
print "<p>", stats.states,
if stats.states == 1:
print " state,",
else:
print " states,",
print stats.transitions,
if stats.transitions == 1:
print " transition",
else:
print " transitions",
print "</p>"
sys.stdout.flush()
print "Content-Type: text/html" print "Content-Type: text/html"
print print
@ -188,6 +203,8 @@ elif trans_fm:
print 'done.</p>' print 'done.</p>'
sys.stdout.flush() sys.stdout.flush()
print_stats(automaton)
if show_automaton_dot: if show_automaton_dot:
print '<pre>'; sys.stdout.flush() print '<pre>'; sys.stdout.flush()
s = spot.ostringstream() s = spot.ostringstream()
@ -210,6 +227,7 @@ if show_automaton_gif:
if show_degen_dot or show_degen_gif: if show_degen_dot or show_degen_gif:
print '<H3>Degeneralized automaton</H3>' print '<H3>Degeneralized automaton</H3>'
degen = spot.tgba_tba_proxy(automaton) degen = spot.tgba_tba_proxy(automaton)
print_stats(degen)
if show_degen_dot: if show_degen_dot:
print '<pre>'; sys.stdout.flush() print '<pre>'; sys.stdout.flush()
s = spot.ostringstream() s = spot.ostringstream()