Swarming implies that a single instance of the kripke
structure (or product) will be explored by diffrent threads
with their own exploration order. Most of the modification
aims to have a thread safe kripke structure.
* spot/kripke/kripke.hh, spot/ltsmin/ltsmin.cc,
spot/ltsmin/ltsmin.hh, spot/mc/ec.hh,
spot/mc/intersect.hh, spot/mc/reachability.hh,
spot/misc/hash.hh, spot/twacube/twacube.hh,
tests/core/twacube.test, tests/ltsmin/modelcheck.cc: here.
Passing atomic propositions by reference allows to
save very little memory so it doesn't worth complexifying
memory management.
* spot/twacube/twacube.cc, spot/twacube/twacube.hh: here.
From the working draft: "The macro ATOMIC_FLAG_INIT shall be defined
in such a way that it can be used to initialize an object of type
atomic_flag to the clear state. The macro can be used in the form:
atomic_flag guard = ATOMIC_FLAG_INIT; It is unspecified whether the
macro can be used in other initialization contexts."
* bricks/brick-shmem.h: here.
Warning! this patch introduces redundancy (or difference)
between wether you ask for a kripkecube or a kripke.
* spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh: here.
In order to reuse the computation of the
intersection between kripke and twa efficiently,
we use template inheritance through the
"mixin templates" technique.
* spot/Makefile.am, spot/mc/Makefile.am,
spot/mc/ec.hh, spot/mc/unionfind.cc,
spot/mc/unionfind.hh: here.
Use ltldo:... instead of error:... and warning:... and also improve
the diagnostic displayed after a translation failure to mention the
tool and formula.
Incidentally, this fixes a spurious test case failure observed by
Philipp Schlehuber on CentOS7.7 where glibc 2.17 is installed. With
this system, when posix_spawn() starts a binary that does not exist,
it returns success and let the child die with exit code 127. On more
recent glibc, posix_spawn() manages to return execve()'s errno, as if
the child had not been created. We handle those two different ways to
fail, but before this patch one used to print "error:..." and the
other "ltldo:...".
* bin/ltldo.cc: Display the program_name in error message. Display
the command name and formula on translation failure.
* tests/core/ltldo.test: Adjust test case.
* NEWS: Mention the fix.
Bison <3.6 used to complain about "$undefined", while Bison >=3.6 now
write "invalid token".
* tests/core/parseaut.test, tests/core/parseerr.test,
tests/core/sugar.test: Adjust expected diagnostics to match Bison pre
and post 3.6.
Closes#405. This shows no difference on the test suite,
but that is thanks to the previous patch: without it, an
example in automata.ipynb would have an extra edge.
* spot/twaalgos/cleanacc.cc (simplify_acceptance): Call
unit_propagation() before simplify_complementary_marks_here() and
fuse_marks_here(), because that is simpler to perform.
* spot/twaalgos/remfin.cc (default_strategy): Detect transitions
from the main copy that are completely accepting and that do not
need to be repeated in the clones.
* tests/python/remfin.py: Add a test case.
* tests/core/ltl2dstar4.test: Improve expected results.
* NEWS: Mention the change.
This remove some restrictions that prevented fuse_marks_here from
simplifying certain patterns, as noted in the first comment of
issue #405.
* spot/twaalgos/cleanacc.cc (find_interm_rec, find_fusable): Remove
some unnecessary restrictions to singleton marks, and replace the hack
put one non-singleton mark at the beginning of the singleton list by a
sort.
* tests/python/simplacc.py: Add two test cases.
* tests/python/automata.ipynb, tests/core/remfin.test: Improve
expected results.
* NEWS: Mention the bug.
Allocate the first chunk when the fixpool is created. This avoid a
undefined behavior reported in issue #413 without requiring an extra
comparison in allocate().
* spot/misc/fixpool.hh, spot/misc/fixpool.cc (new_chunk_): New method
extracted from allocate(). Use it in the constructor as well.
* NEWS: Mention the bug.
Fixes#15.
* spot/twaalgos/minimize.hh, spot/twaalgos/minimize.cc
(minimize_obligation_garanteed_to_work): New function.
* spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Use it if
wdba-minimize=1. Handle new default for wdba-minimize.
* NEWS, bin/spot-x.cc: Document those changes.
* tests/core/ltl2tgba2.test: Add some test cases.
* tests/core/genltl.test: Improve expected results.
