diff --git a/ChangeLog b/ChangeLog index 130835ad5..07de466a1 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2011-01-18 Alexandre Duret-Lutz + + Preliminary implementation of an ajax-based ltl2tgba translator. + + * configure.ac: Output wrap/python/ajax/Makefile. + * wrap/python/Makefile.am (SUBDIRS): Add ajax. + * wrap/python/ajax/Makefile.am, wrap/python/ajax/README, + wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/spot.in: New files. + * wrap/python/ajax/css/, wrap/python/ajax/js, + wrap/python/ajax/logos: New directories. + * README: Document wrap/python/ajax/. + 2011-01-17 Alexandre Duret-Lutz Do not output empty parse error blocks in the CGI script. diff --git a/README b/README index 319de03c3..a51b67266 100644 --- a/README +++ b/README @@ -143,6 +143,7 @@ wrap/ Wrappers for other languages. python/ Python bindings for Spot and BuDDy tests/ Tests for these bindings cgi-bin/ Python-based CGI script (ltl-to-tgba translator) + ajax/ Moderner LTL-to-TGBA translator, using Ajax. iface/ Interfaces to other libraries. gspn/ GreatSPN interface. examples/ Supporting models used by the test cases. diff --git a/configure.ac b/configure.ac index 9150918d7..d8b29c9fb 100644 --- a/configure.ac +++ b/configure.ac @@ -1,4 +1,4 @@ -# Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et +# Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -134,6 +134,7 @@ AC_CONFIG_FILES([ src/tgbatest/Makefile wrap/Makefile wrap/python/Makefile + wrap/python/ajax/Makefile wrap/python/cgi-bin/Makefile wrap/python/tests/Makefile ]) diff --git a/wrap/python/Makefile.am b/wrap/python/Makefile.am index 930eacbe3..601921caa 100644 --- a/wrap/python/Makefile.am +++ b/wrap/python/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2010 Laboratoire de Recherche et Development de +## Copyright (C) 2010, 2011 Laboratoire de Recherche et Development de ## l'Epita (LRDE). ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -21,7 +21,7 @@ ## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA ## 02111-1307, USA. -SUBDIRS = . cgi-bin tests +SUBDIRS = . cgi-bin ajax tests AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_srcdir)/src $(BUDDY_CPPFLAGS) \ -DSWIG_TYPE_TABLE=spot diff --git a/wrap/python/ajax/Makefile.am b/wrap/python/ajax/Makefile.am new file mode 100644 index 000000000..9676d8333 --- /dev/null +++ b/wrap/python/ajax/Makefile.am @@ -0,0 +1,56 @@ +## Copyright (C) 2011 Laboratoire d'Informatique de Paris 6 (LIP6), +## département Systèmes Répartis Coopératifs (SRC), Université Pierre +## et Marie Curie. +## +## This file is part of Spot, a model checking library. +## +## Spot is free software; you can redistribute it and/or modify it +## under the terms of the GNU General Public License as published by +## the Free Software Foundation; either version 2 of the License, or +## (at your option) any later version. +## +## Spot is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +## License for more details. +## +## You should have received a copy of the GNU General Public License +## along with Spot; see the file COPYING. If not, write to the Free +## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +## 02111-1307, USA. + +nodist_noinst_SCRIPTS = spot.py +EXTRA_DIST = $(srcdir)/spot.in README ltl2tgba.html css/ltl2tgba.css \ + css/tipTip.css js/jquery.tipTip.minified.js logos/lip6sys64.png \ + logos/lrde64.png logos/spot64s.png \ + css/ui-lightness/jquery-ui-1.8.8.custom.css \ + css/ui-lightness/images/ui-icons_222222_256x240.png \ + css/ui-lightness/images/ui-bg_glass_100_f6f6f6_1x400.png \ + css/ui-lightness/images/ui-bg_glass_100_fdf5ce_1x400.png \ + css/ui-lightness/images/ui-bg_diagonals-thick_18_b81900_40x40.png \ + css/ui-lightness/images/ui-icons_ffd27a_256x240.png \ + css/ui-lightness/images/ui-icons_ffffff_256x240.png \ + css/ui-lightness/images/ui-icons_228ef1_256x240.png \ + css/ui-lightness/images/ui-bg_flat_10_000000_40x100.png \ + css/ui-lightness/images/ui-bg_highlight-soft_100_eeeeee_1x100.png \ + css/ui-lightness/images/ui-icons_ef8c08_256x240.png \ + css/ui-lightness/images/ui-bg_gloss-wave_35_f6a828_500x100.png \ + css/ui-lightness/images/ui-bg_glass_65_ffffff_1x400.png \ + css/ui-lightness/images/ui-bg_diagonals-thick_20_666666_40x40.png \ + css/ui-lightness/images/ui-bg_highlight-soft_75_ffe45c_1x100.png + +CLEANFILES = $(nodist_noinst_SCRIPTS) + +spot.py: $(srcdir)/spot.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' \ + <$(srcdir)/spot.in >spot.tmp + chmod +x spot.tmp + mv -f spot.tmp $@ + +clean-local: + rm -rf spotimg diff --git a/wrap/python/ajax/README b/wrap/python/ajax/README new file mode 100644 index 000000000..714334f59 --- /dev/null +++ b/wrap/python/ajax/README @@ -0,0 +1,69 @@ +ltl2tgba.html is a dynamic web page that translates user-supplied LTL +formulae to Transition-based Generalized Büchi Automata. The actual +translation work is performed by a CGI script in Python: spot.py. + +This is actually meant to be a moderner rewrite of the cgi script in +../cgi-bin/ + +There are two ways to use the page: 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. + + + +Standalone usage +================ + +Simply run the spot.py from this directory. This will create a +directory called spotimg/ in the current directory (this will hold the +generated pictures) and start an HTTP server on port 8000. Point your +browser to http://localhost:8000/ltl2tgba.html and you should be OK. + +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 spot.py to some place were CGI execution is allowed. + Depending on your HTTP server's configuration, you may have + to rename the script as spot.cgi or something else, so + 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 + AddHandle cgi-script .py + + # Allow CGI execution in some directory. + Options +ExecCGI + +3) In the directory where you have installed spot.py, + create a subdirectory called spotimg/. This is where + the script will output 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. + + spot.py purges old files (>15min) from this directory + each time it runs. + +4) Copy the directories css/, js/, and logos/ along with ltl2tgba.html + to there destination. You may have to adjust a few paths at the + top of the html page. diff --git a/wrap/python/ajax/css/ltl2tgba.css b/wrap/python/ajax/css/ltl2tgba.css new file mode 100644 index 000000000..19a3e605e --- /dev/null +++ b/wrap/python/ajax/css/ltl2tgba.css @@ -0,0 +1,76 @@ + +html {overflow-y:scroll;} + +.ltl2tgba .ui-widget { + font-size: 1em; +} + +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; +} +#lrdelogo { + position:fixed; + left:10px; + bottom:84px; + z-index:1; +} +#lip6logo { + position:fixed; + left:10px; + bottom:10px; + z-index:1; +} + +.ltl2tgba div.ui-widget-content { + padding: 3px; + margin: 2px 0px; +} + +.ltl2tgba h3 { + font-size:1em; + margin: 0; + padding: 0px 0.2em 0px; + border-bottom:1px solid #eee; + text-transform: capitalize; +} + +.ltl2tgba .head .ui-icon { + float: right; + margin: 0.2em 0px; +} + +.ltl2tgba .formula, #tiptip_content .formula { + font-family: monospace; + font-weight: bold; + font-size: 1.1em; +} + +.ltl2tgba .parse-error { + font-family: monospace; + white-space: pre; + color: red; + font-size: 1.1em; +} + +.ltl2tgba .ec-error { + color: red; +} + +.ltl2tgba .neverclaim, .ltl2tgba .accrun { + font-family: monospace; + white-space: pre; + font-size: 1.1em; +} diff --git a/wrap/python/ajax/css/tipTip.css b/wrap/python/ajax/css/tipTip.css new file mode 100644 index 000000000..70e54f971 --- /dev/null +++ b/wrap/python/ajax/css/tipTip.css @@ -0,0 +1,114 @@ +/* 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); + } +} diff --git a/wrap/python/ajax/css/ui-lightness/images/ui-bg_diagonals-thick_18_b81900_40x40.png b/wrap/python/ajax/css/ui-lightness/images/ui-bg_diagonals-thick_18_b81900_40x40.png new file mode 100644 index 000000000..954e22dbd Binary files /dev/null and b/wrap/python/ajax/css/ui-lightness/images/ui-bg_diagonals-thick_18_b81900_40x40.png differ diff --git a/wrap/python/ajax/css/ui-lightness/images/ui-bg_diagonals-thick_20_666666_40x40.png b/wrap/python/ajax/css/ui-lightness/images/ui-bg_diagonals-thick_20_666666_40x40.png new file mode 100644 index 000000000..64ece5707 Binary files /dev/null and b/wrap/python/ajax/css/ui-lightness/images/ui-bg_diagonals-thick_20_666666_40x40.png differ diff --git a/wrap/python/ajax/css/ui-lightness/images/ui-bg_flat_10_000000_40x100.png b/wrap/python/ajax/css/ui-lightness/images/ui-bg_flat_10_000000_40x100.png new file mode 100644 index 000000000..abdc01082 Binary files /dev/null and b/wrap/python/ajax/css/ui-lightness/images/ui-bg_flat_10_000000_40x100.png differ diff --git a/wrap/python/ajax/css/ui-lightness/images/ui-bg_glass_100_f6f6f6_1x400.png b/wrap/python/ajax/css/ui-lightness/images/ui-bg_glass_100_f6f6f6_1x400.png new file mode 100644 index 000000000..9b383f4d2 Binary files /dev/null and b/wrap/python/ajax/css/ui-lightness/images/ui-bg_glass_100_f6f6f6_1x400.png differ diff --git a/wrap/python/ajax/css/ui-lightness/images/ui-bg_glass_100_fdf5ce_1x400.png b/wrap/python/ajax/css/ui-lightness/images/ui-bg_glass_100_fdf5ce_1x400.png new file mode 100644 index 000000000..a23baad25 Binary files /dev/null and b/wrap/python/ajax/css/ui-lightness/images/ui-bg_glass_100_fdf5ce_1x400.png differ diff --git a/wrap/python/ajax/css/ui-lightness/images/ui-bg_glass_65_ffffff_1x400.png b/wrap/python/ajax/css/ui-lightness/images/ui-bg_glass_65_ffffff_1x400.png new file mode 100644 index 000000000..42ccba269 Binary files /dev/null and b/wrap/python/ajax/css/ui-lightness/images/ui-bg_glass_65_ffffff_1x400.png differ diff --git a/wrap/python/ajax/css/ui-lightness/images/ui-bg_gloss-wave_35_f6a828_500x100.png b/wrap/python/ajax/css/ui-lightness/images/ui-bg_gloss-wave_35_f6a828_500x100.png new file mode 100644 index 000000000..39d5824d6 Binary files /dev/null and b/wrap/python/ajax/css/ui-lightness/images/ui-bg_gloss-wave_35_f6a828_500x100.png differ diff --git a/wrap/python/ajax/css/ui-lightness/images/ui-bg_highlight-soft_100_eeeeee_1x100.png b/wrap/python/ajax/css/ui-lightness/images/ui-bg_highlight-soft_100_eeeeee_1x100.png new file mode 100644 index 000000000..f1273672d Binary files /dev/null and b/wrap/python/ajax/css/ui-lightness/images/ui-bg_highlight-soft_100_eeeeee_1x100.png differ diff --git a/wrap/python/ajax/css/ui-lightness/images/ui-bg_highlight-soft_75_ffe45c_1x100.png b/wrap/python/ajax/css/ui-lightness/images/ui-bg_highlight-soft_75_ffe45c_1x100.png new file mode 100644 index 000000000..359397acf Binary files /dev/null and b/wrap/python/ajax/css/ui-lightness/images/ui-bg_highlight-soft_75_ffe45c_1x100.png differ diff --git a/wrap/python/ajax/css/ui-lightness/images/ui-icons_222222_256x240.png b/wrap/python/ajax/css/ui-lightness/images/ui-icons_222222_256x240.png new file mode 100644 index 000000000..b273ff111 Binary files /dev/null and b/wrap/python/ajax/css/ui-lightness/images/ui-icons_222222_256x240.png differ diff --git a/wrap/python/ajax/css/ui-lightness/images/ui-icons_228ef1_256x240.png b/wrap/python/ajax/css/ui-lightness/images/ui-icons_228ef1_256x240.png new file mode 100644 index 000000000..a641a371a Binary files /dev/null and b/wrap/python/ajax/css/ui-lightness/images/ui-icons_228ef1_256x240.png differ diff --git a/wrap/python/ajax/css/ui-lightness/images/ui-icons_ef8c08_256x240.png b/wrap/python/ajax/css/ui-lightness/images/ui-icons_ef8c08_256x240.png new file mode 100644 index 000000000..85e63e9f6 Binary files /dev/null and b/wrap/python/ajax/css/ui-lightness/images/ui-icons_ef8c08_256x240.png differ diff --git a/wrap/python/ajax/css/ui-lightness/images/ui-icons_ffd27a_256x240.png b/wrap/python/ajax/css/ui-lightness/images/ui-icons_ffd27a_256x240.png new file mode 100644 index 000000000..e117effa3 Binary files /dev/null and b/wrap/python/ajax/css/ui-lightness/images/ui-icons_ffd27a_256x240.png differ diff --git a/wrap/python/ajax/css/ui-lightness/images/ui-icons_ffffff_256x240.png b/wrap/python/ajax/css/ui-lightness/images/ui-icons_ffffff_256x240.png new file mode 100644 index 000000000..42f8f992c Binary files /dev/null and b/wrap/python/ajax/css/ui-lightness/images/ui-icons_ffffff_256x240.png differ diff --git a/wrap/python/ajax/css/ui-lightness/jquery-ui-1.8.8.custom.css b/wrap/python/ajax/css/ui-lightness/jquery-ui-1.8.8.custom.css new file mode 100644 index 000000000..f97e39265 --- /dev/null +++ b/wrap/python/ajax/css/ui-lightness/jquery-ui-1.8.8.custom.css @@ -0,0 +1,572 @@ +/* + * jQuery UI CSS Framework 1.8.8 + * + * Copyright 2010, AUTHORS.txt (http://jqueryui.com/about) + * Dual licensed under the MIT or GPL Version 2 licenses. + * http://jquery.org/license + * + * http://docs.jquery.com/UI/Theming/API + */ + +/* Layout helpers +----------------------------------*/ +.ui-helper-hidden { display: none; } +.ui-helper-hidden-accessible { position: absolute !important; clip: rect(1px 1px 1px 1px); clip: rect(1px,1px,1px,1px); } +.ui-helper-reset { margin: 0; padding: 0; border: 0; outline: 0; line-height: 1.3; text-decoration: none; font-size: 100%; list-style: none; } +.ui-helper-clearfix:after { content: "."; display: block; height: 0; clear: both; visibility: hidden; } +.ui-helper-clearfix { display: inline-block; } +/* required comment for clearfix to work in Opera \*/ +* html .ui-helper-clearfix { height:1%; } +.ui-helper-clearfix { display:block; } +/* end clearfix */ +.ui-helper-zfix { width: 100%; height: 100%; top: 0; left: 0; position: absolute; opacity: 0; filter:Alpha(Opacity=0); } + + +/* Interaction Cues +----------------------------------*/ +.ui-state-disabled { cursor: default !important; } + + +/* Icons +----------------------------------*/ + +/* states and images */ +.ui-icon { display: block; text-indent: -99999px; overflow: hidden; background-repeat: no-repeat; } + + +/* Misc visuals +----------------------------------*/ + +/* Overlays */ +.ui-widget-overlay { position: absolute; top: 0; left: 0; width: 100%; height: 100%; } + + +/* + * jQuery UI CSS Framework 1.8.8 + * + * Copyright 2010, AUTHORS.txt (http://jqueryui.com/about) + * Dual licensed under the MIT or GPL Version 2 licenses. + * http://jquery.org/license + * + * http://docs.jquery.com/UI/Theming/API + * + * To view and modify this theme, visit http://jqueryui.com/themeroller/?ffDefault=Trebuchet%20MS,%20Tahoma,%20Verdana,%20Arial,%20sans-serif&fwDefault=bold&fsDefault=1.1em&cornerRadius=4px&bgColorHeader=f6a828&bgTextureHeader=12_gloss_wave.png&bgImgOpacityHeader=35&borderColorHeader=e78f08&fcHeader=ffffff&iconColorHeader=ffffff&bgColorContent=eeeeee&bgTextureContent=03_highlight_soft.png&bgImgOpacityContent=100&borderColorContent=dddddd&fcContent=333333&iconColorContent=222222&bgColorDefault=f6f6f6&bgTextureDefault=02_glass.png&bgImgOpacityDefault=100&borderColorDefault=cccccc&fcDefault=1c94c4&iconColorDefault=ef8c08&bgColorHover=fdf5ce&bgTextureHover=02_glass.png&bgImgOpacityHover=100&borderColorHover=fbcb09&fcHover=c77405&iconColorHover=ef8c08&bgColorActive=ffffff&bgTextureActive=02_glass.png&bgImgOpacityActive=65&borderColorActive=fbd850&fcActive=eb8f00&iconColorActive=ef8c08&bgColorHighlight=ffe45c&bgTextureHighlight=03_highlight_soft.png&bgImgOpacityHighlight=75&borderColorHighlight=fed22f&fcHighlight=363636&iconColorHighlight=228ef1&bgColorError=b81900&bgTextureError=08_diagonals_thick.png&bgImgOpacityError=18&borderColorError=cd0a0a&fcError=ffffff&iconColorError=ffd27a&bgColorOverlay=666666&bgTextureOverlay=08_diagonals_thick.png&bgImgOpacityOverlay=20&opacityOverlay=50&bgColorShadow=000000&bgTextureShadow=01_flat.png&bgImgOpacityShadow=10&opacityShadow=20&thicknessShadow=5px&offsetTopShadow=-5px&offsetLeftShadow=-5px&cornerRadiusShadow=5px + */ + + +/* Component containers +----------------------------------*/ +.ui-widget { font-family: Trebuchet MS, Tahoma, Verdana, Arial, sans-serif; font-size: 1.1em; } +.ui-widget .ui-widget { font-size: 1em; } +.ui-widget input, .ui-widget select, .ui-widget textarea, .ui-widget button { font-family: Trebuchet MS, Tahoma, Verdana, Arial, sans-serif; font-size: 1em; } +.ui-widget-content { border: 1px solid #dddddd; background: #eeeeee url(images/ui-bg_highlight-soft_100_eeeeee_1x100.png) 50% top repeat-x; color: #333333; } +.ui-widget-content a { color: #333333; } +.ui-widget-header { border: 1px solid #e78f08; background: #f6a828 url(images/ui-bg_gloss-wave_35_f6a828_500x100.png) 50% 50% repeat-x; color: #ffffff; font-weight: bold; } +.ui-widget-header a { color: #ffffff; } + +/* Interaction states +----------------------------------*/ +.ui-state-default, .ui-widget-content .ui-state-default, .ui-widget-header .ui-state-default { border: 1px solid #cccccc; background: #f6f6f6 url(images/ui-bg_glass_100_f6f6f6_1x400.png) 50% 50% repeat-x; font-weight: bold; color: #1c94c4; } +.ui-state-default a, .ui-state-default a:link, .ui-state-default a:visited { color: #1c94c4; text-decoration: none; } +.ui-state-hover, .ui-widget-content .ui-state-hover, .ui-widget-header .ui-state-hover, .ui-state-focus, .ui-widget-content .ui-state-focus, .ui-widget-header .ui-state-focus { border: 1px solid #fbcb09; background: #fdf5ce url(images/ui-bg_glass_100_fdf5ce_1x400.png) 50% 50% repeat-x; font-weight: bold; color: #c77405; } +.ui-state-hover a, .ui-state-hover a:hover { color: #c77405; text-decoration: none; } +.ui-state-active, .ui-widget-content .ui-state-active, .ui-widget-header .ui-state-active { border: 1px solid #fbd850; background: #ffffff url(images/ui-bg_glass_65_ffffff_1x400.png) 50% 50% repeat-x; font-weight: bold; color: #eb8f00; } +.ui-state-active a, .ui-state-active a:link, .ui-state-active a:visited { color: #eb8f00; text-decoration: none; } +.ui-widget :active { outline: none; } + +/* Interaction Cues +----------------------------------*/ +.ui-state-highlight, .ui-widget-content .ui-state-highlight, .ui-widget-header .ui-state-highlight {border: 1px solid #fed22f; background: #ffe45c url(images/ui-bg_highlight-soft_75_ffe45c_1x100.png) 50% top repeat-x; color: #363636; } +.ui-state-highlight a, .ui-widget-content .ui-state-highlight a,.ui-widget-header .ui-state-highlight a { color: #363636; } +.ui-state-error, .ui-widget-content .ui-state-error, .ui-widget-header .ui-state-error {border: 1px solid #cd0a0a; background: #b81900 url(images/ui-bg_diagonals-thick_18_b81900_40x40.png) 50% 50% repeat; color: #ffffff; } +.ui-state-error a, .ui-widget-content .ui-state-error a, .ui-widget-header .ui-state-error a { color: #ffffff; } +.ui-state-error-text, .ui-widget-content .ui-state-error-text, .ui-widget-header .ui-state-error-text { color: #ffffff; } +.ui-priority-primary, .ui-widget-content .ui-priority-primary, .ui-widget-header .ui-priority-primary { font-weight: bold; } +.ui-priority-secondary, .ui-widget-content .ui-priority-secondary, .ui-widget-header .ui-priority-secondary { opacity: .7; filter:Alpha(Opacity=70); font-weight: normal; } +.ui-state-disabled, .ui-widget-content .ui-state-disabled, .ui-widget-header .ui-state-disabled { opacity: .35; filter:Alpha(Opacity=35); background-image: none; } + +/* Icons +----------------------------------*/ + +/* states and images */ +.ui-icon { width: 16px; height: 16px; background-image: url(images/ui-icons_222222_256x240.png); } +.ui-widget-content .ui-icon {background-image: url(images/ui-icons_222222_256x240.png); } +.ui-widget-header .ui-icon {background-image: url(images/ui-icons_ffffff_256x240.png); } +.ui-state-default .ui-icon { background-image: url(images/ui-icons_ef8c08_256x240.png); } +.ui-state-hover .ui-icon, .ui-state-focus .ui-icon {background-image: url(images/ui-icons_ef8c08_256x240.png); } +.ui-state-active .ui-icon {background-image: url(images/ui-icons_ef8c08_256x240.png); } +.ui-state-highlight .ui-icon {background-image: url(images/ui-icons_228ef1_256x240.png); } +.ui-state-error .ui-icon, .ui-state-error-text .ui-icon {background-image: url(images/ui-icons_ffd27a_256x240.png); } + +/* positioning */ +.ui-icon-carat-1-n { background-position: 0 0; } +.ui-icon-carat-1-ne { background-position: -16px 0; } +.ui-icon-carat-1-e { background-position: -32px 0; } +.ui-icon-carat-1-se { background-position: -48px 0; } +.ui-icon-carat-1-s { background-position: -64px 0; } +.ui-icon-carat-1-sw { background-position: -80px 0; } +.ui-icon-carat-1-w { background-position: -96px 0; } +.ui-icon-carat-1-nw { background-position: -112px 0; } +.ui-icon-carat-2-n-s { background-position: -128px 0; } +.ui-icon-carat-2-e-w { background-position: -144px 0; } +.ui-icon-triangle-1-n { background-position: 0 -16px; } +.ui-icon-triangle-1-ne { background-position: -16px -16px; } +.ui-icon-triangle-1-e { background-position: -32px -16px; } +.ui-icon-triangle-1-se { background-position: -48px -16px; } +.ui-icon-triangle-1-s { background-position: -64px -16px; } +.ui-icon-triangle-1-sw { background-position: -80px -16px; } +.ui-icon-triangle-1-w { background-position: -96px -16px; } +.ui-icon-triangle-1-nw { background-position: -112px -16px; } +.ui-icon-triangle-2-n-s { background-position: -128px -16px; } +.ui-icon-triangle-2-e-w { background-position: -144px -16px; } +.ui-icon-arrow-1-n { background-position: 0 -32px; } +.ui-icon-arrow-1-ne { background-position: -16px -32px; } +.ui-icon-arrow-1-e { background-position: -32px -32px; } +.ui-icon-arrow-1-se { background-position: -48px -32px; } +.ui-icon-arrow-1-s { background-position: -64px -32px; } +.ui-icon-arrow-1-sw { background-position: -80px -32px; } +.ui-icon-arrow-1-w { background-position: -96px -32px; } +.ui-icon-arrow-1-nw { background-position: -112px -32px; } +.ui-icon-arrow-2-n-s { background-position: -128px -32px; } +.ui-icon-arrow-2-ne-sw { background-position: -144px -32px; } +.ui-icon-arrow-2-e-w { background-position: -160px -32px; } +.ui-icon-arrow-2-se-nw { background-position: -176px -32px; } +.ui-icon-arrowstop-1-n { background-position: -192px -32px; } +.ui-icon-arrowstop-1-e { background-position: -208px -32px; } +.ui-icon-arrowstop-1-s { background-position: -224px -32px; } +.ui-icon-arrowstop-1-w { background-position: -240px -32px; } +.ui-icon-arrowthick-1-n { background-position: 0 -48px; } +.ui-icon-arrowthick-1-ne { background-position: -16px -48px; } +.ui-icon-arrowthick-1-e { background-position: -32px -48px; } +.ui-icon-arrowthick-1-se { background-position: -48px -48px; } +.ui-icon-arrowthick-1-s { background-position: -64px -48px; } +.ui-icon-arrowthick-1-sw { background-position: -80px -48px; } +.ui-icon-arrowthick-1-w { background-position: -96px -48px; } +.ui-icon-arrowthick-1-nw { background-position: -112px -48px; } +.ui-icon-arrowthick-2-n-s { background-position: -128px -48px; } +.ui-icon-arrowthick-2-ne-sw { background-position: -144px -48px; } +.ui-icon-arrowthick-2-e-w { background-position: -160px -48px; } +.ui-icon-arrowthick-2-se-nw { background-position: -176px -48px; } +.ui-icon-arrowthickstop-1-n { background-position: -192px -48px; } +.ui-icon-arrowthickstop-1-e { background-position: -208px -48px; } +.ui-icon-arrowthickstop-1-s { background-position: -224px -48px; } +.ui-icon-arrowthickstop-1-w { background-position: -240px -48px; } +.ui-icon-arrowreturnthick-1-w { background-position: 0 -64px; } +.ui-icon-arrowreturnthick-1-n { background-position: -16px -64px; } +.ui-icon-arrowreturnthick-1-e { background-position: -32px -64px; } +.ui-icon-arrowreturnthick-1-s { background-position: -48px -64px; } +.ui-icon-arrowreturn-1-w { background-position: -64px -64px; } +.ui-icon-arrowreturn-1-n { background-position: -80px -64px; } +.ui-icon-arrowreturn-1-e { background-position: -96px -64px; } +.ui-icon-arrowreturn-1-s { background-position: -112px -64px; } +.ui-icon-arrowrefresh-1-w { background-position: -128px -64px; } +.ui-icon-arrowrefresh-1-n { background-position: -144px -64px; } +.ui-icon-arrowrefresh-1-e { background-position: -160px -64px; } +.ui-icon-arrowrefresh-1-s { background-position: -176px -64px; } +.ui-icon-arrow-4 { background-position: 0 -80px; } +.ui-icon-arrow-4-diag { background-position: -16px -80px; } +.ui-icon-extlink { background-position: -32px -80px; } +.ui-icon-newwin { background-position: -48px -80px; } +.ui-icon-refresh { background-position: -64px -80px; } +.ui-icon-shuffle { background-position: -80px -80px; } +.ui-icon-transfer-e-w { background-position: -96px -80px; } +.ui-icon-transferthick-e-w { background-position: -112px -80px; } +.ui-icon-folder-collapsed { background-position: 0 -96px; } +.ui-icon-folder-open { background-position: -16px -96px; } +.ui-icon-document { background-position: -32px -96px; } +.ui-icon-document-b { background-position: -48px -96px; } +.ui-icon-note { background-position: -64px -96px; } +.ui-icon-mail-closed { background-position: -80px -96px; } +.ui-icon-mail-open { background-position: -96px -96px; } +.ui-icon-suitcase { background-position: -112px -96px; } +.ui-icon-comment { background-position: -128px -96px; } +.ui-icon-person { background-position: -144px -96px; } +.ui-icon-print { background-position: -160px -96px; } +.ui-icon-trash { background-position: -176px -96px; } +.ui-icon-locked { background-position: -192px -96px; } +.ui-icon-unlocked { background-position: -208px -96px; } +.ui-icon-bookmark { background-position: -224px -96px; } +.ui-icon-tag { background-position: -240px -96px; } +.ui-icon-home { background-position: 0 -112px; } +.ui-icon-flag { background-position: -16px -112px; } +.ui-icon-calendar { background-position: -32px -112px; } +.ui-icon-cart { background-position: -48px -112px; } +.ui-icon-pencil { background-position: -64px -112px; } +.ui-icon-clock { background-position: -80px -112px; } +.ui-icon-disk { background-position: -96px -112px; } +.ui-icon-calculator { background-position: -112px -112px; } +.ui-icon-zoomin { background-position: -128px -112px; } +.ui-icon-zoomout { background-position: -144px -112px; } +.ui-icon-search { background-position: -160px -112px; } +.ui-icon-wrench { background-position: -176px -112px; } +.ui-icon-gear { background-position: -192px -112px; } +.ui-icon-heart { background-position: -208px -112px; } +.ui-icon-star { background-position: -224px -112px; } +.ui-icon-link { background-position: -240px -112px; } +.ui-icon-cancel { background-position: 0 -128px; } +.ui-icon-plus { background-position: -16px -128px; } +.ui-icon-plusthick { background-position: -32px -128px; } +.ui-icon-minus { background-position: -48px -128px; } +.ui-icon-minusthick { background-position: -64px -128px; } +.ui-icon-close { background-position: -80px -128px; } +.ui-icon-closethick { background-position: -96px -128px; } +.ui-icon-key { background-position: -112px -128px; } +.ui-icon-lightbulb { background-position: -128px -128px; } +.ui-icon-scissors { background-position: -144px -128px; } +.ui-icon-clipboard { background-position: -160px -128px; } +.ui-icon-copy { background-position: -176px -128px; } +.ui-icon-contact { background-position: -192px -128px; } +.ui-icon-image { background-position: -208px -128px; } +.ui-icon-video { background-position: -224px -128px; } +.ui-icon-script { background-position: -240px -128px; } +.ui-icon-alert { background-position: 0 -144px; } +.ui-icon-info { background-position: -16px -144px; } +.ui-icon-notice { background-position: -32px -144px; } +.ui-icon-help { background-position: -48px -144px; } +.ui-icon-check { background-position: -64px -144px; } +.ui-icon-bullet { background-position: -80px -144px; } +.ui-icon-radio-off { background-position: -96px -144px; } +.ui-icon-radio-on { background-position: -112px -144px; } +.ui-icon-pin-w { background-position: -128px -144px; } +.ui-icon-pin-s { background-position: -144px -144px; } +.ui-icon-play { background-position: 0 -160px; } +.ui-icon-pause { background-position: -16px -160px; } +.ui-icon-seek-next { background-position: -32px -160px; } +.ui-icon-seek-prev { background-position: -48px -160px; } +.ui-icon-seek-end { background-position: -64px -160px; } +.ui-icon-seek-start { background-position: -80px -160px; } +/* ui-icon-seek-first is deprecated, use ui-icon-seek-start instead */ +.ui-icon-seek-first { background-position: -80px -160px; } +.ui-icon-stop { background-position: -96px -160px; } +.ui-icon-eject { background-position: -112px -160px; } +.ui-icon-volume-off { background-position: -128px -160px; } +.ui-icon-volume-on { background-position: -144px -160px; } +.ui-icon-power { background-position: 0 -176px; } +.ui-icon-signal-diag { background-position: -16px -176px; } +.ui-icon-signal { background-position: -32px -176px; } +.ui-icon-battery-0 { background-position: -48px -176px; } +.ui-icon-battery-1 { background-position: -64px -176px; } +.ui-icon-battery-2 { background-position: -80px -176px; } +.ui-icon-battery-3 { background-position: -96px -176px; } +.ui-icon-circle-plus { background-position: 0 -192px; } +.ui-icon-circle-minus { background-position: -16px -192px; } +.ui-icon-circle-close { background-position: -32px -192px; } +.ui-icon-circle-triangle-e { background-position: -48px -192px; } +.ui-icon-circle-triangle-s { background-position: -64px -192px; } +.ui-icon-circle-triangle-w { background-position: -80px -192px; } +.ui-icon-circle-triangle-n { background-position: -96px -192px; } +.ui-icon-circle-arrow-e { background-position: -112px -192px; } +.ui-icon-circle-arrow-s { background-position: -128px -192px; } +.ui-icon-circle-arrow-w { background-position: -144px -192px; } +.ui-icon-circle-arrow-n { background-position: -160px -192px; } +.ui-icon-circle-zoomin { background-position: -176px -192px; } +.ui-icon-circle-zoomout { background-position: -192px -192px; } +.ui-icon-circle-check { background-position: -208px -192px; } +.ui-icon-circlesmall-plus { background-position: 0 -208px; } +.ui-icon-circlesmall-minus { background-position: -16px -208px; } +.ui-icon-circlesmall-close { background-position: -32px -208px; } +.ui-icon-squaresmall-plus { background-position: -48px -208px; } +.ui-icon-squaresmall-minus { background-position: -64px -208px; } +.ui-icon-squaresmall-close { background-position: -80px -208px; } +.ui-icon-grip-dotted-vertical { background-position: 0 -224px; } +.ui-icon-grip-dotted-horizontal { background-position: -16px -224px; } +.ui-icon-grip-solid-vertical { background-position: -32px -224px; } +.ui-icon-grip-solid-horizontal { background-position: -48px -224px; } +.ui-icon-gripsmall-diagonal-se { background-position: -64px -224px; } +.ui-icon-grip-diagonal-se { background-position: -80px -224px; } + + +/* Misc visuals +----------------------------------*/ + +/* Corner radius */ +.ui-corner-tl { -moz-border-radius-topleft: 4px; -webkit-border-top-left-radius: 4px; border-top-left-radius: 4px; } +.ui-corner-tr { -moz-border-radius-topright: 4px; -webkit-border-top-right-radius: 4px; border-top-right-radius: 4px; } +.ui-corner-bl { -moz-border-radius-bottomleft: 4px; -webkit-border-bottom-left-radius: 4px; border-bottom-left-radius: 4px; } +.ui-corner-br { -moz-border-radius-bottomright: 4px; -webkit-border-bottom-right-radius: 4px; border-bottom-right-radius: 4px; } +.ui-corner-top { -moz-border-radius-topleft: 4px; -webkit-border-top-left-radius: 4px; border-top-left-radius: 4px; -moz-border-radius-topright: 4px; -webkit-border-top-right-radius: 4px; border-top-right-radius: 4px; } +.ui-corner-bottom { -moz-border-radius-bottomleft: 4px; -webkit-border-bottom-left-radius: 4px; border-bottom-left-radius: 4px; -moz-border-radius-bottomright: 4px; -webkit-border-bottom-right-radius: 4px; border-bottom-right-radius: 4px; } +.ui-corner-right { -moz-border-radius-topright: 4px; -webkit-border-top-right-radius: 4px; border-top-right-radius: 4px; -moz-border-radius-bottomright: 4px; -webkit-border-bottom-right-radius: 4px; border-bottom-right-radius: 4px; } +.ui-corner-left { -moz-border-radius-topleft: 4px; -webkit-border-top-left-radius: 4px; border-top-left-radius: 4px; -moz-border-radius-bottomleft: 4px; -webkit-border-bottom-left-radius: 4px; border-bottom-left-radius: 4px; } +.ui-corner-all { -moz-border-radius: 4px; -webkit-border-radius: 4px; border-radius: 4px; } + +/* Overlays */ +.ui-widget-overlay { background: #666666 url(images/ui-bg_diagonals-thick_20_666666_40x40.png) 50% 50% repeat; opacity: .50;filter:Alpha(Opacity=50); } +.ui-widget-shadow { margin: -5px 0 0 -5px; padding: 5px; background: #000000 url(images/ui-bg_flat_10_000000_40x100.png) 50% 50% repeat-x; opacity: .20;filter:Alpha(Opacity=20); -moz-border-radius: 5px; -webkit-border-radius: 5px; border-radius: 5px; }/* + * jQuery UI Resizable 1.8.8 + * + * Copyright 2010, AUTHORS.txt (http://jqueryui.com/about) + * Dual licensed under the MIT or GPL Version 2 licenses. + * http://jquery.org/license + * + * http://docs.jquery.com/UI/Resizable#theming + */ +.ui-resizable { position: relative;} +.ui-resizable-handle { position: absolute;font-size: 0.1px;z-index: 99999; display: block;} +.ui-resizable-disabled .ui-resizable-handle, .ui-resizable-autohide .ui-resizable-handle { display: none; } +.ui-resizable-n { cursor: n-resize; height: 7px; width: 100%; top: -5px; left: 0; } +.ui-resizable-s { cursor: s-resize; height: 7px; width: 100%; bottom: -5px; left: 0; } +.ui-resizable-e { cursor: e-resize; width: 7px; right: -5px; top: 0; height: 100%; } +.ui-resizable-w { cursor: w-resize; width: 7px; left: -5px; top: 0; height: 100%; } +.ui-resizable-se { cursor: se-resize; width: 12px; height: 12px; right: 1px; bottom: 1px; } +.ui-resizable-sw { cursor: sw-resize; width: 9px; height: 9px; left: -5px; bottom: -5px; } +.ui-resizable-nw { cursor: nw-resize; width: 9px; height: 9px; left: -5px; top: -5px; } +.ui-resizable-ne { cursor: ne-resize; width: 9px; height: 9px; right: -5px; top: -5px;}/* + * jQuery UI Selectable 1.8.8 + * + * Copyright 2010, AUTHORS.txt (http://jqueryui.com/about) + * Dual licensed under the MIT or GPL Version 2 licenses. + * http://jquery.org/license + * + * http://docs.jquery.com/UI/Selectable#theming + */ +.ui-selectable-helper { position: absolute; z-index: 100; border:1px dotted black; } +/* + * jQuery UI Accordion 1.8.8 + * + * Copyright 2010, AUTHORS.txt (http://jqueryui.com/about) + * Dual licensed under the MIT or GPL Version 2 licenses. + * http://jquery.org/license + * + * http://docs.jquery.com/UI/Accordion#theming + */ +/* IE/Win - Fix animation bug - #4615 */ +.ui-accordion { width: 100%; } +.ui-accordion .ui-accordion-header { cursor: pointer; position: relative; margin-top: 1px; zoom: 1; } +.ui-accordion .ui-accordion-li-fix { display: inline; } +.ui-accordion .ui-accordion-header-active { border-bottom: 0 !important; } +.ui-accordion .ui-accordion-header a { display: block; font-size: 1em; padding: .5em .5em .5em .7em; } +.ui-accordion-icons .ui-accordion-header a { padding-left: 2.2em; } +.ui-accordion .ui-accordion-header .ui-icon { position: absolute; left: .5em; top: 50%; margin-top: -8px; } +.ui-accordion .ui-accordion-content { padding: 1em 2.2em; border-top: 0; margin-top: -2px; position: relative; top: 1px; margin-bottom: 2px; overflow: auto; display: none; zoom: 1; } +.ui-accordion .ui-accordion-content-active { display: block; }/* + * jQuery UI Autocomplete 1.8.8 + * + * Copyright 2010, AUTHORS.txt (http://jqueryui.com/about) + * Dual licensed under the MIT or GPL Version 2 licenses. + * http://jquery.org/license + * + * http://docs.jquery.com/UI/Autocomplete#theming + */ +.ui-autocomplete { position: absolute; cursor: default; } + +/* workarounds */ +* html .ui-autocomplete { width:1px; } /* without this, the menu expands to 100% in IE6 */ + +/* + * jQuery UI Menu 1.8.8 + * + * Copyright 2010, AUTHORS.txt (http://jqueryui.com/about) + * Dual licensed under the MIT or GPL Version 2 licenses. + * http://jquery.org/license + * + * http://docs.jquery.com/UI/Menu#theming + */ +.ui-menu { + list-style:none; + padding: 2px; + margin: 0; + display:block; + float: left; +} +.ui-menu .ui-menu { + margin-top: -3px; +} +.ui-menu .ui-menu-item { + margin:0; + padding: 0; + zoom: 1; + float: left; + clear: left; + width: 100%; +} +.ui-menu .ui-menu-item a { + text-decoration:none; + display:block; + padding:.2em .4em; + line-height:1.5; + zoom:1; +} +.ui-menu .ui-menu-item a.ui-state-hover, +.ui-menu .ui-menu-item a.ui-state-active { + font-weight: normal; + margin: -1px; +} +/* + * jQuery UI Button 1.8.8 + * + * Copyright 2010, AUTHORS.txt (http://jqueryui.com/about) + * Dual licensed under the MIT or GPL Version 2 licenses. + * http://jquery.org/license + * + * http://docs.jquery.com/UI/Button#theming + */ +.ui-button { display: inline-block; position: relative; padding: 0; margin-right: .1em; text-decoration: none !important; cursor: pointer; text-align: center; zoom: 1; overflow: visible; } /* the overflow property removes extra width in IE */ +.ui-button-icon-only { width: 2.2em; } /* to make room for the icon, a width needs to be set here */ +button.ui-button-icon-only { width: 2.4em; } /* button elements seem to need a little more width */ +.ui-button-icons-only { width: 3.4em; } +button.ui-button-icons-only { width: 3.7em; } + +/*button text element */ +.ui-button .ui-button-text { display: block; line-height: 1.4; } +.ui-button-text-only .ui-button-text { padding: .1em .3em; } +.ui-button-icon-only .ui-button-text, .ui-button-icons-only .ui-button-text { padding: .4em; text-indent: -9999999px; } +.ui-button-text-icon-primary .ui-button-text, .ui-button-text-icons .ui-button-text { padding: .4em 1em .4em 2.1em; } +.ui-button-text-icon-secondary .ui-button-text, .ui-button-text-icons .ui-button-text { padding: .4em 2.1em .4em 1em; } +.ui-button-text-icons .ui-button-text { padding-left: 2.1em; padding-right: 2.1em; } +/* no icon support for input elements, provide padding by default */ +input.ui-button { padding: .4em 1em; } + +/*button icon element(s) */ +.ui-button-icon-only .ui-icon, .ui-button-text-icon-primary .ui-icon, .ui-button-text-icon-secondary .ui-icon, .ui-button-text-icons .ui-icon, .ui-button-icons-only .ui-icon { position: absolute; top: 50%; margin-top: -8px; } +.ui-button-icon-only .ui-icon { left: 50%; margin-left: -8px; } +.ui-button-text-icon-primary .ui-button-icon-primary, .ui-button-text-icons .ui-button-icon-primary, .ui-button-icons-only .ui-button-icon-primary { left: .5em; } +.ui-button-text-icon-secondary .ui-button-icon-secondary, .ui-button-text-icons .ui-button-icon-secondary, .ui-button-icons-only .ui-button-icon-secondary { right: .5em; } +.ui-button-text-icons .ui-button-icon-secondary, .ui-button-icons-only .ui-button-icon-secondary { right: .5em; } + +/*button sets*/ +.ui-buttonset { margin-right: 7px; } +.ui-buttonset .ui-button { margin-left: 0; margin-right: -.3em; } + +/* workarounds */ +button.ui-button::-moz-focus-inner { border: 0; padding: 0; } /* reset extra padding in Firefox */ +/* + * jQuery UI Dialog 1.8.8 + * + * Copyright 2010, AUTHORS.txt (http://jqueryui.com/about) + * Dual licensed under the MIT or GPL Version 2 licenses. + * http://jquery.org/license + * + * http://docs.jquery.com/UI/Dialog#theming + */ +.ui-dialog { position: absolute; padding: .2em; width: 300px; overflow: hidden; } +.ui-dialog .ui-dialog-titlebar { padding: .4em 1em; position: relative; } +.ui-dialog .ui-dialog-title { float: left; margin: .1em 16px .1em 0; } +.ui-dialog .ui-dialog-titlebar-close { position: absolute; right: .3em; top: 50%; width: 19px; margin: -10px 0 0 0; padding: 1px; height: 18px; } +.ui-dialog .ui-dialog-titlebar-close span { display: block; margin: 1px; } +.ui-dialog .ui-dialog-titlebar-close:hover, .ui-dialog .ui-dialog-titlebar-close:focus { padding: 0; } +.ui-dialog .ui-dialog-content { position: relative; border: 0; padding: .5em 1em; background: none; overflow: auto; zoom: 1; } +.ui-dialog .ui-dialog-buttonpane { text-align: left; border-width: 1px 0 0 0; background-image: none; margin: .5em 0 0 0; padding: .3em 1em .5em .4em; } +.ui-dialog .ui-dialog-buttonpane .ui-dialog-buttonset { float: right; } +.ui-dialog .ui-dialog-buttonpane button { margin: .5em .4em .5em 0; cursor: pointer; } +.ui-dialog .ui-resizable-se { width: 14px; height: 14px; right: 3px; bottom: 3px; } +.ui-draggable .ui-dialog-titlebar { cursor: move; } +/* + * jQuery UI Slider 1.8.8 + * + * Copyright 2010, AUTHORS.txt (http://jqueryui.com/about) + * Dual licensed under the MIT or GPL Version 2 licenses. + * http://jquery.org/license + * + * http://docs.jquery.com/UI/Slider#theming + */ +.ui-slider { position: relative; text-align: left; } +.ui-slider .ui-slider-handle { position: absolute; z-index: 2; width: 1.2em; height: 1.2em; cursor: default; } +.ui-slider .ui-slider-range { position: absolute; z-index: 1; font-size: .7em; display: block; border: 0; background-position: 0 0; } + +.ui-slider-horizontal { height: .8em; } +.ui-slider-horizontal .ui-slider-handle { top: -.3em; margin-left: -.6em; } +.ui-slider-horizontal .ui-slider-range { top: 0; height: 100%; } +.ui-slider-horizontal .ui-slider-range-min { left: 0; } +.ui-slider-horizontal .ui-slider-range-max { right: 0; } + +.ui-slider-vertical { width: .8em; height: 100px; } +.ui-slider-vertical .ui-slider-handle { left: -.3em; margin-left: 0; margin-bottom: -.6em; } +.ui-slider-vertical .ui-slider-range { left: 0; width: 100%; } +.ui-slider-vertical .ui-slider-range-min { bottom: 0; } +.ui-slider-vertical .ui-slider-range-max { top: 0; }/* + * jQuery UI Tabs 1.8.8 + * + * Copyright 2010, AUTHORS.txt (http://jqueryui.com/about) + * Dual licensed under the MIT or GPL Version 2 licenses. + * http://jquery.org/license + * + * http://docs.jquery.com/UI/Tabs#theming + */ +.ui-tabs { position: relative; padding: .2em; zoom: 1; } /* position: relative prevents IE scroll bug (element with position: relative inside container with overflow: auto appear as "fixed") */ +.ui-tabs .ui-tabs-nav { margin: 0; padding: .2em .2em 0; } +.ui-tabs .ui-tabs-nav li { list-style: none; float: left; position: relative; top: 1px; margin: 0 .2em 1px 0; border-bottom: 0 !important; padding: 0; white-space: nowrap; } +.ui-tabs .ui-tabs-nav li a { float: left; padding: .1em .3em; text-decoration: none; } +.ui-tabs .ui-tabs-nav li.ui-tabs-selected { margin-bottom: 0; padding-bottom: 1px; } +.ui-tabs .ui-tabs-nav li.ui-tabs-selected a, .ui-tabs .ui-tabs-nav li.ui-state-disabled a, .ui-tabs .ui-tabs-nav li.ui-state-processing a { cursor: text; } +.ui-tabs .ui-tabs-nav li a, .ui-tabs.ui-tabs-collapsible .ui-tabs-nav li.ui-tabs-selected a { cursor: pointer; } /* first selector in group seems obsolete, but required to overcome bug in Opera applying cursor: text overall if defined elsewhere... */ +.ui-tabs .ui-tabs-panel { display: block; border-width: 0; padding: 1em 1.4em; background: none; } +.ui-tabs .ui-tabs-hide { display: none !important; } +/* + * jQuery UI Datepicker 1.8.8 + * + * Copyright 2010, AUTHORS.txt (http://jqueryui.com/about) + * Dual licensed under the MIT or GPL Version 2 licenses. + * http://jquery.org/license + * + * http://docs.jquery.com/UI/Datepicker#theming + */ +.ui-datepicker { width: 17em; padding: .2em .2em 0; display: none; } +.ui-datepicker .ui-datepicker-header { position:relative; padding:.2em 0; } +.ui-datepicker .ui-datepicker-prev, .ui-datepicker .ui-datepicker-next { position:absolute; top: 2px; width: 1.8em; height: 1.8em; } +.ui-datepicker .ui-datepicker-prev-hover, .ui-datepicker .ui-datepicker-next-hover { top: 1px; } +.ui-datepicker .ui-datepicker-prev { left:2px; } +.ui-datepicker .ui-datepicker-next { right:2px; } +.ui-datepicker .ui-datepicker-prev-hover { left:1px; } +.ui-datepicker .ui-datepicker-next-hover { right:1px; } +.ui-datepicker .ui-datepicker-prev span, .ui-datepicker .ui-datepicker-next span { display: block; position: absolute; left: 50%; margin-left: -8px; top: 50%; margin-top: -8px; } +.ui-datepicker .ui-datepicker-title { margin: 0 2.3em; line-height: 1.8em; text-align: center; } +.ui-datepicker .ui-datepicker-title select { font-size:1em; margin:1px 0; } +.ui-datepicker select.ui-datepicker-month-year {width: 100%;} +.ui-datepicker select.ui-datepicker-month, +.ui-datepicker select.ui-datepicker-year { width: 49%;} +.ui-datepicker table {width: 100%; font-size: .9em; border-collapse: collapse; margin:0 0 .4em; } +.ui-datepicker th { padding: .7em .3em; text-align: center; font-weight: bold; border: 0; } +.ui-datepicker td { border: 0; padding: 1px; } +.ui-datepicker td span, .ui-datepicker td a { display: block; padding: .2em; text-align: right; text-decoration: none; } +.ui-datepicker .ui-datepicker-buttonpane { background-image: none; margin: .7em 0 0 0; padding:0 .2em; border-left: 0; border-right: 0; border-bottom: 0; } +.ui-datepicker .ui-datepicker-buttonpane button { float: right; margin: .5em .2em .4em; cursor: pointer; padding: .2em .6em .3em .6em; width:auto; overflow:visible; } +.ui-datepicker .ui-datepicker-buttonpane button.ui-datepicker-current { float:left; } + +/* with multiple calendars */ +.ui-datepicker.ui-datepicker-multi { width:auto; } +.ui-datepicker-multi .ui-datepicker-group { float:left; } +.ui-datepicker-multi .ui-datepicker-group table { width:95%; margin:0 auto .4em; } +.ui-datepicker-multi-2 .ui-datepicker-group { width:50%; } +.ui-datepicker-multi-3 .ui-datepicker-group { width:33.3%; } +.ui-datepicker-multi-4 .ui-datepicker-group { width:25%; } +.ui-datepicker-multi .ui-datepicker-group-last .ui-datepicker-header { border-left-width:0; } +.ui-datepicker-multi .ui-datepicker-group-middle .ui-datepicker-header { border-left-width:0; } +.ui-datepicker-multi .ui-datepicker-buttonpane { clear:left; } +.ui-datepicker-row-break { clear:both; width:100%; } + +/* RTL support */ +.ui-datepicker-rtl { direction: rtl; } +.ui-datepicker-rtl .ui-datepicker-prev { right: 2px; left: auto; } +.ui-datepicker-rtl .ui-datepicker-next { left: 2px; right: auto; } +.ui-datepicker-rtl .ui-datepicker-prev:hover { right: 1px; left: auto; } +.ui-datepicker-rtl .ui-datepicker-next:hover { left: 1px; right: auto; } +.ui-datepicker-rtl .ui-datepicker-buttonpane { clear:right; } +.ui-datepicker-rtl .ui-datepicker-buttonpane button { float: left; } +.ui-datepicker-rtl .ui-datepicker-buttonpane button.ui-datepicker-current { float:right; } +.ui-datepicker-rtl .ui-datepicker-group { float:right; } +.ui-datepicker-rtl .ui-datepicker-group-last .ui-datepicker-header { border-right-width:0; border-left-width:1px; } +.ui-datepicker-rtl .ui-datepicker-group-middle .ui-datepicker-header { border-right-width:0; border-left-width:1px; } + +/* IE6 IFRAME FIX (taken from datepicker 1.5.3 */ +.ui-datepicker-cover { + display: none; /*sorry for IE5*/ + display/**/: block; /*sorry for IE5*/ + position: absolute; /*must have*/ + z-index: -1; /*must have*/ + filter: mask(); /*must have*/ + top: -4px; /*must have*/ + left: -4px; /*must have*/ + width: 200px; /*must have*/ + height: 200px; /*must have*/ +}/* + * jQuery UI Progressbar 1.8.8 + * + * Copyright 2010, AUTHORS.txt (http://jqueryui.com/about) + * Dual licensed under the MIT or GPL Version 2 licenses. + * http://jquery.org/license + * + * http://docs.jquery.com/UI/Progressbar#theming + */ +.ui-progressbar { height:2em; text-align: left; } +.ui-progressbar .ui-progressbar-value {margin: -1px; height:100%; } diff --git a/wrap/python/ajax/js/jquery.tipTip.minified.js b/wrap/python/ajax/js/jquery.tipTip.minified.js new file mode 100644 index 000000000..cdf3a892b --- /dev/null +++ b/wrap/python/ajax/js/jquery.tipTip.minified.js @@ -0,0 +1,21 @@ + /* + * 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=$('
');var tiptip_content=$('
');var tiptip_arrow=$('
');$("body").append(tiptip_holder.html(tiptip_content).prepend(tiptip_arrow.html('
')))}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).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); \ No newline at end of file diff --git a/wrap/python/ajax/logos/lip6sys64.png b/wrap/python/ajax/logos/lip6sys64.png new file mode 100644 index 000000000..a6e43c2f8 Binary files /dev/null and b/wrap/python/ajax/logos/lip6sys64.png differ diff --git a/wrap/python/ajax/logos/lrde64.png b/wrap/python/ajax/logos/lrde64.png new file mode 100644 index 000000000..f1091dc29 Binary files /dev/null and b/wrap/python/ajax/logos/lrde64.png differ diff --git a/wrap/python/ajax/logos/spot64s.png b/wrap/python/ajax/logos/spot64s.png new file mode 100644 index 000000000..a6d8e91e8 Binary files /dev/null and b/wrap/python/ajax/logos/spot64s.png differ diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html new file mode 100644 index 000000000..3b603b2cb --- /dev/null +++ b/wrap/python/ajax/ltl2tgba.html @@ -0,0 +1,403 @@ + + + + Spot's on-line LTL-to-TGBA translator + + + + + + + + + + + + + + + +
+ +

