diff --git a/ChangeLog b/ChangeLog index db211db3c..adf6e4c49 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,4 +1,6 @@ -2004-02-02 Alexandre Duret-Lutz +2004-02-02 Alexandre Duret-Lutz + + * wrap/python/cgi/ltl2tgba.in: Output a description of the syntax. * wrap/python/cgi/ltl2tgba.in: Import spot and redirect stderr to stdout early. @@ -37,8 +39,6 @@ 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. * src/tgbalagos/Makefile.am: Add them. * wrap/python/spot.i: Include src/tgbalagos/dupexp.hh and diff --git a/wrap/python/cgi/ltl2tgba.in b/wrap/python/cgi/ltl2tgba.in index f51e49bb4..db1f093b6 100644 --- a/wrap/python/cgi/ltl2tgba.in +++ b/wrap/python/cgi/ltl2tgba.in @@ -116,8 +116,9 @@ def render_bdd(basename, dictionary, bdd): render_dot(basename) -print "LTL-to-Büchi test" -print "

Input

" +print "LTL-to-Büchi test" +print """

Spot's on-line +LTL-to-Büchi translator

""" formula = form.getfirst('formula', '') @@ -130,12 +131,18 @@ options = [ ('show_degen_dot', 'print degeneralized Büchi automaton as .dot', 0), ('show_degen_gif', 'draw degeneralized Büchi automaton', 0), ('show_dictionnay', 'print BDD dictionary', 0), - ('show_relation_dot', 'print the transition relation as .dot', 0), - ('show_relation_set', 'print the transition relation as a BDD set', 0), - ('show_relation_gif', 'draw the transition relation', 0), - ('show_acceptance_dot', 'print the acceptance relation as .dot' , 0), - ('show_acceptance_set', 'print the acceptance relation as a BDD set', 0), - ('show_acceptance_gif', 'draw the acceptance relation', 0), + ('show_relation_dot', + 'print the transition relation as .dot (LaCIM only)', 0), + ('show_relation_set', + 'print the transition relation as a BDD set (LaCIM only)', 0), + ('show_relation_gif', + 'draw the transition relation (LaCIM only)', 0), + ('show_acceptance_dot', + 'print the acceptance relation as .dot (LaCIM only)' , 0), + ('show_acceptance_set', + 'print the acceptance relation as a BDD set (LaCIM only)', 0), + ('show_acceptance_gif', + 'draw the acceptance relation (LaCIM only)', 0), ('show_lbtt', 'convert automaton for LBTT', 0), ] @@ -146,8 +153,72 @@ translators = [ ] print """

-Formula to translate:
-Translator:
""" % (myself, formula) +Formula to translate: +
+ +

Use alphanumeric identifiers or double-quoted strings for atomic +propositions, and parentheses for grouping.
Identifiers cannot +start with the letter of a prefix operator (F, +G, or X): for instance GFa +means G(F(a)). Use "GFa" if you really want +to refer to GFa as a proposition.
Conversly, infix +letter operators are not assumed to be operators if they are part of +an indentifier: aUb is an atomic proposition, unlike +a U b and (a)U(b)
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Unary operators
(prefix)		Binary operators
(infix)		Constants
not:!and:& && + . * + /\xor:^ xortrue:1 + true
eventually:F + <>or:| || + + \/until:Ufalse:0 + false
always:G + []implies:-> + =>release:R + V
next:X ()equivalent:<-> + <=> +

+Translator:
""" % (myself, cgi.escape(formula, True)) trans = form.getfirst("trans", default_translator)