* 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.
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.
SCC information).
* src/tgbatest/ltl2tgba.cc (syntax, main): Add a -ks option.
* src/tgbatest/ltl2tgba.test, bench/ltlclasses/run,
bench/ltlcounter/run: Use -ks instead of -k to speed things up.
tgba_tba_proxy used to spend a lot of time (re)computing the
acceptance condition common to all outgoing transition of a state.
* src/tgba/tgbatba.hh (accmap_): New cache.
(common_acceptance_conditions_of_original_state): New method.
* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::~sync)
Call common_acceptance_conditions_of_original_state() instead of
computing the result.
(~tgba_tba_proxy): Cleanup the cache.
(common_acceptance_conditions_of_original_state): Implement it.
families of LTL formulae.
* src/ltltest/genltl.cc: New file. Based on five classes of
formulae defined in a paper by Cichón, Czubak, and Jasiński.
* src/ltltest/Makefile.am (noinst_PROGRAMS): Build genltl.
* src/ltlvisit/tostrinc.hh (to_spin_string): Add a full_parent
optional parameter, like for the to_string() function.
* src/ltlvisit/tostrinc.cc (to_string_visitor): Fix the
handling of full_parent.
(to_spin_string_visitor): Handle full_parent.
reduce_visitor::visit(binop).
* src/ltlvisit/reduce.cc (eventual_universal_visitor::recurse_):
Move this method...
(recurse_eu): ... outside as a separate function. Likewise for
the universal/eventual result struct.
(reduce_visitor::visit(binop)): Call recurse_eu() once to replace
two calls to is_eventual and is_universal, thus replacing two
recursions by one.
* src/ltlvisit/syntimpl.cc (eventual_universal_visitor): Use
a union to store the eventual and universal properties as two
bit in a bit-field, and "AND" both of them at once.
(eventual_universal_visitor::recurse_un,
eventual_universal_visitor::recurse_ev): Replace these
two functions by ...
(eventual_universal_visitor::recurse_): ... this one, that
returns both bits as an unsigned.
* src/tgbatest/ltl2tgba.cc (main): Either replay the accepting
run or print it, but do not do both.
* src/tgbatest/emptchk.test: Adjust. I.e. use -C instead of -CR
when we expect the run to be displayed.
* src/tgbatest/randtgba.cc (main): Remove the set but unused opt_A
variable (the upcoming GCC 4.6 would warn about it) and set opt_ec
to 1 if -A is used without -e.
* src/tgbaalgos/reducerun.hh (tgba_run): Predeclare as a struct
since this is what it is.
* src/tgbatest/randtgba.cc (main): Avoid using "i" with two
different type in the same loop.
* src/kripke/fairkripke.hh, src/kripke/fairkripke.cc,
* src/kripke/kripke.hh, src/kripke/kripke.cc: Finalize and
document the Kripke interface. I have tested it by updating
checkpn to use it.
before some optional operations (like more optimizations, or a
product).
* src/tgbatest/ltl2tgba.cc (-N, -NN): Make sure we print the last
automaton computed, not just the automaton when we degeneralized
it. We may have applied other algorithms since the original
degeneralization.
options -C and -CR for that.
* src/tgbatest/ltl2tgba.cc: Add option -C and -CR to control
whether we want the accepting run to be printed or replayed.
* src/tgbatest/dfs.test, src/tgbatest/eltl2tgba.test,
src/tgbatest/emptchk.test, src/tgbatest/emptchke.test,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlcounter.test: Use -CR.