+

+

LTL Formula to translateFold

+
+
Send
+
+
+

Use alphanumeric identifiers or double-quoted strings for atomic +propositions, and parentheses for grouping.
Identifiers cannot +start with the letter of a prefix operator (F, +G, or X): for instance GFa +means G(F(a)). Use "GFa" if you really want +to refer to GFa as a proposition.
Conversely, infix +letter operators are not assumed to be operators if they are part of +an identifier: aUb is an atomic proposition, unlike +a U b and (a)U(b).

+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Unary operators
(prefix)		Binary operators
(infix)		Constants
not:!and:& && + . /\(strong) until:Utrue:1 + true
eventually:F + <>or:| || + + \/weak until:Wfalse:0 + false
always:G + []implies:-> + =>(weak) release:R + V
next:X ()equivalent:<-> + <=>strong release:M
xor:^ xor
+
+
+
+

Formula SimplificationsFold

+
+
+
+
+
+
+
+
+ + +
+
+ Output the (simplified) formula as:
+
+
+
+
+
+ Translate the (simplified) formula as:
+
+
+
+ Translate the (simplified) formula as:
+
+
+
+
+
+ Translate the (simplified) formula as:
+
+
+ then
+
+
+
+
+
+
+ + +
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

Automaton SimplificationsFold

