#!@PYTHON@
# -*- mode: python; coding: iso-8859-1 -*-
# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie.
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with Spot; see the file COPYING.  If not, write to the Free
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
# 02111-1307, USA.

import sys
import os
import cgi
import cgitb; cgitb.enable()
import signal

print "Content-Type: text/html"
print

# Redirect stderr to stdout.
os.close(sys.stderr.fileno())
os.dup2(sys.stdout.fileno(), sys.stderr.fileno())

sys.path.insert(0, '@pythondir@')
# Directory for temporary files (images and other auxiliary files).
imgdir = 'spotimg'

import spot
import buddy

def print_footer():
    print '<hr>'
    print 'ltl2tgba.py @PACKAGE_VERSION@; Spot', spot.version()

# 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
# bring a web server to its knees.  Doing so also protects us from any
# infinite loop in Spot.
#
# We use alarm(30) because 30 seconds ought to be enough for everyone.
# We create a process group for the script and its children (dot).
# Upon SIGALRM, we kill the whole process group.
#
# For all this to work, SIGALRM and SIGTERM must not be blocked.
# Apache (at least in my tests with version 2.0.48) blocks them by
# default.  I haven't figured a Python way to unblock them, so the
# spot bindings supply unblock_signal(signum) for this purpose.

def alarm_handler(signum, frame):
    print """<p><font color="red">The script was aborted because
it has been running for too long.</font>  Please try a shorter formula,
or different options (not drawing automata usually helps).
If you want to benchmark big formulae it is
better to install Spot on your own computer.</p>"""
    print_footer()
    sys.stdout.flush()
    os.kill(0, signal.SIGTERM)

def reset_alarm():
    signal.alarm(30)

spot.unblock_signal(signal.SIGALRM)
spot.unblock_signal(signal.SIGTERM)
os.setpgrp()
signal.signal(signal.SIGALRM, alarm_handler)
reset_alarm()


# Cleanup stale files from our image directory.
os.system('find ' + imgdir + ' -type f -amin +10 -print | xargs rm -f')

myself = os.environ['SCRIPT_NAME'];
form = cgi.FieldStorage()
filled = form.has_key('formula')
# FIXME: This assumes Apache.
uid = os.environ['UNIQUE_ID'];
imgprefix = imgdir + '/' + uid

def escaped_print_dot(dict, what):
    print '<pre>'; sys.stdout.flush()
    s = spot.ostringstream()
    spot.bdd_print_dot(s, dict, what)
    print cgi.escape(s.str())
    del s
    print '</pre>'; sys.stdout.flush()

def escaped_print_set(dict, what):
    print '<pre>'; sys.stdout.flush()
    s = spot.ostringstream()
    spot.bdd_print_set(s, dict, what)
    print cgi.escape(s.str())
    del s
    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,",
    # compute the number of acceptance conditions
    acc = all = automaton.all_acceptance_conditions()
    count = 0
    while all != buddy.bddfalse:
        all -= buddy.bdd_satone(all)
        count += 1
    if count > 0:
        print count,
        if count <= 1:
            print "acceptance condition:",
        else:
            print "acceptance conditions:",
            sys.stdout.flush()
        spot.bdd_print_accset(spot.get_cout(), automaton.get_dict(), acc)
    else:
        print "no acceptance condition (all cycles are accepting)"
    print "</p>"
    sys.stdout.flush()

def render_dot(basename):
    os.spawnlp(os.P_WAIT, 'dot', 'dot', '-Tpng', '-Gsize=14,14', '-o',
               basename + '.png', basename + '.dot')
    reset_alarm()
    print '<img src="' + basename + '.png">'

def render_automaton(basename, automata):
    outfile = spot.ofstream(basename + '.dot')
    spot.dotty_reachable(outfile, automata)
    del outfile
    render_dot(basename)

def render_bdd(basename, dictionary, bdd):
    outfile = spot.ofstream(basename + '.dot')
    spot.bdd_print_dot(outfile, dictionary, bdd)
    del outfile
    render_dot(basename)


print "<TITLE>LTL-to-B&uuml;chi test</TITLE>"
print """<H1><a href="http://spot.lip6.fr/">Spot</a>'s on-line
LTL-to-B&uuml;chi translator</H1>"""

formula = form.getfirst('formula', '')

