#!@PYTHON@
# -*- mode: python; coding: iso-8859-1 -*-
# Copyright (C) 2007, 2009, 2010 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2003, 2004, 2006 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 os

# Directory for temporary files (images and other auxiliary files).
imgdir = 'spotimg'

from CGIHTTPServer import CGIHTTPRequestHandler
class MyHandler(CGIHTTPRequestHandler):
    def is_cgi(self):
        if self.path == '/ltl2tgba.py':
            self.cgi_info = '', 'ltl2tgba.py'
            return True
        return False

if not os.environ.has_key('SCRIPT_NAME'):
    # If this is not run as a cgi script, let's start an HTTP server.
    from BaseHTTPServer import HTTPServer
    server_address=('',8000)
    if not os.access(imgdir, os.F_OK):
        os.mkdir(imgdir, 0755)
        print "Directory spotimg/ created."
    httpd = HTTPServer(server_address, MyHandler)
    print "Point your browser to http://localhost:8000/ltl2tgba.py"
    httpd.serve_forever()

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

print "Content-Type: text/html"
print

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

# Assume Spot is installed
sys.path.insert(0, '@pythondir@')

if (os.environ.has_key('SERVER_SOFTWARE') and
    os.environ['SERVER_SOFTWARE'].startswith(MyHandler.server_version)):
    # We might be running from the build tree (but it's not sure).
    # Add the build and source directories first in the search path.
    # If we are not in the right place, python will find the installed
    # libraries later.
    sys.path.insert(0, '@srcdir@/..')
    sys.path.insert(0, '..')
    # Darwin needs some help in figuring out where non-installed libtool
    # libraries are (on this platform libtool encodes the expected final
    # path of dependent libraries in each library).
    m = '../.libs:@top_builddir@/src/.libs:@top_builddir@/buddy/src/.libs'
    os.environ['DYLD_LIBRARY_PATH'] = m
    import ltihooks

# Extra HTML headers.
extra_header = ''
# extra_header = '<LINK REL="stylesheet" TYPE="text/css" HREF="style.css">'

# Extra notice to display after the Send button.
extra_form_notice = ''

# Location of the dot command
dot = 'dot' # in PATH.
dot_bgcolor = '-Gbgcolor=#FFFFFF'
# dot = '/usr/local/bin/dot'

ltl2tgba_version = '@PACKAGE_VERSION@'

def print_footer():
    print '<hr>'
    print 'ltl2tgba.py ' + ltl2tgba_version + '; Spot', spot.version()
    print '</BODY></HTML>'

try:
    execfile('ltl2tgba.opt')
except IOError:
    pass

import spot
import buddy

# 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 +15 -print | xargs rm -f')

myself = os.environ['SCRIPT_NAME'];
form = cgi.FieldStorage()
filled = form.has_key('formula')
uid = str(uuid.uuid1())
imgprefix = imgdir + '/' + uid

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
    count = automaton.number_of_acceptance_conditions()
    if count > 0:
        print count,
        if count <= 1:
            print "acceptance condition:",
        else:
            print "acceptance conditions:",
            sys.stdout.flush()
        acc = automaton.all_acceptance_conditions()
        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()
    # Decide whether we will render the automaton or not.
    # (A webserver is not a calcul center...)
    if stats.states > 64:
        return "Automaton has too much states"
    if float(stats.transitions)/stats.states > 10:
        return "Automaton has too much transitions per states"
    return False

def render_dot(basename):
    os.spawnlp(os.P_WAIT, dot, dot, dot_bgcolor, '-Tpng',
               '-Gsize=14,14', '-o', basename + '.png', basename + '.txt')
    reset_alarm()
    b = cgi.escape(basename)
    print '<img src="' + b + '.png"><br>(<a href="' + b + '.txt">dot source</a>)'
    sys.stdout.flush()

def render_automaton(basename, automata, dont_run_dot, deco = False):
    outfile = spot.ofstream(basename + '.txt')
    if not deco:
        spot.dotty_reachable(outfile, automata)
    else:
        spot.dotty_reachable(outfile, automata, deco)
    del outfile
    if dont_run_dot:
        print ('<p>' + dont_run_dot + ''' to be rendered on-line.  However
you may download the <a href="''' + cgi.escape(basename)
               + '.txt">source in dot format</a> and render it yourself.')
    else:
        render_dot(basename)

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


print """
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<HTML lang="en"><HEAD>
<TITLE>Spot's on-line LTL-to-TGBA 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-TGBA translator</H1>""" % extra_header

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

color_fm = "#DFC6F8"
color_lacim = "#F8C6DF"
color_taa = "#D8C6FF"

options_common = [
    ('show_formula_png',    'draw the formula',                            0),
    ('show_automaton_png',  'draw Büchi automaton',                        1),
    ('show_degen_png',      'draw degeneralized Büchi automaton',          0),
    ('show_never_claim',    'output Spin never claim',                     0),
    ('show_lbtt',           'convert automaton for LBTT',                  0),
    ]
