Commit graph

  • b8aae428e5 org: add missing documentation for prop_complete Alexandre Duret-Lutz 2018-07-10 17:28:43 +02:00
  • 8d475780d2 * HACKING: typos Antoine Martin 2018-07-09 11:13:16 +02:00
  • 8edd064859 * doc/tl/tl.tex: Convert to utf-8. Alexandre Duret-Lutz 2018-07-05 22:19:15 +02:00
  • 23722c031f contains: fix the semantics Alexandre Duret-Lutz 2018-08-01 17:17:25 +02:00
  • 4ce0d92896 tl: add some implication-based rewritings for "<->", "->", and "xor" Alexandre Duret-Lutz 2018-08-01 15:00:45 +02:00
  • a0005cd3c9 * spot/twa/acc.hh: fix constness Maximilien Colange 2018-07-28 16:46:41 +02:00
  • 8d5d453efa ltlsynt: new algorithm, based on LAR Maximilien Colange 2018-07-24 01:01:11 +02:00
  • bd75ab5b39 ltlsynt: rework synthesis algorithms Maximilien Colange 2018-05-04 18:12:47 +02:00
  • 516e9536df LAR made smarter with symmetry-based degeneralization Maximilien Colange 2018-07-25 18:49:01 +02:00
  • 3303b86a89 ltl-split: translate any "safety" with "rest" Alexandre Duret-Lutz 2018-07-26 18:15:19 +02:00
  • a14f96813d * spot/twaalgos/translate.cc: Typos in comments. Alexandre Duret-Lutz 2018-07-26 17:02:52 +02:00
  • 469d2b4ef4 genem: fix removal of unsatisfied Fin(x) sets Alexandre Duret-Lutz 2018-07-26 15:14:28 +02:00
  • 9f81df2cd4 scc_info: fix split_on_sets Alexandre Duret-Lutz 2018-07-26 14:04:52 +02:00
  • b52f4ea711 * .gitlab-ci.yml (debpkg-stable): Typo. Alexandre Duret-Lutz 2018-07-24 16:53:30 +02:00
  • 4b8910d3f9 ltlfilt: introduce --suspendable Alexandre Duret-Lutz 2018-07-24 14:52:14 +02:00
  • 465536d1fe translate any automaton to a parity automaton Maximilien Colange 2018-07-23 10:59:38 +02:00
  • da996ecbaf use the generic emptiness check Alexandre Duret-Lutz 2018-07-24 10:54:36 +02:00
  • 86b6506268 * spot/twa/twa.cc: Typo. Alexandre Duret-Lutz 2018-07-24 09:50:31 +02:00
  • d708174cfe genem: implement a generic emptiness check for twa_graph_ptr Alexandre Duret-Lutz 2017-04-04 13:55:54 +02:00
  • 74dfd73aae HACKING: directory has moved Etienne Renault 2018-07-20 16:56:19 +02:00
  • 8aeadb5966 remove duplicated includes Etienne Renault 2018-07-20 16:21:01 +02:00
  • a1877ab4e1 remove useless forward declaration Etienne Renault 2018-07-20 15:55:27 +02:00
  • d08193508e modernize std::string("foo") into "foo"s Alexandre Duret-Lutz 2018-07-19 11:02:47 +02:00
  • 832ee81f75 escape_rfc4180: document relation with std::quote Alexandre Duret-Lutz 2018-07-18 17:39:02 +02:00
  • 6875284f94 fix two issues related to jupyter notebook execution Alexandre Duret-Lutz 2018-07-11 15:43:01 +02:00
  • d941b9e176 org: add missing documentation for prop_complete Alexandre Duret-Lutz 2018-07-10 17:28:43 +02:00
  • 46590af693 more documentation for twa_graph internals Alexandre Duret-Lutz 2018-07-10 17:17:59 +02:00
  • d8bc50dcb7 * HACKING: typos Antoine Martin 2018-07-09 11:13:16 +02:00
  • 9b8af36527 * doc/tl/tl.tex: Convert to utf-8. Alexandre Duret-Lutz 2018-07-05 22:19:15 +02:00
  • e7aa334a71 tl: add support for X[n], F[n:m] and G[n:m] Alexandre Duret-Lutz 2018-07-05 17:29:25 +02:00
  • 2616ea7c80 org: do not define the viewport twice Alexandre Duret-Lutz 2018-07-05 13:54:21 +02:00
  • db19141f7a Bump version to 2.6.0.dev Alexandre Duret-Lutz 2018-07-04 17:11:24 +02:00
  • 215b0dcbf0 Release Spot 2.6 Alexandre Duret-Lutz 2018-07-04 17:07:09 +02:00
  • 70b212d8b8 org: add instructions for install RPM packages Alexandre Duret-Lutz 2018-07-04 14:27:57 +02:00
  • 0a9c1d3347 * spot.spec.in: Use --disable-devel --enable-optimizations. Alexandre Duret-Lutz 2018-07-04 14:21:31 +02:00
  • 0d2b8aacd1 Fix GITPATCH computation Alexandre Duret-Lutz 2018-07-04 09:50:07 +02:00
  • 0411099506 trival: prefer a global operator== relying on implicit conversion Alexandre Duret-Lutz 2018-07-03 23:28:41 +02:00
  • 43d426aaae complement: improve code coverage Antoine Martin 2018-07-02 18:36:56 +02:00
  • 4ca38d225a * spot/twaalgos/product.hh: Typos in comments. Clément Gillard 2018-04-11 16:49:45 +02:00
  • b9482a5bcc * .gitlab-ci.yml: Typo. Alexandre Duret-Lutz 2018-07-02 16:44:34 +02:00
  • 34ffc1fa1f isdet: fix documentation error Antoine Martin 2018-07-02 16:37:55 +02:00
  • c717b58827 implement NCSB complementation Antoine Martin 2018-06-05 15:11:47 +02:00
  • 8d233692b2 gitlab-ci: publish the RPM packages Alexandre Duret-Lutz 2018-07-02 14:27:27 +02:00
  • 3a03144754 * AUTHORS: Add Antoine. Alexandre Duret-Lutz 2018-07-01 16:37:53 +02:00
  • e48c6c40d0 ltl-split: deal with suspendable formulas that are false Alexandre Duret-Lutz 2018-06-30 20:39:30 +02:00
  • d82419de1a * NEWS: Adjust for the release of Owl 18.06. Alexandre Duret-Lutz 2018-06-30 17:19:58 +02:00
  • c1b7497f84 gfguarantee: fix selection of moved init state Alexandre Duret-Lutz 2018-06-30 16:38:56 +02:00
  • 04d05104fa bin: conform to GNU Coding Standards for --version Alexandre Duret-Lutz 2018-06-29 20:53:46 +02:00
  • 4e8b35d7ca twa: introduce exclusive_word() and exclusive_run() Alexandre Duret-Lutz 2018-06-29 20:50:19 +02:00
  • 3c12015181 build rpm package during ci Antoine Martin 2018-06-26 16:19:31 +02:00
  • f5f5daec9a translate: enable a restricted form of ltl-split for TGBA/BA Alexandre Duret-Lutz 2018-06-28 23:02:26 +02:00
  • 4235b007f3 org: clarify that ltl2tgba does not only output TGBA Alexandre Duret-Lutz 2018-06-27 16:49:31 +02:00
  • 90e8cb9d2d * NEWS: Fix typos reported by Fanda. Alexandre Duret-Lutz 2018-06-27 15:52:57 +02:00
  • 2402d721a9 modernize the logo Alexandre Duret-Lutz 2018-06-27 15:16:48 +02:00
  • dd973d120e doc: download plantuml.jar from lrde.epita.fr Alexandre Duret-Lutz 2018-06-26 14:24:22 +02:00
  • 5f46becc01 * NEWS: Include a comparison with ltl3tela 1.1.2. Alexandre Duret-Lutz 2018-06-26 10:29:42 +02:00
  • 64df179bff org: update hierarchy examples Alexandre Duret-Lutz 2018-06-25 20:45:13 +02:00
  • 0a8c6479b7 translate: extract obligations terms when translating LTL to Parity Alexandre Duret-Lutz 2018-06-25 15:36:05 +02:00
  • 0690a547a5 * NEWS: Update the micro benchmarks. Alexandre Duret-Lutz 2018-06-22 17:42:37 +02:00
  • a325de8678 postproc: simplify the acceptance condition Alexandre Duret-Lutz 2018-06-22 17:09:18 +02:00
  • 4532c0c13c python: install everythin into pyexecdir Alexandre Duret-Lutz 2018-06-22 10:57:27 +02:00
  • 621fb818e3 improve translation of ms-phi-h=2..3 Alexandre Duret-Lutz 2018-06-20 17:46:11 +02:00
  • c9131aee72 add a pool allocator for STL containers Maximilien Colange 2017-10-19 14:14:49 +02:00
  • 3fe74f1cb9 make valgrind understand our memory pools Maximilien Colange 2016-12-03 11:44:14 +01:00
  • b7e77743db org: fix lists of escape sequences Alexandre Duret-Lutz 2018-06-19 22:03:48 +02:00
  • 4815a361de translate: add ltl-split option Alexandre Duret-Lutz 2018-06-19 16:42:30 +02:00
  • 4f2e9512a2 product_susp: new function Alexandre Duret-Lutz 2018-06-14 10:32:59 +02:00
  • a4a8ae9a20 don't use tabs for indentation Antoine Martin 2018-06-15 14:34:33 +02:00
  • 1183a935c7 fix a bug in aiger printer Maximilien Colange 2018-06-07 15:11:16 +02:00
  • 9489a65bc6 ltlsynt: more deterministic behavior Maximilien Colange 2018-06-14 11:02:18 +02:00
  • 653deaa934 fix typo in dir-locals Antoine Martin 2018-06-14 13:39:03 +02:00
  • f2128360a7 update ltlsynt documentation Maximilien Colange 2018-06-13 14:27:48 +02:00
  • fbc372e292 scc_filter: add quick test for very-weak Alexandre Duret-Lutz 2018-06-11 20:24:17 +02:00
  • 729921c0a0 ltl2tgba_fm: mark persistence formulas as weak automata Alexandre Duret-Lutz 2018-06-11 16:14:58 +02:00
  • 95d732e331 specialize scc_filter for inherently_weak automata Alexandre Duret-Lutz 2018-06-11 15:01:49 +02:00
  • 2fad1ff6de * NEWS: Reorder and fix some typos. Alexandre Duret-Lutz 2018-06-08 17:40:36 +02:00
  • 1341c656be genltl: add --gf-equiv-xn, --gf-implies-xn Alexandre Duret-Lutz 2018-06-08 15:51:11 +02:00
  • 7e9325866f gf_guarantee_to_ba: save states using histories Alexandre Duret-Lutz 2018-06-08 15:09:10 +02:00
  • 730c6bbca2 minimize_wdba: use a product to decide accepting SCCs Alexandre Duret-Lutz 2018-06-05 17:42:44 +02:00
  • 4afd1856a6 * .gitlab-ci.yml (debian-gcc-snapshot): Fix path to log files. Alexandre Duret-Lutz 2018-06-05 00:56:03 +02:00
  • ca1c67a73d simplifier: add two new rules Alexandre Duret-Lutz 2018-06-04 13:49:40 +02:00
  • 8e3b982985 * NEWS: Reorganize recent entries. Alexandre Duret-Lutz 2018-06-03 21:01:43 +02:00
  • c535871ffd genltl: --ms-example now has two arguments Alexandre Duret-Lutz 2018-06-03 19:35:02 +02:00
  • 2e50f9e986 autfilt: implement --has-univ-branching and --has-exist-branching Alexandre Duret-Lutz 2018-06-03 19:21:15 +02:00
  • 939f63eec9 genltl: add support for --sejk-f=n,m Alexandre Duret-Lutz 2018-06-03 18:17:48 +02:00
  • c76df95c69 genltl: three new families --sejk-{j,k,patterns} Alexandre Duret-Lutz 2018-06-03 14:38:04 +02:00
  • e87d308eba improve alternation removal to match G&O construction Alexandre Duret-Lutz 2018-05-30 10:01:52 +02:00
  • 6d9d35c985 acc: turn some assertions into exceptions Alexandre Duret-Lutz 2018-05-26 09:44:18 +02:00
  • be0997c97a fix a9293f329 Alexandre Duret-Lutz 2018-05-25 17:47:58 +02:00
  • b12eb0508f fix and check shifting issue Alexandre Duret-Lutz 2018-05-25 11:29:59 +02:00
  • 23e0d718fd * tests/python/except.py: Make sure exceptions are raised. Alexandre Duret-Lutz 2018-05-25 11:16:05 +02:00
  • a9293f329e fix warnings when compiling without assertions Maximilien Colange 2018-05-25 14:09:47 +02:00
  • e886609269 optimize split_2step Maximilien Colange 2018-05-07 15:57:23 +02:00
  • 5a819e0c93 twa_graph: add a method to merge states with same outgoing edges Maximilien Colange 2018-05-25 10:26:03 +02:00
  • 5b9088006c a few improvements to mark_t Maximilien Colange 2018-05-25 11:42:29 +02:00
  • 88a6bd82a3 document --enable-max-accsets Alexandre Duret-Lutz 2018-05-24 17:53:37 +02:00
  • 2e165f188d rename SPOT_NB_ACC to SPOT_MAX_ACCSETS Alexandre Duret-Lutz 2018-05-24 17:52:42 +02:00
  • cc2c4615d0 bitset: optimize the code generated by shifts in common cases Alexandre Duret-Lutz 2018-05-24 17:20:16 +02:00
  • e979791071 common: typo Alexandre Duret-Lutz 2018-05-24 17:19:00 +02:00
  • b17a9f8578 * tests/sanity/style.test: Allow {{x}} in constructors. Alexandre Duret-Lutz 2018-05-24 18:02:59 +02:00