False/True are problematic in Python, and I don't like that the
enum is op::False but the constructor formula::ff(). So let's
just use ff and tt everywhere, and also eword instead of EmptyWord.
* src/ltlast/formula.hh (False, True, EmptyWord, AP, is_false, is_true):
Rename to...
(ff, tt, eword, ap, is_ff, is_tt): ... these.
* iface/ltsmin/ltsmin.cc, src/ltlast/formula.cc,
src/ltlvisit/apcollect.cc, src/ltlvisit/dot.cc, src/ltlvisit/mark.cc,
src/ltlvisit/mutation.cc, src/ltlvisit/print.cc,
src/ltlvisit/relabel.cc, src/ltlvisit/simpfg.cc,
src/ltlvisit/simplify.cc, src/ltlvisit/snf.cc, src/ltlvisit/unabbrev.cc,
src/twa/acc.cc, src/twa/acc.hh, src/twa/formula2bdd.cc,
src/twaalgos/gtec/gtec.cc, src/twaalgos/hoa.cc, src/twaalgos/ltl2taa.cc,
src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/neverclaim.cc,
src/twaalgos/product.cc, src/twaalgos/remfin.cc, src/twaalgos/safety.cc,
src/tests/parseerr.test, src/tests/utf8.test, wrap/python/spot.py:
Adjust.
* src/twaalgos/totgba.hh, src/twaalgos/totgba.cc: Implement
the new function.
* NEWS: Mention this new function.
* src/bin/man/spot-x.x: Document SPOT_STREETT_CONV_MIN.
* src/tests/ltl2dstar4.test: Add tests.
* src/tests/Makefile.am: Add it.
* src/bin/autfilt.cc: Do do call remove_fin explicitely
when --tgba is used, let the postprocessor do it.
* src/twa/acc.hh: Add shift operators for acceptance marks.
* src/twaalgos/remfin.cc: Use the new algorithm.
* src/twaalgos/sccinfo.cc, src/twaalgos/sccinfo.hh: Add
a new method to supply the acceptance sets visited by an SCC.
* src/twaalgos/sccfilter.cc (acc_filter_some, acc_filter_all): Merge
into...
(acc_filter_mask): ... this single parametrized class, and only
remove sets that are only used as Inf.
* src/twa/acc.hh: Add missing operator~.
* src/tests/sccsimpl.test: Add test case.
* src/tests/sccdot.test: Adjust.
* NEWS: Mention the bug.
* src/bin/randaut.cc: Replace the --acc-type and --acc-sets
options by a more general --acceptance option, that take either
an acceptance formula, or an acceptance name parametred by ranges.
Also accept a range for the number of atomic propositions.
* src/twaalgos/randomgraph.cc (random_acceptance): Move...
* src/twa/acc.cc, src/twa/acc.hh (random): ... here.
(parse_acc_code): Generalize to accept ranges instead of
numbers whenever sensible, and accept a 'random' acceptance.
* src/tests/randaut.test: Adjust tests and add more.
* wrap/python/tests/randaut.ipynb: Adjust call to randaut.
It has two modes: strict or not. In strict mode (tested in
hoaparse.test), the acceptance formula has to match exactly the one
given in the HOA spec. In non-strict mode (tested in accparse2.py)
any equivalent formula is accepted.
* src/twa/acc.cc, src/twa/acc.hh (acc_cond::is_parity): New method.
* src/twaalgos/hoa.cc: Use it.
* src/tests/hoaparse.test: Test it.
* wrap/python/spot_impl.i: Bind it.
* wrap/python/tests/accparse2.py: New file.
* wrap/python/tests/Makefile.am: Add it.
So far the HOA output would emit an acc-name only
for generalized-Buchi or inferior types (Buchi, all).
It now knows about none, co-Buchi, generalized-co-Buchi,
Rabin, Streett, and generalized-Rabin as well.
* src/twa/acc.cc, src/twa/acc.hh: Add detection code.
* src/twaalgos/hoa.cc: Use it.
* src/tests/remfin.test, src/tests/maskacc.test,
src/tests/complete.test, src/tests/sim3.test,
src/tests/ltl2dstar.test: Adjust tests.
* src/tests/hoaparse.test: Adjust and add more tests.
* src/twa/acc.cc, src/twa/acc.hh: Add method to create
standard acceptance conditions, and adjust the parse_acc_code
to recognize them
* wrap/python/spot_impl.i (acc_cond::acc_code): Add a printer.
* wrap/python/tests/accparse.ipynb: New test file.
* wrap/python/tests/Makefile.am: Add it.
* src/tests/satmin2.test: Use the new syntax.
* src/twaalgos/dtgbasat.cc (sat_minimize): Use any arbitrary
acceptance condition passed via the "acc" option.
* src/twa/acc.hh (mark_t::max_set): New method.
* src/tests/satmin2.test: Add two test cases with DRA as input
and DSA as output.
This is still missing tests.
* src/bin/autfilt.cc: Add a --sat-minimize option.
* src/misc/optionmap.cc, src/misc/optionmap.hh: Allow passing strings.
* src/twa/acc.cc, src/twa/acc.hh: Add helper functions needed
by the SAT-encoder.
* src/twaalgos/complete.hh: Typos.
* src/twaalgos/dtbasat.hh: Adjust comment.
* src/twaalgos/dtgbasat.cc, src/twaalgos/dtgbasat.hh: Generalize
to take the target acceptance as input.
* src/twaalgos/postproc.cc, src/tests/ltl2tgba.cc: Adjust calls.
* src/twaalgos/sbacc.cc, src/twaalgos/sbacc.hh: Don't pass
the pointer by reference.
* src/tests/acc.cc, src/tests/acc.test: More tests
for the acceptance helper function.
