Etienne Renault
|
b4412482c8
|
HACKING: swig-python is required for MacOS
* HACKING: Here.
|
2020-06-04 17:26:58 +02:00 |
|
Etienne Renault
|
3acf2ca689
|
rpm: add unpackaged files
* spot.spec.in: Here.
|
2020-06-04 14:09:54 +02:00 |
|
Etienne Renault
|
c20abb5a0f
|
debian: remove useless directive
* debian/libspot-dev.install: Here.
|
2020-06-04 06:45:38 +02:00 |
|
Etienne Renault
|
330cd80fed
|
twacube: fix typo
* spot/twacube/twacube.hh: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
c06085a60b
|
are_equivalent: remove redundant code
* spot/twacube_algos/convert.cc: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
ff48c81198
|
twacube_to_twa: allows use of existing BDD_dict
* spot/twacube_algos/convert.cc,
spot/twacube_algos/convert.hh: Here.
* tests/core/twacube.cc: Test it.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
b1b59d0eae
|
cube: incorrect use of reverse_binder in are_equivalent
Thanks to A. Martin for reporting this.
* spot/twacube_algos/convert.cc,
tests/core/twacube.cc: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
e564dd1263
|
atomic: check if -latomic is required for std::atomic
* configure.ac,
m4/l_atomic.m4,
python/Makefile.am,
tests/Makefile.am: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
6e0e6b923d
|
NEWS: mention cube-based transformations
* NEWS: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
61561ee9ac
|
raspbian: add missing library
* tests/Makefile.am,
python/Makefile.am: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
9a8745fcff
|
tests: ignore thread affinity
* tests/ltsmin/check.test,
tests/ltsmin/testconvert.test: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
7c9ae3d361
|
tests: add missing library
* tests/Makefile.am: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
2a41772ff9
|
mc: remove old FIXME
* spot/mc/mc_instanciator.hh: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
1dc6ead1e0
|
mc: do not mix static and SPOT_API
* spot/mc/mc_instanciator.hh: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
6d390a342d
|
kripke: add missing SPOT_API
* spot/kripke/kripke.hh: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
e484e0c471
|
mc: concept-like check for mc_algorithms
* spot/mc/mc_instanciator.hh: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
85ff53c45e
|
twacube: fix erroneous translation
* spot/twacube_algos/convert.cc,
tests/core/twacube.test: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
89675a2762
|
twacube_algos: add support for are_equivalent
* spot/twacube_algos/convert.cc,
spot/twacube_algos/convert.hh,
tests/core/twacube.cc: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
92845612a1
|
sanity: please 80 columns
* spot/ltsmin/spins_kripke.hh,
spot/twacube/twacube.cc,
spot/twacube_algos/convert.cc: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
227627c739
|
mc: correct SPOT_API
* spot/mc/mc.hh: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
070dc4880a
|
modelcheck: more relevant information for --csv
* tests/ltsmin/check.test,
tests/ltsmin/modelcheck.cc: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
bdb95dcde9
|
mc: keep information about the finisher
* spot/mc/bloemen.hh,
spot/mc/bloemen_ec.hh,
spot/mc/cndfs.hh,
spot/mc/deadlock.hh,
spot/mc/lpar13.hh,
spot/mc/mc.hh,
spot/mc/mc_instanciator.hh: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
cb8eb7e9b2
|
check: update with new modelcheck options/output
* tests/ltsmin/check.test: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
ff57f59dba
|
modelcheck: add missing --kripke option
* tests/ltsmin/modelcheck.cc: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
a3df930a60
|
mc: please include.test
* spot/mc/bloemen.hh,
spot/mc/bloemen_ec.hh,
spot/mc/deadlock.hh,
spot/mc/lpar13.hh,
spot/mc/mc.hh: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
17579ad9ad
|
mc: rework and test conversion into twa
* spot/mc/Makefile.am,
spot/mc/reachability.hh,
spot/mc/utils.hh,
tests/Makefile.am,
tests/ltsmin/.gitignore,
tests/ltsmin/testconvert.cc,
tests/ltsmin/testconvert.test: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
568fcdfc9a
|
mc: rework product_to_twa
* spot/mc/utils.hh: Here.
|
2020-06-03 12:22:41 +02:00 |
|
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
|
2d59a5c752
|
mc: clarify method name
* spot/mc/bloemen.hh,
spot/mc/bloemen_ec.hh,
spot/mc/cndfs.hh,
spot/mc/deadlock.hh,
spot/mc/lpar13.hh,
spot/mc/mc_instanciator.hh: 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
|
b32e451292
|
kripke: please style.test
* spot/kripke/kripke.hh: 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
|
907a3cfbbf
|
twacube: check nullptr during conversion
* spot/twacube_algos/convert.cc: Here.
|
2020-06-03 12:22:41 +02:00 |
|
Etienne Renault
|
53ea1131e6
|
Fixup: missing dependency bloemen
* spot/mc/Makefile.am: here.
|
2020-06-03 12:22:41 +02:00 |
|
|
|
fcf6bb3d3d
|
twacube: mark get_initial method as const
* spot/twacube/twacube.hh,spot/twacube/twacube.cc: Here.
|
2020-06-03 12:22:40 +02:00 |
|
|
|
0ad380ef12
|
twacube: mark succ() as const
* spot/twacube/twacube.hh: Here.
|
2020-06-03 12:22:40 +02:00 |
|
|
|
a14f63dd25
|
twacube: add num_states and num_edges
* spot/twacube/twacube.hh: Here.
|
2020-06-03 12:22:40 +02:00 |
|
|
|
49a3cf1148
|
twacube: mark get_ap method as const
* spot/twacube/twacube.hh,spot/twacube/twacube.cc: Here.
|
2020-06-03 12:22:40 +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 |
|
Etienne Renault
|
87afcd2f87
|
twacube: fix bug in swarming for large formulae
This bug is similar to the one described in commit
d956fdc385b4dd9a5c5b3a63a0de80a09eb8e40d.
* spot/twacube/twacube.hh: Here.
|
2020-06-03 12:22:40 +02:00 |
|
|
|
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 |
|
|
|
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
|
949881935a
|
ltsmin: rework spins_interface
* spot/ltsmin/ltsmin.cc,
spot/ltsmin/spins_interface.cc,
spot/ltsmin/spins_interface.hh: here.
|
2020-06-03 12:22:40 +02:00 |
|
Etienne Renault
|
7a8a4f4d77
|
ltdl: should not appear in public headers
* spot/ltsmin/Makefile.am,
spot/ltsmin/spins_interface.hh,
spot/ltsmin/spins_interface.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 |
|
