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

* wrap/python/cgi/ltl2tgba.in: Color translators and their options.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2004-02-20 22:51:13 +00:00
parent 153962aa9d
commit ab26065f4c
2 changed files with 36 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2004-02-21 Alexandre Duret-Lutz <adl@src.lip6.fr>
* wrap/python/cgi/ltl2tgba.in: Color translators and their options.
2004-02-20 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-02-20 Alexandre Duret-Lutz <adl@src.lip6.fr>
* wrap/python/cgi/ltl2tgba.in: Present the options in a table. * wrap/python/cgi/ltl2tgba.in: Present the options in a table.

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

@ -38,12 +38,17 @@ sys.path.insert(0, '@pythondir@')
# Directory for temporary files (images and other auxiliary files). # Directory for temporary files (images and other auxiliary files).
imgdir = 'spotimg' imgdir = 'spotimg'
# Extra HTML headers.
extra_header = ''
# extra_header = '<LINK REL="stylesheet" TYPE="text/css" HREF="style.css">'
import spot import spot
import buddy import buddy
def print_footer(): def print_footer():
print '<hr>' print '<hr>'
print 'ltl2tgba.py @PACKAGE_VERSION@; Spot', spot.version() print 'ltl2tgba.py @PACKAGE_VERSION@; Spot', spot.version()
print '</BODY></HTML>'
# We want the script to kill itself whenever it run for more than 30 # We want the script to kill itself whenever it run for more than 30
# seconds. `dot' can be very long at drawing huge graphs, and may # seconds. `dot' can be very long at drawing huge graphs, and may
@ -161,31 +166,39 @@ def render_bdd(basename, dictionary, bdd):
render_dot(basename) render_dot(basename)
print "<TITLE>LTL-to-B&uuml;chi test</TITLE>" print """
print """<H1><a href="http://spot.lip6.fr/">Spot</a>'s on-line <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
LTL-to-B&uuml;chi translator</H1>""" <HTML lang="en"><HEAD>
<TITLE>Spot's on-line LTL-to-Buchi translator</TITLE>
<META NAME="keywords" CONTENT="Spot,LTL,automata,B&uuml;chi,translation,TGBA">
%s</HEAD>
<BODY>
<H1><a href="http://spot.lip6.fr/">Spot</a>'s on-line
LTL-to-B&uuml;chi translator</H1>""" % extra_header
formula = form.getfirst('formula', '') formula = form.getfirst('formula', '')
#F8F0E8
color_fm = '#E0D8E0'
color_lacim = "#F8D8E8"
options = [( options = [(
'Common options', 0, [ 'Common options', 0, '', [
('show_formula_png', 'draw the formula', 0), ('show_formula_png', 'draw the formula', 0),
('show_automaton_png', 'draw Büchi automaton', 1), ('show_automaton_png', 'draw Büchi automaton', 1),
('show_degen_png', 'draw degeneralized Büchi automaton', 0), ('show_degen_png', 'draw degeneralized Büchi automaton', 0),
('show_lbtt', 'convert automaton for LBTT', 0), ('show_lbtt', 'convert automaton for LBTT', 0),
]), ( ]), (
'Debugging options', 0, [ 'Debugging options', 0, '', [
('show_parse', 'show traces during parsing', 0), ('show_parse', 'show traces during parsing', 0),
('show_dictionnay', 'print BDD dictionary', 0), ('show_dictionnay', 'print BDD dictionary', 0),
]), ( ]), (
'Couvreur/FM options', 1, [ 'Couvreur/FM options', 1, color_fm, [
('opt_exprop', 'optimize determinism', 1), ('opt_exprop', 'optimize determinism', 1),
('opt_symb_merge', ('opt_symb_merge',
'merge states with same symbolic successor representation', 1), 'merge states with same symbolic successor representation', 1),
]), ( ]), (
'Couvreur/Lacim options', 1, [ 'Couvreur/LaCIM options', 1, color_lacim, [
('show_relation_set', ('show_relation_set',
'print the transition relation as a BDD set', 0), 'print the transition relation as a BDD set', 0),
('show_relation_png', ('show_relation_png',
@ -198,8 +211,8 @@ options = [(
default_translator = 'trans_fm'; default_translator = 'trans_fm';
translators = [ translators = [
('trans_fm', 'Convreur/FM'), ('trans_fm', 'Couvreur/FM', color_fm),
('trans_lacim', 'Convreur/LaCIM'), ('trans_lacim', 'Couvreur/LaCIM', color_lacim),
] ]
print ("""<FORM action="%s" method="post"><P> print ("""<FORM action="%s" method="post"><P>
@ -276,19 +289,21 @@ column = [[], []]
column[0].append("<TH>Algorithm</TH>") column[0].append("<TH>Algorithm</TH>")
trans = form.getfirst("trans", default_translator) trans = form.getfirst("trans", default_translator)
for opt, desc, in translators: for opt, desc, color in translators:
if trans == opt: if trans == opt:
str = "checked" str = "checked"
else: else:
str = "" str = ""
globals()[opt] = str globals()[opt] = str
s = '<TD><INPUT type="radio" name="trans" value="%s" %s>%s</TD>' s = '<TD bgcolor=%s><INPUT type="radio" name="trans" value="%s" %s>%s</TD>'
column[0].append(s % (opt, str, desc)) column[0].append(s % (color, opt, str, desc))
print """</TD></TR></TABLE><TABLE>""" print """</TD></TR></TABLE><TABLE>"""
for opt_group, opt_column, opt_list in options: for opt_group, opt_column, opt_color, opt_list in options:
column[opt_column].append("<TH>" + opt_group + "</TH>") if opt_color:
opt_color = ' bgcolor="%s"' % opt_color
column[opt_column].append(("<TH%s>" % opt_color) + opt_group + "</TH>")
for opt, desc, arg, in opt_list: for opt, desc, arg, in opt_list:
if formula: if formula:
val = int(form.getfirst(opt, 0)) val = int(form.getfirst(opt, 0))
@ -299,8 +314,8 @@ for opt_group, opt_column, opt_list in options:
else: else:
str = "" str = ""
globals()[opt] = val globals()[opt] = val
s = '<TD><INPUT type="checkbox" name="%s" value="1"%s>%s</TD>' s = '<TD%s><INPUT type="checkbox" name="%s" value="1"%s>%s</TD>'
column[opt_column].append(s % (opt, str, desc)) column[opt_column].append(s % (opt_color, opt, str, desc))
print '<TABLE>' print '<TABLE>'
width = range(len(column)) width = range(len(column))