+
+
+
+
+
+
+

Emptiness-check AlgorithmFold

+
+ Search accepting run using algorithm: + with these + options: + +
+
+
+
+

ResultsFold

+
+
+
+
+ + diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in new file mode 100755 index 000000000..2dce02025 --- /dev/null +++ b/wrap/python/ajax/spot.in @@ -0,0 +1,403 @@ +#!@PYTHON@ +# -*- mode: python; coding: iso-8859-1 -*- +# Copyright (C) 2011 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 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +import os + +# Directory for temporary files (images and other auxiliary files). +imgdir = 'spotimg' + +# Location of the dot command +dot = '@DOT@' +dot_bgcolor = '-Gbgcolor=#FFFFFF00' + +svg_output = False # FIXME: SVG output seems to be working well with + # Firefox only. We have to figure out how + # to get the correct size and transparent + # background in Chrome. + +from CGIHTTPServer import CGIHTTPRequestHandler +class MyHandler(CGIHTTPRequestHandler): + def is_cgi(self): + if self.path.startswith('/cgi-bin/spot.py'): + self.cgi_info = '', self.path[9:] + return True + return False + +if not os.environ.has_key('SCRIPT_NAME'): + # If this is not run as a cgi script, let's start an HTTP server. + from BaseHTTPServer import HTTPServer + server_address=('',8000) + if not os.access(imgdir, os.F_OK): + os.mkdir(imgdir, 0755) + print "Directory spotimg/ created." + httpd = HTTPServer(server_address, MyHandler) + print "Point your browser to http://localhost:8000/ltl2tgba.html" + httpd.serve_forever() + +import sys +import cgi +import cgitb; cgitb.enable() +import signal +import uuid + +print "Content-Type: text/html" +print + +# Redirect stderr to stdout. +os.close(sys.stderr.fileno()) +os.dup2(sys.stdout.fileno(), sys.stderr.fileno()) + +# Assume Spot is installed +sys.path.insert(0, '@pythondir@') + +if (os.environ.has_key('SERVER_SOFTWARE') and + os.environ['SERVER_SOFTWARE'].startswith(MyHandler.server_version)): + # We might be running from the build tree (but it's not sure). + # Add the build and source directories first in the search path. + # If we are not in the right place, python will find the installed + # libraries later. + sys.path.insert(0, '@srcdir@/../.libs') + sys.path.insert(0, '@srcdir@/..') + sys.path.insert(0, '../.libs') + sys.path.insert(0, '..') + # Darwin needs some help in figuring out where non-installed libtool + # libraries are (on this platform libtool encodes the expected final + # path of dependent libraries in each library). + m = '../.libs:@top_builddir@/src/.libs:@top_builddir@/buddy/src/.libs' + os.environ['DYLD_LIBRARY_PATH'] = m + +try: + execfile('ltl2tgba.opt') +except IOError: + pass + +import spot +import buddy + +def alarm_handler(signum, frame): + print """

