get rid of the Python-based CGI translator
We now have a separate project for its replacement at https://gitlab.lrde.epita.fr/spot/spot-web-app/ * python/ajax/: Remove directory. * python/Makefile.am, configure.ac, README: Adjust. * NEWS: Mention this.
This commit is contained in:
Alexandre Duret-Lutz
parent
22ad9f5ed2
commit
1be313ef0b
15 changed files with 5 additions and 2131 deletions
6
NEWS
6
NEWS
|
|
@ -1,6 +1,10 @@
|
||||||
New in spot 2.6.1.dev (not yet released)
|
New in spot 2.6.1.dev (not yet released)
|
||||||
|
|
||||||
Nothing yet.
|
Build:
|
||||||
|
|
||||||
|
- We no longer distribute the Python-based CGI script + javascript
|
||||||
|
code for the online translator. Its replacement has its own
|
||||||
|
repository: https://gitlab.lrde.epita.fr/spot/spot-web-app/
|
||||||
|
|
||||||
New in spot 2.6.1 (2018-08-04)
|
New in spot 2.6.1 (2018-08-04)
|
||||||
|
|
||||||
|
|
|
||||||
1
README
1
README
|
|
@ -228,7 +228,6 @@ bench/ Benchmarks for ...
|
||||||
stutter/ ... stutter-invariance checking algorithms,
|
stutter/ ... stutter-invariance checking algorithms,
|
||||||
wdba/ ... WDBA minimization (for obligation properties).
|
wdba/ ... WDBA minimization (for obligation properties).
|
||||||
python/ Python bindings for Spot and BuDDy
|
python/ Python bindings for Spot and BuDDy
|
||||||
ajax/ LTL-to-TGBA translator with web interface, using Javascript.
|
|
||||||
|
|
||||||
Third party software
|
Third party software
|
||||||
--------------------
|
--------------------
|
||||||
|
|
|
||||||
|
|
@ -244,7 +244,6 @@ AC_CONFIG_FILES([
|
||||||
spot/twaalgos/Makefile
|
spot/twaalgos/Makefile
|
||||||
spot/twa/Makefile
|
spot/twa/Makefile
|
||||||
spot/gen/Makefile
|
spot/gen/Makefile
|
||||||
python/ajax/Makefile
|
|
||||||
python/Makefile
|
python/Makefile
|
||||||
tests/core/defs
|
tests/core/defs
|
||||||
tests/ltsmin/defs:tests/core/defs.in
|
tests/ltsmin/defs:tests/core/defs.in
|
||||||
|
|
|
||||||
|
|
@ -20,8 +20,6 @@
|
||||||
## You should have received a copy of the GNU General Public License
|
## You should have received a copy of the GNU General Public License
|
||||||
## along with this program. If not, see <http://www.gnu.org/licenses/>.
|
## along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||||
|
|
||||||
SUBDIRS = . ajax
|
|
||||||
|
|
||||||
AUTOMAKE_OPTIONS = subdir-objects
|
AUTOMAKE_OPTIONS = subdir-objects
|
||||||
|
|
||||||
AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_builddir) -I$(top_srcdir) \
|
AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_builddir) -I$(top_srcdir) \
|
||||||
|
|
|
||||||
|
|
@ -1,40 +0,0 @@
|
||||||
## -*- coding: utf-8 -*-
|
|
||||||
## Copyright (C) 2011, 2012, 2015, 2016, 2018 Laboratoire de Recherche et
|
|
||||||
## Développement de l'Epita (LRDE).
|
|
||||||
##
|
|
||||||
## 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
|
|
||||||
|
|
||||||
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 css/loading.gif protocol.txt
|
|
||||||
|
|
||||||
CLEANFILES = $(nodist_noinst_SCRIPTS)
|
|
||||||
|
|
||||||
spotcgi.py: $(srcdir)/spotcgi.in Makefile
|
|
||||||
sed -e 's|[@]PYTHON[@]|@PYTHON@|g' \
|
|
||||||
-e 's|[@]pythondir[@]|@pythondir@|g' \
|
|
||||||
-e 's|[@]srcdir[@]|@srcdir@|g' \
|
|
||||||
-e 's|[@]top_builddir[@]|@top_builddir@|g' \
|
|
||||||
-e 's|[@]PACKAGE_VERSION[@]|@PACKAGE_VERSION@|g' \
|
|
||||||
-e 's|[@]DOT[@]|@DOT@|g' \
|
|
||||||
-e 's|[@]LTL3BA[@]|@LTL3BA@|g' \
|
|
||||||
<$(srcdir)/spotcgi.in >spotcgi.tmp
|
|
||||||
chmod +x spotcgi.tmp
|
|
||||||
mv -f spotcgi.tmp $@
|
|
||||||
|
|
||||||
clean-local:
|
|
||||||
rm -rf spotimg
|
|
||||||
|
|
@ -1,90 +0,0 @@
|
||||||
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: spotcgi.py.
|
|
||||||
|
|
||||||
There are two ways to use the script: using a web server such as
|
|
||||||
Apache, or standalone.
|
|
||||||
|
|
||||||
In both cases you should ensure that the command `dot', from the
|
|
||||||
GraphViz package, is in the PATH. configure should have picked it up.
|
|
||||||
|
|
||||||
The "ltl3ba" tab will only be enabled if ltl3ba is available (as
|
|
||||||
checked by ./configure) and supports options -v/-T/-T3 (checked by the
|
|
||||||
CGI script). These option were introduced into ltl3ba version 1.1.0.
|
|
||||||
|
|
||||||
|
|
||||||
Standalone usage
|
|
||||||
================
|
|
||||||
|
|
||||||
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/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.
|
|
||||||
|
|
||||||
|
|
||||||
Installing on a real web server
|
|
||||||
===============================
|
|
||||||
|
|
||||||
1) Install Spot first (run `make install' from the top-level).
|
|
||||||
|
|
||||||
The CGI script uses the Python bindings and assume they
|
|
||||||
have been installed. Near the top of the script, you
|
|
||||||
should see a call to sys.path.insert(), with the expected
|
|
||||||
location of the Python bindings for spot. This path was
|
|
||||||
configured from ./configure's arguments and you should not
|
|
||||||
have to fiddle with it. I'm mentionning it just in case.
|
|
||||||
|
|
||||||
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 spotcgi.cgi or something else, so
|
|
||||||
that the server accepts to run it.
|
|
||||||
|
|
||||||
Apache users in trouble should look at the following options
|
|
||||||
before digging the Apache manual deeper. These can go
|
|
||||||
in a .htaccess file (if allowed).
|
|
||||||
|
|
||||||
# Treat *.py files as CGI scripts
|
|
||||||
AddHandler cgi-script .py
|
|
||||||
|
|
||||||
# Allow CGI execution in some directory.
|
|
||||||
Options +ExecCGI
|
|
||||||
|
|
||||||
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
|
|
||||||
variable at the top of the script.)
|
|
||||||
|
|
||||||
This directory must be writable by the Unix user that
|
|
||||||
will run the script when the HTTP server processes the
|
|
||||||
request.
|
|
||||||
|
|
||||||
spotcgi.py purges old files at most once every hour.
|
|
||||||
|
|
||||||
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.
|
|
||||||
|
|
||||||
|
|
||||||
Debugging
|
|
||||||
=========
|
|
||||||
|
|
||||||
When working on the script, remember that the contents of spotimg/ is
|
|
||||||
used as a cache and that a request will not be processed again if its
|
|
||||||
result is in the cache. So if you don't understand why the change you
|
|
||||||
have performed has no effect, make sure you are performing some fresh
|
|
||||||
query, or wipe the contents of the cache (i.e., erase all files inside
|
|
||||||
spotimg/ but not the spotimg/ directory itself).
|
|
||||||
|
|
||||||
|
|
||||||
The hash string displayed in the web browser is the query string sent
|
|
||||||
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=spotcgi.py
|
|
||||||
% export SERVER_SOFTWARE=SimpleHTTP
|
|
||||||
% ./spotcgi.py
|
|
||||||
Binary file not shown.
|
Before Width: | Height: | Size: 4.1 KiB |
|
|
@ -1,114 +0,0 @@
|
||||||
/* TipTip CSS - Version 1.2 */
|
|
||||||
|
|
||||||
#tiptip_holder {
|
|
||||||
display: none;
|
|
||||||
position: absolute;
|
|
||||||
top: 0;
|
|
||||||
left: 0;
|
|
||||||
z-index: 99999;
|
|
||||||
}
|
|
||||||
|
|
||||||
#tiptip_holder.tip_top {
|
|
||||||
padding-bottom: 5px;
|
|
||||||
}
|
|
||||||
|
|
||||||
#tiptip_holder.tip_bottom {
|
|
||||||
padding-top: 5px;
|
|
||||||
}
|
|
||||||
|
|
||||||
#tiptip_holder.tip_right {
|
|
||||||
padding-left: 5px;
|
|
||||||
}
|
|
||||||
|
|
||||||
#tiptip_holder.tip_left {
|
|
||||||
padding-right: 5px;
|
|
||||||
}
|
|
||||||
|
|
||||||
#tiptip_content {
|
|
||||||
font-family: Trebuchet MS, Tahoma, Verdana, Arial, sans-serif;
|
|
||||||
font-size: 1em;
|
|
||||||
color: #fff;
|
|
||||||
text-shadow: 0 0 2px #000;
|
|
||||||
padding: 4px 8px;
|
|
||||||
border: 1px solid rgba(255,255,255,0.25);
|
|
||||||
background-color: rgb(25,25,25);
|
|
||||||
background-color: rgba(25,25,25,0.92);
|
|
||||||
background-image: -webkit-gradient(linear, 0% 0%, 0% 100%, from(transparent), to(#000));
|
|
||||||
border-radius: 3px;
|
|
||||||
-webkit-border-radius: 3px;
|
|
||||||
-moz-border-radius: 3px;
|
|
||||||
box-shadow: 0 0 3px #555;
|
|
||||||
-webkit-box-shadow: 0 0 3px #555;
|
|
||||||
-moz-box-shadow: 0 0 3px #555;
|
|
||||||
}
|
|
||||||
|
|
||||||
#tiptip_arrow, #tiptip_arrow_inner {
|
|
||||||
position: absolute;
|
|
||||||
border-color: transparent;
|
|
||||||
border-style: solid;
|
|
||||||
border-width: 6px;
|
|
||||||
height: 0;
|
|
||||||
width: 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
#tiptip_holder.tip_top #tiptip_arrow {
|
|
||||||
border-top-color: #fff;
|
|
||||||
border-top-color: rgba(255,255,255,0.35);
|
|
||||||
}
|
|
||||||
|
|
||||||
#tiptip_holder.tip_bottom #tiptip_arrow {
|
|
||||||
border-bottom-color: #fff;
|
|
||||||
border-bottom-color: rgba(255,255,255,0.35);
|
|
||||||
}
|
|
||||||
|
|
||||||
#tiptip_holder.tip_right #tiptip_arrow {
|
|
||||||
border-right-color: #fff;
|
|
||||||
border-right-color: rgba(255,255,255,0.35);
|
|
||||||
}
|
|
||||||
|
|
||||||
#tiptip_holder.tip_left #tiptip_arrow {
|
|
||||||
border-left-color: #fff;
|
|
||||||
border-left-color: rgba(255,255,255,0.35);
|
|
||||||
}
|
|
||||||
|
|
||||||
#tiptip_holder.tip_top #tiptip_arrow_inner {
|
|
||||||
margin-top: -7px;
|
|
||||||
margin-left: -6px;
|
|
||||||
border-top-color: rgb(25,25,25);
|
|
||||||
border-top-color: rgba(25,25,25,0.92);
|
|
||||||
}
|
|
||||||
|
|
||||||
#tiptip_holder.tip_bottom #tiptip_arrow_inner {
|
|
||||||
margin-top: -5px;
|
|
||||||
margin-left: -6px;
|
|
||||||
border-bottom-color: rgb(25,25,25);
|
|
||||||
border-bottom-color: rgba(25,25,25,0.92);
|
|
||||||
}
|
|
||||||
|
|
||||||
#tiptip_holder.tip_right #tiptip_arrow_inner {
|
|
||||||
margin-top: -6px;
|
|
||||||
margin-left: -5px;
|
|
||||||
border-right-color: rgb(25,25,25);
|
|
||||||
border-right-color: rgba(25,25,25,0.92);
|
|
||||||
}
|
|
||||||
|
|
||||||
#tiptip_holder.tip_left #tiptip_arrow_inner {
|
|
||||||
margin-top: -6px;
|
|
||||||
margin-left: -7px;
|
|
||||||
border-left-color: rgb(25,25,25);
|
|
||||||
border-left-color: rgba(25,25,25,0.92);
|
|
||||||
}
|
|
||||||
|
|
||||||
/* Webkit Hacks */
|
|
||||||
@media screen and (-webkit-min-device-pixel-ratio:0) {
|
|
||||||
#tiptip_content {
|
|
||||||
padding: 4px 8px 5px 8px;
|
|
||||||
background-color: rgba(45,45,45,0.88);
|
|
||||||
}
|
|
||||||
#tiptip_holder.tip_bottom #tiptip_arrow_inner {
|
|
||||||
border-bottom-color: rgba(45,45,45,0.88);
|
|
||||||
}
|
|
||||||
#tiptip_holder.tip_top #tiptip_arrow_inner {
|
|
||||||
border-top-color: rgba(20,20,20,0.92);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,129 +0,0 @@
|
||||||
html {overflow-y:scroll;}
|
|
||||||
|
|
||||||
.ltl2tgba .ui-widget {
|
|
||||||
font-size: 1em;
|
|
||||||
}
|
|
||||||
|
|
||||||
input.formula {
|
|
||||||
width: 720px;
|
|
||||||
}
|
|
||||||
|
|
||||||
span#send {
|
|
||||||
width: 60px;
|
|
||||||
margin-left: 4px;
|
|
||||||
margin-right: 0px;
|
|
||||||
}
|
|
||||||
|
|
||||||
.shadow {
|
|
||||||
-moz-box-shadow: 2px 2px 2px #888888;
|
|
||||||
-webkit-box-shadow: 2px 1px 2px #888888;
|
|
||||||
box-shadow: 2px 2px 2px #888888;
|
|
||||||
}
|
|
||||||
|
|
||||||
div.ltl2tgba {
|
|
||||||
width: 800px;
|
|
||||||
position:relative;
|
|
||||||
left:0px;
|
|
||||||
top:0px;
|
|
||||||
margin-left: auto;
|
|
||||||
margin-right: auto;
|
|
||||||
z-index:10;
|
|
||||||
}
|
|
||||||
|
|
||||||
#spotlogo {
|
|
||||||
position:fixed;
|
|
||||||
left:10px;
|
|
||||||
top:10px;
|
|
||||||
z-index:1;
|
|
||||||
}
|
|
||||||
#mailicon {
|
|
||||||
position:fixed;
|
|
||||||
left:10px;
|
|
||||||
top:84px;
|
|
||||||
z-index:1;
|
|
||||||
}
|
|
||||||
#results-body {
|
|
||||||
overflow: auto;
|
|
||||||
}
|
|
||||||
.ltldoc {
|
|
||||||
text-align: right;
|
|
||||||
}
|
|
||||||
|
|
||||||
table.ltltable
|
|
||||||
{
|
|
||||||
border-collapse:collapse;
|
|
||||||
font-size: 90%;
|
|
||||||
}
|
|
||||||
|
|
||||||
.ltldocrow {
|
|
||||||
font-weight: bold;
|
|
||||||
vertical-align:top;
|
|
||||||
}
|
|
||||||
|
|
||||||
.ltl2tgba div.ui-widget-content {
|
|
||||||
padding: 3px;
|
|
||||||
margin: 2px 0px;
|
|
||||||
background: #eeeeee;
|
|
||||||
}
|
|
||||||
|
|
||||||
.ltl2tgba h3 {
|
|
||||||
font-size:1em;
|
|
||||||
margin: 0;
|
|
||||||
padding: 0px 0.2em 0px;
|
|
||||||
border-bottom:1px solid #eee;
|
|
||||||
text-transform: capitalize;
|
|
||||||
}
|
|
||||||
|
|
||||||
.floatright {
|
|
||||||
float: right;
|
|
||||||
}
|
|
||||||
|
|
||||||
.colleft {
|
|
||||||
float: left;
|
|
||||||
width: 49%;
|
|
||||||
}
|
|
||||||
|
|
||||||
.ltl2tgba .head .ui-icon {
|
|
||||||
float: right;
|
|
||||||
margin: 1px 0px;
|
|
||||||
}
|
|
||||||
|
|
||||||
.ltl2tgba .formula, #tiptip_content .formula {
|
|
||||||
font-family: monospace;
|
|
||||||
font-weight: bold;
|
|
||||||
font-size: 1.1em;
|
|
||||||
}
|
|
||||||
|
|
||||||
.ltl2tgba .error {
|
|
||||||
color: red;
|
|
||||||
}
|
|
||||||
|
|
||||||
.ltl2tgba .parse-error {
|
|
||||||
font-family: monospace;
|
|
||||||
white-space: pre;
|
|
||||||
color: red;
|
|
||||||
font-size: 1.1em;
|
|
||||||
}
|
|
||||||
|
|
||||||
.ltl2tgba .ec-error {
|
|
||||||
color: red;
|
|
||||||
}
|
|
||||||
|
|
||||||
.ltl2tgba .loading {
|
|
||||||
display: block;
|
|
||||||
margin: 0 auto;
|
|
||||||
text-align: center;
|
|
||||||
}
|
|
||||||
|
|
||||||
.ltl2tgba .neverclaim, .ltl2tgba .accrun {
|
|
||||||
font-family: monospace;
|
|
||||||
white-space: pre;
|
|
||||||
font-size: 1.1em;
|
|
||||||
}
|
|
||||||
|
|
||||||
#ltl3ba-tab {
|
|
||||||
margin-left: 1em;
|
|
||||||
}
|
|
||||||
|
|
||||||
.ui-button-text-only .ui-button-text { padding: .1em .3em; }
|
|
||||||
.ui-tabs .ui-tabs-nav li a { float: left; padding: .1em .3em; text-decoration: none; }
|
|
||||||
18
python/ajax/js/jquery.ba-bbq.min.js
vendored
18
python/ajax/js/jquery.ba-bbq.min.js
vendored
|
|
@ -1,18 +0,0 @@
|
||||||
/*
|
|
||||||
* jQuery BBQ: Back Button & Query Library - v1.3pre - 8/26/2010
|
|
||||||
* http://benalman.com/projects/jquery-bbq-plugin/
|
|
||||||
*
|
|
||||||
* Copyright (c) 2010 "Cowboy" Ben Alman
|
|
||||||
* Dual licensed under the MIT and GPL licenses.
|
|
||||||
* http://benalman.com/about/license/
|
|
||||||
*/
|
|
||||||
(function($,r){var h,n=Array.prototype.slice,t=decodeURIComponent,a=$.param,j,c,m,y,b=$.bbq=$.bbq||{},s,x,k,e=$.event.special,d="hashchange",B="querystring",F="fragment",z="elemUrlAttr",l="href",w="src",p=/^.*\?|#.*$/g,u,H,g,i,C,E={};function G(I){return typeof I==="string"}function D(J){var I=n.call(arguments,1);return function(){return J.apply(this,I.concat(n.call(arguments)))}}function o(I){return I.replace(H,"$2")}function q(I){return I.replace(/(?:^[^?#]*\?([^#]*).*$)?.*/,"$1")}function f(K,P,I,L,J){var R,O,N,Q,M;if(L!==h){N=I.match(K?H:/^([^#?]*)\??([^#]*)(#?.*)/);M=N[3]||"";if(J===2&&G(L)){O=L.replace(K?u:p,"")}else{Q=m(N[2]);L=G(L)?m[K?F:B](L):L;O=J===2?L:J===1?$.extend({},L,Q):$.extend({},Q,L);O=j(O);if(K){O=O.replace(g,t)}}R=N[1]+(K?C:O||!N[1]?"?":"")+O+M}else{R=P(I!==h?I:location.href)}return R}a[B]=D(f,0,q);a[F]=c=D(f,1,o);a.sorted=j=function(J,K){var I=[],L={};$.each(a(J,K).split("&"),function(P,M){var O=M.replace(/(?:%5B|=).*$/,""),N=L[O];if(!N){N=L[O]=[];I.push(O)}N.push(M)});return $.map(I.sort(),function(M){return L[M]}).join("&")};c.noEscape=function(J){J=J||"";var I=$.map(J.split(""),encodeURIComponent);g=new RegExp(I.join("|"),"g")};c.noEscape(",/");c.ajaxCrawlable=function(I){if(I!==h){if(I){u=/^.*(?:#!|#)/;H=/^([^#]*)(?:#!|#)?(.*)$/;C="#!"}else{u=/^.*#/;H=/^([^#]*)#?(.*)$/;C="#"}i=!!I}return i};c.ajaxCrawlable(0);$.deparam=m=function(L,I){var K={},J={"true":!0,"false":!1,"null":null};$.each(L.replace(/\+/g," ").split("&"),function(O,T){var N=T.split("="),S=t(N[0]),M,R=K,P=0,U=S.split("]["),Q=U.length-1;if(/\[/.test(U[0])&&/\]$/.test(U[Q])){U[Q]=U[Q].replace(/\]$/,"");U=U.shift().split("[").concat(U);Q=U.length-1}else{Q=0}if(N.length===2){M=t(N[1]);if(I){M=M&&!isNaN(M)?+M:M==="undefined"?h:J[M]!==h?J[M]:M}if(Q){for(;P<=Q;P++){S=U[P]===""?R.length:U[P];R=R[S]=P<Q?R[S]||(U[P+1]&&isNaN(U[P+1])?{}:[]):M}}else{if($.isArray(K[S])){K[S].push(M)}else{if(K[S]!==h){K[S]=[K[S],M]}else{K[S]=M}}}}else{if(S){K[S]=I?h:""}}});return K};function A(K,I,J){if(I===h||typeof I==="boolean"){J=I;I=a[K?F:B]()}else{I=G(I)?I.replace(K?u:p,""):I}return m(I,J)}m[B]=D(A,0);m[F]=y=D(A,1);$[z]||($[z]=function(I){return $.extend(E,I)})({a:l,base:l,iframe:w,img:w,input:w,form:"action",link:l,script:w});k=$[z];function v(L,J,K,I){if(!G(K)&&typeof K!=="object"){I=K;K=J;J=h}return this.each(function(){var O=$(this),M=J||k()[(this.nodeName||"").toLowerCase()]||"",N=M&&O.attr(M)||"";O.attr(M,a[L](N,K,I))})}$.fn[B]=D(v,B);$.fn[F]=D(v,F);b.pushState=s=function(L,I){if(G(L)&&/^#/.test(L)&&I===h){I=2}var K=L!==h,J=c(location.href,K?L:{},K?I:2);location.href=J};b.getState=x=function(I,J){return I===h||typeof I==="boolean"?y(I):y(J)[I]};b.removeState=function(I){var J={};if(I!==h){J=x();$.each($.isArray(I)?I:arguments,function(L,K){delete J[K]})}s(J,2)};e[d]=$.extend(e[d],{add:function(I){var K;function J(M){var L=M[F]=c();M.getState=function(N,O){return N===h||typeof N==="boolean"?m(L,N):m(L,O)[N]};K.apply(this,arguments)}if($.isFunction(I)){K=I;return J}else{K=I.handler;I.handler=J}}})})(jQuery,this);
|
|
||||||
/*
|
|
||||||
* jQuery hashchange event - v1.3 - 7/21/2010
|
|
||||||
* http://benalman.com/projects/jquery-hashchange-plugin/
|
|
||||||
*
|
|
||||||
* Copyright (c) 2010 "Cowboy" Ben Alman
|
|
||||||
* Dual licensed under the MIT and GPL licenses.
|
|
||||||
* http://benalman.com/about/license/
|
|
||||||
*/
|
|
||||||
(function($,e,b){var c="hashchange",h=document,f,g=$.event.special,i=h.documentMode,d="on"+c in e&&(i===b||i>7);function a(j){j=j||location.href;return"#"+j.replace(/^[^#]*#?(.*)$/,"$1")}$.fn[c]=function(j){return j?this.bind(c,j):this.trigger(c)};$.fn[c].delay=50;g[c]=$.extend(g[c],{setup:function(){if(d){return false}$(f.start)},teardown:function(){if(d){return false}$(f.stop)}});f=(function(){var j={},p,m=a(),k=function(q){return q},l=k,o=k;j.start=function(){p||n()};j.stop=function(){p&&clearTimeout(p);p=b};function n(){var r=a(),q=o(m);if(r!==m){l(m=r,q);$(e).trigger(c)}else{if(q!==m){location.href=location.href.replace(/#.*/,"")+q}}p=setTimeout(n,$.fn[c].delay)}$.browser.msie&&!d&&(function(){var q,r;j.start=function(){if(!q){r=$.fn[c].src;r=r&&r+a();q=$('<iframe tabindex="-1" title="empty"/>').hide().one("load",function(){r||l(a());n()}).attr("src",r||"javascript:0").insertAfter("body")[0].contentWindow;h.onpropertychange=function(){try{if(event.propertyName==="title"){q.document.title=h.title}}catch(s){}}}};j.stop=k;o=function(){return a(q.location.href)};l=function(v,s){var u=q.document,t=$.fn[c].domain;if(v!==s){u.title=h.title;u.open();t&&u.write('<script>document.domain="'+t+'"<\/script>');u.close();q.location.hash=v}}})();return j})()})(jQuery,this);
|
|
||||||
9
python/ajax/js/jquery.ba-dotimeout.min.js
vendored
9
python/ajax/js/jquery.ba-dotimeout.min.js
vendored
|
|
@ -1,9 +0,0 @@
|
||||||
/*
|
|
||||||
* jQuery doTimeout: Like setTimeout, but better! - v1.0 - 3/3/2010
|
|
||||||
* http://benalman.com/projects/jquery-dotimeout-plugin/
|
|
||||||
*
|
|
||||||
* Copyright (c) 2010 "Cowboy" Ben Alman
|
|
||||||
* Dual licensed under the MIT and GPL licenses.
|
|
||||||
* http://benalman.com/about/license/
|
|
||||||
*/
|
|
||||||
(function($){var a={},c="doTimeout",d=Array.prototype.slice;$[c]=function(){return b.apply(window,[0].concat(d.call(arguments)))};$.fn[c]=function(){var f=d.call(arguments),e=b.apply(this,[c+f[0]].concat(f));return typeof f[0]==="number"||typeof f[1]==="number"?this:e};function b(l){var m=this,h,k={},g=l?$.fn:$,n=arguments,i=4,f=n[1],j=n[2],p=n[3];if(typeof f!=="string"){i--;f=l=0;j=n[1];p=n[2]}if(l){h=m.eq(0);h.data(l,k=h.data(l)||{})}else{if(f){k=a[f]||(a[f]={})}}k.id&&clearTimeout(k.id);delete k.id;function e(){if(l){h.removeData(l)}else{if(f){delete a[f]}}}function o(){k.id=setTimeout(function(){k.fn()},j)}if(p){k.fn=function(q){if(typeof p==="string"){p=g[p]}p.apply(m,d.call(n,i))===true&&!q?o():e()};o()}else{if(k.fn){j===undefined?e():k.fn(j===false);return true}else{e()}}}})(jQuery);
|
|
||||||
|
|
@ -1,21 +0,0 @@
|
||||||
/*
|
|
||||||
* TipTip
|
|
||||||
* Copyright 2010 Drew Wilson
|
|
||||||
* www.drewwilson.com
|
|
||||||
* code.drewwilson.com/entry/tiptip-jquery-plugin
|
|
||||||
*
|
|
||||||
* Version 1.3 - Updated: Mar. 23, 2010
|
|
||||||
*
|
|
||||||
* This Plug-In will create a custom tooltip to replace the default
|
|
||||||
* browser tooltip. It is extremely lightweight and very smart in
|
|
||||||
* that it detects the edges of the browser window and will make sure
|
|
||||||
* the tooltip stays within the current window size. As a result the
|
|
||||||
* tooltip will adjust itself to be displayed above, below, to the left
|
|
||||||
* or to the right depending on what is necessary to stay within the
|
|
||||||
* browser window. It is completely customizable as well via CSS.
|
|
||||||
*
|
|
||||||
* This TipTip jQuery plug-in is dual licensed under the MIT and GPL licenses:
|
|
||||||
* http://www.opensource.org/licenses/mit-license.php
|
|
||||||
* http://www.gnu.org/licenses/gpl.html
|
|
||||||
*/
|
|
||||||
(function($){$.fn.tipTip=function(options){var defaults={activation:"hover",keepAlive:false,maxWidth:"200px",edgeOffset:3,defaultPosition:"bottom",delay:400,fadeIn:200,fadeOut:200,attribute:"title",content:false,enter:function(){},exit:function(){}};var opts=$.extend(defaults,options);if($("#tiptip_holder").length<=0){var tiptip_holder=$('<div id="tiptip_holder" style="max-width:'+opts.maxWidth+';"></div>');var tiptip_content=$('<div id="tiptip_content"></div>');var tiptip_arrow=$('<div id="tiptip_arrow"></div>');$("body").append(tiptip_holder.html(tiptip_content).prepend(tiptip_arrow.html('<div id="tiptip_arrow_inner"></div>')))}else{var tiptip_holder=$("#tiptip_holder");var tiptip_content=$("#tiptip_content");var tiptip_arrow=$("#tiptip_arrow")}return this.each(function(){var org_elem=$(this);if(opts.content){var org_title=opts.content}else{var org_title=org_elem.attr(opts.attribute)}if(org_title!=""){if(!opts.content){org_elem.removeAttr(opts.attribute)}var timeout=false;if(opts.activation=="hover"){org_elem.hover(function(){active_tiptip()},function(){if(!opts.keepAlive){deactive_tiptip()}});if(opts.keepAlive){tiptip_holder.hover(function(){},function(){deactive_tiptip()})}}else if(opts.activation=="focus"){org_elem.focus(function(){active_tiptip()}).blur(function(){deactive_tiptip()})}else if(opts.activation=="click"){org_elem.click(function(){active_tiptip();return false}).hover(function(){},function(){if(!opts.keepAlive){deactive_tiptip()}});if(opts.keepAlive){tiptip_holder.hover(function(){},function(){deactive_tiptip()})}}function active_tiptip(){opts.enter.call(this);tiptip_content.html(org_title);tiptip_holder.hide().removeAttr("class").css("margin","0");tiptip_arrow.removeAttr("style");var top=parseInt(org_elem.offset()['top']);var left=parseInt(org_elem.offset()['left']);var org_width=parseInt(org_elem.outerWidth());var org_height=parseInt(org_elem.outerHeight());var tip_w=tiptip_holder.outerWidth();var tip_h=tiptip_holder.outerHeight();var w_compare=Math.round((org_width-tip_w)/2);var h_compare=Math.round((org_height-tip_h)/2);var marg_left=Math.round(left+w_compare);var marg_top=Math.round(top+org_height+opts.edgeOffset);var t_class="";var arrow_top="";var arrow_left=Math.round(tip_w-12)/2;if(opts.defaultPosition=="bottom"){t_class="_bottom"}else if(opts.defaultPosition=="top"){t_class="_top"}else if(opts.defaultPosition=="left"){t_class="_left"}else if(opts.defaultPosition=="right"){t_class="_right"}var right_compare=(w_compare+left)<parseInt($(window).scrollLeft());var left_compare=(tip_w+left)>parseInt($(window).width());if((right_compare&&w_compare<0)||(t_class=="_right"&&!left_compare)||(t_class=="_left"&&left<(tip_w+opts.edgeOffset+5))){t_class="_right";arrow_top=Math.round(tip_h-13)/2;arrow_left=-12;marg_left=Math.round(left+org_width+opts.edgeOffset);marg_top=Math.round(top+h_compare)}else if((left_compare&&w_compare<0)||(t_class=="_left"&&!right_compare)){t_class="_left";arrow_top=Math.round(tip_h-13)/2;arrow_left=Math.round(tip_w);marg_left=Math.round(left-(tip_w+opts.edgeOffset+5));marg_top=Math.round(top+h_compare)}var top_compare=(top+org_height+opts.edgeOffset+tip_h+8)>parseInt($(window).height()+$(window).scrollTop());var bottom_compare=((top+org_height)-(opts.edgeOffset+tip_h+8))<0;if(top_compare||(t_class=="_bottom"&&top_compare)||(t_class=="_top"&&!bottom_compare)){if(t_class=="_top"||t_class=="_bottom"){t_class="_top"}else{t_class=t_class+"_top"}arrow_top=tip_h;marg_top=Math.round(top-(tip_h+5+opts.edgeOffset))}else if(bottom_compare|(t_class=="_top"&&bottom_compare)||(t_class=="_bottom"&&!top_compare)){if(t_class=="_top"||t_class=="_bottom"){t_class="_bottom"}else{t_class=t_class+"_bottom"}arrow_top=-12;marg_top=Math.round(top+org_height+opts.edgeOffset)}if(t_class=="_right_top"||t_class=="_left_top"){marg_top=marg_top+5}else if(t_class=="_right_bottom"||t_class=="_left_bottom"){marg_top=marg_top-5}if(t_class=="_left_top"||t_class=="_left_bottom"){marg_left=marg_left+5}tiptip_arrow.css({"margin-left":arrow_left+"px","margin-top":arrow_top+"px"});tiptip_holder.css({"margin-left":marg_left+"px","margin-top":marg_top+"px"}).attr("class","tip"+t_class);if(timeout){clearTimeout(timeout)}timeout=setTimeout(function(){tiptip_holder.stop(true,true).fadeIn(opts.fadeIn)},opts.delay)}function deactive_tiptip(){opts.exit.call(this);if(timeout){clearTimeout(timeout)}tiptip_holder.fadeOut(opts.fadeOut)}}})}})(jQuery);
|
|
||||||
|
|
@ -1,124 +0,0 @@
|
||||||
This outlines the arguments passed by ltl2tgba.html to spot.py.
|
|
||||||
|
|
||||||
|
|
||||||
Specifying the formula to work with
|
|
||||||
|
|
||||||
f=... the formula
|
|
||||||
|
|
||||||
Formula simplifications (pick many)
|
|
||||||
|
|
||||||
r=br enable Basic Reductions
|
|
||||||
r=lf allow larger formulas
|
|
||||||
r=si enable Syntactic Implications
|
|
||||||
r=eu enable Eventuality and Universality
|
|
||||||
r=lc enable Language Containment
|
|
||||||
|
|
||||||
Choosing the desired output (pick one)
|
|
||||||
|
|
||||||
o=v output version (no other argument needed)
|
|
||||||
o=f output formula
|
|
||||||
o=m output monitor
|
|
||||||
o=a output automaton
|
|
||||||
o=r output run
|
|
||||||
o=t output testing automaton
|
|
||||||
o=v3 output LTL3BA's version (no other argument needed)
|
|
||||||
|
|
||||||
Type of formula output if o=f (pick one)
|
|
||||||
|
|
||||||
ff=o Spot syntax
|
|
||||||
ff=i Spin syntax
|
|
||||||
ff=l LBT syntax
|
|
||||||
ff=g graphviz output of the AST
|
|
||||||
ff=p property dump
|
|
||||||
|
|
||||||
Type of automaton if o=a (pick one)
|
|
||||||
|
|
||||||
af=t TGBA
|
|
||||||
af=s SBA
|
|
||||||
af=i Spin neverclaim
|
|
||||||
|
|
||||||
Type of monitor if o=m (pick one)
|
|
||||||
|
|
||||||
mf=d deterministic
|
|
||||||
mf=n nondeterministic
|
|
||||||
|
|
||||||
Type of automaton for run if o=r (pick one)
|
|
||||||
|
|
||||||
ra=t run on TGBA
|
|
||||||
ra=s run on SBA
|
|
||||||
|
|
||||||
Type of run output if o=r (pick one)
|
|
||||||
|
|
||||||
rf=p print run as text
|
|
||||||
rf=d draw run
|
|
||||||
|
|
||||||
Type of testing automaton if o=t (pick one)
|
|
||||||
|
|
||||||
tf=t TA
|
|
||||||
tf=g GTA
|
|
||||||
tf=a TGTA
|
|
||||||
|
|
||||||
Translator algorithm (pick one)
|
|
||||||
|
|
||||||
t=fm Couvreur/FM
|
|
||||||
t=la Couvreur/LaCIM
|
|
||||||
t=ta Tauriainen/TAA
|
|
||||||
t=l3 LTL3BA
|
|
||||||
t=cs Compositional Suspension
|
|
||||||
|
|
||||||
Couvreur/FM options if t=fm (pick many)
|
|
||||||
|
|
||||||
fm=od Optimize Determinism
|
|
||||||
fm=sm Symbolic Merge
|
|
||||||
fm=bp Branching Postponement
|
|
||||||
fm=fl Fair-Loop approximations
|
|
||||||
|
|
||||||
Couvreur/LA options if t=la
|
|
||||||
|
|
||||||
la=sp Symbolic Pruning
|
|
||||||
|
|
||||||
Tauriainen/TAA options if t=ta
|
|
||||||
|
|
||||||
ta=lc refined rules based on Language Containment
|
|
||||||
|
|
||||||
LTL3BA output options if t=l3 (pick one)
|
|
||||||
|
|
||||||
lo=T output a TGBA
|
|
||||||
lo=U output a BA
|
|
||||||
|
|
||||||
LTL3BA processing options if t=l3 (pick many)
|
|
||||||
|
|
||||||
l3=l LTL formula simplification
|
|
||||||
l3=P suspension in TGBA construction
|
|
||||||
l3=A suspension in alternating automaton construction
|
|
||||||
l3=C SCC simplifications
|
|
||||||
l3=M more deterministic output
|
|
||||||
l3=S direct simulation
|
|
||||||
l3=o on-the-fly simplifications
|
|
||||||
l3=p a-posteriori simplifications
|
|
||||||
|
|
||||||
Compositional Suspension options (pick many)
|
|
||||||
|
|
||||||
cs=w WDBA minimization
|
|
||||||
cs=s simulation
|
|
||||||
cs=e early start of suspended automatas
|
|
||||||
cs=c do not compose suspended formulae (for debugging)
|
|
||||||
cs=o compose obligation subformulae
|
|
||||||
|
|
||||||
Automaton simplifications (pick many)
|
|
||||||
|
|
||||||
as=ps Prune SCC
|
|
||||||
as=wd WDBA minimiztion
|
|
||||||
as=ds Direct Simulation reduction
|
|
||||||
as=rs Reverse Simulation reduction
|
|
||||||
as=is Iterated Simulation reduction (disables ds and rs)
|
|
||||||
|
|
||||||
Testing Automaton options (pick many)
|
|
||||||
|
|
||||||
to=l add a catch-all livelock state
|
|
||||||
to=s produce single-pass variant
|
|
||||||
to=m merge bisimilar states
|
|
||||||
|
|
||||||
Global options
|
|
||||||
|
|
||||||
g=8 Enable UTF-8 output.
|
|
||||||
|
|
@ -1,827 +0,0 @@
|
||||||
#!@PYTHON@
|
|
||||||
# -*- mode: python; coding: utf-8 -*-
|
|
||||||
# Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de
|
|
||||||
# Recherche et Développement de l'Epita (LRDE).
|
|
||||||
#
|
|
||||||
# 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
|
|
||||||
|
|
||||||
import os
|
|
||||||
import sys
|
|
||||||
|
|
||||||
script = ('SCRIPT_NAME' in os.environ)
|
|
||||||
|
|
||||||
if script:
|
|
||||||
# 3600s = 1h
|
|
||||||
sys.stdout.write("""Cache-Control: max-age=3600
|
|
||||||
Content-Type: text/html
|
|
||||||
|
|
||||||
""")
|
|
||||||
|
|
||||||
# Directory for temporary files (images and other auxiliary files).
|
|
||||||
imgdir = 'spotimg'
|
|
||||||
|
|
||||||
# Cache lookup for the QUERY_STRING
|
|
||||||
qs = os.getenv('QUERY_STRING')
|
|
||||||
if qs:
|
|
||||||
import hashlib
|
|
||||||
# We (optimistically) assume no collision from sha1(qs)
|
|
||||||
cachedir = imgdir + '/' + hashlib.sha1(qs.encode('utf-8')).hexdigest()
|
|
||||||
cachename = cachedir + '/html'
|
|
||||||
try:
|
|
||||||
# Is this a request we have already processed?
|
|
||||||
cache = open(cachename, "rb", 0)
|
|
||||||
if hasattr(sys.stdout, 'buffer'):
|
|
||||||
# Python 3+
|
|
||||||
sys.stdout.flush()
|
|
||||||
sys.stdout.buffer.write(cache.read())
|
|
||||||
else:
|
|
||||||
# Python 2.x
|
|
||||||
sys.stdout.write(cache.read())
|
|
||||||
# Touch the directory containing the files we used, so
|
|
||||||
# it that it survives the browser's cache.
|
|
||||||
os.utime(cachedir, None)
|
|
||||||
exit(0)
|
|
||||||
except IOError:
|
|
||||||
# We failed to open the file.
|
|
||||||
# Let's run the rest of the script to create it.
|
|
||||||
pass
|
|
||||||
elif script:
|
|
||||||
sys.stdout.write("<b>QUERY_STRING unset!</b>\n")
|
|
||||||
exit(0)
|
|
||||||
|
|
||||||
# Location of the dot command
|
|
||||||
dot = '@DOT@'
|
|
||||||
dot_bgcolor = '-Gbgcolor=#FFFFFF00'
|
|
||||||
|
|
||||||
svg_output = False # SVG output used to working well with Firefox
|
|
||||||
# only. It now seems to work with recent Chrome
|
|
||||||
# versions as well, but it is still a problem with
|
|
||||||
# Safari, and IE.
|
|
||||||
output_both = True # Create both PNG and SVG. If svg_output is False,
|
|
||||||
# the SVG will be given as a link under the PNG.
|
|
||||||
# Otherwise the PNG is used as alternate contents
|
|
||||||
# for the SVG object.
|
|
||||||
|
|
||||||
if not script:
|
|
||||||
# If this is not run as a cgi script, let's start an HTTP server.
|
|
||||||
try:
|
|
||||||
# Python 3+
|
|
||||||
from http.server import CGIHTTPRequestHandler, HTTPServer
|
|
||||||
except ImportError:
|
|
||||||
# Python 2.x
|
|
||||||
from CGIHTTPServer import CGIHTTPRequestHandler
|
|
||||||
from BaseHTTPServer import HTTPServer
|
|
||||||
|
|
||||||
class MyHandler(CGIHTTPRequestHandler):
|
|
||||||
def is_cgi(self):
|
|
||||||
if self.path.startswith('/cgi-bin/spotcgi.py'):
|
|
||||||
self.cgi_info = '', self.path[9:]
|
|
||||||
return True
|
|
||||||
return False
|
|
||||||
MyHandler.extensions_map[".hoa"] = 'text/x-hoa'
|
|
||||||
|
|
||||||
server_address=('', 8000)
|
|
||||||
if not os.access(imgdir, os.F_OK):
|
|
||||||
# 493 = 0755 but we would have to write 0755 or 0o755
|
|
||||||
# depending on the python version...
|
|
||||||
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/trans.html\n")
|
|
||||||
httpd.serve_forever()
|
|
||||||
|
|
||||||
import cgi
|
|
||||||
import signal
|
|
||||||
import time
|
|
||||||
import os.path
|
|
||||||
|
|
||||||
# We do not output in cachedir directely, in case two
|
|
||||||
# CGI scripts process the same request concurrently.
|
|
||||||
tmpdir = cachedir + '-' + str(os.getpid())
|
|
||||||
cachename = tmpdir + '/html'
|
|
||||||
|
|
||||||
sys.stdout.flush()
|
|
||||||
# Reopen stdout without buffering
|
|
||||||
sys.stdout = os.fdopen(sys.stdout.fileno(), "wb", 0)
|
|
||||||
|
|
||||||
# Redirect stderr to stdout at a low level (so that
|
|
||||||
# even errors from subprocesses get printed).
|
|
||||||
os.dup2(sys.stdout.fileno(), sys.stderr.fileno())
|
|
||||||
|
|
||||||
import cgitb
|
|
||||||
sys.excepthook = cgitb.Hook(file=sys.stderr)
|
|
||||||
|
|
||||||
# Create the temporary cache directory
|
|
||||||
os.mkdir(tmpdir, 493) # See comment above about 0o755 or 0755.
|
|
||||||
|
|
||||||
# Redirect stdout to the cache file, at a low level
|
|
||||||
# for similar reason.
|
|
||||||
fd = os.open(cachename, os.O_CREAT | os.O_WRONLY, 420) # 420 = 0644
|
|
||||||
os.dup2(fd, sys.stdout.fileno())
|
|
||||||
|
|
||||||
# We had to reopen stdout in binary mode to enable unbuffered output,
|
|
||||||
# (disallowed on text I/O by Python 3.x) so starting now, we are not
|
|
||||||
# allowed to send strings to sys.stdout. Always use the following
|
|
||||||
# method instead.
|
|
||||||
def unbufprint(s):
|
|
||||||
if sys.getdefaultencoding() != 'ascii' and type(s) != bytes:
|
|
||||||
sys.stdout.write(s.encode("utf-8"))
|
|
||||||
else:
|
|
||||||
sys.stdout.write(s)
|
|
||||||
|
|
||||||
def finish(kill = False):
|
|
||||||
# Output the result and exit.
|
|
||||||
os.dup2(sys.stderr.fileno(), sys.stdout.fileno())
|
|
||||||
|
|
||||||
cache = open(cachename, "rb", 0)
|
|
||||||
sys.stdout.write(cache.read())
|
|
||||||
|
|
||||||
# Rename tmpdir to its permanent name for caching purpose.
|
|
||||||
# os.rename will fail if cachedir already exist. Since we tested
|
|
||||||
# that initially, it can only happen when two CGI script are
|
|
||||||
# processing the same request concurrently. In that case the
|
|
||||||
# other result is as good as ours, so we just ignore the error.
|
|
||||||
# (We don't bother removing the temporary directory -- it will be
|
|
||||||
# removed by the next cache prune and cannot be created again in
|
|
||||||
# the meantime.)
|
|
||||||
try:
|
|
||||||
os.rename(tmpdir, cachedir)
|
|
||||||
except OSError:
|
|
||||||
pass
|
|
||||||
|
|
||||||
if kill:
|
|
||||||
# Kill all children
|
|
||||||
os.killpg(child, signal.SIGTERM)
|
|
||||||
# Should we prune the cache?
|
|
||||||
stamp = imgdir + '/cache.stamp'
|
|
||||||
now = time.time()
|
|
||||||
try:
|
|
||||||
# Prune at most once every hour
|
|
||||||
if now - os.path.getmtime(stamp) < 3600:
|
|
||||||
exit(0)
|
|
||||||
except OSError:
|
|
||||||
# It's OK if the file did not exist.
|
|
||||||
# We will create it.
|
|
||||||
pass
|
|
||||||
# Erase all directories that are older than 2 hours, and all
|
|
||||||
# files that have only one hardlinks. Files that have more than
|
|
||||||
# one hardlinks are referenced to by directories; so the hardlink
|
|
||||||
# count will decrease when the directory is purged.
|
|
||||||
os.system('find ' + imgdir + ' -mindepth 1 -maxdepth 1 -mmin +120 '
|
|
||||||
+ '\( -type d -o -links 1 \) -exec rm -rf {} +')
|
|
||||||
# Create or update the stamp so we know when to run the next prune.
|
|
||||||
open(stamp, "wb", 0)
|
|
||||||
exit(0)
|
|
||||||
|
|
||||||
# Assume Spot is installed
|
|
||||||
sys.path.insert(0, '@pythondir@')
|
|
||||||
|
|
||||||
if ('SERVER_SOFTWARE' in os.environ and
|
|
||||||
os.environ['SERVER_SOFTWARE'].startswith('SimpleHTTP')):
|
|
||||||
# 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, '../.libs')
|
|
||||||
sys.path.insert(0, '../spot/.libs')
|
|
||||||
sys.path.insert(0, '..')
|
|
||||||
|
|
||||||
try:
|
|
||||||
# execfile('ltl2tgba.opt') no longuer work with Python 3.
|
|
||||||
exec(compile(open("ltl2tgba.opt").read(), "ltl2tgba.opt", 'exec'))
|
|
||||||
except IOError:
|
|
||||||
pass
|
|
||||||
|
|
||||||
import spot
|
|
||||||
import buddy
|
|
||||||
|
|
||||||
spot.setup(size='8.2,8.2',fillcolor='#FDEDD3')
|
|
||||||
|
|
||||||
def alarm_handler(signum, frame):
|
|
||||||
unbufprint("""<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.
|
|
||||||
If you want to benchmark big formulae it is
|
|
||||||
better to install Spot on your own computer.</p>\n""")
|
|
||||||
finish(kill=True)
|
|
||||||
|
|
||||||
def run_dot(basename, ext):
|
|
||||||
outname = basename + '.' + ext
|
|
||||||
# Do not call "dot" to generate a file that already exists.
|
|
||||||
if not os.access(outname, os.F_OK):
|
|
||||||
os.spawnlp(os.P_WAIT, dot, dot, dot_bgcolor, '-T' + ext,
|
|
||||||
'-o', outname, basename + '.txt')
|
|
||||||
# Create a unused hardlink that points to the output picture
|
|
||||||
# just to remember how many cache entries are sharing it.
|
|
||||||
os.link(outname, tmpdir + "/" + ext)
|
|
||||||
|
|
||||||
def render_dot(basename, hoaname = None):
|
|
||||||
unbufprint('<div class="dot">')
|
|
||||||
b = cgi.escape(basename)
|
|
||||||
|
|
||||||
if svg_output or output_both:
|
|
||||||
run_dot(basename, 'svg')
|
|
||||||
if not svg_output or output_both:
|
|
||||||
run_dot(basename, 'png')
|
|
||||||
pngstr = '<img src="' + b + '.png">'
|
|
||||||
|
|
||||||
if svg_output:
|
|
||||||
unbufprint('<object type="image/svg+xml" data="' + b + '.svg">')
|
|
||||||
if output_both:
|
|
||||||
unbufprint(pngstr)
|
|
||||||
else:
|
|
||||||
unbufprint('Your browser does not support SVG.')
|
|
||||||
unbufprint('</object>' + '<br>(<a href="' + b
|
|
||||||
+ '.txt">dot</a>)')
|
|
||||||
else:
|
|
||||||
unbufprint('<img src="' + b + '.png"><br>(<a href="' + b
|
|
||||||
+ '.txt">dot</a>)')
|
|
||||||
if output_both:
|
|
||||||
unbufprint(' (<a href="' + b + '.svg">svg</a>)')
|
|
||||||
if hoaname:
|
|
||||||
unbufprint(' (<a href="' + hoaname + '">hoa</a>)')
|
|
||||||
unbufprint('</div>\n')
|
|
||||||
|
|
||||||
def save_hoa(automaton):
|
|
||||||
hoasrc = spot.ostringstream()
|
|
||||||
spot.print_hoa(hoasrc, automaton, 't' if buchi_type == 't' else '')
|
|
||||||
hoasrc = hoasrc.str()
|
|
||||||
hoasrc += '\n'
|
|
||||||
if sys.getdefaultencoding() != 'ascii':
|
|
||||||
hoasrc = hoasrc.encode('utf-8')
|
|
||||||
autprefix = (imgdir + '/' + hashlib.sha1(hoasrc).hexdigest())
|
|
||||||
hoaname = autprefix + '.hoa'
|
|
||||||
if not os.access(hoaname, os.F_OK):
|
|
||||||
hoaout = open(hoaname, "wb", 0)
|
|
||||||
hoaout.write(hoasrc)
|
|
||||||
hoaout.close()
|
|
||||||
# Create a unused hardlink that points to the output HOA
|
|
||||||
# just to remember how many cache entries are sharing it.
|
|
||||||
os.link(hoaname, tmpdir + "/hoa")
|
|
||||||
return hoaname
|
|
||||||
|
|
||||||
def render_dot_maybe(dotsrc, dont_run_dot, hoaname = None):
|
|
||||||
# The dot output is named after the SHA1 of the dot source.
|
|
||||||
# This way we can cache two different requests that generate
|
|
||||||
# the same automaton (e.g., when changing a simplification
|
|
||||||
# option that has no influence).
|
|
||||||
if sys.getdefaultencoding() != 'ascii':
|
|
||||||
dotsrc = dotsrc.encode('utf-8')
|
|
||||||
# If the text rendering engine (usually Pango) used by dot does
|
|
||||||
# not draw overlines correctly, uncomment the following two
|
|
||||||
# lines. Pango 1.28.4 seems not to support combining overline
|
|
||||||
# while 1.30 does.
|
|
||||||
#import re
|
|
||||||
#dotsrc = re.sub(r'(.)(̅|̄)', r'¬\1', dotsrc);
|
|
||||||
autprefix = (imgdir + '/' + hashlib.sha1(dotsrc).hexdigest())
|
|
||||||
dotname = autprefix + '.txt'
|
|
||||||
if not os.access(dotname, os.F_OK):
|
|
||||||
dotout = open(dotname, "wb", 0)
|
|
||||||
dotout.write(dotsrc)
|
|
||||||
dotout.close()
|
|
||||||
# Create a unused hardlink that points to the output picture
|
|
||||||
# just to remember how many cache entries are sharing it.
|
|
||||||
os.link(dotname, tmpdir + "/txt")
|
|
||||||
|
|
||||||
if dont_run_dot:
|
|
||||||
unbufprint('<p>' + dont_run_dot + ''' to be rendered on-line.
|
|
||||||
However you may download the <a href="''' + cgi.escape(autprefix)
|
|
||||||
+ '.txt">source in dot format</a> and render it yourself.</p>\n')
|
|
||||||
else:
|
|
||||||
render_dot(autprefix, hoaname)
|
|
||||||
|
|
||||||
def render_automaton(automaton, dont_run_dot):
|
|
||||||
hoaname = None
|
|
||||||
dotsrc = spot.ostringstream()
|
|
||||||
if isinstance(automaton, spot.ta): # TA/GTA
|
|
||||||
spot.print_dot(dotsrc, automaton)
|
|
||||||
elif hasattr(automaton, 'get_ta'): # TGTA
|
|
||||||
spot.print_dot(dotsrc, automaton.get_ta())
|
|
||||||
else: # TGBA
|
|
||||||
if not dont_run_dot:
|
|
||||||
hoaname = save_hoa(automaton)
|
|
||||||
spot.print_dot(dotsrc, automaton, '.t' if buchi_type == 't' else '.')
|
|
||||||
render_dot_maybe(dotsrc.str(), dont_run_dot, hoaname)
|
|
||||||
|
|
||||||
def render_formula(f):
|
|
||||||
dotsrc = spot.ostringstream()
|
|
||||||
spot.print_dot_psl(dotsrc, f)
|
|
||||||
render_dot_maybe(dotsrc.str(), False)
|
|
||||||
|
|
||||||
def print_stats(automaton, detinfo = False, ta = False):
|
|
||||||
if ta: # TA/GTA
|
|
||||||
if hasattr(automaton, 'get_ta'): # TGTA
|
|
||||||
automaton = automaton.get_ta()
|
|
||||||
stats = spot.stats_reachable(automaton)
|
|
||||||
detinfo = False
|
|
||||||
else:
|
|
||||||
if (buchi_type == 't' and automaton.prop_inherently_weak() and
|
|
||||||
automaton.acc().is_buchi()):
|
|
||||||
unbufprint("Note: this is a weak automaton, using transition-based "
|
|
||||||
"or generalized acceptance does not bring any benefit."
|
|
||||||
"</br>")
|
|
||||||
stats = spot.sub_stats_reachable(automaton)
|
|
||||||
unbufprint("<p>%d state" % stats.states)
|
|
||||||
if stats.states > 1:
|
|
||||||
unbufprint("s")
|
|
||||||
if detinfo:
|
|
||||||
nondet = spot.count_nondet_states(automaton)
|
|
||||||
if nondet == 0:
|
|
||||||
unbufprint(" (deterministic)")
|
|
||||||
else:
|
|
||||||
unbufprint(" (%d nondeterministic)" % nondet)
|
|
||||||
if not hasattr(stats, 'transitions'):
|
|
||||||
unbufprint(", %d edge" % stats.edges)
|
|
||||||
if stats.edges > 1:
|
|
||||||
unbufprint("s")
|
|
||||||
else:
|
|
||||||
unbufprint(", %d edge%s (%d transition%s)"
|
|
||||||
% (stats.edges, 's' if stats.edges > 1 else '',
|
|
||||||
stats.transitions, 's' if stats.transitions > 1 else ''))
|
|
||||||
if hasattr(automaton, 'get_acceptance'):
|
|
||||||
acc = automaton.get_acceptance()
|
|
||||||
if (automaton.is_sba() and automaton.acc().is_buchi() and
|
|
||||||
buchi_type != 't'):
|
|
||||||
unbufprint(", acceptance condition: Büchi")
|
|
||||||
else:
|
|
||||||
unbufprint(", acceptance condition: " + str(acc))
|
|
||||||
if acc.is_t():
|
|
||||||
unbufprint(" (all cycles are accepting)")
|
|
||||||
unbufprint("</p>\n")
|
|
||||||
# Decide whether we will render the automaton or not.
|
|
||||||
# (A webserver is not a computation center...)
|
|
||||||
if stats.states > 64:
|
|
||||||
return "Automaton has too many states"
|
|
||||||
if float(stats.edges)/stats.states > 10:
|
|
||||||
return "Automaton has too many edges per state"
|
|
||||||
return False
|
|
||||||
|
|
||||||
def format_formula(f, kind='div'):
|
|
||||||
if utf8:
|
|
||||||
s = f.to_str('utf8')
|
|
||||||
else:
|
|
||||||
s = f.to_str()
|
|
||||||
return '<%s class="formula spot-format">%s</%s>' % (kind, s, kind)
|
|
||||||
|
|
||||||
form = cgi.FieldStorage()
|
|
||||||
|
|
||||||
output_type = form.getfirst('o', 'v');
|
|
||||||
|
|
||||||
# Version requested.
|
|
||||||
if output_type == 'v':
|
|
||||||
unbufprint('Spot version %s\n' % spot.version())
|
|
||||||
finish()
|
|
||||||
|
|
||||||
# ltl3ba's version
|
|
||||||
if output_type == 'v3':
|
|
||||||
import subprocess
|
|
||||||
try:
|
|
||||||
l3proc = subprocess.Popen(['@LTL3BA@', '-v'], stdout=subprocess.PIPE)
|
|
||||||
(ver, err) = l3proc.communicate()
|
|
||||||
# -M[0|1] is new in 1.1.1, and we use it.
|
|
||||||
l3proc = subprocess.Popen(['@LTL3BA@', '-h'], stdout=subprocess.PIPE)
|
|
||||||
(out, err) = l3proc.communicate()
|
|
||||||
if out.find(b'-M[') < 0:
|
|
||||||
err = 1
|
|
||||||
else:
|
|
||||||
err = 0
|
|
||||||
except:
|
|
||||||
err = 1
|
|
||||||
if err != 0:
|
|
||||||
unbufprint('not available')
|
|
||||||
else:
|
|
||||||
unbufprint(ver.replace(b"\n", b"<br>"))
|
|
||||||
finish()
|
|
||||||
|
|
||||||
spot.unblock_signal(signal.SIGALRM)
|
|
||||||
spot.unblock_signal(signal.SIGTERM)
|
|
||||||
|
|
||||||
child = os.fork()
|
|
||||||
if child != 0:
|
|
||||||
# In parent. We are just waiting for the termination of the
|
|
||||||
# child, or for the timeout alarm. On SIGALRM, we will kill the
|
|
||||||
# child.
|
|
||||||
#
|
|
||||||
# We cannot avoid forking, because Python will not deliver a
|
|
||||||
# signal when a C function is running. So if Spot takes too long
|
|
||||||
# to translate some formula, it would not get interrupted.
|
|
||||||
signal.signal(signal.SIGALRM, alarm_handler)
|
|
||||||
signal.alarm(30)
|
|
||||||
os.waitpid(child, 0)
|
|
||||||
exit(0)
|
|
||||||
|
|
||||||
os.setpgrp()
|
|
||||||
|
|
||||||
# Global options
|
|
||||||
utf8 = False
|
|
||||||
for g in form.getlist('g'):
|
|
||||||
if g == '8':
|
|
||||||
utf8 = True
|
|
||||||
spot.enable_utf8()
|
|
||||||
|
|
||||||
formula = form.getfirst('f', '')
|
|
||||||
|
|
||||||
env = spot.default_environment.instance()
|
|
||||||
pf = spot.parse_infix_psl(formula, env)
|
|
||||||
f = pf.f
|
|
||||||
|
|
||||||
if pf.errors:
|
|
||||||
# Try the LBT parser in case someone is throwing LBT formulas at us.
|
|
||||||
pg = spot.parse_prefix_ltl(formula, env)
|
|
||||||
if pg.errors:
|
|
||||||
unbufprint('<div class="parse-error">')
|
|
||||||
err = pf.format_errors(spot.get_cout())
|
|
||||||
unbufprint('</div>')
|
|
||||||
else:
|
|
||||||
f = pg.f
|
|
||||||
|
|
||||||
# Do not continue if we could not parse anything sensible.
|
|
||||||
if not f:
|
|
||||||
finish()
|
|
||||||
|
|
||||||
# Formula simplifications
|
|
||||||
simpopt = spot.tl_simplifier_options(False, False, False,
|
|
||||||
False, False, False, True)
|
|
||||||
dored = False
|
|
||||||
for r in form.getlist('r'):
|
|
||||||
dored = True
|
|
||||||
if r == 'br':
|
|
||||||
simpopt.reduce_basics = True
|
|
||||||
elif r == 'lf':
|
|
||||||
simpopt.reduce_size_strictly = False
|
|
||||||
elif r == 'si':
|
|
||||||
simpopt.synt_impl = True
|
|
||||||
elif r == 'eu':
|
|
||||||
simpopt.event_univ = True
|
|
||||||
elif r == 'lc':
|
|
||||||
simpopt.containment_checks = True
|
|
||||||
simpopt.containment_checks_stronger = True
|
|
||||||
if dored:
|
|
||||||
# Not keeping the ltl simplifier aive will also clear the as_bdd()
|
|
||||||
# cache.
|
|
||||||
f = spot.tl_simplifier(simpopt).simplify(f)
|
|
||||||
|
|
||||||
# Formula manipulation only.
|
|
||||||
if output_type == 'f':
|
|
||||||
formula_format = form.getfirst('ff', 'o')
|
|
||||||
# o = Spot, i = Spin, l = LBT, g = GraphViz, p = properties
|
|
||||||
if formula_format == 'o':
|
|
||||||
unbufprint(format_formula(f))
|
|
||||||
elif formula_format == 'i':
|
|
||||||
unbufprint('<div class="formula spin-format">'
|
|
||||||
+ spot.str_spin_ltl(f) + '</div>')
|
|
||||||
if f.is_psl_formula() and not f.is_ltl_formula():
|
|
||||||
s = ''
|
|
||||||
if simpopt.reduce_size_strictly:
|
|
||||||
s = '<br><b>Try enabling larger formula rewritings.</b>'
|
|
||||||
unbufprint('<div class="error">The above formula contains PSL operators that Spin will not understand.%s</div>' % s)
|
|
||||||
elif formula_format == 'l':
|
|
||||||
if not f.is_ltl_formula():
|
|
||||||
unbufprint('<div class="error">PSL formulas cannot be expressed in this format.</div>')
|
|
||||||
else:
|
|
||||||
unbufprint('<div class="formula lbt-format">' + spot.str_lbt_ltl(f) + '</div>')
|
|
||||||
elif formula_format == 'g':
|
|
||||||
render_formula(f)
|
|
||||||
elif formula_format == 'p':
|
|
||||||
if utf8:
|
|
||||||
s = spot.str_utf8_psl(f)
|
|
||||||
else:
|
|
||||||
s = str(f)
|
|
||||||
unbufprint('Properties for ' + format_formula(f, 'span') + '<ul>\n')
|
|
||||||
unbufprint('<div style="float:right">' +
|
|
||||||
spot.mp_hierarchy_svg(f) + '</div>')
|
|
||||||
for p in spot.list_formula_props(f):
|
|
||||||
unbufprint('<li>%s</li>\n' % p)
|
|
||||||
|
|
||||||
if not f.is_syntactic_stutter_invariant():
|
|
||||||
if spot.is_stutter_invariant(f):
|
|
||||||
unbufprint('<li>stutter invariant</li>')
|
|
||||||
else:
|
|
||||||
unbufprint('<li>stutter sensitive</li>')
|
|
||||||
unbufprint('</ul>\n')
|
|
||||||
finish()
|
|
||||||
|
|
||||||
# Formula translation.
|
|
||||||
translator = form.getfirst('t', 'fm')
|
|
||||||
|
|
||||||
if f.is_psl_formula() and not f.is_ltl_formula() and translator != 'fm':
|
|
||||||
unbufprint('''<div class="error">The PSL formula %s
|
|
||||||
cannot be translated using this algorithm. Please use Couveur/FM.'''
|
|
||||||
% format_formula(f, 'span'))
|
|
||||||
finish()
|
|
||||||
|
|
||||||
dict = spot.make_bdd_dict()
|
|
||||||
|
|
||||||
if output_type == 't' and not spot.is_stutter_invariant(f):
|
|
||||||
unbufprint('<b>Warning:</b> Testing automata are only valid '
|
|
||||||
+ 'for stutter-insensitive formulas, but the input is not.</br>')
|
|
||||||
|
|
||||||
# Should the automaton be displayed as a SBA?
|
|
||||||
issba = False
|
|
||||||
|
|
||||||
if translator == 'fm':
|
|
||||||
exprop = False
|
|
||||||
symb_merge = False
|
|
||||||
branching_postponement = False
|
|
||||||
fair_loop_approx = False
|
|
||||||
for fm in form.getlist('fm'):
|
|
||||||
if fm == 'od':
|
|
||||||
exprop = True
|
|
||||||
elif fm == 'sm':
|
|
||||||
symb_merge = True
|
|
||||||
elif fm == 'bp':
|
|
||||||
branching_postponement = True
|
|
||||||
elif fm == 'fl':
|
|
||||||
fair_loop_approx = True
|
|
||||||
automaton = spot.ltl_to_tgba_fm(f, dict,
|
|
||||||
exprop, symb_merge,
|
|
||||||
branching_postponement, fair_loop_approx)
|
|
||||||
elif translator == 'ta':
|
|
||||||
refined_rules = False
|
|
||||||
if form.getfirst('ta', '') == 'lc':
|
|
||||||
refined_rules = True
|
|
||||||
automaton = spot.ensure_digraph(spot.ltl_to_taa(f, dict, refined_rules))
|
|
||||||
|
|
||||||
elif translator == 'l3':
|
|
||||||
l3out = '-H2'
|
|
||||||
# 1.0.1 had determinization and simulation turned off by default,
|
|
||||||
# we need -M0 and -S0 with 1.1.1 for the same effect
|
|
||||||
l3opt = { '-l', '-P', '-A', '-c', '-C', '-o', '-p', '-M0', '-S0' }
|
|
||||||
for lo in form.getfirst('lo', 'T'):
|
|
||||||
if lo == 'U':
|
|
||||||
l3out = '-H3'
|
|
||||||
issba = True
|
|
||||||
for l3 in form.getlist('l3'):
|
|
||||||
if l3 == 'l':
|
|
||||||
l3opt.remove('-l')
|
|
||||||
elif l3 == 'P':
|
|
||||||
l3opt.remove('-P')
|
|
||||||
elif l3 == 'A':
|
|
||||||
l3opt.remove('-A')
|
|
||||||
elif l3 == 'C':
|
|
||||||
l3opt.remove('-C')
|
|
||||||
l3opt.remove('-c')
|
|
||||||
elif l3 == 'M':
|
|
||||||
l3opt.remove('-M0')
|
|
||||||
l3opt.add('-M1')
|
|
||||||
elif l3 == 'S':
|
|
||||||
l3opt.remove('-S0')
|
|
||||||
l3opt.add('-S2') # was -S in 1.0.1
|
|
||||||
elif l3 == 'o':
|
|
||||||
l3opt.remove('-o')
|
|
||||||
elif l3 == 'p':
|
|
||||||
l3opt.remove('-p')
|
|
||||||
args = ["@LTL3BA@", l3out]
|
|
||||||
args.extend(l3opt)
|
|
||||||
# Relabel the formula in case it contains unsupported atomic
|
|
||||||
# propositions (e.g., starting with _ or double-quoted).
|
|
||||||
m = spot.relabeling_map()
|
|
||||||
g = spot.relabel(f, spot.Pnn, m)
|
|
||||||
args.extend(['-f', "'" + spot.str_spin_ltl(g) + "' |"])
|
|
||||||
try:
|
|
||||||
automaton = spot.automaton(" ".join(args), no_sid=True)
|
|
||||||
except RuntimeError as e:
|
|
||||||
unbufprint('<div class="error">{}</div>'.format(e))
|
|
||||||
finish()
|
|
||||||
spot.relabel_here(automaton, m)
|
|
||||||
elif translator == 'cs':
|
|
||||||
donot_inject = False
|
|
||||||
cs_nowdba = True
|
|
||||||
cs_nosimul = True
|
|
||||||
cs_early_start = False
|
|
||||||
for cs in form.getlist('cs'):
|
|
||||||
if cs == 'c':
|
|
||||||
donot_inject = True
|
|
||||||
elif cs == 'w':
|
|
||||||
cs_nowdba = False
|
|
||||||
elif cs == 's':
|
|
||||||
cs_nosimul = False
|
|
||||||
elif cs == 'e':
|
|
||||||
cs_early_start = True
|
|
||||||
|
|
||||||
automaton = spot.compsusp(f, dict, cs_nowdba, cs_nosimul,
|
|
||||||
cs_early_start, donot_inject)
|
|
||||||
else:
|
|
||||||
unbufprint('''<div class="error">unsupported translator</div>''')
|
|
||||||
finish()
|
|
||||||
|
|
||||||
buchi_type = None
|
|
||||||
|
|
||||||
# Monitor output
|
|
||||||
if output_type == 'm':
|
|
||||||
issba = True
|
|
||||||
mf = form.getfirst('mf', 'd')
|
|
||||||
pp = spot.postprocessor()
|
|
||||||
pp.set_type(spot.postprocessor.Monitor)
|
|
||||||
if mf == 'd':
|
|
||||||
pp.set_pref(spot.postprocessor.Deterministic)
|
|
||||||
elif mf == 'n':
|
|
||||||
pp.set_pref(spot.postprocessor.Small)
|
|
||||||
automaton = pp.run(automaton, f)
|
|
||||||
unbufprint('<div class="automata-stats">')
|
|
||||||
dont_run_dot = print_stats(automaton)
|
|
||||||
unbufprint('</div>')
|
|
||||||
automaton.set_name(str(f))
|
|
||||||
render_automaton(automaton, dont_run_dot)
|
|
||||||
automaton = 0
|
|
||||||
finish()
|
|
||||||
|
|
||||||
# Automaton simplifications
|
|
||||||
prune_scc = False
|
|
||||||
wdba_minimize = False
|
|
||||||
direct_simul = False
|
|
||||||
reverse_simul = False
|
|
||||||
iterated_simul = False
|
|
||||||
for s in form.getlist('as'):
|
|
||||||
if s == 'ps':
|
|
||||||
prune_scc = True
|
|
||||||
elif s == 'wd':
|
|
||||||
wdba_minimize = True
|
|
||||||
elif s == 'ds':
|
|
||||||
direct_simul = True
|
|
||||||
elif s == 'rs':
|
|
||||||
reverse_simul = True
|
|
||||||
elif s == 'is':
|
|
||||||
iterated_simul = True
|
|
||||||
|
|
||||||
ta_type = None
|
|
||||||
|
|
||||||
if output_type == 'a':
|
|
||||||
buchi_type = form.getfirst('af', 't')
|
|
||||||
elif output_type == 'r':
|
|
||||||
buchi_type = form.getfirst('ra', 't')
|
|
||||||
elif output_type == 't':
|
|
||||||
ta_type = form.getfirst('tf', 't')
|
|
||||||
else:
|
|
||||||
unbufprint("Unkown output type 'o=%s'.\n" % output_type)
|
|
||||||
automaton = 0
|
|
||||||
finish()
|
|
||||||
|
|
||||||
degen = False
|
|
||||||
neverclaim = False
|
|
||||||
|
|
||||||
if buchi_type == 's' or ta_type == 't':
|
|
||||||
degen = True
|
|
||||||
elif buchi_type == 'i':
|
|
||||||
degen = True
|
|
||||||
neverclaim = True
|
|
||||||
|
|
||||||
if output_type == 't' and ta_type == 't':
|
|
||||||
degen = True
|
|
||||||
|
|
||||||
if prune_scc:
|
|
||||||
# Do not suppress all useless acceptance conditions if
|
|
||||||
# degeneralization or simulation is requested: keeping those that
|
|
||||||
# lead to accepting states usually helps.
|
|
||||||
automaton = spot.scc_filter(automaton, not (degen
|
|
||||||
or direct_simul
|
|
||||||
or reverse_simul
|
|
||||||
or iterated_simul))
|
|
||||||
|
|
||||||
if wdba_minimize:
|
|
||||||
minimized = spot.minimize_obligation(automaton, f)
|
|
||||||
if minimized != automaton:
|
|
||||||
automaton = minimized
|
|
||||||
minimized = 0
|
|
||||||
degen = False # No need to degeneralize anymore
|
|
||||||
direct_simul = False # No need to simulate anymore
|
|
||||||
reverse_simul = False
|
|
||||||
iterated_simul = False
|
|
||||||
|
|
||||||
if direct_simul and not iterated_simul:
|
|
||||||
automaton = spot.simulation(automaton)
|
|
||||||
if reverse_simul and not iterated_simul:
|
|
||||||
automaton = spot.cosimulation(automaton)
|
|
||||||
if iterated_simul:
|
|
||||||
automaton = spot.iterated_simulations(automaton)
|
|
||||||
|
|
||||||
if prune_scc and (direct_simul or reverse_simul):
|
|
||||||
# Make a second pass after the simulation, since these might leave
|
|
||||||
# extra acceptance conditions.
|
|
||||||
automaton = spot.scc_filter(automaton, not degen)
|
|
||||||
|
|
||||||
if degen or neverclaim:
|
|
||||||
degen = spot.degeneralize(automaton)
|
|
||||||
else:
|
|
||||||
degen = automaton
|
|
||||||
|
|
||||||
# Buchi Automaton Output
|
|
||||||
if output_type == 'a':
|
|
||||||
if buchi_type == 'i':
|
|
||||||
s = spot.ostringstream()
|
|
||||||
spot.print_never_claim(s, degen)
|
|
||||||
unbufprint('<div class="neverclaim">%s</div>' % cgi.escape(s.str()))
|
|
||||||
del s
|
|
||||||
else: # 't' or 's'
|
|
||||||
dont_run_dot = print_stats(degen, True)
|
|
||||||
automaton.set_name(str(f))
|
|
||||||
render_automaton(degen, dont_run_dot)
|
|
||||||
degen = 0
|
|
||||||
automaton = 0
|
|
||||||
finish()
|
|
||||||
|
|
||||||
# Testing automaton Output
|
|
||||||
if output_type == 't':
|
|
||||||
livelock = False
|
|
||||||
singlepass = False
|
|
||||||
bisimulation = False
|
|
||||||
for to in form.getlist('to'):
|
|
||||||
if to == 'l':
|
|
||||||
livelock = True
|
|
||||||
elif to == 's':
|
|
||||||
singlepass = True
|
|
||||||
elif to == 'm':
|
|
||||||
bisimulation = True
|
|
||||||
propset = spot.atomic_prop_collect_as_bdd(f, automaton)
|
|
||||||
if ta_type == 'a':
|
|
||||||
tautomaton = spot.tgba_to_tgta(degen, propset)
|
|
||||||
if bisimulation:
|
|
||||||
tautomaton = spot.minimize_tgta(tautomaton)
|
|
||||||
else:
|
|
||||||
tautomaton = spot.tgba_to_ta(degen, propset, ta_type == 't',
|
|
||||||
True, singlepass, livelock)
|
|
||||||
if bisimulation:
|
|
||||||
tautomaton = spot.minimize_ta(tautomaton)
|
|
||||||
dont_run_dot = print_stats(tautomaton, ta = True)
|
|
||||||
render_automaton(tautomaton, dont_run_dot)
|
|
||||||
tautomaton = 0
|
|
||||||
degen = 0
|
|
||||||
automaton = 0
|
|
||||||
finish()
|
|
||||||
|
|
||||||
# Buchi Run Output
|
|
||||||
if output_type == 'r':
|
|
||||||
|
|
||||||
print_acc_run = False
|
|
||||||
s = form.getfirst('rf', 'd')
|
|
||||||
draw_acc_run = False
|
|
||||||
if s == 'p':
|
|
||||||
print_acc_run = True
|
|
||||||
elif s == 'd':
|
|
||||||
draw_acc_run = True
|
|
||||||
|
|
||||||
err = ""
|
|
||||||
opt = (form.getfirst('ec', 'Cou99') + "(" +
|
|
||||||
form.getfirst('eo', '') + ")")
|
|
||||||
eci, err = spot.make_emptiness_check_instantiator(opt)
|
|
||||||
|
|
||||||
if not eci:
|
|
||||||
unbufprint('<div class="parse-error">Cannot parse "' + opt
|
|
||||||
+ '" near "' + err + '".</div>')
|
|
||||||
ec = 0
|
|
||||||
else:
|
|
||||||
ec_a = 0
|
|
||||||
n_acc = degen.acc().num_sets()
|
|
||||||
n_max = eci.max_sets()
|
|
||||||
n_min = eci.min_sets()
|
|
||||||
if (n_acc <= n_max):
|
|
||||||
if (n_acc >= n_min):
|
|
||||||
ec_a = degen
|
|
||||||
else:
|
|
||||||
unbufprint('<div class="ec-error">Cannot run ' + opt
|
|
||||||
+ ' on automata with less than ' + str(n_min)
|
|
||||||
+ ' acceptance set.<br/>Please build '
|
|
||||||
+ 'a degeneralized Büchi automaton if you '
|
|
||||||
+ 'want to try this algorithm.</div>')
|
|
||||||
else:
|
|
||||||
unbufprint('<div class="ec-error">Cannot run ' + opt
|
|
||||||
+ ' on automata with more than ' + str(n_max)
|
|
||||||
+ ' acceptance set.<br/>Please build '
|
|
||||||
+ 'a degeneralized Büchi automaton if you '
|
|
||||||
+ 'want to try this algorithm.</div>')
|
|
||||||
if ec_a:
|
|
||||||
ec = eci.instantiate(ec_a)
|
|
||||||
else:
|
|
||||||
ec = 0
|
|
||||||
|
|
||||||
if ec:
|
|
||||||
ec_res = ec.check()
|
|
||||||
if not ec_res:
|
|
||||||
unbufprint('<div class="ec">No accepting run found.</div>')
|
|
||||||
else:
|
|
||||||
ec_run = ec_res.accepting_run()
|
|
||||||
unbufprint('<div class="ec">An accepting run was found.<br/>')
|
|
||||||
if ec_run:
|
|
||||||
if print_acc_run:
|
|
||||||
unbufprint('<div class="accrun">%s</div>' %
|
|
||||||
cgi.escape(str(ec_run)))
|
|
||||||
if draw_acc_run:
|
|
||||||
render_automaton(ec_run.as_twa(), False)
|
|
||||||
del ec_run
|
|
||||||
del ec_res
|
|
||||||
unbufprint('</div>')
|
|
||||||
finish()
|
|
||||||
|
|
@ -1,754 +0,0 @@
|
||||||
<!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 online LTL-to-TGBA translator</title>
|
|
||||||
<meta http-equiv="Content-type" content="text/html;charset=UTF-8">
|
|
||||||
<meta name="keywords" content="Spot,LTL,automata,Büchi,translation,TGBA">
|
|
||||||
<meta name="description" content="Translate LTL or PSL formulas into Büchi automata online using the Spot model-checking library">
|
|
||||||
<link rev=Made href="mailto:spot@lrde.epita.fr" title="Spot's discussion list">
|
|
||||||
<link rel="stylesheet" href="css/tipTip.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="https://ajax.googleapis.com/ajax/libs/jquery/1.7.2/jquery.min.js"></script>
|
|
||||||
<link rel="stylesheet" href="https://ajax.googleapis.com/ajax/libs/jqueryui/1.10.1/themes/ui-lightness/jquery-ui.css">
|
|
||||||
<script type="text/javascript" src="https://ajax.googleapis.com/ajax/libs/jqueryui/1.10.1/jquery-ui.min.js"></script>
|
|
||||||
<link rel="stylesheet" href="css/trans.css">
|
|
||||||
<script type="text/javascript" src="js/jquery.tipTip.minified.js"></script>
|
|
||||||
<script type="text/javascript" src="js/jquery.ba-bbq.min.js"></script>
|
|
||||||
<script type="text/javascript" src="js/jquery.ba-dotimeout.min.js"></script>
|
|
||||||
<script type="text/javascript">
|
|
||||||
jQuery(document).ready(function(){
|
|
||||||
$.spotvars = { autoupdate: false,
|
|
||||||
scrolldown: true,
|
|
||||||
internalchange: false};
|
|
||||||
$(".tabs").tabs();
|
|
||||||
$("#send").button();
|
|
||||||
$("#results").hide();
|
|
||||||
$("h1").hide();
|
|
||||||
$("abbr").tipTip({maxWidth: "300px", delay: 1000,
|
|
||||||
edgeOffset: 3,
|
|
||||||
defaultPosition: "below"});
|
|
||||||
$(".rtip").tipTip({maxWidth: "300px", delay: 1000,
|
|
||||||
edgeOffset: 10,
|
|
||||||
defaultPosition: "right"});
|
|
||||||
$(".btip").tipTip({maxWidth: "300px", delay: 1000,
|
|
||||||
edgeOffset: 10,
|
|
||||||
defaultPosition: "bottom"});
|
|
||||||
$(".ftip").tipTip({maxWidth: "300px", delay: 1000,
|
|
||||||
edgeOffset: 4,
|
|
||||||
defaultPosition: "left",
|
|
||||||
content: "<b>Click<\/b> to fold/unfold.<br><b>Ctrl+Click<\/b> to remove (any option set will remain set)."
|
|
||||||
});
|
|
||||||
$(".restip").tipTip({maxWidth: "300px", delay: 1000,
|
|
||||||
edgeOffset: 4,
|
|
||||||
defaultPosition: "left",
|
|
||||||
content: "<b>Click<\/b> to fold/unfold.<br><b>Ctrl+Click<\/b> to remove."
|
|
||||||
});
|
|
||||||
$(".ltltip").tipTip({maxWidth: "300px", delay: 1000,
|
|
||||||
edgeOffset: 4,
|
|
||||||
defaultPosition: "left",
|
|
||||||
content: "<b>Click<\/b> to fold/unfold."
|
|
||||||
});
|
|
||||||
$("#brcheckbox").change(function() {
|
|
||||||
if (!$(this).is(':checked')) {
|
|
||||||
$("#lfcheckbox").removeAttr('checked');
|
|
||||||
}
|
|
||||||
})
|
|
||||||
|
|
||||||
$("#lfcheckbox").change(function() {
|
|
||||||
if ($(this).is(':checked')) {
|
|
||||||
$("#brcheckbox").attr('checked', true);
|
|
||||||
}
|
|
||||||
})
|
|
||||||
|
|
||||||
$("#ltl3ba-T").change(function() {
|
|
||||||
if ($(this).is(':checked')) {
|
|
||||||
$("#ltl3ba-S").removeAttr('checked');
|
|
||||||
}
|
|
||||||
})
|
|
||||||
$("#ltl3ba-S").change(function() {
|
|
||||||
if ($(this).is(':checked')) {
|
|
||||||
$("#ltl3ba-U").attr('checked', true);
|
|
||||||
}
|
|
||||||
})
|
|
||||||
$("#to-s").change(function() {
|
|
||||||
if ($(this).is(':checked')) {
|
|
||||||
$("#to-l").removeAttr('checked');
|
|
||||||
}
|
|
||||||
})
|
|
||||||
$("#to-l").change(function() {
|
|
||||||
if ($(this).is(':checked')) {
|
|
||||||
$("#to-s").removeAttr('checked');
|
|
||||||
}
|
|
||||||
})
|
|
||||||
$("#tf-t,#tf-g").change(function() {
|
|
||||||
if ($(this).is(':checked')) {
|
|
||||||
$("#to-l,#to-s").removeAttr('disabled');
|
|
||||||
}
|
|
||||||
})
|
|
||||||
$("#tf-a").change(function() {
|
|
||||||
if ($(this).is(':checked')) {
|
|
||||||
$("#to-l,#to-s").attr('disabled', true);
|
|
||||||
}
|
|
||||||
})
|
|
||||||
$("#as-ds,#as-rs").change(function() {
|
|
||||||
if ($(this).is(':checked')) {
|
|
||||||
$("#as-is").removeAttr('checked');
|
|
||||||
}
|
|
||||||
})
|
|
||||||
$("#as-is").change(function() {
|
|
||||||
if ($(this).is(':checked')) {
|
|
||||||
$("#as-ds,#as-rs").removeAttr('checked');
|
|
||||||
}
|
|
||||||
})
|
|
||||||
|
|
||||||
function hideOrShowPanels(output, duration) {
|
|
||||||
switch (output)
|
|
||||||
{
|
|
||||||
case 'f':
|
|
||||||
$('#translator-tabs,#autsimp-tabs,#run-tabs,#tester-tabs').hide(duration);
|
|
||||||
break;
|
|
||||||
case 'm':
|
|
||||||
$('#autsimp-tabs,#run-tabs,#tester-tabs').hide(duration);
|
|
||||||
$('#translator-tabs').not('.killed').show(duration);
|
|
||||||
break;
|
|
||||||
case 'a':
|
|
||||||
$('#translator-tabs,#autsimp-tabs').not('.killed').show(duration);
|
|
||||||
$('#run-tabs,#tester-tabs').hide(duration);
|
|
||||||
break;
|
|
||||||
case 't':
|
|
||||||
$('#translator-tabs,#autsimp-tabs,#tester-tabs').not('.killed').show(duration);
|
|
||||||
$('#run-tabs').hide(duration);
|
|
||||||
break;
|
|
||||||
case 'r':
|
|
||||||
$('#translator-tabs,#autsimp-tabs,#run-tabs').not('.killed').show(duration);
|
|
||||||
$('#tester-tabs').hide(duration);
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
function updateFormFromHash(duration) {
|
|
||||||
var hashparam = jQuery.deparam.fragment();
|
|
||||||
if (jQuery.isEmptyObject(hashparam))
|
|
||||||
return;
|
|
||||||
if (!$.spotvars.internalchange)
|
|
||||||
$("input,select", "#trform").each(function() {
|
|
||||||
var name = this.name;
|
|
||||||
var value = [];
|
|
||||||
if (name && hashparam[name] != undefined) {
|
|
||||||
value = hashparam[name];
|
|
||||||
if (value.constructor != Array)
|
|
||||||
value = [value];
|
|
||||||
}
|
|
||||||
switch(this.type || this.tagName.toLowerCase()) {
|
|
||||||
case "radio":
|
|
||||||
case "checkbox":
|
|
||||||
this.checked = false;
|
|
||||||
for(var i = 0; i < value.length; i++) {
|
|
||||||
this.checked |= (value[i] == this.value);
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
case "select":
|
|
||||||
for(var opt = 0; opt < this.options.length; opt++) {
|
|
||||||
var option = this.options[opt];
|
|
||||||
option.selected = false;
|
|
||||||
for (var i = 0; i < value.length; i++) {
|
|
||||||
option.selected |= (value[i] == option.value);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
default:
|
|
||||||
this.value=value.join(',');
|
|
||||||
}
|
|
||||||
});
|
|
||||||
$("#brcheckbox,#tf-a").change();
|
|
||||||
$.spotvars.autoupdate = true;
|
|
||||||
$.spotvars.internalchange = false;
|
|
||||||
var o = $('input[name="o"]').val();
|
|
||||||
hideOrShowPanels(o, duration);
|
|
||||||
$("#output-tabs").tabs('option', 'active',
|
|
||||||
$('#output-tabs a[href="#tabs-o' + o + '"]').parent().index() - 1);
|
|
||||||
var t = $('input[name="t"]').val();
|
|
||||||
$("#translator-tabs").tabs('option', 'active',
|
|
||||||
$('#translator-tabs a[href="#tabs-t' + t + '"]').parent().index() - 1);
|
|
||||||
updateResults();
|
|
||||||
}
|
|
||||||
|
|
||||||
$(window).bind('hashchange', function(e) { updateFormFromHash('fast') });
|
|
||||||
|
|
||||||
$.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/spotcgi.py", "o=v3", function(data) {
|
|
||||||
if (data != 'not available') {
|
|
||||||
$("#ltl3ba-link").attr("title", data)
|
|
||||||
.tipTip({maxWidth: "400px", delay: 1000,
|
|
||||||
edgeOffset: 10,
|
|
||||||
defaultPosition: "right"});
|
|
||||||
} else {
|
|
||||||
var index = $('#translator-tabs a[href="#tabs-tl3"]').parent().index();
|
|
||||||
$("#translator-tabs").tabs("option", "disabled", [index - 1]);
|
|
||||||
}
|
|
||||||
});
|
|
||||||
|
|
||||||
function fold(ui, callback) {
|
|
||||||
var icon = ui.children(".ui-icon");
|
|
||||||
icon.removeClass("ui-icon-circle-arrow-n")
|
|
||||||
.addClass("ui-icon-circle-arrow-s");
|
|
||||||
ui.siblings('[class!="dontcollapse"]').hide('fast', callback);
|
|
||||||
}
|
|
||||||
function unfold(ui, noshowsiblings) {
|
|
||||||
var icon = ui.children(".ui-icon");
|
|
||||||
icon.removeClass("ui-icon-circle-arrow-s")
|
|
||||||
.addClass("ui-icon-circle-arrow-n");
|
|
||||||
if (!noshowsiblings) {
|
|
||||||
ui.siblings('[class!="dontcollapse"]').show('fast');
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
function foldToggle(ui) {
|
|
||||||
var icon = ui.children(".ui-icon");
|
|
||||||
if (icon.hasClass("ui-icon-circle-arrow-n")) {
|
|
||||||
icon.removeClass("ui-icon-circle-arrow-n")
|
|
||||||
.addClass("ui-icon-circle-arrow-s");
|
|
||||||
ui.siblings('[class!="dontcollapse"]').hide('fast');
|
|
||||||
} else {
|
|
||||||
icon.removeClass("ui-icon-circle-arrow-s")
|
|
||||||
.addClass("ui-icon-circle-arrow-n");
|
|
||||||
ui.siblings('[class!="dontcollapse"]').show('fast');
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
function updateHash() {
|
|
||||||
var str = $("#trform").serialize();
|
|
||||||
// This will trigger updateResults.
|
|
||||||
window.location.hash = "#" + str;
|
|
||||||
$.spotvars.internalchange = true;
|
|
||||||
// updateResults();
|
|
||||||
}
|
|
||||||
|
|
||||||
function updateResults() {
|
|
||||||
// If the answer takes more that 200ms to arrive,
|
|
||||||
// display a busy indicator.
|
|
||||||
$.doTimeout('res-update', 200, function(){
|
|
||||||
$("#results-body").hide();
|
|
||||||
$("#results-loading").show();
|
|
||||||
$("#results").show();
|
|
||||||
unfold($("#results-head"), true);
|
|
||||||
})
|
|
||||||
// don't read window.location.hash, because
|
|
||||||
// it has been %-decoded by firefox, which
|
|
||||||
// cause problems when formulae include '&'.
|
|
||||||
var fragment = location.href.replace(/^[^#]*#?(.*)$/, '$1');
|
|
||||||
console.log("fragment: " + fragment);
|
|
||||||
$("#results-body")
|
|
||||||
.load("/cgi-bin/spotcgi.py",
|
|
||||||
fragment,
|
|
||||||
function(response, status, xhr) {
|
|
||||||
$.doTimeout('res-update');
|
|
||||||
if (status == "error") {
|
|
||||||
var msg = "Sorry but there was an error: ";
|
|
||||||
$("#results-body").html(msg + xhr.status + " "
|
|
||||||
+ xhr.statusText);
|
|
||||||
}
|
|
||||||
$("#results-loading").hide();
|
|
||||||
$("#results-body").show();
|
|
||||||
$("#results").show();
|
|
||||||
unfold($("#results-head"), true);
|
|
||||||
fold($("#ltl-head"), function() {
|
|
||||||
if ($.spotvars.scrolldown)
|
|
||||||
$('html,body').animate({scrollTop: $("#results-head").offset().top}, 'slow');
|
|
||||||
$.spotvars.scrolldown = false;
|
|
||||||
});
|
|
||||||
return true;
|
|
||||||
});
|
|
||||||
}
|
|
||||||
|
|
||||||
function autoUpdate() {
|
|
||||||
if ($.spotvars.autoupdate)
|
|
||||||
updateHash();
|
|
||||||
return $.spotvars.autoupdate;
|
|
||||||
}
|
|
||||||
|
|
||||||
$("#send").click(updateHash);
|
|
||||||
$("input,select").change(autoUpdate);
|
|
||||||
$('input[name="f"]').attr('spellcheck', false).focus()
|
|
||||||
.keydown(function(e){
|
|
||||||
if (e.keyCode == 13) {
|
|
||||||
$.spotvars.scrolldown = true;
|
|
||||||
updateHash();
|
|
||||||
}
|
|
||||||
});
|
|
||||||
$('.collapsible .head').click(function(e) {
|
|
||||||
var cl = e.target.classList;
|
|
||||||
if (!cl.contains('head')
|
|
||||||
&& !cl.contains('ui-icon-circle-arrow-n')
|
|
||||||
&& !cl.contains('ui-icon-circle-arrow-s')) {
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
if (e.ctrlKey) {
|
|
||||||
if ($(this).attr('id') != 'ltl-head')
|
|
||||||
$(this).parent().hide('fast').addClass("killed");
|
|
||||||
} else {
|
|
||||||
foldToggle($(this));
|
|
||||||
}
|
|
||||||
return false;
|
|
||||||
});
|
|
||||||
$("#output-tabs").on("tabsactivate", function(event, ui) {
|
|
||||||
var v = ui.newPanel[0].id[6]; // 'tabs-om' => 'm'.
|
|
||||||
$('input[name="o"]').val(v)
|
|
||||||
if (!autoUpdate())
|
|
||||||
hideOrShowPanels(v, 'fast')
|
|
||||||
return true;
|
|
||||||
});
|
|
||||||
$('#output-tabs').tabs('option', 'active', $('#tabs-oa').index());
|
|
||||||
$('#translator-tabs').on("tabsactivate", function(event, ui) {
|
|
||||||
$('input[name="t"]').val(ui.newPanel[0].id.substring(6));
|
|
||||||
autoUpdate();
|
|
||||||
return true;
|
|
||||||
});
|
|
||||||
|
|
||||||
// Update the form from the hash value
|
|
||||||
updateFormFromHash(0);
|
|
||||||
});
|
|
||||||
</script>
|
|
||||||
</head>
|
|
||||||
<body>
|
|
||||||
<div id="spotlogo">
|
|
||||||
<a href="http://spot.lrde.epita.fr/"><img border=0 src="spot2.svg" 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 class="ltl2tgba">
|
|
||||||
<h1>Translator of LTL to Transition-based Generalized Büchi Automata</h1>
|
|
||||||
<!-- The action below will not be used. -->
|
|
||||||
<FORM id="trform" action="#"><P>
|
|
||||||
<div class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
|
|
||||||
<h3 id="ltl-head" class="ui-widget-header ui-corner-all head">LTL (or PSL) Formula to translate<span class="ui-icon ui-icon-circle-arrow-n ltltip">Fold</span></h3>
|
|
||||||
<div class="dontcollapse">
|
|
||||||
<INPUT class="formula" type="text" name="f" value=""><span id="send" class="btip" title="Submit the formula and all options. You may simply hit <b>enter</b> after typing the formula. After the first submission the form will auto-update itself anytime you change an option.">Send</span></div>
|
|
||||||
<div id="ltl-help">
|
|
||||||
<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 (<span class="formula">F</span>,
|
|
||||||
<span class="formula">G</span>, or <span class="formula">X</span>): for instance <span class="formula">GFa</span>
|
|
||||||
means <span class="formula">G(F(a))</span>. Use <span class="formula">"GFa"</span> if you really want
|
|
||||||
to refer to <span class="formula">GFa</span> as a proposition.<br>Conversely, infix
|
|
||||||
letter operators are not assumed to be operators if they are part of
|
|
||||||
an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
|
|
||||||
<span class="formula">a U b</span> and <span class="formula">(a)U(b)</span>.</p>
|
|
||||||
<table border="0" width="100%" rules="groups" frame="void" cellpadding="3" cellspacing="0" class="ltltable">
|
|
||||||
<colgroup>
|
|
||||||
<colgroup span=2>
|
|
||||||
<colgroup span=2>
|
|
||||||
<colgroup span=2>
|
|
||||||
<colgroup span=2>
|
|
||||||
<thead>
|
|
||||||
<tr>
|
|
||||||
<th></th>
|
|
||||||
<th colspan=2>Constants</th>
|
|
||||||
<th colspan=2>Unary operators</th>
|
|
||||||
<th colspan=4>Binary operators (infix)</th>
|
|
||||||
</tr>
|
|
||||||
</thead>
|
|
||||||
<tbody>
|
|
||||||
<tr>
|
|
||||||
<td class="ltldocrow" rowspan=3>Boolean</td>
|
|
||||||
<td class="ltldoc">false:</td><td><span class="formula">0</span> <span class="formula">false</span></td>
|
|
||||||
<td class="ltldoc">not:</td><td><span class="formula">!</span> <span class="formula">~</span></td>
|
|
||||||
<td class="ltldoc">and:</td><td><span class="formula">&</span> <span class="formula">&&</span>
|
|
||||||
<span class="formula">/\</span></td>
|
|
||||||
<td class="ltldoc">implies:</td><td><span class="formula">-></span>
|
|
||||||
<span class="formula">--></span>
|
|
||||||
<span class="formula">=></span></td>
|
|
||||||
</tr>
|
|
||||||
<tr>
|
|
||||||
<td class="ltldoc">true:</td><td><span class="formula">1</span> <span class="formula">true</span></td>
|
|
||||||
<td></td><td></td>
|
|
||||||
<td class="ltldoc">or:</td><td><span class="formula">|</span> <span class="formula">||</span>
|
|
||||||
<span class="formula">+</span> <span class="formula">\/</span></td>
|
|
||||||
<td class="ltldoc">equivalent:</td><td><span class="formula"><-></span>
|
|
||||||
<span class="formula"><--></span>
|
|
||||||
<span class="formula"><=></span></td>
|
|
||||||
</tr>
|
|
||||||
<tr>
|
|
||||||
<td></td><td></td>
|
|
||||||
<td></td><td></td>
|
|
||||||
<td class="ltldoc">xor:</td><td><span class="formula">xor</span> <span class="formula">^</span></td>
|
|
||||||
<td></td><td></td>
|
|
||||||
</tr>
|
|
||||||
</tbody>
|
|
||||||
<tbody>
|
|
||||||
<tr>
|
|
||||||
<td class="ltldocrow" rowspan=3><ABBR title="Linear-time Temporal Logic">LTL</ABBR></td>
|
|
||||||
<td></td><td></td>
|
|
||||||
<td class="ltldoc">eventually:</td><td><span class="formula">F</span>
|
|
||||||
<span class="formula"><></span></td>
|
|
||||||
<td class="ltldoc">(strong) until:</td><td><span class="formula">U</span></td>
|
|
||||||
<td class="ltldoc">weak until:</td><td><span class="formula">W</span></td>
|
|
||||||
</tr>
|
|
||||||
<tr>
|
|
||||||
<td></td><td></td>
|
|
||||||
<td class="ltldoc">always:</td><td><span class="formula">G</span>
|
|
||||||
<span class="formula">[]</span></td>
|
|
||||||
<td class="ltldoc">(weak) release:</td><td><span class="formula">R</span>
|
|
||||||
<span class="formula">V</span></td>
|
|
||||||
<td class="ltldoc">strong release:</td><td><span class="formula">M</span></td>
|
|
||||||
</tr>
|
|
||||||
<tr>
|
|
||||||
<td></td><td></td>
|
|
||||||
<td class="ltldoc">next:</td><td><span class="formula">X</span> <span class="formula">()</span></td>
|
|
||||||
<td></td><td></td>
|
|
||||||
<td></td><td></td>
|
|
||||||
</tr>
|
|
||||||
</tbody>
|
|
||||||
<tbody>
|
|
||||||
<tr>
|
|
||||||
<td class="ltldocrow" rowspan=4><ABBR title="Sequential Extended Regular
|
|
||||||
Expression">SERE</ABBR></td>
|
|
||||||
<td class="ltldoc">ε:</td><td><span class="formula">[*0]</span></td>
|
|
||||||
<td class="ltldoc">Kleene star:</td><td><span class="formula">[*] </span><span class="formula">[+]</span> <span class="formula">[*</span><i>i..j</i><span class="formula">]</span></td>
|
|
||||||
<td class="ltldoc">concatenation:</td><td><span class="formula">;</span></td>
|
|
||||||
<td class="ltldoc">fusion:</td><td><span class="formula">:</span></td>
|
|
||||||
</tr>
|
|
||||||
<tr>
|
|
||||||
<td></td><td></td>
|
|
||||||
<td class="ltldoc">goto:</td><td><span class="formula">[-></span><i>i..j</i><span class="formula">]</span></td>
|
|
||||||
<td class="ltldoc">intersection:</td><td><span class="formula">&&</span> <span class="formula">/\</span></td>
|
|
||||||
<td class="ltldoc"><ABBR title="Non-Length-Matching">NLM</ABBR> and:</td><td><span class="formula">&</span></td>
|
|
||||||
</tr>
|
|
||||||
<tr>
|
|
||||||
<td></td><td></td>
|
|
||||||
<td class="ltldoc">nonconsec. rep.:</td><td><span class="formula">[=</span><i>i..j</i><span class="formula">]</span></td>
|
|
||||||
<td class="ltldoc">union:</td><td><span class="formula">|</span> <span class="formula">||</span> <span class="formula">+</span> <span class="formula">\/</span></td>
|
|
||||||
<td></td><td></td>
|
|
||||||
</tr>
|
|
||||||
<tr>
|
|
||||||
<td></td><td></td>
|
|
||||||
<td class="ltldoc"><abbr title="The operator <span class='formula'>[:+]</span> corresponds to the <span class='formula'>⊕</span> operator introduced by Dax et al. (<i>Specification Languages for Stutter-Invariant Regular Properties</i>, ATVA'09). The other two are generalizations to different bounds.">iterated fusion</abbr>:</td><td><span class="formula">[:*] </span><span class="formula">[:+]</span> <span class="formula">[:*</span><i>i..j</i><span class="formula">]</span></td>
|
|
||||||
<td></td><td></td>
|
|
||||||
<td></td><td></td>
|
|
||||||
</tr>
|
|
||||||
</tbody>
|
|
||||||
<tbody>
|
|
||||||
<tr>
|
|
||||||
<td class="ltldocrow" rowspan=2><ABBR title="Property Specification Language">PSL</ABBR></td>
|
|
||||||
<td></td><td></td>
|
|
||||||
<td class="ltldoc">weak closure:</td><td><span class="formula">{</span><i>s</i><span class="formula">}</span></td>
|
|
||||||
<td class="ltldoc">triggers:</td><td><span class="formula">{</span><i>s</i><span class="formula">}[]-></span><i>p</i><br><span class="formula">{</span><i>s</i><span class="formula">}|-></span><i>p</i><br><span class="formula">{</span><i>s</i><span class="formula">}(</span><i>p</i><span class="formula">)</span></td>
|
|
||||||
<td class="ltldoc"><ABBR title="Non-Overlapping">Non-Ov.</ABBR> trigger:</td><td><span class="formula">{</span><i>s</i><span class="formula">}[]=></span><i>p</i><br><span class="formula">{</span><i>s</i><span class="formula">}|=></span><i>p</i></td>
|
|
||||||
</tr>
|
|
||||||
<tr>
|
|
||||||
<td></td><td></td>
|
|
||||||
<td class="ltldoc">strong closure:</td><td><span class="formula">{</span><i>s</i><span class="formula">}!</span></td>
|
|
||||||
<td class="ltldoc">seq:</td><td><span class="formula">{</span><i>s</i><span class="formula">}<>-></span><i>p</i></td>
|
|
||||||
<td class="ltldoc"><ABBR title="Non-Overlapping">Non-Ov.</ABBR> seq:</td><td><span class="formula">{</span><i>s</i><span class="formula">}<>=></span><i>p</i></td>
|
|
||||||
</tr>
|
|
||||||
</tbody>
|
|
||||||
</table>
|
|
||||||
</div>
|
|
||||||
</div>
|
|
||||||
<div class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
|
|
||||||
<h3 class="ui-widget-header ui-corner-all head">Formula Simplifications<span class="ui-icon ui-icon-circle-arrow-n ftip">Fold</span></h3>
|
|
||||||
<div>
|
|
||||||
<label class="rtip" title="Apply simple, unconditional rewriting rules to simplify formula. For instance <span class='formula'>F(a)|F(b)</span> is rewritten as <span class='formula'>F(a|b)</span>.">
|
|
||||||
<INPUT id="brcheckbox" type="checkbox" name="r" value="br" checked>
|
|
||||||
basic rewritings
|
|
||||||
</label>
|
|
||||||
<label class="rtip" title="Enable basic rewriting rules that may produce bigger formulas.">
|
|
||||||
<INPUT id="lfcheckbox" type="checkbox" name="r" value="lf" checked>
|
|
||||||
allow larger formulas
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Use rewriting rules based on implications between subformulas, when these implications can be proved syntactically. For instance <span class='formula'>a U Fa</span> can be reduced to <span class='formula'>Fa</span> because the latter is obviously implied by <span class='formula'>a</span>.">
|
|
||||||
<INPUT type="checkbox" name="r" value="si" checked>
|
|
||||||
syntactic implication
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Apply simplification rules when subformulas are <b>pure eventuality</b> or <b>purely universal</b>. For instance <span class='formula'>FGFa</span> can be rewritten to <span class='formula'>GFa</span> because the latter is a pure eventuality.">
|
|
||||||
<INPUT type="checkbox" name="r" value="eu" checked>
|
|
||||||
eventuality and universality
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Try to reduce the formula by testing inclusion between automata built for various subformulas. This can be rather slow on large formulas.">
|
|
||||||
<INPUT type="checkbox" name="r" value="lc">
|
|
||||||
language containment
|
|
||||||
</label>
|
|
||||||
<label class="rtip floatright" title="Encode all formulas using UTF-8 characters.">
|
|
||||||
<INPUT type="checkbox" name="g" value="8">
|
|
||||||
UTF-8 output
|
|
||||||
</label>
|
|
||||||
</div>
|
|
||||||
</div>
|
|
||||||
<div id="output-tabs" class="tabs collapsible shadow">
|
|
||||||
<ul class="head">
|
|
||||||
<li>Desired Output:</li>
|
|
||||||
<li><a href="#tabs-of" class="btip" title="Simplify the formula, but do not convert it as an automaton.">Formula</a></li>
|
|
||||||
<li><a href="#tabs-om" class="btip" title="Create a monitor accepting all finite prefixes compatible with the formula.">Monitor</a></li>
|
|
||||||
<li><a href="#tabs-oa" class="btip" title="Translate the LTL formula into Büchi automaton.">Büchi Automaton</a></li>
|
|
||||||
<li><a href="#tabs-or" class="btip" title="Translate the LTL formula into Büchi automaton, and exhibit an accepting run.">Büchi Run</a></li>
|
|
||||||
<li><a href="#tabs-ot" class="btip" title="Translate the LTL formula into a Testing Automaton, or some variant.">Testing Automaton</a></li>
|
|
||||||
<li class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>
|
|
||||||
</ul>
|
|
||||||
<input type="hidden" name="o">
|
|
||||||
<div>
|
|
||||||
<div id="tabs-of">
|
|
||||||
Output the (simplified) formula as:<br>
|
|
||||||
<label class="rtip" title="Use letter operators (such as <span class='formula'>G</span> or <span class='formula'>F</span>) when possible, and unless UTF-8 output is activated.">
|
|
||||||
<INPUT type="radio" name="ff" value="o" checked>
|
|
||||||
text in Spot's syntax
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="This output can be given to Spin or any other tool using a similar syntax. Spot can also read it back. Operators such as such as <span class='formula'>M</span> and <span class='formula'>W</span>, which are not supported by Spin are rewritten away.">
|
|
||||||
<INPUT type="radio" name="ff" value="i">
|
|
||||||
text in Spin's syntax
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="This output can be given to LBT, LBTT, ltl2dstar, scheck, or any other tool using a similar syntax. Spot can also read it back. The original syntax only support atomic propositions named <span class='formula'>p0</span>, <span class='formula'>p1</span>, etc. As an extension, also supported by ltl2dstar, other atomic proposition are enclosed in double quotes. PSL formulas are not supported.">
|
|
||||||
<INPUT type="radio" name="ff" value="l">
|
|
||||||
text in LBT's syntax
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="A graphical representation of Spot's internal representation. Actually this is not a tree but an acyclic graph, because equal subformulas are shared.">
|
|
||||||
<INPUT type="radio" name="ff" value="g">
|
|
||||||
a syntactic tree
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Various properties of the formula.">
|
|
||||||
<INPUT type="radio" name="ff" value="p">
|
|
||||||
property information
|
|
||||||
</label><br>
|
|
||||||
</div>
|
|
||||||
<div id="tabs-om">
|
|
||||||
Translate the (simplified) formula as:<br>
|
|
||||||
<label class="rtip" title="A deterministic monitor is a DFA that accepts all the prefixes of the executions that satisfy the formula.">
|
|
||||||
<INPUT type="radio" name="mf" value="d" checked>
|
|
||||||
a deterministic monitor
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="A nondeterministic monitor is an NFA that accepts all the prefixes of the executions that satisfy the formula.">
|
|
||||||
<INPUT type="radio" name="mf" value="n" checked>
|
|
||||||
a nondeterministic monitor
|
|
||||||
</label><br>
|
|
||||||
</div>
|
|
||||||
<div id="tabs-oa">
|
|
||||||
Translate the (simplified) formula as:<br>
|
|
||||||
<label class="rtip" title="A Transition-based Generalized Büchi Automaton (TGBA) is the main kind of automaton used by Spot. It is what all the translation algorithm below will output.">
|
|
||||||
<INPUT type="radio" name="af" value="t" checked>
|
|
||||||
a transition-based generalized Büchi automaton
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Degeneralize the TGBA to obtain a Büchi automaton with a single set of accepting states.">
|
|
||||||
<INPUT type="radio" name="af" value="s">
|
|
||||||
a state-based degeneralized Büchi automaton
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Degeneralize the TGBA to obtain a Büchi automaton with a single set of accepting states (as with previous option), then output the automaton as a neverclaim that can be fed to Spin.">
|
|
||||||
<INPUT type="radio" name="af" value="i">
|
|
||||||
a Spin neverclaim
|
|
||||||
</label><br>
|
|
||||||
</div>
|
|
||||||
<div id="tabs-or">
|
|
||||||
Translate the (simplified) formula as:<br>
|
|
||||||
<label class="rtip" title="A Transition-based Generalized Büchi Automaton (TGBA) is the main kind of automaton used by Spot. It is what all the translation algorithm below will output.">
|
|
||||||
<INPUT type="radio" name="ra" value="t" checked>
|
|
||||||
a transition-based generalized Büchi automaton
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Degeneralize the TGBA to obtain a Büchi automaton with a single set of accepting states.">
|
|
||||||
<INPUT type="radio" name="ra" value="s">
|
|
||||||
a state-based degeneralized Büchi automaton
|
|
||||||
</label><br>
|
|
||||||
then<br>
|
|
||||||
<label class="rtip" title="Produce a textual description of run accepted by the automaton.">
|
|
||||||
<INPUT type="radio" name="rf" value="p">
|
|
||||||
print an accepting run
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Use color to show an accepting run in the automaton.">
|
|
||||||
<INPUT type="radio" name="rf" value="d" checked>
|
|
||||||
draw an accepting run as a lasso-shaped automaton
|
|
||||||
</label><br>
|
|
||||||
</div>
|
|
||||||
<div id="tabs-ot">
|
|
||||||
Translate the (simplified) formula into a Büchi automaton, and then convert it into:<br>
|
|
||||||
<label class="rtip" title="Instead of reading valuations of all atomic propositions testing automata only watch the changes to these valuation. A transitions labeled by <span class='formula'>a</span> may be crossed only if these atomic proposition change in the system. Additionally, testing automata have two acceptance conditions: states can be Büchi accepting or livelock accepting (or both, or none).">
|
|
||||||
<INPUT id="tf-t" type="radio" name="tf" value="t">
|
|
||||||
a Testing Automaton (TA)
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="GTA are testing automata extended with multiple Büchi acceptance conditions.">
|
|
||||||
<INPUT id="tf-g" type="radio" name="tf" value="g">
|
|
||||||
a Generalized Testing Automaton (GTA)
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="TGTA are similar to TGBA except instead of reading valuations of all atomic propositions testing automata only watch the changes to these valuation. They have multiple Büchi acceptance conditions on transitions, but no livelock acceptance.">
|
|
||||||
<INPUT id="tf-a" type="radio" name="tf" value="a" checked>
|
|
||||||
a Transition-based Generalized Testing Automaton (TGTA)
|
|
||||||
</label><br>
|
|
||||||
</div>
|
|
||||||
</div>
|
|
||||||
</div>
|
|
||||||
<div id="translator-tabs" class="tabs collapsible shadow">
|
|
||||||
<ul class="head">
|
|
||||||
<li>Translator Algorithm:</li>
|
|
||||||
<li><a href="#tabs-tfm" class="btip" title="A tableau construction that uses BDDs to symbolically represent each state of the automaton. This produces better results than Tauriainen/TAA, and is the only algorithm that has been extended to support PSL operators.">Couvreur/FM</a></li>
|
|
||||||
<li><a href="#tabs-tta" class="btip" title="An implementation of Heikki Tauriainen's Ph.D. thesis algorithm to translate LTL formulas via very weak alternating automata with transition-based generalized acceptance conditions.">Tauriainen/TAA</a></li>
|
|
||||||
<li><a href="#tabs-tcs" class="btip" title="Compositional suspension.<br>A technique presented at Spin'13. Suspendable formulas are formulas such as <span class='formula'>GFa</span> or <span class='formula'>FGb</span> whose verification can always be postponed by a finite number of step. In this approach, we extract all suspendable subformulas, translate them separately from the main, skeleton automaton, only to merge them back in the accepting SCC. This translation uses Couvreur/FM for the intermediate parts.">Comp.Susp.</a></li>
|
|
||||||
<li id="ltl3ba-tab"><a href="#tabs-tl3" class="btip" title="An improved version of LTL2BA, overhauled by Tomáš Babiak during his Ph.D., and described at TACAS'12.<br>LTL3BA is not part of Spot. Options in this tab correspond to options offered by LTL3BA, and have some overlap with the options offered by Spot that are still applied before (LTL simplifications) and after (automata simplifications) LTL3BA is called.">LTL3BA</a></li>
|
|
||||||
<li class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>
|
|
||||||
</ul>
|
|
||||||
<input type="hidden" name="t" value="fm">
|
|
||||||
<div>
|
|
||||||
<div id="tabs-tfm">
|
|
||||||
<label class="rtip" title="Try to optimize the automaton for determinism when building it. Warning: this option can be expensive if the formula uses a lot of different atomic propositions because the algorithm has to consider all possible valuations.">
|
|
||||||
<INPUT type="checkbox" name="fm" value="od" checked>
|
|
||||||
optimize determinism
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="All states that share the same set of outgoing transitions will be merged. This optimization comes for free in the implementation, so there is no point in disabling it unless you want to study its effect.">
|
|
||||||
<INPUT type="checkbox" name="fm" value="sm" checked>
|
|
||||||
merge states with same symbolic successor representation
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Attempt to delay non-deterministic branching. It sometimes helps to reduce the indeterminism (look at the effect on <span class='formula'>X(a) R b</span>), but it may also produce bigger automata.">
|
|
||||||
<INPUT type="checkbox" name="fm" value="bp">
|
|
||||||
branching postponement
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Try to syntactically detect if a state can be part of a fair loop, and if so, do not use acceptance conditions for that state. This optimization seems to have more negative effects than positive effects...">
|
|
||||||
<INPUT type="checkbox" name="fm" value="fl">
|
|
||||||
fair-loop approximations
|
|
||||||
</label><br>
|
|
||||||
</div>
|
|
||||||
<div id="tabs-tta">
|
|
||||||
<label class="rtip" title="Enable a refined set of translation rules, based on language inclusion between subformulas. Because language inclusion between formula is tested using automata operations on translations for subformulas, this option can be slow.">
|
|
||||||
<INPUT type="checkbox" name="ta" value="lc" checked>
|
|
||||||
language containment
|
|
||||||
</label><br>
|
|
||||||
</div>
|
|
||||||
<div id="tabs-tl3">
|
|
||||||
Use <a href="https://sourceforge.net/projects/ltl3ba/" id="ltl3ba-link">LTL3BA</a> to build:
|
|
||||||
<label class="rtip" title="Stop LTL3BA once it has built a Transition-based Generalized Büchi Automaton. Spot will take it from here and optionally apply more optimizations.">
|
|
||||||
<INPUT id="ltl3ba-T" type="radio" name="lo" value="T" checked>
|
|
||||||
a TGBA
|
|
||||||
</label> or <label class="rtip" title="Run LTL3BA until it produces its final Büchi Automaton. Spot will consider this BA has a TGBA if further optimizations have been requested below.">
|
|
||||||
<INPUT id="ltl3ba-U" type="radio" name="lo" value="U">
|
|
||||||
a BA
|
|
||||||
</label><br>
|
|
||||||
<div class="colleft">
|
|
||||||
<label class="rtip" title="LTL simplifications performed in LTL3BA are independent of those Spot may have performed upstream.">
|
|
||||||
<INPUT type="checkbox" name="l3" value="l" checked>
|
|
||||||
LTL simplifications
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="See next tooltip for an explanation of suspension. LTL3BA supports suspension also in the construction of an intermediate alternating automaton, where it is only used for one step.">
|
|
||||||
<INPUT type="checkbox" name="l3" value="A" checked>
|
|
||||||
suspension in alternating automaton
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Suspension is a technique to postpone the verification of some subformulae. An easy way to picture it is to look at the formula <span class='formula'>F(a)&GF(b)</span>: the <span class='formula'>GF(b)</span> part does not need to be checked before some <span class='formula'>a</span> has been seen. On this example, suspension amounts to translating <span class='formula'>F(a&GF(b))</span> but the technique is more general than such LTL rewritings.">
|
|
||||||
<INPUT type="checkbox" name="l3" value="P" checked>
|
|
||||||
suspension in TGBA
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="During the construction, each newly created transition or state is immediately compared to existing transitions or states and merged if possible.">
|
|
||||||
<INPUT type="checkbox" name="l3" value="o" checked>
|
|
||||||
on-the-fly simplifications
|
|
||||||
</label><br>
|
|
||||||
</div>
|
|
||||||
<label class="rtip" title="Perform the same simplifications as the on-the-fly simplification but on the final automaton, plus some SCC simplifications.">
|
|
||||||
<INPUT type="checkbox" name="l3" value="p" checked>
|
|
||||||
a-posteriori simplifications
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Compute Strongly Connected Components to simplify the automaton.">
|
|
||||||
<INPUT type="checkbox" name="l3" value="C" checked>
|
|
||||||
SCC simplifications
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Try to improve the automaton's determinism when building it. This may produce larger automata.">
|
|
||||||
<INPUT type="checkbox" name="l3" value="M" checked>
|
|
||||||
more deterministic output
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Compute a direct (a.k.a. strong fair) simulation relation to reduce the size of the Büchi automaton.">
|
|
||||||
<INPUT id="ltl3ba-S" type="checkbox" name="l3" value="S">
|
|
||||||
direct simulation on BA
|
|
||||||
</label><br>
|
|
||||||
</div>
|
|
||||||
<div id="tabs-tcs">
|
|
||||||
<label class="rtip" title="Apply WDBA minimization on skeleton automaton when possible.">
|
|
||||||
<INPUT type="checkbox" name="cs" value="w">
|
|
||||||
WDBA minimization of intermediate automaton
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Apply direct simulation on skeleton automaton. This is only done when the WDBA minimization could not work.">
|
|
||||||
<INPUT type="checkbox" name="cs" value="s" checked>
|
|
||||||
direct simulation on intermediate automaton
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Start suspension on transitions that enter accepting SCCs instead of waiting to be in the SCC. (Not discussed in the Spin'13 paper.)">
|
|
||||||
<INPUT type="checkbox" name="cs" value="e">
|
|
||||||
early start of suspended automata
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Output the skeleton automaton, with suspension labels showing where suspended formulae should be attached.
|
|
||||||
Unlike in our Spin'13 paper, we consider negated suspension labels and missing suspension labels
|
|
||||||
equivalently: the important data is the place of the positive suspension labels.">
|
|
||||||
<INPUT type="checkbox" name="cs" value="c">
|
|
||||||
do not compose suspended formulas (for debugging)
|
|
||||||
</label><br>
|
|
||||||
<!--
|
|
||||||
<label class="rtip" title="Consider obligation subformulas as atomic propositions initially, and compose their WDBA-minimized translation.">
|
|
||||||
<INPUT type="checkbox" name="cs" value="o">
|
|
||||||
compose WDBA-minimized obligation sub-formulas
|
|
||||||
</label><br> -->
|
|
||||||
</div>
|
|
||||||
</div>
|
|
||||||
</div>
|
|
||||||
<div id="autsimp-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
|
|
||||||
<h3 class="ui-widget-header ui-corner-all head">Automaton Simplifications<span class="ui-icon ui-icon-circle-arrow-n ftip">Fold</span></h3>
|
|
||||||
<div>
|
|
||||||
<label class="rtip" title="Compute the SCCs of the automaton. Eliminate all the useless SCCs (i.e. those that cannot be part of an accepting run). Also attempt to remove redundant acceptance conditions.">
|
|
||||||
<INPUT type="checkbox" name="as" value="ps" checked>
|
|
||||||
prune unaccepting SCCs
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="<b>Obligation properties</b> are properties that can be represented by a Weak Deterministic Büchi Automaton (WDBA). Any WDBA has a minimal form that can be constructed in a way that is similar to DFA minimization.<br>Using this option, any automaton (WDBA or not) will be tentatively determinized and minimized; the result will be used only if it is equivalent to the original automaton (i.e., if the property was indeed an obligation property).">
|
|
||||||
<INPUT type="checkbox" name="as" value="wd">
|
|
||||||
determinize and minimize obligation properties
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Attempt to reduce the automaton by using <b>direct simulation</b> on the TGBA. Basically a state <b>A</b> can be merged into a state <b>B</b> if the <b>suffixes</b> reachable from <b>A</b> are included into those reachable from <b>B</b>. This algorithm may also improve determinism as a side effect.">
|
|
||||||
<INPUT id="as-ds" type="checkbox" name="as" value="ds">
|
|
||||||
direct simulation
|
|
||||||
</label>
|
|
||||||
<label class="rtip" title="Attempt to reduce the automaton by using <b>reverse simulation</b> on the TGBA. Basically a state <b>A</b> can be merged into a state <b>B</b> if the <b>prefixes</b> reachable from <b>A</b> are included into those reachable from <b>B</b> This can also improve codeterminism as a side effect.">
|
|
||||||
<INPUT id="as-rs" type="checkbox" name="as" value="rs">
|
|
||||||
reverse simulation
|
|
||||||
</label>
|
|
||||||
<label class="rtip" title="Apply <b>direct</b> and <b>reverse simulation</b> alternatively until the automaton is not reduced further.">
|
|
||||||
<INPUT id="as-is" type="checkbox" name="as" value="is">
|
|
||||||
iterated simulations
|
|
||||||
</label><br>
|
|
||||||
</div>
|
|
||||||
</div>
|
|
||||||
<div id="run-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
|
|
||||||
<h3 class="ui-widget-header ui-corner-all
|
|
||||||
head">Emptiness-check Algorithm<span class="ui-icon ui-icon-circle-arrow-n ftip">Fold</span></h3>
|
|
||||||
<div>
|
|
||||||
Search accepting run using algorithm:
|
|
||||||
<select name="ec">
|
|
||||||
<option value="Cou99" selected>Cou99</option>
|
|
||||||
<option value="CVWY90">CVWY90</option>
|
|
||||||
<option value="GV04">GV04</option>
|
|
||||||
<option value="SE05">SE05</option>
|
|
||||||
<option value="Tau03">Tau03</option>
|
|
||||||
<option value="Tau03_opt">Tau03_opt</option>
|
|
||||||
</select> with these
|
|
||||||
<a href="http://spot.lip6.fr/wiki/EmptinessCheckOptions">options</a>:
|
|
||||||
<INPUT type="text" maxlength="40" name="eo" value="">
|
|
||||||
</div>
|
|
||||||
</div>
|
|
||||||
<div id="tester-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
|
|
||||||
<h3 class="ui-widget-header ui-corner-all head">Testing Automaton Options<span class="ui-icon ui-icon-circle-arrow-n ftip">Fold</span></h3>
|
|
||||||
<div>
|
|
||||||
<label class="rtip" title="Divert all livelock accepting paths to a single livelock acceptance state.">
|
|
||||||
<INPUT id="to-l" type="checkbox" name="to" value="l">
|
|
||||||
use a catch-all livelock state
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Ensure that all livelock accepting states are also Büchi-accepting, so that the testing automaton can be tested for emptiness in a single pass.">
|
|
||||||
<INPUT id="to-s" type="checkbox" name="to" value="s" checked>
|
|
||||||
produce a single-pass testing automaton
|
|
||||||
</label><br>
|
|
||||||
<label class="rtip" title="Merge bisimilar states in the final testing automaton.">
|
|
||||||
<INPUT type="checkbox" name="to" value="m" checked>
|
|
||||||
merge bisimilar states
|
|
||||||
</label><br>
|
|
||||||
</div>
|
|
||||||
</div>
|
|
||||||
</FORM>
|
|
||||||
<div id="results" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
|
|
||||||
<h3 id="results-head" class="ui-widget-header ui-corner-all head">Results<span class="ui-icon ui-icon-circle-arrow-n restip">Fold</span></h3>
|
|
||||||
<div id="results-loading" class="dontcollapse"><img src="css/loading.gif" class="loading" border=0 alt="loading..."></div>
|
|
||||||
<div id="results-body">
|
|
||||||
Loading...
|
|
||||||
</div>
|
|
||||||
</div>
|
|
||||||
</div>
|
|
||||||
</body>
|
|
||||||
</html>
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue