alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
6176 commits 6 branches 0 tags 36 MiB
Commit graph

1030 commits

Author SHA1 Message Date
Etienne Renault
369a8b8b14 mc: merge deadlock and reachabilty algorithms 
* spot/mc/deadlock.hh,
spot/mc/mc.hh,
spot/mc/mc_instanciator.hh,
tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
1736a7364c modelcheck: formula can be nullptr 
* tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
c19163cced cube: rename get_ap into ap 
* spot/kripke/kripke.hh,
spot/ltsmin/spins_kripke.hh,
spot/ltsmin/spins_kripke.hxx,
spot/mc/mc_instanciator.hh,
spot/mc/utils.hh,
spot/twacube/twacube.cc,
spot/twacube/twacube.hh,
spot/twacube_algos/convert.cc,
tests/core/twacube.cc,
tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
ee01fdf209 mc: rename ec_renault13lpar into lpar13 
* spot/mc/ec.hh: Rename to ...
* spot/mc/lpar13.hh: ... this.
* spot/mc/Makefile.am,
spot/mc/mc_instanciator.hh,
tests/ltsmin/modelcheck.cc: Here
 2020-06-03 12:22:41 +02:00
Etienne Renault
5bb29d646b mc: refactor parallel algorithms 
* spot/mc/Makefile.am,
spot/mc/bloemen.hh,
spot/mc/bloemen_ec.hh,
spot/mc/cndfs.hh,
spot/mc/deadlock.hh,
spot/mc/ec.hh,
spot/mc/intersect.hh,
spot/mc/mc.hh,
spot/mc/mc_instanciator.hh,
spot/mc/utils.hh,
tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
f8448fad89 kripkecube: modernize is_a_kripkecube_ptr 
* spot/kripke/kripke.hh,
spot/ltsmin/spins_kripke.hh,
spot/mc/bloemen.hh,
spot/mc/bloemen_ec.hh,
spot/mc/cndfs.hh,
spot/mc/deadlock.hh,
spot/mc/intersect.hh,
spot/mc/reachability.hh,
tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
b52e941b04 ltsmin: prefer '\n' for std::cerr 
* tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:40 +02:00
Antoine Martin
276892229c mc: implement CNDFS 
* spot/mc/Makefile.am: add cndfs.hh
* spot/mc/cndfs.hh, spot/mc/mc.hh: implementation here
* tests/ltsmin/check.test: test CNDFS
* tests/ltsmin/modelcheck.cc: add CNDFS option
 2020-06-03 12:22:40 +02:00
Antoine Martin
298e6f2b47 mc: bloemen emptiness check 
* spot/mc/bloemen_ec.hh,
spot/mc/mc.hh,
tests/ltsmin/check.test,
tests/ltsmin/modelcheck.cc: here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
35f1423e20 prefer -pthread to -lpthread 
* configure.ac,
spot/ltsmin/Makefile.am,
tests/Makefile.am: Here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
2b9471b9a7 please gcc snapshot 
* spot/bricks/brick-assert,
spot/bricks/brick-bitlevel,
spot/bricks/brick-shmem,
spot/bricks/brick-types,
spot/mc/bloemen.hh,
spot/mc/ec.hh,
spot/mc/intersect.hh,
tests/core/bricks.cc: Here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
eb4e3f8be9 modelcheck: fix erroneous report in deadlock 
* tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
01cceef29a bricks: move into spot directory 
* bricks/brick-assert, bricks/brick-bitlevel,
bricks/brick-hash, bricks/brick-hashset,
bricks/brick-shmem, bricks/brick-types: Rename as .. .
* spot/bricks/brick-assert, spot/bricks/brick-bitlevel,
spot/bricks/brick-hash, spot/bricks/brick-hashset,
spot/bricks/brick-shmem, spot/bricks/brick-types: ... this
* Makefile.am, README, debian/copyright,
debian/libspot-dev.install, m4/bricks.m4,
spot/Makefile.am, spot/ltsmin/spins_kripke.hh,
spot/ltsmin/spins_kripke.hxx, spot/mc/bloemen.hh
spot/mc/deadlock.hh, tests/Makefile.am,
tests/core/bricks.cc: here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
23edf52dd5 fixpool: propose alternative policy 
In 3fe74f1c, fixed_size_pool was changed in order to
help memcheck to detect "potential" memory leaks. In a
multithreaded context, this could raise false alarm. To
solve this, we proprose 2 policies for the pool, one with
the check and one without.

* spot/misc/fixpool.cc: deleted ...
* spot/ltsmin/ltsmin.cc, spot/ltsmin/spins_kripke.hh,
spot/mc/deadlock.hh, spot/misc/Makefile.am,
spot/misc/fixpool.cc, spot/misc/fixpool.hh,
spot/priv/allocator.hh, spot/ta/tgtaproduct.cc,
spot/ta/tgtaproduct.hh, spot/twa/twaproduct.cc,
spot/twa/twaproduct.hh, tests/core/mempool.cc: Here.
 2020-06-03 12:22:26 +02:00
Etienne Renault
fe1be20f09 twacube: fix dot output in tests 
* tests/core/twacube.test: Here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
5062d1c2fa modelcheck: conversions now report about the options 
* tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
5d30286dd6 twacube: 'mark_t' is deprecated 
* spot/mc/ec.hh, spot/mc/intersect.hh,
tests/core/twacube.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
9827b1d096 modelcheck: capture exceptions by const reference 
* tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
88dc500aa7 tests: fix call to print_dot according to default arguments 
* tests/core/twacube.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
a9178fbe64 modelcheck: update output and documentation 
Fixes #330.

* tests/ltsmin/README,
tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
011115cb1d tests: include missing config.h 
* spot/mc/unionfind.cc,
spot/twacube/cube.cc,
spot/twacube/twacube.cc,
spot/twacube_algos/convert.cc,
tests/core/bricks.cc,
tests/core/cube.cc,
tests/core/twacube.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
34b9e89f5d tests: please modelcheck interface 
* tests/ltsmin/finite3.test: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
f397def03e tests: add tests for parallel algorithms 
* tests/ltsmin/check.test: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
63a4b4085a mc: bloemen count unique states 
* spot/mc/bloemen.hh, tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
80746e4332 modelcheck: update tests 
* tests/ltsmin/check.test,
tests/ltsmin/check2.test,
tests/ltsmin/check3.test,
tests/ltsmin/finite2.test,
tests/ltsmin/finite3.test: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
e6e3b568ca mc: parallel version of bloemen 
* spot/mc/bloemen.hh,
tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
01093f992e mc: sequential version of Bloemen 
* spot/mc/Makefile.am, spot/mc/bloemen.hh,
spot/mc/mc.hh, tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
15e72e90cc mc: add swarmed deadlock-detection 
* spot/mc/Makefile.am, spot/mc/deadlock.hh,
spot/mc/mc.hh, tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
f486dab241 ltsmin: move modelchek in mc directory 
* spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh,
spot/mc/Makefile.am, tests/ltsmin/modelcheck.cc,
spot/mc/mc.hh: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
d2549334f9 modelcheck: please gcc catch-value errors 
* tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
a147fd65dc tests: add pthread library 
* tests/Makefile.am: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
7ae7e2e831 includes: must not check *.hxx 
* tests/sanity/includes.test: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
6c5c308ea8 bricks: adapt with the new bricks 
* bricks/brick-hash, tests/core/bricks.cc: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
72948661e9 swarming: add support everywhere 
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.
 2020-06-03 10:33:53 +02:00
