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

* wrap/python/cgi/ltl2tgba.in: Print degeneralized statistics

Browse source 
when show_never_claim.  Change the title to LTL-to-TGBA.
This commit is contained in:
Alexandre Duret-Lutz 2004-04-22 10:13:10 +00:00
parent d07e549832
commit 28288e0478
2 changed files with 11 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,3 +1,8 @@
2004-04-22 Alexandre Duret-Lutz <adl@src.lip6.fr>
* wrap/python/cgi/ltl2tgba.in: Print degeneralized statistics
when show_never_claim. Change the title to LTL-to-TGBA.
2004-04-21 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-04-21 Alexandre Duret-Lutz <adl@src.lip6.fr>
* wrap/python/cgi/ltl2tgba.in (print_footer): Make ltl2tgba.py's * wrap/python/cgi/ltl2tgba.in (print_footer): Make ltl2tgba.py's

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

@ -184,12 +184,12 @@ def render_bdd(basename, dictionary, bdd):
print """ print """
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<HTML lang="en"><HEAD> <HTML lang="en"><HEAD>
<TITLE>Spot's on-line LTL-to-Buchi translator</TITLE> <TITLE>Spot's on-line LTL-to-TGBA translator</TITLE>
<META NAME="keywords" CONTENT="Spot,LTL,automata,B&uuml;chi,translation,TGBA"> <META NAME="keywords" CONTENT="Spot,LTL,automata,B&uuml;chi,translation,TGBA">
%s</HEAD> %s</HEAD>
<BODY> <BODY>
<H1><a href="http://spot.lip6.fr/">Spot</a>'s on-line <H1><a href="http://spot.lip6.fr/">Spot</a>'s on-line
LTL-to-B&uuml;chi translator</H1>""" % extra_header LTL-to-TGBA translator</H1>""" % extra_header
formula = form.getfirst('formula', '') formula = form.getfirst('formula', '')
@ -423,15 +423,14 @@ if show_automaton_png:
render_automaton(imgprefix + '-a', automaton, dont_run_dot) render_automaton(imgprefix + '-a', automaton, dont_run_dot)
if show_degen_png or show_never_claim: if show_degen_png or show_never_claim:
print '<H3>Degeneralized automaton</H3>'
degen = spot.tgba_tba_proxy(automaton) degen = spot.tgba_tba_proxy(automaton)
dont_run_dot = print_stats(degen)
if show_degen_png:
render_automaton(imgprefix + '-d', degen, dont_run_dot)
else: else:
degen = 0 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: if show_never_claim:
print '<H3>Never claim (for degeneralized automaton)</H3>' print '<H3>Never claim (for degeneralized automaton)</H3>'
print '<PRE>' print '<PRE>'