* bin/genaut.cc: Use RANGE instead of N, and document it.
Output the FORMAT documentation, and fix handling of %F and %L.
* tests/core/genaut.test: New file.
* tests/Makefile.am: Add it.
Adds the method spot::acc_cond::is_streett_like() that behaves like
spot::acc_cond::is_streett() except that it works on a wider range
of acceptance conditions, called Streett-like. Also adds
spot::acc_cond::streett_like_pairs() that returns a boolean assessing
whether the acceptance condition is Streett-like and also returns all
the Streett_like pairs.
Defines the new struct type spot::acc_cond::rs_pair.
Similarily, Adds the methods spot::acc_cond::is_rabin_like() and
spot::acc_cond::rabin_like_pairs().
* NEWS: Mention this modification
* python/spot/impl.i: Declares the new struct to SWIG, and defines
the streett_like_pairs() vector as an output parameter, which makes
the python code return a tuple (boolean, vector) rather than a
pass-by-reference vector.
* spot/twa/acc.cc, spot/twa/acc.hh: Declares an implements the new
methods and the new nested struct.
* tests/Makefile.am: Add new tests to the suite
* tests/python/rs_like.py: Tests the new methods and
the SWIG bindings.
* spot/twaalgos/degen.cc, spot/twaalgos/degen.hh,
spot/twaalgos/mask.hh: Store original states in "original-states"
properties.
* spot/twaalgos/dot.cc: Add support for option 'd'.
* bin/common_aoutput.cc: Document it.
* doc/org/concepts.org, NEWS: Document "original-states".
* tests/core/readsave.test: Add some tests.
spot::mark_t::sets() was modified so that it now returns an iterable
object rather than an std::vector<unsigned>.
* NEWS: Mention the modification.
* python/spot/impl.i: Declares mark_container as iterable to SWIG.
* spot/parseaut/parseaut.yy: Adapts to the modification.
* spot/twa/acc.hh: Implement the modification.
* tests/python/acc_cond.ipynb: Adapts to the modification.
Reported by Thibaud Michaud
* spot/twaalgos/sbacc.cc: Do not label rejecting SCCs with the empty
mark, as it might be accepting.
* tests/core/sbacc.test: Add test cases.
* NEWS: Mention the bug.
* NEWS: Mention this addition.
* bin/autfilt.cc: Add dualize option
* tests/Makefile.am: Add dualize option test file to the suite.
* tests/core/dualize.test: Test the dualize option.
* NEWS: Mention the implementation
* python/spot/impl.i: Add dualize() to python interface.
* spot/twaalgos/Makefile.am: Add dualize.cc,hh to the build
* spot/twaalgos/dualize.cc: Implement dualize() that takes an automaton
and returns its dual
* spot/twaalgos/dualize.hh: Implement dualize()
* tests/Makefile.am: Add dualize tests to the test suite
* tests/python/dualize.py: Test cases for dualize
when fin_alone sets where presents (i.e., not really Rabin condition),
the rabin_to_buchi_maybe() could fail to notice DBA-typeness.
* spot/twaalgos/remfin.cc: Don't set scc_ba_type to false when
fin_alone is present.
* tests/core/remfin.test: Add a test case.
* spot/twaalgos/sum.cc: Fix the sum of automatas having universal
initial transitions.
* tests/core/explsum.test: Add test case testing the handling of
universal initial transitions in sum.
The algorithm had two problems: it was removing only useless
destination from universal destination (instead of removing the entire
edge), and it was not properly iterating over the entire reachable
automaton.
* spot/twa/twagraph.cc: Fix it.
* spot/twa/twagraph.hh: Adjust documentation.
* tests/core/alternating.test: Add more tests.
* tests/python/twagraph.py: Adjust.
* NEWS: Mention the bug.
For #212.
* spot/twa/twa.hh: Rename prop_deterministic() as prop_universal(),
and keep the old name as deprecated.
* spot/twaalgos/isdet.cc, spot/twaalgos/isdet.hh: Rename
is_deterministic() as is_universal(), and add a new function
for is_deterministic().
* doc/org/concepts.org, doc/org/hoa.org, doc/org/tut21.org,
spot/tl/hierarchy.cc, spot/twa/twagraph.cc,
spot/twaalgos/are_isomorphic.cc, spot/twaalgos/determinize.cc,
spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc,
spot/twaalgos/hoa.cc, spot/twaalgos/minimize.cc,
spot/twaalgos/postproc.cc, spot/twaalgos/product.cc,
spot/twaalgos/randomgraph.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/simulation.cc, spot/twaalgos/totgba.cc,
spot/twaalgos/word.cc, tests/python/product.ipynb,
tests/python/remfin.py: Adjust.
* NEWS: Mention the change.
Fixes#245.
* bin/genltl.cc: Add the option.
* bin/man/genltl.x: Add reference.
* tests/core/ltl2tgba2.test: Use these patterns.
* doc/org/genltl.org, NEWS: Document the options.
* spot/parsetl/parsetl.yy: Adjust one diagnostic.
* spot/parsetl/scantl.ll: Fix recovering of missing closing brace
in lenient mode.
* tests/python/declenv.py: Move some tests...
* tests/python/ltlparse.py: ... here, and add many more.
* NEWS: Mention the lenient mode bug.
* spot/twaalgos/couvreurnew.cc, spot/twaalgos/gv04.cc,
spot/twaalgos/magic.cc, spot/twaalgos/se05.cc, spot/twaalgos/tau03.cc,
spot/twaalgos/tau03opt.cc: Throw if precondition on acceptance
condition is not satisfied.
* tests/python/misc-ec.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the change.
Fixes#231.
* NEWS: Mention of implementation of sum, sum_and.
* bin/autfilt.cc: Add --sum, --sum-or and --sum-and options.
* python/spot/impl.i: Add bindings for sum, sum_and.
* spot/twaalgos/Makefile.am: Add sum.cc, sum.hh.
* spot/twaalgos/sum.cc: Implement sum, sum_and.
* spot/twaalgos/sum.hh: Declaration of sum, sum_and.
* tests/Makefile.am: Add sum tests.
* tests/core/explsum.test: Test the sum of two automatons,
false or false, unsatisfied mark propagation, handling of univ.
transitions.
* tests/python/sum.py: Check that two automatons that does not
share their bdd dict are not accepted, then run tests over the
sum of randomly generated LTL formulas.
* spot/twaalgos/degen.cc: Make use_cust_acc_orders as unlikely, as it
was never true in the whole test suite before this patch.
* tests/core/ltlcross2.test: Play with degen-order and degen-lcache
options to test more cases.
Follow-up to an email from Ayrat Khalimov.
* python/spot/impl.i: Include twa/formula2bdd.hh.
* python/spot/__init__.py: Make the dictionnary
optional.
* spot/twa/formula2bdd.cc: Throw an exception instead of asserting.
* tests/python/bdditer.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Update.
The goal is to improve coverage stats, but I discovered two issues
while doing so.
* tests/python/twagraph.py: New test case.
* tests/Makefile.am: Add it.
* spot/twa/twagraph.hh: Add fix typos in error messages.
* python/spot/impl.i: Fix broken wrappers for state_from_number and
state_acc_sets.
Reported by Thomas Medioni.
* spot/twa/twagraph.hh (set_univ_init_state): Remove the bogus
template parameter.
* tests/core/twagraph.cc, tests/core/tgbagraph.test: Test the method.
* NEWS: Mention the bug.
Fixes#241.
* spot/twaalgos/postproc.cc: Use the deterministic monitor if it
has as many states as the non-deterministic one.
* spot/twaalgos/minimize.cc (minimize_monitor): Quickly check
for terminal automata.
* spot/twaalgos/stripacc.cc: Set the weak property.
* spot/twaalgos/stripacc.hh: Improve documentation.
* tests/core/monitor.test, tests/core/sbacc.test: Update.
* NEWS: Mention the issue.
Fixes#240.
* spot/twaalgos/postproc.cc: Do not call do_simul on the output of
minimize_monitor(), and do not skip complete() when PREF_==Any.
* tests/core/monitor.test: Add a test case.
* NEWS: Mention the bug.
* doc/org/ltl2tgba.org: Document complete monitors.
* spot/twaalgos/sbacc.cc: Do not assign to one_in twice, and
fix the value of init_acc.
* tests/core/sbacc.test: Add a test case.
* NEWS: Mention the bug.
Fixes#238.
* spot/twa/acc.hh (max_set): Add a version using __builtin_clz().
(min_set): New method.
* tests/core/acc.cc, tests/core/acc.test: Add some tests.
* bin/common_aoutput.cc, bin/common_aoutput.hh, bin/common_output.cc,
bin/common_output.hh: Add options to %x to list atomic propositions
with various quoting scheme. Deprecate --format=%a in favor of the
new --format=%x for consistency with --stats=%x.
* tests/core/format.test, tests/core/remprop.test: Adjust and add more
tests.
* NEWS: Mention these changes.
Put what is done by `autfilt` in a new function, `decompose_acc_scc`.
* bin/autfilt.cc: Move code from here...
* spot/twaalgos/strength.cc, spot/twaalgos/strength.hh: To here.
* tests/python/decompose_scc.py: Test python binding.
See #172.
* bin/autfilt.cc: Add option.
* tests/core/strength.test: Remove ambiguity with
'--decompose-strength'.
* NEWS: Mention it.
* tests/core/scc.test: Test it.
See #172.
While at it, fix typo in doxygen comment.
* spot/twaalgos/strength.cc, spot/twaalgos/strength.hh: New function.
* tests/python/decompose_scc.py, tests/Makefile.am: Test python
binding.
* spot/twaalgos/mask.hh: Fix typo.
Related to #172, where we discussed that scc_info bindings were
missing.
* spot/twaalgos/sccinfo.hh (spot::scc_info::scc_node): Move...
(spot::scc_info_node): ... here to help Swig.
* python/spot/impl.i: Add bindings for scc_info.
* tests/python/sccinfo.py: New file.
* tests/Makefile.am: Add it.
* bin/genltl.cc: Change the name and add the bibtex entry.
* bin/man/genltl.x: Replace LNCS by LNAI.
* tests/core/genltl.test: Also test the %F output.
Fixes#80.
* bin/genltl.cc: Add --kr-n2, --kr-nlogn and --kr-n.
* bin/man/genltl.x: Add the paper in the documentation.
* tests/core/genltl.test: Test them.
Fixes#207
* NEWS: Informations about the option 'y' for --dot added
* bin/common_aoutput.cc: Documentation for the option 'y'
for --dot added
* spot/twaalgos/dot.cc (print_dst, process_link): Functions
modified for the new option
* tests/core/alternating.test: Tests added
