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

5547 commits

This branch
This branch
All branches
Author SHA1 Message Date
Etienne Renault
47c4f19e22 bricks: please gcc Werror=noexcept option 
* bricks/brick-shmem: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
44041efc51 bricks: please gcc Wmacro-redefined option 
* bricks/brick-assert: here.
 2020-06-03 10:33:53 +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
0be3630218 ltsmin: extract kripkecube to ease manipulation 
* spot/ltsmin/Makefile.am,
spot/ltsmin/ltsmin.cc,
spot/ltsmin/ltsmin.hh
spot/ltsmin/spins_kripke.hh,
spot/ltsmin/spins_kripke.hxx: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
5445007070 ltsmin: extract spins interface 
* spot/ltsmin/Makefile.am, spot/ltsmin/ltsmin.cc,
spot/ltsmin/ltsmin.hh,
spot/ltsmin/spins_interface.hh: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
8a930c7572 ltsmin: simplify iterator 
* spot/ltsmin/ltsmin.cc: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
ac54acbb9d brick: please gcc pedantic option 
* bricks/brick-assert: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
03ff789324 mark_t::operator bool() is now explicit 
Follows up cf5d2c2b.

* spot/mc/ec.hh: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
6d282bbc6b ltsmin: update usage of brick-hashset 
From a discussion with Petr Rockai: "the possibly non-intuitive bit
that you probably didn't notice is that the hashset is supposed to be
passed to each thread by value. The copy semantics of the entire
hashset are that of a shared pointer: multiple copies share the same
underlying data. Each thread *must* have its own private copy of the
hashset object (there are bits of state that each thread needs for
bookkeeping and those must not be shared)."

*  spot/ltsmin/ltsmin.cc: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
1a37a08ba4 bricks: update 
* bricks/brick-hashset: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
8ced74f8e6 bricks: please pedantic option for gcc 
* bricks/brick-bitlevel: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
606e4fc88c please pedantic option for gcc 
* spot/kripke/kripke.hh: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
a308d1a60a bricks: add support for gcc prior to 4.9 
* bricks/brick-bitlevel, bricks/brick-hashset,
bricks/brick-shmem, bricks/brick-types: 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
bb9fa4e910 bricks: update and move to c++14 
* Makefile.am, bricks/brick-assert,
bricks/brick-assert.h, spot/ltsmin/ltsmin.cc,
spot/mc/ec.hh: here.

* bricks/brick-bitlevel.h, bricks/brick-hash.h,
bricks/brick-hashset.h, bricks/brick-shmem.h,
bricks/brick-types.h: Rename as ...
* bricks/brick-bitlevel, bricks/brick-hash,
bricks/brick-hashset, bricks/brick-shmem,
bricks/brick-types: ... these
 2020-06-03 10:33:53 +02:00
Etienne Renault
9208726d97 reachability: improve support for callbacks 
* spot/mc/reachability.hh: 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
ae1a3601e6 bricks: propagate use of SPOT_FALLTHROUGH 
* bricks/brick-hash.h, bricks/brick-hashset.h: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
fb4ef40d11 Use SPOT_ASSERT() instead of assert() in public headers 
* spot/mc/ec.hh, spot/mc/intersect.hh,
spot/mc/reachability.hh, spot/mc/utils.hh: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
c515ee92e2 bricks: add missing override 
* bricks/brick-assert.h, bricks/brick-hashset.h,
bricks/brick-shmem.h: 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
9a9a237272 timer: support for walltime 
* spot/misc/timer.hh: 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
7d2abe229b swig: prefer typedef to using 
According to swig3.0. the 'using' keyword
in type aliasing is not fully supported yet.

* spot/ltsmin/ltsmin.hh: 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
94f7c58f44 intersect: statistic provided using an object 
* spot/mc/ec.hh, spot/mc/intersect.hh: 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
e11f24dbc1 twacube: atomic propositions are now passed by copy 
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.
 2020-06-03 10:33:53 +02:00
Etienne Renault
6d3154be94 bricks: ATOMIC_FLAG_INIT initialization 
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.
 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
681c2b2011 ltsmin: use FastConcurrent map 
* spot/ltsmin/ltsmin.cc: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
01f66642f1 bricks: fix clang warnings 
* bricks/brick-hash.h, bricks/brick-shmem.h: 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
b4bbf50794 ltsmin: prodcuce kripkecube 
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.
 2020-06-03 10:33:53 +02:00
Etienne Renault
8e593611f6 convert: kripke and product towards twa 
* spot/mc/Makefile.am, spot/mc/utils.hh: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
3bafe693ef ec: Renault et al LPAR'13 emptiness check 
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.
 2020-06-03 10:33:53 +02:00
Etienne Renault
87de88c80c intersection: for kripke and twacube 
* spot/mc/Makefile.am, spot/mc/intersect.hh: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
94492ffa14 reachability: sequential reachability for kripkecube 
* README, configure.ac, spot/mc/Makefile.am,
spot/mc/reachability.hh: here.
 2020-06-03 10:33:53 +02:00
Etienne Renault
748068a6d0 kripke: define kripkecube structure 
* spot/kripke/kripke.hh: 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
d76236a03f sccinfo: fix doc 
* spot/twaalgos/sccinfo.hh (scc_info_options::NONE): Fix doxygen doc.
 2020-05-29 17:14:17 +02:00
Alexandre Duret-Lutz
9150a2e54b twa: get rid of set_num_sets_() 
* spot/twa/twa.hh (set_num_sets_): Remove, and adjust all uses.
This fixes #414.
 2020-05-25 10:51:44 +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