* spot/twaalgos/isdet.hh, spot/twaalgos/isdet.cc (check_determinism):
New function.
* NEWS: Mention it.
* tests/python/semidet.py: New file.
* tests/Makefile.am: Add it.
* spot/tl/hierarchy.hh, spot/tl/hierarchy.cc (nesting_depth): New
function.
* python/spot/__init__.py: Also make it a method of formula in Python
* bin/common_output.cc, bin/common_output.hh: Implement
--stats=%[OP]n.
* NEWS: Mention it.
* tests/core/format.test, tests/python/formulas.ipynb: Test it.
Our use of
ltl2tgba=ltl2tgba
autfilt=autfilt
...
all over the test cases comes from the time where those tools were not
in PATH and we actually had something like
ltl2tgba=../../bin/ltl2tgba
autfilt=../../bin/autfilt
But today that is useless, and we prefer to write ltl2tgba rather than
$ltl2tgba, so let's remove this old cruft.
* tests/core/basimul.test, tests/core/det.test, tests/core/lbt.test,
tests/core/lenient.test, tests/core/ltl2dstar.test,
tests/core/ltl2dstar2.test, tests/core/ltl2dstar3.test,
tests/core/ltl2dstar4.test, tests/core/ltlcross2.test,
tests/core/ltlcross3.test, tests/core/ltlcross4.test,
tests/core/ltlcrossce2.test, tests/core/ltldo.test,
tests/core/ltlfilt.test, tests/core/optba.test,
tests/core/prodor.test, tests/core/rand.test,
tests/core/randomize.test, tests/core/remfin.test,
tests/core/satmin.test, tests/core/sbacc.test,
tests/core/strength.test, tests/core/stutter-ltl.test,
tests/core/stutter-tgba.test, tests/core/unabbrevwm.test,
tests/core/unambig.test: Get rid of all tool=tool assignments.
To ease debugging and testing, ltlsynt can output the synthesized
strategy as an automaton, not just an aiger circuit.
Also, its exit code has been changed to something meaningful.
* bin/ltlsynt.cc: Various improvements: options, exit code, code style
* spot/twaalgos/aiger.hh, spot/twaalgos/aiger.cc,
spot/twaalgos/Makefile.am: Move the aiger printer to separate files
* tests/core/ltlsynt.test: Clean up and update test file
* tests/Makefile.am: Add the test file to the test suite
* NEWS: document the new aiger printer
* doc/org/concepts.org: document the named property "synthesis-outputs",
used by print_aiger
This is not optimal yet because it still construct a minimal WDBA
internally, but it's better than the previous way to call
minimize_obligation() since it can avoid constructing the minimized
automaton in a few more cases.
* spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: Introduce
is_obligation().
* bin/ltlfilt.cc: Wire it to --obligation.
* spot/twaalgos/minimize.cc: Implement is_wdba_realizable(),
needed by the above.
* tests/core/obligation.test: Test it.
* bin/man/spot-x.x, NEWS: Document it.
Fixes#297. Implement the following rules.
Fin(i) & Fin(j) by f if i and j are complementary
Fin(i) & Inf(i) by f
Inf(i) | Inf(j) by t if i and j are complementary
Fin(i) | Inf(i) by t.
* spot/twaalgos/cleanacc.cc, spot/twaalgos/cleanacc.hh: Here.
* tests/python/merge.py: Add more test cases.
* NEWS: Mention the change.
This improves the coverage for bdd_dict::assert_emptiness() and
bdd_dict::dump().
* tests/core/bdddict.cc, tests/core/bdddict.test: New files.
* tests/Makefile.am, tests/core/.gitignore: Adjust.
Fixes#289.
* spot/twaalgos/stats.cc, spot/twaalgos/stats.hh,
bin/common_aoutput.cc, bin/common_aoutput.hh: plug %g and %G into
acc_cond::name() when arguments are given as %[arg]g. or %[arg]G.
* tests/core/acc2.test: Add test case.
* doc/org/randaut.org, NEWS: Document it.
* spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::name): New method.
* spot/twaalgos/dot.cc: Use it.
* tests/python/acc_cond.ipynb: Add a small test.
* NEWS: Mention it.
* spot/twaalgos/stutter.cc,
spot/twaalgos/stutter.hh (stutter_invariant_letters)
(stutter_invariant_states): Get rid of the broken local variant.
* tests/python/stutter-inv.ipynb, NEWS: Document.
* python/spot/impl.i: Bind vector<bdd>.
Suggested by Tobias Meggendorfer. Fixes#295.
* bin/ltlcross.cc, bin/common_trans.hh, bin/common_trans.cc: Implement
this --reference option.
* NEWS, doc/org/ltlcross.org: Document it.
* tests/core/ltlcross3.test: Test it.
Fixes#293.
* spot/tl/simplify.cc: Test implications that would yield tt or ff
first. In rules of the form "if a => b, a op b = b" also check
if b => a, and in this case return smallest(a,b).
* tests/core/reduccmp.test: Add a test.
* NEWS: Mention it.
This is long overdue, and we probably want to use tls-impl=1 in
ltlsynt.
* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh:
Add support for tls-impl=N.
* tests/core/ltl2tgba.test: Test it.
* bin/spot-x.cc, NEWS: Document it.
* spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh: Implement
stutter-invariance detection at the state level.
* python/spot/impl.i: Instantiate std::vector<bool>
* tests/python/stutter-inv-states.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
These were the most expansive tests, each taking more than 5min.
This should bring them back below 1min.
* tests/core/parity.test: Do not run through valgrind.
* tests/python/toweak.py: Remove one very long case.
Suggested by Maximilien Colange.
* spot/twaalgos/degen.cc: If the output has more SCC than the input,
detect useless SCCs and remove them.
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/degen.hh: Add support for a degen-remscc option.
* bin/spot-x.cc, NEWS: Document it.
* tests/core/degenscc.test: New file.
* tests/Makefile.am: Add it.
* tests/core/det.test: Lower some expected size (yay!).
Fixes#286.
* spot/twaalgos/simulation.cc: Only set the deterministic
property, not the non-deterministic one.
* tests/core/ltl2tgba.test: Add test case.
* NEWS: Mention the issue.
This also fixes some empty lines and unsorted options
that appeared in some tools.
* tests/sanity/bin.test: Ensure this is done.
* bin/README: Add a new paragraph about this.
* bin/autcross.cc, bin/ltlcross.cc: Move the
output options in their own section.
* bin/common_color.cc: Assume color options are
in group -15.
* bin/common_finput.cc, bin/common_finput.hh:
Add a headless variant.
* bin/genltl.cc, bin/ltlfilt.cc, bin/ltlgrind.cc,
bin/randaut.cc, bin/randltl.cc: Do not force the
children groups, so that the options are correctly sorted.
* bin/ltlsynt.cc: Add missing groups.
Fixes#284, reported by Juraj Major.
* spot/twaalgos/totgba.cc: Fix the algorithm.
* spot/twa/acc.hh: More doc for future generations.
* tests/core/scc.test: More test cases.
* NEWS: Mention the issues.
parity_product_or constructs the sum of two parity automata and it keeps
the parity.
* spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here.
* tests/core/parity.cc: Add tests here.
Compute the synchronized product of two parity automata, this product
keeps the parity acceptance.
* spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here
* tests/core/parity.cc: Add tests for spot::parity_product()
Merge the acceptance sets of a parity acceptance with the same priority
level to simplify this acceptance.
* spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here
* tests/core/parity.cc: Add tests for spot::cleanup_parity_acceptance()
