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

* wrap/python/cgi/ltl2tgba.in: Output a description of the syntax.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2004-02-02 23:30:08 +00:00
parent cfcc5e857b
commit 6dc59fa7fa
2 changed files with 84 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

6
ChangeLog
View file

@ -1,4 +1,6 @@
2004-02-02 Alexandre Duret-Lutz <adl@gnu.org> 2004-02-02 Alexandre Duret-Lutz <adl@src.lip6.fr>
* wrap/python/cgi/ltl2tgba.in: Output a description of the syntax.
* wrap/python/cgi/ltl2tgba.in: Import spot and redirect stderr * wrap/python/cgi/ltl2tgba.in: Import spot and redirect stderr
to stdout early. to stdout early.
@ -37,8 +39,6 @@
it to display the size of the generalized and degeneralized it to display the size of the generalized and degeneralized
automata. automata.
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.
* src/tgbalagos/Makefile.am: Add them. * src/tgbalagos/Makefile.am: Add them.
* wrap/python/spot.i: Include src/tgbalagos/dupexp.hh and * wrap/python/spot.i: Include src/tgbalagos/dupexp.hh and

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

@ -116,8 +116,9 @@ def render_bdd(basename, dictionary, bdd):
render_dot(basename) render_dot(basename)
print "<TITLE>LTL-to-Büchi test</TITLE>" print "<TITLE>LTL-to-B&uuml;chi test</TITLE>"
print "<H1>Input</H1>" print """<H1><a href="http://spot.lip6.fr/">Spot</a>'s on-line
LTL-to-B&uuml;chi translator</H1>"""
formula = form.getfirst('formula', '') formula = form.getfirst('formula', '')
@ -130,12 +131,18 @@ options = [
('show_degen_dot', 'print degeneralized Büchi automaton as .dot', 0), ('show_degen_dot', 'print degeneralized Büchi automaton as .dot', 0),
('show_degen_gif', 'draw degeneralized Büchi automaton', 0), ('show_degen_gif', 'draw degeneralized Büchi automaton', 0),
('show_dictionnay', 'print BDD dictionary', 0), ('show_dictionnay', 'print BDD dictionary', 0),
('show_relation_dot', 'print the transition relation as .dot', 0), ('show_relation_dot',
('show_relation_set', 'print the transition relation as a BDD set', 0), 'print the transition relation as .dot (LaCIM only)', 0),
('show_relation_gif', 'draw the transition relation', 0), ('show_relation_set',
('show_acceptance_dot', 'print the acceptance relation as .dot' , 0), 'print the transition relation as a BDD set (LaCIM only)', 0),
('show_acceptance_set', 'print the acceptance relation as a BDD set', 0), ('show_relation_gif',
('show_acceptance_gif', 'draw the acceptance relation', 0), '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), ('show_lbtt', 'convert automaton for LBTT', 0),
] ]
@ -146,8 +153,72 @@ translators = [
] ]
print """<FORM action="%s" method="post"><P> print """<FORM action="%s" method="post"><P>
Formula to translate: <INPUT type="text" name="formula" value="%s"><BR> Formula to translate:
Translator:<TABLE><TR><TD>""" % (myself, formula) <INPUT size=50 type="text" name="formula" value="%s"><BR>
<p>Use alphanumeric identifiers or double-quoted strings for atomic
propositions, and parentheses for grouping.<BR>Identifiers cannot
start with the letter of a prefix operator (<code>F</code>,
<code>G</code>, or <code>X</code>): for instance <code>GFa</code>
means <code>G(F(a))</code>. Use <code>"GFa"</code> if you really want
to refer to <code>GFa</code> as a proposition.<br>Conversly, infix
letter operators are not assumed to be operators if they are part of
an indentifier: <code>aUb</code> is an atomic proposition, unlike
<code>a&nbsp;U&nbsp;b</code> and <code>(a)U(b)</code><br>
<table border="1" rules="groups" frame="border" cellpadding="2">
<colgroup span=2>
<colgroup span=2>
<colgroup span=2>
<colgroup span=2>
<thead>
<tr>
<th colspan=2>Unary operators<br>(prefix)</th>
<th colspan=4>Binary operators<br>(infix)</th>
<th colspan=2>Constants</th>
</tr>
</thead>
<tbody>
<tr>
<td align="right">not:</td><td><code>!</code></td>
<td align="right">and:</td><td><code>&</code> <code>&&</code>
<code>.</code> <code>*</code>
<code>/\</code></td>
<td align="right">xor:</td><td><code>^</code> <code>xor</code></td>
<td align="right">true:</td><td><code>1</code>
<code>true</code></td>
</tr>
<tr>
<td align="right">eventually:</td><td><code>F</code>
<code>&lt;&gt;</code></td>
<td align="right">or:</td><td><code>|</code> <code>||</code>
<code>+</code> <code>\/</code></td>
<td align="right">until:</td><td><code>U</code></td>
<td align="right">false:</td><td><code>0</code>
<code>false</code></td>
</tr>
<tr>
<td align="right">always:</td><td><code>G</code>
<code>[]</code></td>
<td align="right">implies:</td><td><code>-&gt;</code>
<code>=&gt;</code></td>
<td align="right">release:</td><td><code>R</code>
<code>V</code></td>
<td></td><td></td>
</tr>
<tr>
<td align="right">next:</td><td><code>X</code> <code>()</code></td>
<td align="right">equivalent:</td><td><code>&lt;-&gt;
</code> <code>&lt;=&gt;
</code></td>
<td></td><td></td>
<td></td><td></td>
</tr>
</tbody>
</table></p>
Translator:<TABLE><TR><TD>""" % (myself, cgi.escape(formula, True))
trans = form.getfirst("trans", default_translator) trans = form.getfirst("trans", default_translator)