* 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/tgba/wdbacomp.hh, src/tgba/wdbacomp.cc: New file.
* src/tgba/Makefile.am: Add them.
* src/tgbaalgos/minimize.cc (minimize_obligation): Use
wdba_complement().

* src/tgbatest/minimize.cc: Delete.

* 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/minimize.cc (minimize_obligation): Do not
minimize aut_neg_f, complement min_aut_f instead.
* src/tgbaalgos/minimize.hh: Adjust description.

to label transient states.

* 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.

* src/tgbaalgos/scc.hh, src/tgbaalgos/scc.cc (scc_map::trivial,
scc_map::one_state_of): Two new helper functions.

initial states.

* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
(tgba_product_init): New class.

failure because the minimization() algorithm is currently
incorrect when applied to non-weak automata.

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.

* bench/wdba/: New directory.
* bench/Makefile.am (SUBDIRS): Add wdba.
* NEWS: Mention it.
* configure.ac: Output bench/wdba/defs and bench/wdba/Makefile.

* 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'.

under the same heading "automaton conversion".

* 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/tgbatest/ltl2tgba.cc (main): Warn if -Rm is used without
knowing the formula whose automaton is minimized.

* 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/tgbaalgos/safety.hh, src/tgbaalgos/safety.cc: New
files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbatests/ltl2tgba.cc: Add option "-O".
* src/tgbaalgos/scc.hh: Update documentation.
* src/tgbatest/Makefile.am (TESTS): Add safety.test.
* src/tgbatest/safety.test: New file.

Felix Abecassis authored Mar 20, 2010 and Alexandre Duret-Lutz committed Jan 05, 2011

* src/tgbatest/minimize.cc: Delete useless includes.
* src/tgbaalgos/minimize.cc: Delete useless includes,
fixed acceptance conditions.
* src/tgbatest/ltl2tgba.cc: Add -Rm option for minimization.
* src/tgba/tgbaexplicit.cc: Fixed typo.

Felix Abecassis authored Mar 20, 2010 and Alexandre Duret-Lutz committed Jan 05, 2011

* 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.

Felix Abecassis authored Mar 20, 2010 and Alexandre Duret-Lutz committed Jan 05, 2011

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.

Felix Abecassis authored Mar 20, 2010 and Alexandre Duret-Lutz committed Jan 05, 2011

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.

* wrap/python/Makefile.am: Add -DSWIG_TYPE_TABLE=spot.

* configure.ac: Search for swig2.0 and swig.
* wrap/python/Makefile.am: Use $(SWIG).

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.

With this change the output of
ltl2tgba -f -x -k -DS "GF(p_1) & ... & GF(p_n)
uses less than (n+1)^2 transitions when it used
exactly (n+1)*(2^n) transitions before.

* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator): Merge
transitions going to the same states if they are both accepting or
if neither are.
(state_ptr_bool_t, state_ptr_bool_less_than): Helper type to
store a transition in tgba_tba_proxy_succ_iterator.
* src/tgba/tgbatba.cc, src/tgba/tgbatba.hh
(tgba_tba_proxy::transition_annotation): Remove.  We cannot
implement this method if transitions are merged.

* bench/ltlclasses/run: Augment the max size to 20.
* bench/ltlcounter/run: Typo in comment.