* spot/graph/graph.hh: Use the sign bit of destination state X to
designate a universal edge. Store the destinations of such an edge in a
separate array, at index ~X.
* spot/graph/ngraph.hh, tests/core/graph.cc, tests/core/graph.test,
tests/core/ngraph.cc: Adjust test case to the new interface.
This version has optimization for explicit twa, and also for weak and
terminal (depending on whether an accepting run is requested) automata.
* spot/twaalgos/couvreurnew.hh, spot/twaalgos/couvreurnew.cc,
spot/twaalgos/Makefile.am: New files for the new algorithm.
* spot/twaalgos/emptiness.cc, tests/core/randtgba.cc:
Register new algorithm.
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.
* NEWS, spot/twa/twa.hh: Document the change.
* spot/twa/twagraph.hh, spot/kripke/kripkegraph.hh:
Add an exception in get_init_state_number().
get_init_state() now calls get_init_state_number().
* spot/twa/twagraph.cc, spot/twaalgos/simulation.cc,
spot/twaalgos/powerset.cc, spot/twaalgos/complete.cc,
spot/twaalgos/sccfilter.cc: Remove now useless tests.
* spot/twaalgos/hoa.cc: Remove now useless comment.
* spot/twaalgos/minimize.cc: Never return an automaton with no state.
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.
This fixes c9aabcdd.
* spot/ltsmin/ltsmin.cc: Update the extension after compiling
the model. Do not duplicate the symbol lookups for DVE and gal2C.
Also, improve error reporting in case of missing symbol.
* tests/ltsmin/check.test: Remove stray character.
* spot/ltsmin/ltsmin.cc: Handle GAL models.
* tests/Makefile.am: Test the new feature.
* tests/ltsmin/check.test: Also check GAL.
* tests/ltsmin/beem-peterson.4.gal: A new GAL model for tests.
* tests/ltsmin/finite.gal: A new GAL model for tests.
* tests/ltsmin/finite3.test: A new test for GAL.
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.
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.
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.
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.
These were not actually printing in "SERE" mode due to a copy/paste
error. PVS-Studio seems really good at finding those. For #192.
* spot/tl/print.cc: Fix it.
* NEWS: Mention the bug.
This was noticed while looking at a false-positive in the report for
PVS-Studio, in #192.
* spot/misc/optionmap.cc: Do not remove the option from unused_ twice..
For #192.
* bin/common_trans.cc, bin/common_trans.hh, spot/twa/acc.hh:
Add an operator= in addition to the copy constructor.
* spot/twaalgos/ltl2tgba_fm.cc: Use the default constructor.
* spot/ta/taproduct.cc, spot/ta/taproduct.hh: Delete an unused copy
constructor.
