Reported by Salomon Sickert.
* bin/ltlcross.cc: Also call determinize_unknown_acceptance() for
positive automata.
* tests/core/ltlcross3.test: Add another test case.
* NEWS: Mention the fix.
Fixes#420 reported by Salomon Sickert.
* bin/ltlcross.cc: Call determine_unknown_acceptance().
* spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Document
that one_accepting_scc()==-1 can mean "don't know", and update
determine_unknown_acceptance() to set one_acc_scc_.
* tests/core/ltlcross3.test: Add test case.
* NEWS: Mention the fixes.
* spot/twaalgos/alternation.cc, spot/twaalgos/alternation.hh,
spot/twaalgos/complement.cc, spot/twaalgos/complement.hh,
spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh,
spot/twaalgos/minimize.cc, spot/twaalgos/minimize.hh,
spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/powerset.cc, spot/twaalgos/powerset.hh,
spot/twaalgos/product.cc, spot/twaalgos/product.hh: Use an
output_aborter argument to abort if the output is too large.
* bin/ltlcross.cc: Use complement() with an output_aborter
so that ltlcross will not attempt to build complement larger
than 500 states or 5000 edges. Add --determinize-max-states
and --determinize-max-edges options.
* tests/core/ltlcross3.test, tests/core/ltlcrossce2.test,
tests/core/sccsimpl.test, tests/core/wdba2.test,
tests/python/stutter-inv.ipynb: Adjust test cases.
* NEWS: Document this.
* bin/spot-x.cc: Add documentation for postprocessor's
det-max-states and det-max-edges arguments.
* doc/org/ltlcross.org: Update description.
This allows to represent more than 32 acceptance marks.
* configure.ac: add an option to specify the number of marks
* spot/twa/acc.hh: implement it
* tests/python/acc_cond.ipynb, tests/core/acc.cc,
tests/core/ltlcross3.test: update tests
* NEWS: document it
* bin/randltl.cc: fix an include
* bin/common_conv.cc, bin/common_conv.hh: Here.
* bin/autfilt.cc, bin/common_trans.cc, bin/ltlcross.cc, bin/ltldo.cc,
bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randaut.cc, bin/randltl.cc: Pass
the name of the argumennt to the conversion function.
* tests/core/ltlcross3.test, tests/core/ltldo.test,
tests/core/randaut.test: Add test cases.
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.
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.
Suggested by František Blahoudek.
* bin/ltlcross.cc: Implement the two options.
* doc/org/ltlcross.org, NEWS: Document them.
* tests/core/complementation.test: Adjust test case.
* tests/core/ltlcross3.test, tests/core/unambig.test: More tests.
Report from František Blahoudek.
* bin/ltlcross.cc: Do not display stats for automata
that do not exist.
* tests/core/ltlcross3.test: Test it.
* NEWS: Mention the fix.