options_reduce = [
    ('reduce_basics',       'basic rewritings',                            1),
    ('reduce_syntimpl',     'syntactic implication',                       1),
    ('reduce_eventuniv',    'eventuality and universality',                1),
    ]
options_debug = [
    ('show_parse',          'show traces during parsing',                  0),
    ('show_dictionnary',    'print BDD dictionary',                        0),
    ]
options_trans_fm = [
    ('opt_exprop',          'optimize determinism',                        1),
    ('opt_symb_merge',
     'merge states with same symbolic successor representation',           1),
    ('opt_branch_post',     'branching postponement',                      0),
    ('opt_fair_loop_approx','fair-loop approximations',                    0),
    ]
options_trans_lacim = [
    ('show_relation_set',
     'print the transition relation as a BDD set',                         0),
    ('show_relation_png',
     'draw the transition relation',                                       0),
    ('show_acceptance_set',
     'print the acceptance relation as a BDD set',                         0),
    ('show_acceptance_png',
     'draw the acceptance relation',                                       0),
    ]
options_trans_taa = [
    ('refined_rules',
     'refined rules',                                                      1)
    ]

default_translator = 'trans_fm';
translators = [
    ('trans_fm',    'Couvreur/FM',    color_fm),
    ('trans_lacim', 'Couvreur/LaCIM', color_lacim),
    ('trans_taa',   'Tauriainen/TAA', color_taa),
    ]

options_accepting_run = [
    ('print_acc_run', 'print an accepting run...', 0),
    ('draw_acc_run', 'draw an accepting run...', 0),
    ('emptiness_check',
     ['... found using this algorithm: ',
      'Cou99',
      'CVWY90',
      'GV04',
      'SE05',
      'Tau03',
      'Tau03_opt'], 'no'),
    ('emptiness_check_options',
     '...with these <a href="http://spot.lip6.fr/wiki/EmptinessCheckOptions">'
     + 'options</a>:', ''),
    ]

print ("""<FORM action="%s" method="post"><P>
Formula to translate:
<INPUT size=50 type="text"  name="formula" value="%s"><BR>"""
       % (myself, cgi.escape(formula, True)))

if not filled:
    print """
<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>Conversely, infix
letter operators are not assumed to be operators if they are part of
an identifier: <code>aUb</code> is an atomic proposition, unlike
<code>a&nbsp;U&nbsp;b</code> and <code>(a)U(b)</code>.</p>

<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></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>"""

column = [[], []]

def add_options(opt_group, opt_column, opt_color, opt_list):
    if opt_color:
        opt_color = ' bgcolor="%s"' % opt_color
    if opt_group:
        column[opt_column].append(("<TH%s>" % opt_color) + opt_group + "</TH>")
        prefix = ''
    else:
        prefix = '&nbsp;&nbsp;&nbsp;&nbsp;'
    for opt, desc, arg, in opt_list:
        if not isinstance(arg, str):
            if formula:
                val = int(form.getfirst(opt, 0))
            else:
                val = arg

        s = '<TD%s>%s' % (opt_color, prefix);
        if isinstance(desc, list):
            s += '%s <select name="%s">' % (desc[0], opt);
            n = 1
            if val >= len(desc) or val < 1:
                val = n
            for i in desc[1:]:
                if n == val:
                    chk = ' selected'
                else:
                    chk = ''
                s += '<option value="%s"%s>%s' % (n, chk, i);
                n += 1
            s += '</select>'
            val = desc[val]
        elif isinstance(arg, str):
            val = form.getfirst(opt, arg)
            s += (('%s <INPUT type="text" maxlength="40" '
                   + 'name="%s" value="%s">') %
                  (desc, opt, cgi.escape(val, True)))
        else:
            if val:
                chk = ' checked'
            else:
                chk = ''
            s += '<INPUT type="checkbox" name="%s" value="1"%s>%s' % (opt, chk,
                                                                      desc)

        column[opt_column].append((s + '</TD>'))
        globals()[opt] = val


column[0].append("<TH>Algorithm</TH>")
trans = form.getfirst("trans", default_translator)
for opt, desc, color in translators:
    if trans == opt:
	chk = "checked"
    else:
	chk = ""
    globals()[opt] = chk
    s = \
      '<TD bgcolor="%s"><INPUT type="radio" name="trans" value="%s" %s>%s</TD>'
    column[0].append(s % (color, opt, chk, desc))
    add_options('', 0, color, globals()['options_' + opt])

add_options("Search accepting run?", 0, '', options_accepting_run)
add_options("Common Options", 1, '', options_common)
add_options("Formula Simplications", 1, '', options_reduce)
add_options("Debugging Options", 1, '', options_debug)

print '<TABLE>'
width = range(len(column))
depth = 0
for i in width:
    depth = max(len(column[i]), depth)
for d in range(depth):
    print '<TR>'
    for i in width:
        if d < len(column[i]):
            print column[i][d]
        else:
            print '<TD></TD>'
    print '</TR>'
print '</TABLE>'

print '<INPUT type="submit" value="Send">%s</FORM>' % extra_form_notice

