alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Commit graph

  • d2bde1af19 modelcheck: do not load twice model Etienne Renault 2020-06-09 09:01:05 +02:00
  • 4cd23d1fc5 lpar13: call finalize even when empty product Etienne Renault 2020-06-09 07:53:22 +02:00
  • d3eb269078 modelcheck: fix incorrect return value without --csv Etienne Renault 2020-06-09 07:45:24 +02:00
  • 099387d831 mc: fixes #416 Etienne Renault 2020-06-08 18:04:03 +02:00
  • f5585525f0 twacube: cleanup API Etienne Renault 2020-06-08 10:17:06 +02:00
  • c61b721a48 cube: more tests Etienne Renault 2020-06-08 09:19:18 +02:00
  • 6243803018 address a new g++-10 warnings Alexandre Duret-Lutz 2020-06-09 00:32:48 +02:00
  • da9d92eef7 swig: search for swig4.0 Alexandre Duret-Lutz 2020-06-09 00:14:36 +02:00
  • 1a8920d9b6 rpm: fixes commit 3acf2ca6 Etienne Renault 2020-06-05 12:52:35 +02:00
  • b4412482c8 HACKING: swig-python is required for MacOS Etienne Renault 2020-06-04 17:26:58 +02:00
  • 3acf2ca689 rpm: add unpackaged files Etienne Renault 2020-06-04 14:09:54 +02:00
  • c20abb5a0f debian: remove useless directive Etienne Renault 2020-06-04 06:45:38 +02:00
  • 330cd80fed twacube: fix typo Etienne Renault 2020-05-26 12:05:04 +02:00
  • c06085a60b are_equivalent: remove redundant code Etienne Renault 2020-05-22 13:26:23 +02:00
  • ff48c81198 twacube_to_twa: allows use of existing BDD_dict Etienne Renault 2020-05-22 13:13:05 +02:00
  • b1b59d0eae cube: incorrect use of reverse_binder in are_equivalent Etienne Renault 2020-05-22 12:53:12 +02:00
  • e564dd1263 atomic: check if -latomic is required for std::atomic Etienne Renault 2020-05-20 13:43:18 +02:00
  • 6e0e6b923d NEWS: mention cube-based transformations Etienne Renault 2020-05-19 15:31:14 +02:00
  • 61561ee9ac raspbian: add missing library Etienne Renault 2020-05-19 11:49:24 +02:00
  • 9a8745fcff tests: ignore thread affinity Etienne Renault 2020-05-19 10:24:19 +02:00
  • 7c9ae3d361 tests: add missing library Etienne Renault 2020-05-19 08:00:13 +02:00
  • 2a41772ff9 mc: remove old FIXME Etienne Renault 2020-05-19 07:59:33 +02:00
  • 1dc6ead1e0 mc: do not mix static and SPOT_API Etienne Renault 2020-05-19 07:58:48 +02:00
  • 6d390a342d kripke: add missing SPOT_API Etienne Renault 2020-05-15 14:45:47 +02:00
  • e484e0c471 mc: concept-like check for mc_algorithms Etienne Renault 2020-05-15 14:44:59 +02:00
  • 85ff53c45e twacube: fix erroneous translation Etienne Renault 2020-05-07 14:07:27 +02:00
  • 89675a2762 twacube_algos: add support for are_equivalent Etienne Renault 2020-05-07 13:46:32 +02:00
  • 92845612a1 sanity: please 80 columns Etienne Renault 2020-05-14 17:22:22 +02:00
  • 227627c739 mc: correct SPOT_API Etienne Renault 2020-05-14 16:41:13 +02:00
  • 070dc4880a modelcheck: more relevant information for --csv Etienne Renault 2020-05-14 16:00:53 +02:00
  • bdb95dcde9 mc: keep information about the finisher Etienne Renault 2020-05-14 15:58:30 +02:00
  • cb8eb7e9b2 check: update with new modelcheck options/output Etienne Renault 2020-05-14 14:37:52 +02:00
  • ff57f59dba modelcheck: add missing --kripke option Etienne Renault 2020-05-14 14:12:47 +02:00
  • a3df930a60 mc: please include.test Etienne Renault 2020-05-14 14:00:34 +02:00
  • 17579ad9ad mc: rework and test conversion into twa Etienne Renault 2020-05-14 13:22:23 +02:00
  • 568fcdfc9a mc: rework product_to_twa Etienne Renault 2020-05-13 14:02:58 +02:00
  • 369a8b8b14 mc: merge deadlock and reachabilty algorithms Etienne Renault 2020-05-13 13:51:09 +02:00
  • 1736a7364c modelcheck: formula can be nullptr Etienne Renault 2020-05-13 13:28:11 +02:00
  • c19163cced cube: rename get_ap into ap Etienne Renault 2020-05-13 13:04:54 +02:00
  • 2d59a5c752 mc: clarify method name Etienne Renault 2020-05-13 11:51:10 +02:00
  • ee01fdf209 mc: rename ec_renault13lpar into lpar13 Etienne Renault 2020-05-13 11:13:17 +02:00
  • b32e451292 kripke: please style.test Etienne Renault 2020-05-13 11:10:58 +02:00
  • 5bb29d646b mc: refactor parallel algorithms Etienne Renault 2020-05-13 11:06:38 +02:00
  • 907a3cfbbf twacube: check nullptr during conversion Etienne Renault 2020-05-12 13:59:46 +02:00
  • 53ea1131e6 Fixup: missing dependency bloemen Etienne Renault 2019-11-07 15:02:12 +08:00
  • fcf6bb3d3d twacube: mark get_initial method as const Antoine Martin 2020-04-18 20:59:49 +02:00
  • 0ad380ef12 twacube: mark succ() as const Antoine Martin 2020-03-22 23:19:52 +01:00
  • a14f63dd25 twacube: add num_states and num_edges Antoine Martin 2020-02-19 23:00:44 +01:00
  • 49a3cf1148 twacube: mark get_ap method as const Antoine Martin 2020-03-10 18:28:08 +01:00
  • f8448fad89 kripkecube: modernize is_a_kripkecube_ptr Etienne Renault 2019-06-11 14:06:43 +02:00
  • b52e941b04 ltsmin: prefer '\n' for std::cerr Etienne Renault 2019-10-21 15:33:11 +02:00
  • 87afcd2f87 twacube: fix bug in swarming for large formulae Etienne Renault 2019-07-25 15:48:08 +02:00
  • 276892229c mc: implement CNDFS Antoine Martin 2018-07-09 17:05:12 +02:00
  • 298e6f2b47 mc: bloemen emptiness check Antoine Martin 2018-08-08 18:19:16 +02:00
  • 949881935a ltsmin: rework spins_interface Etienne Renault 2019-02-19 10:40:02 +01:00
  • 7a8a4f4d77 ltdl: should not appear in public headers Etienne Renault 2019-02-18 14:08:36 +01:00
  • 35f1423e20 prefer -pthread to -lpthread Etienne Renault 2018-12-03 14:47:09 +00:00
  • 2b9471b9a7 please gcc snapshot Etienne Renault 2018-11-29 16:14:42 +00:00
  • eb4e3f8be9 modelcheck: fix erroneous report in deadlock Etienne Renault 2018-11-29 16:14:12 +00:00
  • ec5e42a8ef mc: fix deadlock according to new bricks Etienne Renault 2018-11-28 15:08:07 +01:00
  • fd28cb5e49 bricks: update excluding C++17 features Etienne Renault 2018-11-28 14:12:51 +01:00
  • 9f372d78de twacube: use default/deleted Etienne Renault 2018-11-05 16:04:30 +01:00
  • b9ac017382 spins_kripke: rewrite, clean and document Etienne Renault 2018-10-26 16:55:33 +02:00
  • 7aa2d292cf ltsmin: remove useless code Etienne Renault 2018-10-25 16:30:57 +02:00
  • d1200cb579 swarming: bug fix Etienne Renault 2018-07-16 07:14:58 +00:00
  • 69457e957b misc: add clz wrapper for builtin Etienne Renault 2018-07-13 09:15:38 +00:00
  • 01cceef29a bricks: move into spot directory Etienne Renault 2018-07-12 09:42:12 +00:00
  • b115d2f9b1 fixpool: remove useless clz encapsulation Etienne Renault 2018-07-11 16:45:16 +00:00
  • 4871635159 bloemen: fix memory leaks Etienne Renault 2018-07-11 15:09:17 +00:00
  • 2dd2d44907 deadlock: fix memory leak Etienne Renault 2018-07-11 14:29:44 +00:00
  • 23edf52dd5 fixpool: propose alternative policy Etienne Renault 2018-07-11 14:28:34 +00:00
  • fe1be20f09 twacube: fix dot output in tests Etienne Renault 2018-07-04 14:01:55 +02:00
  • 5062d1c2fa modelcheck: conversions now report about the options Etienne Renault 2018-07-04 11:19:23 +02:00
  • 5d30286dd6 twacube: 'mark_t' is deprecated Etienne Renault 2018-07-04 11:14:27 +02:00
  • 73ccf2216d bloemen: avoid tail-recursive calls Etienne Renault 2018-03-28 16:31:05 +02:00
  • ae101a509f bloemen: PPOPP'16 is buggy Etienne Renault 2018-03-28 16:21:39 +02:00
  • 9827b1d096 modelcheck: capture exceptions by const reference Etienne Renault 2018-03-28 10:44:26 +02:00
  • 88dc500aa7 tests: fix call to print_dot according to default arguments Etienne Renault 2018-03-15 10:23:17 +01:00
  • a9178fbe64 modelcheck: update output and documentation Etienne Renault 2018-03-14 16:31:16 +01:00
  • 2bd08d956a mc: please Werror=noexcept Etienne Renault 2018-03-14 15:14:10 +01:00
  • 011115cb1d tests: include missing config.h Etienne Renault 2018-03-08 08:18:52 +01:00
  • fe694e2ba2 debian: fix corrupted profile info Etienne Renault 2018-02-20 17:05:22 +01:00
  • 34b9e89f5d tests: please modelcheck interface Etienne Renault 2018-02-20 15:53:18 +01:00
  • f777e96890 mc: recycle iterators in bloemen Etienne Renault 2017-11-22 09:54:56 +01:00
  • f397def03e tests: add tests for parallel algorithms Etienne Renault 2017-11-22 09:49:30 +01:00
  • 63a4b4085a mc: bloemen count unique states Etienne Renault 2017-11-21 13:39:12 +01:00
  • 80746e4332 modelcheck: update tests Etienne Renault 2017-11-20 16:19:33 +01:00
  • 0b917af762 mc: please sanity.test Etienne Renault 2017-11-20 13:30:06 +01:00
  • e6e3b568ca mc: parallel version of bloemen Etienne Renault 2017-11-14 14:31:32 +01:00
  • 01093f992e mc: sequential version of Bloemen Etienne Renault 2017-11-03 14:18:08 +01:00
  • 15e72e90cc mc: add swarmed deadlock-detection Etienne Renault 2017-10-02 11:57:05 +02:00
  • f486dab241 ltsmin: move modelchek in mc directory Etienne Renault 2017-09-29 15:18:50 +02:00
  • 1d4cb26235 ltsmin: remove shared table at model level Etienne Renault 2017-09-29 14:10:45 +02:00
  • d2549334f9 modelcheck: please gcc catch-value errors Etienne Renault 2017-09-28 14:28:10 +02:00
  • a147fd65dc tests: add pthread library Etienne Renault 2017-09-28 13:39:33 +02:00
  • f9b0044623 ltsmin: please private.test Etienne Renault 2017-09-28 09:20:15 +02:00
  • 32b79818dc kripke: avoir internal compiler error Etienne Renault 2017-09-27 17:11:23 +02:00
  • 7bac705e83 twacube: please gcc null-dereference Etienne Renault 2017-09-27 09:06:41 +02:00
  • b8258ac638 twacube: move useless unsigned int to unsigned Etienne Renault 2017-09-26 17:54:07 +02:00
  • cb343ff02d twacube: more documentation Etienne Renault 2017-09-26 17:50:53 +02:00