Reported by Shufang Zhu.

* spot/tl/ltlf.cc, spot/tl/ltlf.hh: Fix the transltion
and update the comments.
* tests/core/ltlfilt.test: Adjust test cases.
* NEWS: Mention the fix.
* THANKS: Add Shufang Zhu.

Compilation of each header file alone, as a safety check, was removed
when introducing "#pragma once" because we did not have to check for
possible double inclusion.  However we still need to compile each
header to make sure they are self-contained.

* tests/sanity/includes.test: Compile each header.
* tests/run.in: Export various compiler and directory flags.
* spot/twaalgos/emptiness_stats.hh, spot/misc/mspool.hh,
spot/misc/fixpool.hh: Include <spot/misc/common.hh>.
* spot/misc/common.hh: Include <cassert>.
* NEWS: Mention the fixed headers.

* spot/parseaut/parseaut.yy: Add a diagnostic.
* tests/core/parseaut.test: Test it.
* NEWS: Document it.

This should solve issue with the Debian package.

* spot/ltsmin/Makefile.am: Use the LTDLINC, LTDLDEPS and LIBLTDL as
documented.
* NEWS: Mention the fix.

Fix #198.  Reported by Maximilien Colange.

* spot/twaalgos/strength.cc (is_terminal): Test that no accepting
transition lead to a rejecting SCC.
* tests/core/strength.test: Add test case.
* spot/twaalgos/strength.hh, spot/twa/twa.hh, doc/org/concepts.org:
Adjust documentation.
* NEWS: Mention the fix.

Reported by František Blahoudek.

* spot/twaalgos/sccfilter.cc: Remove extra print statement.
* NEWS: Mention it.

* NEWS, configure.ac, doc/org/setup.org: Update.

* tests/core/ltl2tgba.test: Add new test-case,
reported by Tomáš Babiak.
* NEWS: Mention the bug fixed by previous patch.

* src/kernel.c: Fix error introduced by 5a862295.
Report from Tomáš Babiak.

* configure.ac, doc/org/setup.org, NEWS: Set version number.

* doc/org/oaut.org (Timing): New section.
* NEWS: Link to it.

* spot/twa/twa.hh, spot/twa/twa.cc (intersects, intersecting_run,
intersecting_word): New functions.
* NEWS: Mention them.
* doc/org/tut51.org, tests/python/bugdet.py: Use them.

* spot/twa/twagraph.hh: Here.

Suggested by Juraj Major.

* spot/twaalgos/sccfilter.cc: Here.
* tests/python/sccfilter.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the news.

Reported by Juraj Major.

* spot/twa/twa.hh: check num_sets() in prop_state_acc() so we do not
have to set it in set_acceptance(), causing trouble if set_acceptance()
is called multiple times.
* tests/python/setacc.py: New test case.
* tests/Makefile.am: Add it.
* THANKS: Add Juraj.
* NEWS: Mention the bug.

* spot/twaalgos/remfin.cc: Do not add a sink states to deterministic
weak automata, and actually apply the "weak" Fin-removal to any weak
automaton.
* tests/core/explprod.test: Add a test case for the previous patch,
but that used to fail because of this bug.
* NEWS: Mention the bug.

* spot/parseaut/public.hh, spot/parseaut/scanaut.ll: When parsing
automata read from some given FD, do not close the file descriptor, as
the caller is likely to already close it, and closing FDs twice is very
bad.  This seems to have be the root of some issue we had with recent
jupyter versions, were 0MQ would crash with "Bad file descriptor"
messages.  Also do not close stdin while we are at it.
* NEWS: Mention the bug.

* tests/python/ipnbdoctest.py: here.

* src/reorder.c, src/kernel.h: Expose bddreordermethod.
* src/bddop.c: Test bddreordermethod before ever calling setjmp().

* spot/twaalgos/ltl2tgba_fm.cc: Replace bdd_exists(a & b, c) by
bdd_appex(a, b, bddop_and, c).

* src/bddop.c (apply_rec, appquant_rec): Define missing shortcuts
for bddop_less, bddop_diff, bddop_revimpl and define them once.

* tests/Makefile.am: Run Python tests before other tests.
* tests/python/ipnbdoctest.py: Add some debug.

* src/kernel.c, src/kernel.h: Here.

Fixes #189.

* bin/ltldo.cc: Here.
* tests/core/ltldo.test: Adjust and add test-case for %R.
* NEWS: Mention the change.

For #189.

* bin/common_aoutput.cc: Do not call sysconf(_SC_CLK_TCK) if that is not
defined.  Also fix the help string, and simplify some conditions.

Alexandre GBAGUIDI AISSE authored Oct 24, 2016 and Alexandre Duret-Lutz committed Nov 08, 2016

For #189.

* NEWS: Update.
* bin/autfilt.cc: Replace stopwatch with process_timer.
* bin/dstar2tgba.cc: Replace stopwatch with process_timer.
* bin/ltl2tgba.cc: Replace stopwatch with process_timer.
* bin/ltlcross.cc: Replace stopwatch with process_timer.
* bin/ltldo.cc: Replace stopwatch with process_timer.
* bin/randaut.cc: Replace stopwatch with process_timer.
* bin/common_aoutput.hh: Implement process_timer, integrate it.
* bin/common_aoutput.cc: Integrate process_timer and implement new
print method.
* spot/misc/timer.hh: Modify timer class and timeinfo struct
i.e. add cutime (children_utime) and cstime (children_stime).
* spot/misc/timer.cc: Help code to behave as before all this.
* spot/twaalgos/dtbasat.cc: Help print_log to behave as before
all this.
* spot/twaalgos/dtwasat.cc: Help print_log to behave as before
all this.
* spot/misc/formater.hh: Add operator<< for spot::timer.

Debian unstable now has Jupyter, but since it moved away from ipython3,
the packages now have different names.

* debian/control: Here.

Jupyter 4.2 just landed in Debian unstable, so we have a few failures
because of all the renamings.

* tests/python/ipnbdoctest.py: Adjust imports for Jupyter 4.2.

This fixes an issue in the on-line translator, where error message would
not be output in the correct <div>.

* spot/parsetl/fmterror.cc (format_parse_errors): Flush the stream.

Fixes #187.

* spot/tl/ltlf.cc, spot/tl/ltlf.hh: New files.
* spot/tl/Makefile.am: Add them.
* bin/ltlfilt.cc: Add a new option.
* bin/man/ltlfilt.x: Add bibliographic reference.
* tests/core/ltlfilt.test: Add more tests.
* tests/python/ltlf.py: New file.
* tests/Makefile.am: Add it.
* python/spot/impl.i: Python bindings.
* NEWS: Mention it.

* spot/twaalgos/determinize.cc (safra_state::merge_redundant_states):
Test is_connected before called bdd_implies.

This fixes the incorrect output of tgba_determinize() reported yesterday
by Reuben Rowe.

* spot/twaalgos/simulation.cc: Do not purge unreachable states when
recording implications.
* tests/python/bugdet.py: New test case.
* tests/Makefile.am: Add it.
* THANKS: Add Reuben.
* NEWS: Mention the bug.