options = [
    ('show_parse',          'show traces during parsing',                  0),
    ('show_formula_dot',    'print the formula as .dot',                   0),
    ('show_formula_gif',    'draw the formula',                            0),
    ('show_automaton_dot',  'print Büchi automaton as .dot',               0),
    ('show_automaton_gif',  'draw Büchi automaton',                        1),
    ('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 (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),
    ]

default_translator = 'trans_fm';
translators = [
    ('trans_fm',        'Convreur/FM'),
    ('trans_lacim',     'Convreur/LaCIM'),
    ]

print """<FORM action="%s" method="post"><P>
Formula to translate:
<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"><tr><td>
<table border="0" rules="groups" frame="void" cellpadding="3" cellspacing=0>
  <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></td></tr></table></p>
Translator:<TABLE><TR><TD>""" % (myself, cgi.escape(formula, True))


trans = form.getfirst("trans", default_translator)
for opt, desc, in translators:
    if trans == opt:
	str = "checked"
    else:
	str = ""
    globals()[opt] = str
    print '<INPUT type="radio" name="trans" value="%s" %s>%s<br>' % (opt, str,
                                                                     desc)

print """</TD></TR></TABLE>
Options:<TABLE><TR><TD>"""

for opt, desc, arg, in options:
    if formula:
	val = int(form.getfirst(opt, 0))
    else:
	val = arg
    if val:
	str = "checked"
    else:
	str = ""
    globals()[opt] = val
    print '<INPUT type="checkbox" name="%s" value="1" %s>%s<br>' % (opt, str,
								    desc)
print '</TD></TR></TABLE><INPUT type="submit" value="Send"></FORM>'

if not filled:
    sys.exit(0)

reset_alarm()

print "<hr><H1>Output</H1>"

env = spot.default_environment.instance()

print "<H2>LTL Formula</H2>"

if show_parse: print '<pre>'
sys.stdout.flush()
sys.stderr.flush()

pel = spot.empty_parse_error_list()
f = spot.parse(formula, pel, env, show_parse)
if show_parse: print '</pre>'

print '<font color="red"><pre>'
err = spot.format_parse_errors(spot.get_cout(), formula, pel)
print '</pre></font>'

if not f:
    print '<p><b>Aborting...</b></p>'
    sys.exit(0)
if err:
    print '<p><b>Continuing anyway...</b></p>'

print "<p>Formula is<code>", f, "</code></p>"

if show_formula_dot:
    print '<pre>'; sys.stdout.flush()
    s = spot.ostringstream()
    spot.dotty(s, f)
    print cgi.escape(s.str())
    del s
    print '</pre>'; sys.stdout.flush()
if show_formula_gif:
    outfile = spot.ofstream(imgprefix + '-f.dot')
    spot.dotty(outfile, f)
    del outfile
    render_dot(imgprefix + '-f')

print '<H2>Automaton</H2>'

dict = spot.bdd_dict()

print '<p>Building automaton...',
sys.stdout.flush()

if trans_lacim:
    automaton = spot.ltl_to_tgba_lacim(f, dict)
elif trans_fm:
    automaton = spot.ltl_to_tgba_fm(f, dict)

print 'done.</p>'
sys.stdout.flush()

print_stats(automaton)

if show_automaton_dot:
    print '<pre>'; sys.stdout.flush()
    s = spot.ostringstream()
    spot.dotty_reachable(s, automaton)
    print cgi.escape(s.str())
    del s
    print '</pre>'; sys.stdout.flush()

if show_automaton_gif:
    render_automaton(imgprefix + '-a', automaton)

if show_degen_dot or show_degen_gif:
    print '<H3>Degeneralized automaton</H3>'
    degen = spot.tgba_tba_proxy(automaton)
    print_stats(degen)
    if show_degen_dot:
	print '<pre>'; sys.stdout.flush()
	s = spot.ostringstream()
	spot.dotty_reachable(s, degen)
	print cgi.escape(s.str())
	del s
	print '</pre>'; sys.stdout.flush()
    if show_degen_gif:
        render_automaton(imgprefix + '-d', degen)
else:
    degen = 0

if show_dictionnay:
    print '<H3>BDD dictionary</H3>'
    print '<pre>'
    sys.stdout.flush()
    automaton.get_dict().dump(spot.get_cout())
    print '</pre>'

if (type(automaton) == spot.tgba_bdd_concretePtr
    and (show_relation_dot or show_relation_set or show_relation_gif)):
    print '<H3>Transition relation</H3>'
    if show_relation_dot:
	escaped_print_dot(automaton.get_dict(),
			  automaton.get_core_data().relation)
    if show_relation_set:
	escaped_print_set(automaton.get_dict(),
			  automaton.get_core_data().relation)
    if show_relation_gif:
        render_bdd(imgprefix + '-b', automaton.get_dict(),
                   automaton.get_core_data().relation)

if (type(automaton) == spot.tgba_bdd_concretePtr
    and (show_acceptance_dot or show_acceptance_set or show_acceptance_gif)):
    print '<H3>Acceptance relation</H3>'
    if show_acceptance_dot:
	escaped_print_dot(automaton.get_dict(),
			  automaton.get_core_data().acceptance_conditions)
    if show_acceptance_set:
	escaped_print_set(automaton.get_dict(),
			  automaton.get_core_data().acceptance_conditions)
    if show_acceptance_gif:
        render_bdd(imgprefix + '-c', automaton.get_dict(),
                   automaton.get_core_data().acceptance_conditions)

if show_lbtt:
    print '<H3>LBTT conversion</H3>'
    if degen:
	print '<H4>Conversion of the generalized automaton</H4>'
    print '<pre>'
    sys.stdout.flush()
    spot.lbtt_reachable(spot.get_cout(), automaton)
    print '</pre>'
    if degen:
	print '<H4>Conversion of the degeneralized automaton</H4>'
	print '<pre>'
	sys.stdout.flush()
	spot.lbtt_reachable(spot.get_cout(), degen)
	print '</pre>'

sys.stdout.flush()

spot.destroy(f)
# Make sure degen is cleared before automaton.
del degen
del automaton

print_footer()