Commit 7cc99800 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Rename the on-line translator to avoid conflicts with the doc

* wrap/python/ajax/css/ltl2tgba.css, wrap/python/ajax/spot.in,
wrap/python/ajax/ltl2tgba.html: Rename ...
* wrap/python/ajax/css/trans.css, wrap/python/ajax/spotcgi.in,
wrap/python/ajax/trans.html: ... as these.
* wrap/python/ajax/Makefile.am, wrap/python/ajax/README: Adjust.
parent b7fbf724
## -*- coding: utf-8 -*-
## Copyright (C) 2011, 2012 Laboratoire d'Informatique de Paris 6
## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
## Pierre et Marie Curie.
## Copyright (C) 2011, 2012, 2015 Laboratoire de Recherche
## et Développement de l'Epita (LRDE).
##
## This file is part of Spot, a model checking library.
##
......@@ -18,8 +17,8 @@
## You should have received a copy of the GNU General Public License
## along with this program. If not, see <http://www.gnu.org/licenses/>.
nodist_noinst_SCRIPTS = spot.py
EXTRA_DIST = $(srcdir)/spot.in README ltl2tgba.html css/ltl2tgba.css \
nodist_noinst_SCRIPTS = spotcgi.py
EXTRA_DIST = $(srcdir)/spotcgi.in README trans.html css/trans.css \
css/tipTip.css js/jquery.tipTip.minified.js js/jquery.ba-bbq.min.js \
js/jquery.ba-dotimeout.min.js logos/lip6sys64.png logos/lrde64.png \
logos/spot64s.png logos/mail.png \
......@@ -43,7 +42,7 @@ EXTRA_DIST = $(srcdir)/spot.in README ltl2tgba.html css/ltl2tgba.css \
CLEANFILES = $(nodist_noinst_SCRIPTS)
spot.py: $(srcdir)/spot.in Makefile
spotcgi.py: $(srcdir)/spotcgi.in Makefile
sed -e 's|[@]PYTHON[@]|@PYTHON@|g' \
-e 's|[@]pythondir[@]|@pythondir@|g' \
-e 's|[@]srcdir[@]|@srcdir@|g' \
......@@ -51,9 +50,9 @@ spot.py: $(srcdir)/spot.in Makefile
-e 's|[@]PACKAGE_VERSION[@]|@PACKAGE_VERSION@|g' \
-e 's|[@]DOT[@]|@DOT@|g' \
-e 's|[@]LTL3BA[@]|@LTL3BA@|g' \
<$(srcdir)/spot.in >spot.tmp
chmod +x spot.tmp
mv -f spot.tmp $@
<$(srcdir)/spotcgi.in >spotcgi.tmp
chmod +x spotcgi.tmp
mv -f spotcgi.tmp $@
clean-local:
rm -rf spotimg
ltl2tgba.html is a dynamic web page that translates user-supplied LTL
formulae to Transition-based Generalized Büchi Automata. The actual
translation work is performed by a CGI script in Python: spot.py.
translation work is performed by a CGI script in Python: spotcgi.py.
There are two ways to use the script: using a web server such as
Apache, or standalone.
......@@ -16,10 +16,10 @@ CGI script). These option were introduced into ltl3ba version 1.1.0.
Standalone usage
================
Simply run spot.py from this directory. This will create a directory
Simply run spotcgi.py from this directory. This will create a directory
called spotimg/ in the current directory (this will hold the generated
pictures) and start an HTTP server on port 8000. Point your browser
to http://localhost:8000/ltl2tgba.html and you should be OK.
to http://localhost:8000/trans.html and you should be OK.
After you have killed the server process (e.g. with Control-C),
you may want to erase the spotimg/ directory.
......@@ -37,9 +37,9 @@ Installing on a real web server
configured from ./configure's arguments and you should not
have to fiddle with it. I'm mentionning it just in case.
2) Copy spot.py to some place were CGI execution is allowed.
2) Copy spotcgi.py to some place were CGI execution is allowed.
Depending on your HTTP server's configuration, you may have
to rename the script as spot.cgi or something else, so
to rename the script as spotcgi.cgi or something else, so
that the server accepts to run it.
Apache users in trouble should look at the following options
......@@ -52,7 +52,7 @@ Installing on a real web server
# Allow CGI execution in some directory.
Options +ExecCGI
3) In the directory where you have installed spot.py,
3) In the directory where you have installed spotcgi.py,
create a subdirectory called spotimg/. This is where
the script will cache its images and other temporary
files. (If you want to change this name, see the imgdir
......@@ -62,10 +62,10 @@ Installing on a real web server
will run the script when the HTTP server processes the
request.
spot.py purges old files at most once every hour.
spotcgi.py purges old files at most once every hour.
4) Copy the directories css/, js/, and logos/ along with ltl2tgba.html
to there destination. You may have to adjust a few paths at the
4) Copy the directories css/, js/, and logos/ along with trans.html
to their destination. You may have to adjust a few paths at the
top of the html page.
......@@ -85,6 +85,6 @@ to the CGI script, so you can simulate the call from the command line
with a command like this:
% export QUERY_STRING="f=a+U+b&r=br&r=lf&r=si&r=eu&o=a&ff=o&mf=d&af=t&ra=t&rf=p&t=fm&fm=od&fm=sm&la=sp&ta=lc&as=ps&ec=Cou99&eo="
% export SCRIPT_NAME=spot.py
% export SCRIPT_NAME=spotcgi.py
% export SERVER_SOFTWARE=SimpleHTTP
% ./spot.py
% ./spotcgi.py
......@@ -86,7 +86,7 @@ if not script:
class MyHandler(CGIHTTPRequestHandler):
def is_cgi(self):
if self.path.startswith('/cgi-bin/spot.py'):
if self.path.startswith('/cgi-bin/spotcgi.py'):
self.cgi_info = '', self.path[9:]
return True
return False
......@@ -98,7 +98,7 @@ if not script:
os.mkdir(imgdir, 493)
sys.stdout.write("Directory spotimg/ created.\n")
httpd = HTTPServer(server_address, MyHandler)
sys.stdout.write("Point your browser to http://localhost:8000/ltl2tgba.html\n")
sys.stdout.write("Point your browser to http://localhost:8000/trans.html\n")
httpd.serve_forever()
import cgi
......
......@@ -8,9 +8,9 @@
<link rev=Made href="mailto:spot@lrde.epita.fr" title="Spot's discussion list">
<link rel="stylesheet" href="css/ui-lightness/jquery-ui-1.8.13.custom.css">
<link rel="stylesheet" href="css/tipTip.css">
<link rel="stylesheet" href="css/ltl2tgba.css">
<link rel="icon" href="http://spot.lip6.fr/img/favicon.ico" type="image/x-icon">
<link rel="shortcut icon" href="http://spot.lip6.fr/img/favicon.ico" type="image/x-icon">
<link rel="stylesheet" href="css/trans.css">
<link rel="icon" href="http://spot.lrde.epita.fr/img/favicon.ico" type="image/x-icon">
<link rel="shortcut icon" href="http://spot.lrde.epita.fr/img/favicon.ico" type="image/x-icon">
<script type="text/javascript" src="http://ajax.googleapis.com/ajax/libs/jquery/1.7.2/jquery.min.js"></script>
<script type="text/javascript" src="http://ajax.googleapis.com/ajax/libs/jqueryui/1.8.13/jquery-ui.min.js"></script>
<script type="text/javascript" src="js/jquery.tipTip.minified.js"></script>
......@@ -173,14 +173,14 @@
$(window).bind('hashchange', function(e) { updateFormFromHash('fast') });
$.get("/cgi-bin/spot.py", "o=v", function(data) {
$.get("/cgi-bin/spotcgi.py", "o=v", function(data) {
$("#spottip").attr("title", "This page uses <b>" + data + "<\/b> to process LTL formulas and automata. Please download the <b>Spot<\/b> library and install it on your computer if you want to do the same from the command line, or from another program.")
.tipTip({maxWidth: "400px", delay: 1000,
edgeOffset: 10,
defaultPosition: "right"});
});
$.get("/cgi-bin/spot.py", "o=v3", function(data) {
$.get("/cgi-bin/spotcgi.py", "o=v3", function(data) {
if (data != 'not available') {
$("#ltl3ba-link").attr("title", data)
.tipTip({maxWidth: "400px", delay: 1000,
......@@ -242,7 +242,7 @@
// cause problems when formulae include '&'.
var fragment = location.href.replace(/^[^#]*#?(.*)$/, '$1');
$("#results-body")
.load("/cgi-bin/spot.py",
.load("/cgi-bin/spotcgi.py",
fragment,
function(response, status, xhr) {
$.doTimeout('res-update');
......@@ -309,7 +309,7 @@
</head>
<body>
<div id="spotlogo">
<a href="http://spot.lip6.fr/"><img border=0 src="logos/spot64s.png" alt="Spot Logo" class="rtip" id="spottip" title="This page uses the <b>Spot</b> library to process LTL formulas and automata. Please download <b>Spot</b> and install it on your computer if you want to do the same from the command line, or from another program."></a></div>
<a href="http://spot.lrde.epita.fr/"><img border=0 src="logos/spot64s.png" alt="Spot Logo" class="rtip" id="spottip" title="This page uses the <b>Spot</b> library to process LTL formulas and automata. Please download <b>Spot</b> and install it on your computer if you want to do the same from the command line, or from another program."></a></div>
<div id="mailicon">
<a href="mailto:spot@lrde.epita.fr"><img border=0 src="logos/mail.png" alt="Spot Logo" class="rtip" title="A bug? A question? Please e-mail us at <b>spot@lrde.epita.fr</b>."></a></div>
<div id="lrdelogo">
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment