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

Commit graph

  • fbf9d98e15 Fix typo Etienne Renault 2017-09-26 14:40:10 +02:00
  • d95428d245 ltsmin: remove ltdl from public headers Etienne Renault 2017-04-18 17:28:43 +02:00
  • d3b143574b bricks: please gcc error=noexcept option Etienne Renault 2017-03-17 13:49:41 +01:00
  • 1fc3d7f935 bricks: gcc-7 doesn't align variables up to a maximum of 16 bytes Etienne Renault 2017-03-17 13:34:42 +01:00
  • ad005121ae bricks: please gcc-4.8 for auto specifier Etienne Renault 2017-03-17 10:46:39 +01:00
  • 941608060e ltsmin: fix call to destructor Etienne Renault 2017-03-16 17:00:15 +01:00
  • 3c868c228b ltsmin: do not take iterators by copy Etienne Renault 2017-03-16 16:57:54 +01:00
  • df872ce6d9 ltsmin: placement new requires placement delete Etienne Renault 2017-03-16 16:54:32 +01:00
  • 47c4f19e22 bricks: please gcc Werror=noexcept option Etienne Renault 2017-03-16 12:03:53 +01:00
  • 44041efc51 bricks: please gcc Wmacro-redefined option Etienne Renault 2017-03-15 17:22:17 +01:00
  • 7ae7e2e831 includes: must not check *.hxx Etienne Renault 2017-03-16 10:14:39 +01:00
  • 0be3630218 ltsmin: extract kripkecube to ease manipulation Etienne Renault 2017-03-15 17:16:28 +01:00
  • 5445007070 ltsmin: extract spins interface Etienne Renault 2017-03-15 16:21:33 +01:00
  • 8a930c7572 ltsmin: simplify iterator Etienne Renault 2017-03-15 16:01:00 +01:00
  • ac54acbb9d brick: please gcc pedantic option Etienne Renault 2017-03-15 15:15:33 +01:00
  • 03ff789324 mark_t::operator bool() is now explicit Etienne Renault 2017-03-15 09:32:12 +01:00
  • 6d282bbc6b ltsmin: update usage of brick-hashset Etienne Renault 2017-03-15 08:44:29 +01:00
  • 1a37a08ba4 bricks: update Etienne Renault 2017-03-14 17:01:32 +01:00
  • 8ced74f8e6 bricks: please pedantic option for gcc Etienne Renault 2017-03-03 08:41:32 +01:00
  • 606e4fc88c please pedantic option for gcc Etienne Renault 2017-03-03 06:37:34 +01:00
  • a308d1a60a bricks: add support for gcc prior to 4.9 Etienne Renault 2016-12-06 15:35:51 +01:00
  • 6c5c308ea8 bricks: adapt with the new bricks Etienne Renault 2016-12-03 17:43:23 +01:00
  • bb9fa4e910 bricks: update and move to c++14 Etienne Renault 2016-12-01 18:56:33 +01:00
  • 9208726d97 reachability: improve support for callbacks Etienne Renault 2016-11-23 11:11:19 +01:00
  • 72948661e9 swarming: add support everywhere Etienne Renault 2016-10-27 12:03:14 +02:00
  • ae1a3601e6 bricks: propagate use of SPOT_FALLTHROUGH Etienne Renault 2016-10-26 08:52:23 +02:00
  • fb4ef40d11 Use SPOT_ASSERT() instead of assert() in public headers Etienne Renault 2016-09-29 15:59:29 +02:00
  • c515ee92e2 bricks: add missing override Etienne Renault 2016-09-29 15:26:42 +02:00
  • 50d888adf8 Twacube must share the order of atomic propositions Etienne Renault 2016-09-28 16:31:01 +02:00
  • a1787dd1ce modelcheck: support for csv extraction Etienne Renault 2016-05-04 10:57:25 +02:00
  • 9a9a237272 timer: support for walltime Etienne Renault 2016-05-04 10:56:21 +02:00
  • 765bb8a7c4 Promote use of shared_ptr Etienne Renault 2016-04-25 15:36:26 +02:00
  • 7d2abe229b swig: prefer typedef to using Etienne Renault 2016-04-22 21:32:14 +02:00
  • 9799f2884e modelcheck: support for twacube Etienne Renault 2016-04-21 13:38:39 +02:00
  • 94f7c58f44 intersect: statistic provided using an object Etienne Renault 2016-04-22 15:27:36 +02:00
  • d430129bb1 convert: simplify interfaces Etienne Renault 2016-04-20 14:22:21 +02:00
  • e11f24dbc1 twacube: atomic propositions are now passed by copy Etienne Renault 2016-04-20 14:05:04 +02:00
  • 6d3154be94 bricks: ATOMIC_FLAG_INIT initialization Etienne Renault 2016-04-11 15:48:18 +02:00
  • f04074bd6d sanity: replace tabulars by spaces Etienne Renault 2016-04-11 14:20:34 +02:00
  • 681c2b2011 ltsmin: use FastConcurrent map Etienne Renault 2016-04-11 13:02:40 +02:00
  • 01f66642f1 bricks: fix clang warnings Etienne Renault 2016-03-15 17:18:33 +01:00
  • 458f506336 bricks: add bricks for concurrent hashmap Etienne Renault 2016-03-15 15:41:28 +01:00
  • 4337abc5a6 modelcheck: rewrite and use argp Etienne Renault 2016-03-10 13:27:42 +01:00
  • b4bbf50794 ltsmin: prodcuce kripkecube Etienne Renault 2016-03-10 13:27:24 +01:00
  • 8e593611f6 convert: kripke and product towards twa Etienne Renault 2016-01-12 09:58:39 +01:00
  • 3bafe693ef ec: Renault et al LPAR'13 emptiness check Etienne Renault 2016-03-17 16:23:28 +01:00
  • 87de88c80c intersection: for kripke and twacube Etienne Renault 2015-11-30 15:26:42 +01:00
  • 94492ffa14 reachability: sequential reachability for kripkecube Etienne Renault 2015-11-25 14:44:07 +01:00
  • 748068a6d0 kripke: define kripkecube structure Etienne Renault 2015-10-19 16:06:27 +02:00
  • b87693bcc3 convert: twacube to twa translation Etienne Renault 2015-12-05 07:58:27 +01:00
  • aceb37ab50 convert: twa to twacube translation Etienne Renault 2015-10-02 16:33:27 +02:00
  • 8d57700d6a convert: BDD to cube conversions Etienne Renault 2015-11-30 15:32:51 +01:00
  • 7c3fdd6b97 Introduce cube data structure Etienne Renault 2015-11-30 15:31:17 +01:00
  • b7abe6f4b4 ltldo: improve error messages Alexandre Duret-Lutz 2020-05-31 16:19:51 +02:00
  • 8e9e706003 * tests/sanity/80columns.test: Force LC_ALL. Alexandre Duret-Lutz 2020-05-30 14:28:50 +02:00
  • d76236a03f sccinfo: fix doc Alexandre Duret-Lutz 2020-05-29 17:14:17 +02:00
  • 9150a2e54b twa: get rid of set_num_sets_() Alexandre Duret-Lutz 2020-05-25 10:51:44 +02:00
  • f6cf8e4d8a ltlsynt: use wdba-minimize=2 and ba-simul=0 Alexandre Duret-Lutz 2020-05-24 20:32:27 +02:00
  • 0413ecfbb8 ltlsynt: Change default options Florian Renkin 2020-05-23 14:31:59 +02:00
  • 494471a50b ltlsynt: Add more elements in csv Florian Renkin 2020-05-23 14:29:48 +02:00
  • 3fd5f38248 ltlsynt: Add -x option for translation Florian Renkin 2020-05-23 14:13:33 +02:00
  • 1752b18f14 work around diagnostic changes in Bison 3.6 Alexandre Duret-Lutz 2020-05-24 14:05:46 +02:00
  • a395309f4b ltlsynt: add --algo=ps Alexandre Duret-Lutz 2020-05-24 09:45:35 +02:00
  • 49188715cd simplify_acc: perform unit-propagation earlier Alexandre Duret-Lutz 2020-05-23 12:00:56 +02:00
  • 6074202b9b remfin: do not clone transitions that are accepting in main Alexandre Duret-Lutz 2020-05-23 11:56:16 +02:00
  • 260a141b1c improve fuse_marks_here by detecting more patterns Alexandre Duret-Lutz 2020-05-22 16:09:26 +02:00
  • 645935f796 fixpool: allocate a new chunk on creation Alexandre Duret-Lutz 2020-05-22 15:33:40 +02:00
  • a0767e3c1e postproc: option to wdba-minimize only when sure Alexandre Duret-Lutz 2020-05-21 15:42:05 +02:00
  • 579ff63817 * doc/org/satmin.org: Remove extra newlines (fixes #410). Alexandre Duret-Lutz 2020-05-18 17:08:40 +02:00
  • 208d0f7885 stats: speed up the computation of transitions Alexandre Duret-Lutz 2020-05-18 16:52:31 +02:00
  • da96a509e9 [buddy] avoid cache errors in bdd_satcount() and friends Alexandre Duret-Lutz 2020-05-18 19:25:14 +02:00
  • 66aa6d0883 ltlsynt: make sure the previous Xor optimization actually works Alexandre Duret-Lutz 2020-05-16 19:22:28 +02:00
  • 6bfa9793d6 translate: improve handling of Xor and Equiv at top-level for -G -D Alexandre Duret-Lutz 2020-05-16 18:03:38 +02:00
  • 3ab2dd17a7 product: add product_xor() and product_xnor() Alexandre Duret-Lutz 2020-05-16 16:20:39 +02:00
  • a78137f9d4 * NEWS, configure.ac: Bump version to 2.9.0.dev. Alexandre Duret-Lutz 2020-04-30 09:03:48 +02:00
  • eeb5713a30 release Spot 2.9 Alexandre Duret-Lutz 2020-04-30 09:00:35 +02:00
  • ce2529b27b * doc/org/oaut.org: Refresh some examples; remove unecessary output. Alexandre Duret-Lutz 2020-04-30 08:44:23 +02:00
  • 118df55bc3 [buddy] workaround newer clang warning Alexandre Duret-Lutz 2020-04-29 23:04:51 +02:00
  • 82d69241f1 ltlsynt: add a --csv=FILENAME option Alexandre Duret-Lutz 2020-04-29 22:44:25 +02:00
  • a7051b32c8 dot: fix #393 Alexandre Duret-Lutz 2020-04-29 21:14:36 +02:00
  • 3ea63e9a75 dot: fix #392 Alexandre Duret-Lutz 2020-04-29 10:48:05 +02:00
  • 6706042019 postproc: fix issue #402 Alexandre Duret-Lutz 2020-04-25 19:59:11 +02:00
  • fe340ae8db ltlsynt: fix lar.old implementation Alexandre Duret-Lutz 2020-04-25 16:29:03 +02:00
  • a6da6ed95a ltlsynt: add option to call to_parity_old Alexandre Duret-Lutz 2020-04-20 14:48:23 +02:00
  • 192ca91087 * .gitlab-ci.yml (raspbian): Add /wip/ exception. Alexandre Duret-Lutz 2020-04-19 14:35:51 +02:00
  • cc12d514be avoid mark_t::count() when possible Alexandre Duret-Lutz 2020-04-18 23:23:44 +02:00
  • c0e1b3e52a cleanacc: keep acceptance order when removing complementary colors Alexandre Duret-Lutz 2020-04-18 22:05:43 +02:00
  • 262b24e6d7 unit_propagation: Correct result when multiple colors are possible Florian Renkin 2020-04-18 19:29:41 +02:00
  • 100fe3f00c to_parity: Correct the colors when we have parity pref. + true_clean Florian Renkin 2020-04-18 18:56:56 +02:00
  • ed5cccba8a python: fix to_parity default option handling Alexandre Duret-Lutz 2020-04-18 00:30:25 +02:00
  • fd0d752bc3 to_parity: only call reduce_parity() when prefix_parity is enabled Alexandre Duret-Lutz 2020-04-17 15:20:53 +02:00
  • 102ef04364 simplify_acc: loop over the simplifications Alexandre Duret-Lutz 2020-04-16 22:53:09 +02:00
  • b62e1bb13c simplify_acc: fix an infinite loop Alexandre Duret-Lutz 2020-04-16 22:40:49 +02:00
  • 68012e6a85 to_parity: Correct the expected number of states Florian Renkin 2020-04-17 16:47:02 +02:00
  • 685d6d8ba0 to_parity: Add an option to force degeneralization Florian Renkin 2020-04-17 14:23:59 +02:00
  • 527b62c5ff to_parity: Remove merge_states Florian Renkin 2020-04-17 13:51:58 +02:00
  • 142f1afab2 unit_propagation: Add a test with multiple unit clauses Florian Renkin 2020-04-17 13:38:46 +02:00
  • 927ea7046b unit_propagation: Correct a problem with multiple marks Florian Renkin 2020-04-16 22:08:07 +02:00
  • 8c48003943 to_parity: Use merge_states Florian Renkin 2020-04-15 11:15:27 +02:00
  • 875846f51f toparity: false transitions are not a problem anymore Alexandre Duret-Lutz 2020-04-16 10:54:10 +02:00