Fixes#15.
* spot/twaalgos/minimize.hh, spot/twaalgos/minimize.cc
(minimize_obligation_garanteed_to_work): New function.
* spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Use it if
wdba-minimize=1. Handle new default for wdba-minimize.
* NEWS, bin/spot-x.cc: Document those changes.
* tests/core/ltl2tgba2.test: Add some test cases.
* tests/core/genltl.test: Improve expected results.
Juraj Major reported a case with 32 APs where ltlcross would take
forever to gather statistics. It turns out that for each edge,
twa_sub_statistics was enumerating all compatible assignments of 32
APs. This uses bdd_satcountset() instead, and also store the result
in a long long to avoid overflows.
* spot/twaalgos/stats.cc (twa_sub_statistics): Improve the code for
counting transitions.
* bin/common_aoutput.hh, bin/ltlcross.cc, spot/twaalgos/stats.hh:
Store transition counts are long long.
* tests/core/readsave.test: Add test case.
* NEWS: Mention the bug.
* src/bddop.c (bdd_satcount, bdd_satcountln): If the number of
declared variables changed since we last used it, reset misccache.
Otherwise, bdd_satcount() and friends might return incorrect results
after the number of variable is changed. These is needed for the next
patch in Spot to pass all tests.
(misccache_varnum): New global variable to track that.
(bdd_satcountset): Make sure that bdd_satcountset(bddtrue, bddtrue)
return 1.0 and not 0.0.
* spot/tl/simplify.hh, spot/tl/simplify.cc,
spot/twaalgos/translate.cc: Update the tl_simplification
options after all preferences have been given.
* bin/ltlsynt.cc: Display the size of the translation output.
* tests/core/ltlsynt.test: Add test case.
* spot/tl/formula.hh: Add variant of formula::is that support 4
arguments.
* spot/tl/simplify.hh, spot/tl/simplify.cc: Add option keep_top_xor
to preserve Xor and Equiv at the top-level.
* spot/twaalgos/translate.cc: Adjust ltl-split to deal with Xor and
Equiv for the -D -G case.
* NEWS: Mention that.
* tests/core/ltl2tgba2.test: Add test case.
* tests/python/simstate.py: Adjust expected result.
Reported by Florian Renkin.
* spot/twaalgos/emptiness.cc (reduce): If the automaton uses Fin
acceptance, check the reduced cycle and revert to the original cycle
if necessary.
* tests/python/intrun.py: New file.
* tests/Makefile.am: Add it.
* spot/twaalgos/emptiness.hh: Improve documentation.
* spot/twaalgos/genem.cc: In the spot29 implementation for the generic
case, when Fin(fo)=true and Fin(fo)=false have to be tested
separately, the second test can be done by a loop instead of a
recursion, to avoid unnecessary processing of the acceptance
condition. Suggested by Jan Strejček.
On some architectures this test fails due to several
reasons:
- missing headers
- use of valueAt instead of count in ConCS. Indeed,
valueAt acts similarly to count but avoids some validity
check that are required when the hashmap is growing.
This patch also:
- removes inaccurate comments from bricks.test.
- test more features for hashset.
* spot/bricks/brick-hashset,
tests/core/bricks.cc,
tests/core/bricks.test: Here.
