* spot/twaalgos/aiger.cc: Simplify some bit operatitions. Force the
ordering of operations in aig_and, that was causing a test case to
fail on ARM, and greatly simplify the code and data structures used in
remove_unused().
* tests/core/ltlsynt.test: Adjust expected output.
On some architectures (e.g., ARM, or even some -flto setups on Intel)
C++ exceptions to not traverse the C functions. So even if the C++
main() has a try/catch, it will not catch the exception thrown by C++
code called from the argp module (which is compiled in C).
* bin/common_setup.cc, bin/common_setup.hh: Define some macros
and function to factorize exception handling.
* bin/autcross.cc, bin/autfilt.cc, bin/common_aoutput.cc,
bin/common_color.cc, bin/common_finput.cc, bin/common_hoaread.cc,
bin/common_output.cc, bin/common_post.cc, bin/common_trans.cc,
bin/dstar2tgba.cc, bin/genaut.cc, bin/genltl.cc, bin/ltl2tgba.cc,
bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc, bin/ltlfilt.cc,
bin/ltlgrind.cc, bin/ltlsynt.cc, bin/randaut.cc, bin/randltl.cc:
Protect all parse_opt() functions, even those where there is currently
no exception risk.
* spot/twaalgos/aiger.cc: Simplify some bit operatitions. Force the
ordering of operations in aig_and, that was causing a test case to
fail on ARM, and greatly simplify the code and data structures used in
remove_unused().
* tests/core/ltlsynt.test: Adjust expected output.
On some architectures (e.g., ARM, or even some -flto setups on Intel)
C++ exceptions to not traverse the C functions. So even if the C++
main() has a try/catch, it will not catch the exception thrown by C++
code called from the argp module (which is compiled in C).
* bin/common_setup.cc, bin/common_setup.hh: Define some macros
and function to factorize exception handling.
* bin/autcross.cc, bin/autfilt.cc, bin/common_aoutput.cc,
bin/common_color.cc, bin/common_finput.cc, bin/common_hoaread.cc,
bin/common_output.cc, bin/common_post.cc, bin/common_trans.cc,
bin/dstar2tgba.cc, bin/genaut.cc, bin/genltl.cc, bin/ltl2tgba.cc,
bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc, bin/ltlfilt.cc,
bin/ltlgrind.cc, bin/ltlsynt.cc, bin/randaut.cc, bin/randltl.cc:
Protect all parse_opt() functions, even those where there is currently
no exception risk.
Suggested by Victor Khomenko.
* bin/ltl2tgba.cc, bin/ltldo.cc: Implement it.
* doc/org/hierarchy.org: Use it.
* tests/core/ltldo2.test: Test it.
* bin/common_output.cc: Typo.
* NEWS: Mention the new option.
Suggested by Victor Khomenko.
* bin/ltl2tgba.cc, bin/ltldo.cc: Implement it.
* doc/org/hierarchy.org: Use it.
* tests/core/ltldo2.test: Test it.
* bin/common_output.cc: Typo.
* NEWS: Mention the new option.
This was prompted by reports by Andrew Wells and Yong Li.
* NEWS, doc/tl/tl.tex: Document the changes.
* THANKS: Add Andrew.
* bin/ltlfilt.cc: Match --ltl before --from-ltlf if needed.
* spot/parsetl/parsedecl.hh, spot/parsetl/parsetl.yy,
spot/parsetl/scantl.ll: Parse X[!].
* spot/tl/formula.cc, spot/tl/formula.hh: Declare the new operator.
* spot/tl/ltlf.cc: Adjust to handle op::X and op::strong_X correctly.
* spot/tl/dot.cc, spot/tl/mark.cc, spot/tl/mutation.cc,
spot/tl/print.cc, spot/tl/simplify.cc, spot/tl/snf.cc,
spot/tl/unabbrev.cc, spot/twa/formula2bdd.cc,
spot/twaalgos/ltl2taa.cc, spot/twaalgos/ltl2tgba_fm.cc,
tests/core/ltlgrind.test, tests/core/rand.test,
tests/core/sugar.test, tests/python/randltl.ipynb: Adjust.
* tests/core/ltlfilt.test, tests/core/sugar.test,
tests/core/utf8.test: More tests.
* tests/Makefile.am (ltsmin_modelcheck_LDADD): Add -lpthread as it
seems Debian's libtool does not carries this dependency over from
libspotltsmin.la. Also using $(LTLIBMULTITHREAD) does not work,
because that would add -pthread which is currently ignored when
linking shared libraries (because libtool adds -nostdlib for some
reason).
Bison 3.0 was released in 2013, and the current Debian stable (buster)
has version 3.3.2.
* m4/bison.m4: Remove -Wno-precedence and -Wno-empty-rule, keep
-Wno-deprecated just to protect from future deprecation warnings that
would be interpreted as errors.
* spot/parseaut/parseaut.yy, spot/parsetl/parsetl.yy: Use %empty
rules, prefer %precedence over %nonassoc, update %error-versbose and
%name-prefix to their more modern equivalent.
* spot/misc/trival.hh (maybe): Mark this function as noexcept to
please the compiler while compiling the parsers.
std::cerr will flush after each operator<< by default, so it's simpler
to use \n instead of std::endl, especially if we can merge \n into the
previous string. Ideally we should prefer \n for std::cout as well,
but there are reasonable cases where we want to call std::endl there,
so it's hard to enforce.
* tests/sanity/style.test: Diagnose occurrences of cerr.*<<.*endl.
* bin/autcross.cc, bin/autfilt.cc, bin/ltlcross.cc, bin/ltlsynt.cc,
spot/tl/formula.cc, spot/twa/bdddict.cc, tests/core/checkpsl.cc,
tests/core/checkta.cc, tests/core/consterm.cc, tests/core/emptchk.cc,
tests/core/equalsf.cc, tests/core/ikwiad.cc, tests/core/kind.cc,
tests/core/length.cc, tests/core/ltlrel.cc, tests/core/parity.cc,
tests/core/randtgba.cc, tests/core/reduc.cc, tests/core/syntimpl.cc,
tests/ltsmin/modelcheck.cc: Fix them.
Reported by Salomon Sickert.
* spot/twaalgos/complement.cc: Make sure the output of postproc
is deterministic.
* tests/core/ltlcross.test: Add test case.
* NEWS: Mention the bug.
* spot/twaalgos/product.cc: The res pointer should be
passed by reference since we reset it to nullptr when
output_aborter says "too large".
* python/spot/impl.i: Add binding for powerset.hh,
so we can use output_aborter in Python.
* tests/python/prodexpt.py: Test it.
