* 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.
* src/evtgbaparse/Makefile.am, src/ltlparse/Makefile.am,
src/neverparse/Makefile.am, src/tgbaparse/Makefile.am
(AM_CPPFLAGS): Define -DYY_NO_INPUT so that the unused yyinput()
function does not get compiled.
* src/eltlparse/Makefile.am (AM_CPPFLAGS): Likewise.
(AM_CXXFLAGS): Also enable warnings.
* src/eltlparse/eltlparse.yy: Move helper functions from
the "%code requires" block to the "%code" block, so that they
do not appear in the eltlparse.hh file (which is included in
two places...).
* iface/nips/nips.cc (search_error_callback_assert): Comment
this unused function.
* src/misc/hash.hh (identity_hash): New function.
* src/tgba/tgbaexplicit.hh (tgba_explicit_number): Use
identity_hash<int> instead of std::tr1::hash<int> that does not
exist with g++-3.3.
* 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.
translation contain useless SCCs that where not ignored for
minimization.
* src/tgbaalgos/minimize.cc (minimize_wdba): Strip useless
SCCs before minimization.
* src/tgbatest/ltl2tgba.test: Add a check.
understood by Spot.
* src/neverparse/neverclaimparse.yy: Support "if :: false fi;"
instructions. Spin sometimes output these on dead states.
Also rewrite the "transitions" rule as a left recursion.
* src/tgbatest/neverclaimread.test: Adjust output because
of the right->left recursion change, and add two more formula
to submit to Spin to test its output.
* src/tgbaalgos/minimize.cc (minimize_dfa): Take final and
non_final sets.
(minimize_wdba): Fill in non_final at the same time as final.
(minimize_monitor): Call state_set() to fill non_final.
(init_sets): Simplify and rename as ...
(state_set): ... this.
* 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.
* src/tgbaalgos/minimize.cc (minimize): Move the minimization
code into...
(minimize_dfa): ... this new function, and fix the condition
under which a partition is considered to be minimal. Also
use a map instead of a list to lookup known formulae.
* src/tgbaalgos/powerset.hh (power_map): New structure, allowing
the caller to retrieve the set of original states corresponding to
the set in the deterministic automaton.
(power_set): Adjust prototype to take a power_map instead of the
acc_list.
* src/tgbaalgos/powerset.cc (power_set): Strip all code using
acc_list, and update power_set.
* src/tgbaalgos/minimize.cc (minimize): Rewrite, using an
algorithm similar to the one in the Dax paper to check whether
state of the minimized automaton should be accepting.
correct from ltl2tgba to the library.
* src/tgbaalgos/minimize.hh,
src/tgbaalgos/minimize.cc (minimize_obligation): New function.
* src/tgbatests/ltl2tgba.cc (main): Fix constness of automata,
and call minimize_obligation() for -R3b.
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.
* src/tgbatest/wdba.test: Speed up execution by running only a
couple of formula with valgrind. Half of those with`-l -R3b' and
the other half with `-f -R3'.
* src/tgbatest/ltl2tgba.cc (-M): New option for building
deterministic monitors.
* src/tgbaalgos/minimize.cc (minimize): Take a monitor
argument and adjust the code.
* src/tgbaalgos/minimize.hh (minimize): Document it.
* src/tgbaalgos/minimize.cc (init_sets, minimize): Fix memory
leaks and a usage of the wrong automaton.
* src/tgbatest/wdba.test: Try using -Rm with -R3 or -R3b, and with
valgrind. This caught all the bugs fixed above.
* src/tgbaalgos/minimize.cc (minimize): Don't add acceptance
conditions if the final set is empty.
* src/tgbaalgos/powerset.cc (tgba_powerset): Add the initial state
to acc_list if it is accepting. Also do not compute an SCC build
map if we don't have to build acc_list.
* src/tgbatest/ltl2tgba.cc (main): Use WDBA-minimization only when
it is correct. Either we can quickly determine that a formula or
its negation is a safety formula, or we can slowly check the
equivalence of the WDBA-minimized automaton and the original
automaton.
* src/tgbatest/wdba.test: New test.
* src/tgbatest/safety.test: Adjust comment.
* src/tgbatest/spotlbtt.test: Use -Rm.
* src/tgbatest/Makefile.am (TESTS): Add wdba.test.
* src/tgbatest/ltl2tgba.cc (main): Delete the minimized automaton.
* src/tgbaalgos/minimize.cc (minimize): Remove the call to
unregister_variable() at the end. It was both
wrong (unregistering only the first variable) and useless ("delete
del_a" will unregister all these variables). Use a map and a set
to keep track of free BDD variable and reuse them, otherwise the
algorithm would sometimes use more variables than allocated.
* src/tgbatest/minimize.cc: New file. Minimize an automaton
from a LTL formula and compare the size of the initial automaton
to the size of the minimized automaton.
New files. Algorithm to minimize an automaton using first the powerset
construction to determinize the input automaton, the automaton is then
minimized using the standard algorithm, using BDDs to check if states
are equivalent.
from the initial automaton.
* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
Added class tgba_explicit_number, a tgba_explicit where states are
labelled by integers.
* src/tgbaalgos/powerset.hh, src/tgbaalgos/powerset.cc:
When building the deterministic automaton, keep track of which states
were created from an accepting state in the initial automaton.
The states are added to the new optional parameter (if not 0),
acc_list.
Use tgba_explicit_number instead of tgba_explicit_string to build
the result.
* src/tgbaalgos/scc.cc (spot): Small fix.
Print everything on std::cout.
This fixes a bug in the powerset of such TGBA on the minimize branch.
* src/tgba/tgbabddconcrete.cc (compute_support_conditions): Also
account for the conditions from the acceptance relations.
* rc/tgba/tgbabddconcretefactory.hh, rc/tgba/tgbabddconcretefactory.cc
(acceptance_conditions_support): New variable to hold the value
of bdd_support(acceptance_conditions_support).
* src/tgba/tgbabddconcretefactory.cc (finish): Update
data_.acceptance_conditions_support.