if not filled:
    print_footer()
    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_png:
    outfile = spot.ofstream(imgprefix + '-f.txt')
    spot.dotty(outfile, f)
    del outfile
    render_dot(imgprefix + '-f')

opt = spot.Reduce_None
if reduce_basics:
    opt = opt + spot.Reduce_Basics
if reduce_syntimpl:
    opt = opt + spot.Reduce_Syntactic_Implications
if reduce_eventuniv:
    opt = opt + spot.Reduce_Eventuality_And_Universality
if opt != spot.Reduce_None:
    f2 = spot.reduce(f, opt)
    f.destroy()
    f = f2
    print "<p>Reduced formula is<code>", f, "</code></p>"

    if show_formula_png:
        outfile = spot.ofstream(imgprefix + '-f2.txt')
        spot.dotty(outfile, f)
        del outfile
        render_dot(imgprefix + '-f2')

print '<H2>Automaton</H2>'

dict = spot.bdd_dict()

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

if opt_exprop:
    exprop = 1
else:
    exprop = 0
if opt_symb_merge:
    symb_merge = 1
else:
    symb_merge = 0
if opt_branch_post:
    branching_postponement = 1
else:
    branching_postponement = 0
if opt_fair_loop_approx:
    fair_loop_approx = 1
else:
    fair_loop_approx = 0

if trans_lacim:
    automaton = spot.ltl_to_tgba_lacim(f, dict)
elif trans_fm:
    automaton = spot.ltl_to_tgba_fm(f, dict,
                                    exprop, symb_merge, branching_postponement,
                                    fair_loop_approx)
elif trans_taa:
    automaton = spot.ltl_to_taa(f, dict, refined_rules)

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

dont_run_dot = print_stats(automaton)

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

if show_degen_png or show_never_claim:
    print '<H3>Degeneralized automaton</H3>'
    degen = spot.tgba_sba_proxy(automaton)
    dont_run_dot = print_stats(degen)
    if show_degen_png:
        render_automaton(imgprefix + '-d', degen, dont_run_dot)
else:
    degen = 0

if show_never_claim:
    print '<H3>Never claim (for degeneralized automaton)</H3>'
    print '<PRE>'
    s = spot.ostringstream()
    spot.never_claim_reachable(s, degen, f)
    print cgi.escape(s.str())
    del s
    print '</PRE>'
    sys.stdout.flush()

if show_dictionnary:
    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_concrete
    and (show_relation_set or show_relation_png)):
    print '<H3>Transition relation</H3>'
    if show_relation_set:
	escaped_print_set(automaton.get_dict(),
			  automaton.get_core_data().relation)
    if show_relation_png:
        render_bdd(imgprefix + '-b', automaton.get_dict(),
                   automaton.get_core_data().relation)

if (type(automaton) == spot.tgba_bdd_concrete
    and (show_acceptance_set or show_acceptance_png)):
    print '<H3>Acceptance relation</H3>'
    if show_acceptance_set:
	escaped_print_set(automaton.get_dict(),
			  automaton.get_core_data().acceptance_conditions)
    if show_acceptance_png:
        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>'


if draw_acc_run or print_acc_run:
    print '<H3>Accepting run</H3>'
    sys.stdout.flush()
    err = ""
    opt = emptiness_check + "(" + emptiness_check_options + ")"
    eci, err = spot.emptiness_check_instantiator.construct(opt)

    ec_msg = "Running " + opt

    if not eci:
        print ('<font color="red">Cannot parse "' + opt + '" near "' + err
               + '".</font>')
    else:
        ec_a = 0
        n_acc = automaton.number_of_acceptance_conditions()
        n_max = eci.max_acceptance_conditions()
        if (n_acc <= n_max):
            ec_a = automaton
        else:
            if degen:
                ec_a = degen
                ec_msg += ' <b>on degeneralized automaton</b>'
            else:
                print ('<font color="red">Cannot run ' + emptiness_check
                       + ' on automata with more than ' + n_max + ' acceptance '
                       + 'conditions.  Please select "draw degeneralized '
                       + 'Büchi automaton" if you want to try this'
                       + ' algorithm on the degeneralized version of the'
                       + ' automaton.</font>')

        if ec_a:
            ec = eci.instantiate(ec_a)

    if ec:
        print '%s: ' % ec_msg
        sys.stdout.flush()
        ec_res = ec.check()
        if not ec_res:
            print "no accepting run found.<br>"
        else:
            ec_run = ec_res.accepting_run()
            print "accepting run found.<br>"
            if ec_run:
                if print_acc_run:
                    print '<pre>'; sys.stdout.flush()
                    s = spot.ostringstream()
                    spot.print_tgba_run(s, ec_a, ec_run)
                    print cgi.escape(s.str())
                    del s
                    print '</pre>'; sys.stdout.flush()
                if draw_acc_run:
                    deco = spot.tgba_run_dotty_decorator(ec_run)
                    dont_run_dot = print_stats(ec_a)
                    render_automaton(imgprefix + '-e', ec_a, dont_run_dot, deco)
                    del deco
                del ec_run
            del ec_res
        del ec
        del ec_a

sys.stdout.flush()

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

del dict
print_footer()