The script was aborted because +it has been running for too long. Please try a shorter formula, +or different options (not drawing automata usually helps). +If you want to benchmark big formulae it is +better to install Spot on your own computer.

""" + sys.stdout.flush() + os.kill(0, signal.SIGTERM) + +def reset_alarm(): + signal.alarm(30) + +def render_dot(basename): + print '
' + if svg_output: + ext = 'svg' + else: + ext = 'png' + os.spawnlp(os.P_WAIT, dot, dot, dot_bgcolor, '-T' + ext, + '-Gsize=8.2,8.2', '-o', basename + '.' + ext, basename + '.txt') + reset_alarm() + b = cgi.escape(basename) + if svg_output: + print ('' + + 'Your browser does not support SVG.') + else: + print ('
(dot source)') + print '
' + sys.stdout.flush() + +def render_automaton(basename, automata, dont_run_dot, deco = False): + outfile = spot.ofstream(basename + '.txt') + if not deco: + spot.dotty_reachable(outfile, automata) + else: + spot.dotty_reachable(outfile, automata, deco) + del outfile + if dont_run_dot: + print ('

' + dont_run_dot + ''' to be rendered on-line. However +you may download the source in dot format and render it yourself.') + else: + render_dot(basename) + + +def print_stats(automaton): + stats = spot.stats_reachable(automaton) + print "

", stats.states, + if stats.states <= 1: + print " state,", + else: + print " states,", + print stats.transitions, + if stats.transitions <= 1: + print " transition,", + else: + print " transitions,", + # compute the number of acceptance conditions + count = automaton.number_of_acceptance_conditions() + if count > 0: + print count, + if count <= 1: + print "acceptance condition:", + else: + print "acceptance conditions:", + sys.stdout.flush() + acc = automaton.all_acceptance_conditions() + spot.bdd_print_accset(spot.get_cout(), automaton.get_dict(), acc) + else: + print "no acceptance condition (all cycles are accepting)" + print "

" + sys.stdout.flush() + # Decide whether we will render the automaton or not. + # (A webserver is not a calcul center...) + if stats.states > 64: + return "Automaton has too much states" + if float(stats.transitions)/stats.states > 10: + return "Automaton has too much transitions per states" + return False + +form = cgi.FieldStorage() +uid = str(uuid.uuid1()) +imgprefix = imgdir + '/' + uid + + +output_type = form.getfirst('o', 'v'); + +# Version requested. +if output_type == 'v': + print 'Spot version ' + spot.version() + exit(0) + +spot.unblock_signal(signal.SIGALRM) +spot.unblock_signal(signal.SIGTERM) +os.setpgrp() +signal.signal(signal.SIGALRM, alarm_handler) +reset_alarm() + +formula = form.getfirst('f', '') + +env = spot.default_environment.instance() +pel = spot.empty_parse_error_list() +f = spot.parse(formula, pel, env) + +if pel: + print '
' + err = spot.format_parse_errors(spot.get_cout(), formula, pel) + print '
' + +# Formula simplifications +opt = spot.Reduce_None +for r in form.getlist('r'): + if r == 'br': + opt = opt + spot.Reduce_Basics + elif r == 'si': + opt = opt + spot.Reduce_Syntactic_Implications + elif r == 'eu': + opt = opt + spot.Reduce_Eventuality_And_Universality + elif r == 'lc': + opt = opt + spot.Reduce_Containment_Checks_Stronger +if opt != spot.Reduce_None: + f2 = spot.reduce(f, opt) + f.destroy() + f = f2 + +# Formula manipulation only. +if output_type == 'f': + formula_format = form.getfirst('ff', 'o') + # o = Spot, i = Spin, g = GraphViz + + if formula_format == 'o': + print '
%s
' % f + elif formula_format == 'i': + print ('
' + + spot.to_spin_string(f) + '
') + elif formula_format == 'g': + outfile = spot.ofstream(imgprefix + '-f.txt') + spot.dotty(outfile, f) + del outfile + render_dot(imgprefix + '-f') + exit(0) + +# Formula translation. +translator = form.getfirst('t', 'fm') + +dict = spot.bdd_dict() + +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 == 'la': + automaton = spot.ltl_to_tgba_lacim(f, dict) + if form.getfirst('la', '') == 'sp': + automaton.delete_unaccepting_scc() +elif translator == 'ta': + refined_rules = False + if form.getfirst('ta', '') == 'lc': + refined_rules = True + automaton = spot.ltl_to_taa(f, dict, refined_rules) + +# Monitor output +if output_type == 'm': + automaton = spot.scc_filter(automaton) + automaton = spot.minimize_monitor(automaton) + print '
' + dont_run_dot = print_stats(automaton) + print '
' + render_automaton(imgprefix + '-a', automaton, dont_run_dot) + automaton = 0 + exit(0) + +# Automaton simplifications +prune_scc = False +wdba_minimize = False +for s in form.getlist('as'): + if s == 'ps': + prune_scc = True + elif s == 'wd': + wdba_minimize = True + +if output_type == 'a': + buchi_type = form.getfirst('af', 't') +elif output_type == 'r': + buchi_type = form.getfirst('ra', 't') +else: + print "Unkown output type 'o=%s'." % output_type + automaton = 0 + exit(0) + +degen = False +neverclaim = False +if buchi_type == 's': + degen = True +elif buchi_type == 'i': + degen = True + neverclaim = True + +if prune_scc: + # Do not suppress all useless acceptance conditions if + # degeneralization is requested: keeping those that lead to + # accepting states usually helps. + automaton = spot.scc_filter(automaton, degen) + +if wdba_minimize: + minimized = spot.minimize_obligation_new(automaton, f) + if minimized: + automaton = minimized + minimized = 0 + degen = False # No need to degeneralize anymore + +if degen or neverclaim: + degen = spot.tgba_sba_proxy(automaton) +else: + degen = automaton + +# Buchi Automaton Output +if output_type == 'a': + if buchi_type == 'i': + s = spot.ostringstream() + spot.never_claim_reachable(s, degen, f) + print '
%s
' % cgi.escape(s.str()) + del s + else: # 't' or 's' + dont_run_dot = print_stats(degen) + render_automaton(imgprefix + '-a', degen, dont_run_dot) + degen = 0 + automaton = 0 + exit(0) + +# Buchi Run Output +if output_type == 'r': + + print_acc_run = False + draw_acc_run = False + s = form.getfirst('rf', 'p') + 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.emptiness_check_instantiator.construct(opt) + + if not eci: + print ('
Cannot parse "' + opt + '" near "' + + err + '".
') + else: + ec_a = 0 + n_acc = degen.number_of_acceptance_conditions() + n_max = eci.max_acceptance_conditions() + if (n_acc <= n_max): + ec_a = automaton + else: + print ('
Cannot run ' + opt + + ' on automata with more than ' + str(n_max) + + ' acceptance condition.
Please build ' + + 'a degeneralized Büchi automaton if you ' + + 'want to try this algorithm.
') + if ec_a: + ec = eci.instantiate(ec_a) + else: + ec = 0 + + if ec: + ec_res = ec.check() + if not ec_res: + print '
No accepting run found.
' + else: + ec_run = ec_res.accepting_run() + print '
An accepting run was found.
' + if ec_run: + if print_acc_run: + s = spot.ostringstream() + spot.print_tgba_run(s, ec_a, ec_run) + print '
%s
' % cgi.escape(s.str()) + del s + + if draw_acc_run: + deco = spot.tgba_run_dotty_decorator(ec_run) + dont_run_dot = print_stats(ec_a) + render_automaton(imgprefix + '-e', ec_a, dont_run_dot, deco) + del deco + del ec_run + del ec_res + print '
' + del ec + del ec_a + degen = 0 + automaton = 0 + exit(0)