Etienne Renault
50d888adf8 Twacube must share the order of atomic propositions 
* spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh,
tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
a1787dd1ce modelcheck: support for csv extraction 
* tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
765bb8a7c4 Promote use of shared_ptr 
* spot/kripke/kripke.hh, spot/ltsmin/ltsmin.cc,
spot/ltsmin/ltsmin.hh, spot/mc/ec.hh, spot/mc/intersect.hh,
spot/mc/utils.hh, spot/twacube/Makefile.am,
spot/twacube/fwd.hh, spot/twacube/twacube.hh,
spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh,
tests/core/twacube.cc, tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
9799f2884e modelcheck: support for twacube 
* spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh,
tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
d430129bb1 convert: simplify interfaces 
* spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh,
tests/core/twacube.cc: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
f04074bd6d sanity: replace tabulars by spaces 
* spot/ltsmin/ltsmin.cc,
spot/mc/ec.hh, spot/mc/intersect.hh,
spot/mc/reachability.hh, spot/mc/unionfind.cc,
spot/mc/utils.hh, spot/twacube/cube.cc,
spot/twacube/twacube.cc,
spot/twacube/twacube.hh,
spot/twacube_algos/convert.cc,
spot/twacube_algos/convert.hh,
tests/core/bricks.cc,
tests/core/cube.cc,
tests/core/twacube.cc,
tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
458f506336 bricks: add bricks for concurrent hashmap 
* Makefile.am, README, bricks/brick-assert.h,
bricks/brick-bitlevel.h, bricks/brick-hash.h,
bricks/brick-hashset.h, bricks/brick-shmem.h,
bricks/brick-types.h, configure.ac,
debian/copyright, debian/libspot-dev.install,
m4/bricks.m4, tests/Makefile.am,
tests/core/.gitignore, tests/core/bricks.cc: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
4337abc5a6 modelcheck: rewrite and use argp 
* tests/Makefile.am, tests/ltsmin/check.test,
tests/ltsmin/finite.test, tests/ltsmin/finite2.test,
tests/ltsmin/kripke.test, tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
b87693bcc3 convert: twacube to twa translation 
* spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh,
tests/core/twacube.cc, tests/core/twacube.test: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
aceb37ab50 convert: twa to twacube translation 
* spot/twacube/Makefile.am, spot/twacube/twacube.cc,
spot/twacube/twacube.hh, spot/twacube_algos/convert.cc,
spot/twacube_algos/convert.hh, tests/Makefile.am,
tests/core/.gitignore, tests/core/twacube.cc,
tests/core/twacube.test: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
8d57700d6a convert: BDD to cube conversions 
* README, configure.ac, spot/Makefile.am,
spot/twacube_algos/Makefile.am, spot/twacube_algos/convert.cc
spot/twacube_algos/convert.hh, tests/core/cube.cc,
tests/core/cube.test: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
7c3fdd6b97 Introduce cube data structure 
* README, configure.ac, spot/Makefile.am,
spot/twacube/Makefile.am, spot/twacube/cube.cc,
spot/twacube/cube.hh, tests/Makefile.am,
tests/core/.gitignore, tests/core/cube.cc,
tests/core/cube.test: here.
 2020-06-03 10:33:53 +02:00
Alexandre Duret-Lutz
b7abe6f4b4 ltldo: improve error messages 
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.
 2020-06-01 11:00:25 +02:00
Alexandre Duret-Lutz
8e9e706003 * tests/sanity/80columns.test: Force LC_ALL. 2020-05-30 14:29:20 +02:00
Alexandre Duret-Lutz
f6cf8e4d8a ltlsynt: use wdba-minimize=2 and ba-simul=0 
* bin/ltlsynt.cc: Here.
* tests/core/ltlsynt.test: Add extra test case.
* NEWS: Mention ltlsynt -x and related defaults.
 2020-05-24 22:16:48 +02:00
Florian Renkin
0413ecfbb8 ltlsynt: Change default options 
* bin/ltlsynt.cc: Change default options.
* tests/core/ltlsynt.test: Add test.
 2020-05-24 20:16:43 +02:00