* wrap/python/ajax/css/ltl2tgba.css: Fix position of the "Send"
button with WebKit. The folding arrow icon had a vertical border
that overlapped with the next line.
the cached result for the requests. So that it survives
the browser's cache.
(finish): Prune the cache only once per hour, and only eraes
files that are older than 2 hours.
* wrap/python/ajax/spot.in (finish): Prune the cache once in a
while. We rely on hardlinks for garbage collecting the pictures
and dot sources that may be shared by different requests.
* wrap/python/ajax/spot.in (render_dot, render_dot_maybe)
(render_automaton, render_formula): Cache the dot source, so that
we do not have to regenerate two pictures from the same contents.
* wrap/python/spot.i: Typo in the ostringstream declaration.
* wrap/python/ajax/spot.in: Use the QUERY_STRING as a hash key to
cache the result of the script. Open stdout without buffering and
redirect it to a file that we can dump later on cache hits. Parts
of this change are extracted from code from Pierre Parutto
<parutto@lrde.epita.fr>.
* AUTHORS: Add him.
* wrap/python/ajax/ltl2tgba.html: Adjust to use
jQuery 1.6.1 and jQuery-UI 1.8.13. Remove a useless check
of $("#autoupdate").attr("checked") since this checkbox no longer
exists.
* wrap/python/ajax/css/ui-lightness/jquery-ui-1.8.8.custom.css:
Replace by ...
* wrap/python/ajax/css/ui-lightness/jquery-ui-1.8.13.custom.css: This.
* wrap/python/ajax/Makefile.am (EXTRA_DIST): Adjust.
* wrap/python/tests/setxor.py, wrap/python/tests/bddnqueen.py:
Clean all used bdd variables before calling bdd_done(), so that
bdd_delref() is never called after bdd_done(). In NDEBUG builds,
bdd_delref() does not check whether the BuDDy is running or not,
and calling it after bdd_done() will crash.
* wrap/python/spot.i, wrap/python/buddy.i: Include <cstddef>
because Swig 2.0.2 uses ptrdiff_t and does not do the include
itself. In g++ most libstdc++ standard headers have been changed
to no longer include <cstddef> as an implementation detail, so
the difference shows.
* src/tgbaalgos/dotty.hh (dotty_reachable): Take a new
assume_sba argument.
* src/tgbaalgos/dotty.cc (dotty_bfs): Take a new
mark_accepting_states arguments.
(dotty_bfs::process_state): Check if a state is accepting using
the state_is_accepting() method for tgba_sba_proxies, or by
looking at the first outgoing transition of the state. Pass
the result to the dectorator.
(dotty_reachable): Adjust function.
* src/tgbaalgos/dottydec.hh, src/tgbaalgos/dottydec.cc,
src/tgbaalgos/rundotdec.hh, src/tgbaalgos/rundotdec.cc
(state_decl): Add an "accepting" argument, and use it to
decorate accepting states with a double border.
* src/tgbatest/ltl2tgba.cc: Keep track of whether the output
is an SBA or not, so that we can tell it to dotty().
* wrap/python/ajax/spot.in: Likewise.
* wrap/python/cgi-bin/ltl2tgba.in: Likewise.
* wrap/python/tests/run.in, iface/nips/nipstest/defs.in,
iface/gspn/defs.in: Do not disable VERBOSE when running from "make
check". Since we have started using parallel-check on 2009-08-31,
we should always send verbose output to the log.
* wrap/python/ajax/spot.in: Do full scc_filter for TGBA (-R3f),
and keep some extra acceptance conditions (-R3) when
degeneralizing. The converse was done.
* wrap/python/ajax/ltl2tgba.html: Remove the auto-update button, and
enable auto-update automatically after the first submission. Add
tools tips for the "Desired Output" tabs, and the Spot logo.
Add a email icon to encourage feedback.
* wrap/python/ajax/ltl2tgba.css: fix sizes of formula field and
send button. Set position of mail icon.
* wrap/python/ajax/logos/mail.png: New logo, based on a public
domain SVG icon retrieved today from
http://commons.wikimedia.org/wiki/File:Internet-mail.svg
* wrap/python/spot.i: Provide a __nonzero__() method for
parse_error_list.
* wrap/python/cgi-bin/ltl2tgba.in: Do not call format_parse_errors()
unconditionally.
* wrap/python/cgi-bin/ltl2tgba.py (reduce_wdba): Use
minimize_obligation_new a pass the formula.
* wrap/python/spot.i (minimize_obligation_new): New function, to
cope with the strange specification of spot::minimize_obligation()
not always creating a new automaton.
* src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc
(minimize): Split into ...
(minimize_wdba, minimize_monitor): ... these two functions.
* src/tgbatest/ltl2tgba.cc (main): Adjust the call to
minimize_monitor.
* wrap/python/cgi-bin/ltl2tgba.in: Adjust the calls to
minimize_monitor and minimize_obligation.
* wrap/python/spot.i: Declare minimize_monitor, minimize_wdba,
minimize_obligations.
* src/tgba/tgbaexplicit.hh (tgba_explicit_string)
(tgba_explicit_formula, tgba_explicit_number): Add fake
declarations so that SWIG can see they inherits from tgba.
monitor available in the CGI script.
* wrap/python/spot.i: Declare the minimize() interface.
* wrap/python/cgi-bin/ltl2tgba.in: Add reduce_dmonitor and
reduce_wdba options.
ltihooks.py apparently breaks the import mechanisms of Python 2.6,
causes SWIG's runtime to fail to share a global type table, and
yields various failures in our tests.
* wrap/python/ltihooks.py: Delete.
* wrap/python/Makefile.am (EXTRA_DIST): remove ltihooks.py.
* wrap/python/tests/bddnqueen.py, wrap/python/tests/interdep.py,
wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py,
wrap/python/tests/ltlsimple.py, wrap/python/tests/minato.py,
wrap/python/tests/modgray.py, wrap/python/tests/optionmap.py,
wrap/python/tests/setxor.py: Do not use ltihooks.
* wrap/python/tests/run.in (pypath): Include the .libs/ directory
in the search path so that Python can find the *.so libraries.
appropriate.
* wrap/python/spot.i (spot::scc_filter): Make it available.
* wrap/python/cgi-bin/ltl2tgba.in (reduce_scc): Call scc_filter.
Use the "full" option unless the show_degen_png or
show_never_claim are set. Also reduce_scc the default.
* wrap/python/cgi-bin/ltl2tgba.in (dot): Use the value computed by
configure.
(os.system): Cleanup stale files only when the form has been
submitted.
(list options): Keep track of the selected value.
(draw_acc_run|print_acc_run): set ec=0 to detect if it has been
later set or not. Fix error message when using generalized
automata with degeneralized emptiness checks.
* wrap/python/cgi-bin/Makefile.am (ltl2tgba.py): Substitute @DOT@.
* wrap/python/cgi-bin/ltl2tgba.in (new): Mark new options as new.
(svg_output, reduce_langcout): Add these new options.
(render_dot): Support svg_output.
* wrap/python/cgi-bin/ltl2tgba.in: Add options to symbolically
prune unaccepting SCCs in LaCIM, and explicitely pruns unaccepting
SCCs in all algorithms.
* src/tgbaalgos/reductgba_sim.hh: Conceal most of the file to
SWIG.
* wrap/python/spot.i: Include reductgba_sim.hh.
server.
* wrap/python/cgi-bin/ltl2tgba.in: Starts a web server if the
script is not called as a CGI. Arrange to load libraries from
the build directory. Create the spotimg/ if needed when run as
a web server.
* wrap/python/cgi-bin/Makefile.am: Adjust build rule and clean
the spotimg directory.
* wrap/python/cgi-bin/README, NEWS: Update.
implementation of rational operators in a future version.
* src/ltlparse/ltlscan.ll: Do not recognize "*".
* wrap/python/cgi-bin/ltl2tgba.in: Undocument it.
* NEWS: Mention this.
* src/tgbatest/kv.test, src/tgbatest/ltl2tgba.test,
src/tgbatest/reductgba.test: Replace "*" by "&".
