* wrap/python/ajax/spot.in: Adjust to the new interface.
* wrap/python/spot.i: Work around missing support for nested classes.
* wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test: More
test.
Suggested by Joachim Klein.
* wrap/python/ajax/ltl2tgba.html: New option.
* wrap/python/ajax/protocol.txt, NEWS: Document it.
* wrap/python/ajax/spot.in: Implement it.
* wrap/python/spot.i: Export src/ltlvisit/lbt.hh.
This translator algorithm is seldom used in practice because we work
with explicit automata everywhere, and this is only useful to build
symbolic automata. Furthermore, the symbolic automata produced by this
algorithm are larger (when looked at explicitly) than those produced by
ltl2tgba_fm or other explicit translators.
The nice side effect of this removal is that we can also remove a lot of
supporting classes, that were relying a lot on BDDs.
* src/tgba/public.hh, src/tgba/statebdd.cc, src/tgba/statebdd.hh,
src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh,
src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbabddconcretefactory.hh,
src/tgba/tgbabddconcreteproduct.cc, src/tgba/tgbabddconcreteproduct.hh,
src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh,
src/tgba/tgbabddfactory.hh, src/tgbaalgos/ltl2tgba_lacim.cc,
src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbatest/bddprod.test,
src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test: Delete all these
files.
* bench/ltlcounter/Makefile.am, bench/ltlcounter/README,
bench/ltlcounter/plot.gnu, bench/ltlcounter/run, src/tgba/Makefile.am,
src/tgbaalgos/Makefile.am, src/tgbatest/Makefile.am,
src/tgbatest/cycles.test, src/tgbatest/dupexp.test,
src/tgbatest/emptchk.test, src/tgbatest/ltl2tgba.cc,
src/tgbatest/ltl2tgba.test, src/tgbatest/ltlcross.test,
src/tgbatest/ltlprod.cc, src/tgbatest/spotlbtt.test,
src/tgbatest/wdba.test, src/tgbatest/wdba2.test,
src/tgba/tgbaexplicit.hh, wrap/python/ajax/ltl2tgba.html,
wrap/python/ajax/spot.in, wrap/python/spot.i,
wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py,
wrap/python/tests/ltl2tgba.test: Adjust.
* wrap/python/ajax/ltl2tgba.html: Augment and update tooltips to match
vocabulary in the Spin'13 paper. Hide the compose obligation option
since it's a work in progress.
* src/tgbaalgos/postproc.hh (run): Rename the first argument as
input_disown to help Swig.
* wrap/python/spot.i: Wrap spot::postprocessor.
* wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/protocol.txt:
Add an option for nondeterministic monitor.
* wrap/python/ajax/spot.in: Honor the new option, and rewrite the
monitor production using postprocessor.
* src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh: Use a ta_explicit
attribute instead of inheriting from it.
(get_ta): New method.
* src/taalgos/minimize.cc, src/taalgos/minimize.hh,
src/taalgos/tgba2ta.cc, src/tgbatest/ltl2tgba.cc: Adjust usage.
* wrap/python/spot.i (as_ta): Remove, now that we have get_ta.
* wrap/python/ajax/spot.in: Use get_ta instead of as_ta.
* src/taalgos/dotty.cc: Clean up output of TAs.
* src/tgbatest/ltl2tgba.cc: Fix memory management, and use the TA
printer for TGTA.
* wrap/python/spot.i (as_ta): New function to convert a tgta_explicit
into a TA.
* wrap/python/ajax/spot.in: Use this new function to display automata.
* wrap/python/spot.i: Add wrapper the new TA algorithms.
* wrap/python/ajax/ltl2tgba.html: Add a testing automaton tab.
* wrap/python/ajax/protocol.txt, wrap/python/ajax/spot.in: Support it.
* wrap/python/ajax/css/loading.gif: New file.
* wrap/python/ajax/css/ltl2tgba.css (.loading): New class.
* wrap/python/ajax/ltl2tgba.html: Display loading.gif after 200ms if
the answer hasn't arrived
* wrap/python/ajax/spot.in: Do not suggest not to draw the automaton
on timeout.
* wrap/python/ajax/js/jquery.ba-dotimeout.min.js: New file.
* wrap/python/ajax/Makefile.am: Distribute it.
* wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/protocol.txt:
Add options 'o' and 'p'.
* wrap/python/ajax/spot.in: Handle these, and use '-v' to check
version.
* wrap/python/ajax/ltl2tgba.html: Display the ltl3ba version, and
disable its tab when unavailable.
* wrap/python/ajax/protocol.txt: Add option for ltl3ba's version.
* wrap/python/ajax/spot.in: Implement this option, and catch
errors when ltl3ba is not installed.
* wrap/python/ajax/ltl2tgba.html: Add a dedicated tab with
two columns of options.
* wrap/python/ajax/css/ltl2tgba.css: Support for two columns.
* wrap/python/ajax/protocol.txt: Document new options.
* wrap/python/ajax/spot.in: Handle the new options.
* wrap/python/ajax/Makefile.am: Substitude LTL3BA in spot.in.
The previous implementation was fine to catch timeout of third-party
tools (like dot), but to good to catch timeout in Spot itself, because
Python will not deliver a SIGALRM while a native function (e.g. Spot's
translation) is running. So we fork() the Python process, with a
parent that does nothing but wait for the termination of the child or
for an alarm. On SIGALRM, the parent kills all children.
* wrap/python/ajax/spot.in: Adjust to fork.
* wrap/python/tests/alarm.py: New test file to test this
scenario in a more controled environment.
* wrap/python/tests/Makefile.am: Add it.
Syntactic implication checks may use as_bdd() to compare Boolean
formulae. By doing so, they register Boolean variables in an order
that is usially detrimental to the LTL translator. The new,
clear_as_bdd_cache() function offers a mean to unregister these
variables, so that the LTL translator will register them again in the
a more natural way.
* src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc
(clear_as_bdd_cache): New function.
* src/tgbatest/ltl2tgba.cc, wrap/python/ajax/spot.in: Call it.
* src/ltlvisit/wmunabbrev.hh, src/ltlvisit/wmunabbrev.cc: New files.
* src/ltlvisit/Makefile.am: Add them.
* src/ltlvisit/tostring.cc (to_spin_string): Use the new rewriting.
* wrap/python/ajax/spot.in: Warn when a "Spin" still contain PSL
operators.
* wrap/python/ajax/ltl2tgba.html: Adjust help text.
* doc/tl/tl.tex, NEWS: Document the new rewriting.
