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

Commit graph

  • 34646bc0ab allow RPM build failure until we can fix it Alexandre Duret-Lutz 2022-01-14 17:40:55 +01:00
  • 346260c684 org: install from GNU Alexandre Duret-Lutz 2022-01-14 17:38:14 +01:00
  • cdbf830010 * doc/org/tut40.org: Finish a sentence. Alexandre Duret-Lutz 2022-01-14 15:52:52 +01:00
  • 25d6bfd64d bib: more references Alexandre Duret-Lutz 2022-01-14 15:49:23 +01:00
  • 480289867f sccinfo: fix accepting run computation Alexandre Duret-Lutz 2022-01-14 15:46:53 +01:00
  • da681e6b4d dot: improve output to work around GraphViz bug Alexandre Duret-Lutz 2022-01-11 22:19:20 +01:00
  • cfb782ce75 bump copyright year Alexandre Duret-Lutz 2022-01-06 16:41:24 +01:00
  • 2298743479 Fixes #495 philipp 2022-01-07 09:28:11 +01:00
  • 852abc770f complement: fix a regression with 2.9.8 Alexandre Duret-Lutz 2021-12-17 12:05:33 +01:00
  • 80fd158ed5 sbacc: remove spurious initial state in some output Alexandre Duret-Lutz 2021-12-16 17:23:06 +01:00
  • 9d6ba3ff77 * tests/python/word.ipynb: Typo. Alexandre Duret-Lutz 2021-12-16 14:20:12 +01:00
  • b860bb242e tl: fix first_match definition Alexandre Duret-Lutz 2021-12-14 14:18:53 +01:00
  • 6dd7097148 org: update mailman urls Alexandre Duret-Lutz 2021-12-13 10:00:51 +01:00
  • 1bd1129494 Fixing state reorder bug for mealy minimization philipp 2021-12-06 00:02:11 +01:00
  • 3612f3416d * NEWS, configure.ac: Bump version to 2.10.2.dev. Alexandre Duret-Lutz 2021-12-03 08:57:33 +01:00
  • 3bee9aebb2 allow RPM build failure until we can fix it Alexandre Duret-Lutz 2022-01-14 17:40:55 +01:00
  • c44aab4025 org: install from GNU Alexandre Duret-Lutz 2022-01-14 17:38:14 +01:00
  • 8ec945f3ac * doc/org/tut40.org: Finish a sentence. Alexandre Duret-Lutz 2022-01-14 15:52:52 +01:00
  • b2b37ba3e9 bib: more references Alexandre Duret-Lutz 2022-01-14 15:49:23 +01:00
  • fc92c88cdb sccinfo: fix accepting run computation Alexandre Duret-Lutz 2022-01-14 15:46:53 +01:00
  • 890423936f dot: improve output to work around GraphViz bug Alexandre Duret-Lutz 2022-01-11 22:19:20 +01:00
  • 78bcd9c453 bump copyright year Alexandre Duret-Lutz 2022-01-06 16:41:24 +01:00
  • 8c33f959a3 hoa: add support for controllable-AP Alexandre Duret-Lutz 2022-01-03 18:04:29 +01:00
  • 7cefe30d97 Fixes #495 philipp 2022-01-07 09:28:11 +01:00
  • 20bcc216a0 introduce the original-classes named property Alexandre Duret-Lutz 2021-12-17 17:51:06 +01:00
  • d8f245a7de complement: fix a regression with 2.9.8 Alexandre Duret-Lutz 2021-12-17 12:05:33 +01:00
  • c0a43cd92b sbacc: remove spurious initial state in some output Alexandre Duret-Lutz 2021-12-16 17:23:06 +01:00
  • 253dd80b53 * tests/python/word.ipynb: Typo. Alexandre Duret-Lutz 2021-12-16 14:20:12 +01:00
  • e7f0df048a tl: fix first_match definition Alexandre Duret-Lutz 2021-12-14 14:18:53 +01:00
  • 4dc6bb08a2 org: update mailman urls Alexandre Duret-Lutz 2021-12-13 10:00:51 +01:00
  • 4babe8db75 Fixing state reorder bug for mealy minimization philipp 2021-12-06 00:02:11 +01:00
  • 929ffc4176 Adapt ltlsynt Philipp Schlehuber 2021-11-22 17:15:03 +01:00
  • 5b6e2a210a Making solved game to mealy more flexible Philipp Schlehuber 2021-11-22 16:23:03 +01:00
  • 488efee7b3 aiger accepts splitted mealy machines Philipp Schlehuber 2021-11-22 14:14:28 +01:00
  • 88356645b4 * spot/parsetl/scantl.ll: Avoid strtoul for short delays. Alexandre Duret-Lutz 2021-12-06 17:01:22 +01:00
  • 216db3aa10 * NEWS, configure.ac: Bump version to 2.10.2.dev. Alexandre Duret-Lutz 2021-12-03 08:57:33 +01:00
  • 6eabc517ad Release Spot 2.10.2 Alexandre Duret-Lutz 2021-12-03 08:54:57 +01:00
  • 4d2262600e formula: is_literal should be const Alexandre Duret-Lutz 2021-12-02 17:31:47 +01:00
  • 8ffd06e9a6 catch overflow in SVA delays during parsing Alexandre Duret-Lutz 2021-12-02 09:25:59 +01:00
  • 6b46401d36 * doc/org/install.org: Stable Debian packages are for Bullseye. Alexandre Duret-Lutz 2021-11-23 10:21:36 +01:00
  • 81f146f648 build: fix multiple Clang13 warnings Jérôme Dubois 2021-11-20 16:51:26 +01:00
  • 2a408bbed1 sched_getcpu() and pthread_setaffinity_np() are non-portable Alexandre Duret-Lutz 2021-11-22 10:23:14 +01:00
  • 5f49209caf twagraph: remove bddfalse edges in purge_dead_states Alexandre Duret-Lutz 2021-11-19 22:13:20 +01:00
  • 59690dd041 * NEWS, configure.ac: Bump version to 2.10.1.dev. Alexandre Duret-Lutz 2021-11-19 09:48:07 +01:00
  • 1782af3924 Release Spot 2.10.1 Alexandre Duret-Lutz 2021-11-19 09:46:12 +01:00
  • 58b349d3ca sbacc: define original-states Alexandre Duret-Lutz 2021-11-18 13:56:28 +01:00
  • afdd38277d formula: catch min/max overflows at construction Alexandre Duret-Lutz 2021-11-18 11:18:06 +01:00
  • 59b361babd fix some unused variable warning in mingw Alexandre Duret-Lutz 2021-11-17 21:54:39 +01:00
  • 81375d7a93 tl: diagnose repetitions that do not fit in uint_8 Alexandre Duret-Lutz 2021-11-17 17:10:38 +01:00
  • f82d26b625 fix configure --help Alexandre Duret-Lutz 2021-11-17 16:36:46 +01:00
  • 6013023794 tests: add missing dependency on libbddx in ltsmin tests Alexandre Duret-Lutz 2021-11-16 23:26:02 +01:00
  • ce18a7896b Work around issue with inttypes.h macros Alexandre Duret-Lutz 2021-11-16 23:25:13 +01:00
  • 51636bc9e3 ltlsynt.cc: Correct help Florian Renkin 2021-11-15 10:20:25 +01:00
  • 5dfa039a48 * doc/org/compile.org: Fix instructions to uses -std=c++17. Alexandre Duret-Lutz 2021-11-16 09:56:37 +01:00
  • a5f080338c Python 3.5 is now needed Alexandre Duret-Lutz 2021-11-16 09:51:59 +01:00
  • bc063b13f3 * spot/bricks/brick-hash: Add missing include. Alexandre Duret-Lutz 2021-11-16 09:47:42 +01:00
  • 186d206302 ltsmin-pml: work around newer jupyter versions Alexandre Duret-Lutz 2021-11-15 23:37:08 +01:00
  • aeb05f0ff0 * doc/org/index.org: Fix link to zlktree.html. Alexandre Duret-Lutz 2021-11-14 22:17:15 +01:00
  • dd8373e788 * NEWS, configure.ac: Bump version to 2.10.0.dev. Alexandre Duret-Lutz 2021-11-13 11:50:20 +01:00
  • 37de3470b8 Release Spot 2.10 Alexandre Duret-Lutz 2021-11-13 11:47:28 +01:00
  • 0706887e62 * doc/Makefile.am (svgo): preserve the IDs in oaut-dot4.svg. Alexandre Duret-Lutz 2021-11-13 11:42:08 +01:00
  • 8d91aa4267 * doc/org/index.org: Advertise more features. Alexandre Duret-Lutz 2021-11-13 11:08:12 +01:00
  • 9d81e9cf8f * tests/python/split.py: Simplify. Alexandre Duret-Lutz 2021-11-12 22:44:56 +01:00
  • 1443d45ac7 synthesis: minor typos Alexandre Duret-Lutz 2021-11-12 22:44:08 +01:00
  • 6555af1f44 python: fix support for std::vector<const_twa_graph_ptr> Alexandre Duret-Lutz 2021-11-12 22:38:37 +01:00
  • 98ebbea17e Renaming and clean up philipp 2021-11-04 00:24:17 +01:00
  • 6ebe3d7447 Use generic split after obtaining direct strategy philipp 2021-10-24 15:47:40 +02:00
  • 75b89db5ac zlktree: fix colored output of acd_transform_sbacc() Alexandre Duret-Lutz 2021-11-10 15:51:13 +01:00
  • 2f528c7190 * tests/python/streett_totgba.py: Remove superfluous comment. Alexandre Duret-Lutz 2021-11-10 15:28:08 +01:00
  • d4967f20e9 Notebooks: correct typos Florian Renkin 2021-11-04 16:37:12 +01:00
  • c72c285552 * doc/spot.bib: Add entries for multi-core emptiness-checks. Alexandre Duret-Lutz 2021-11-05 17:06:20 +01:00
  • 3c5928d216 tl: fix AST rendering of Star/FStar nodes Alexandre Duret-Lutz 2021-11-05 12:15:40 +01:00
  • 9097eca81d * spot/twaalgos/ltl2tgba_fm.cc: Update some comments. Alexandre Duret-Lutz 2021-11-05 10:45:07 +01:00
  • 540b31dbd7 [buddy] Improve bdd_have_common_assignment philipp 2021-11-05 09:02:05 +01:00
  • c5a61da22b [buddy] Fix is_cube() and add tests philipp 2021-11-04 00:31:51 +01:00
  • ece7631e8c [buddy] fix a spurious failure Alexandre Duret-Lutz 2021-11-04 23:19:31 +01:00
  • 7ade97943b * NEWS: Some cleanup, in preparation for the release. Alexandre Duret-Lutz 2021-11-04 17:37:20 +01:00
  • 5a9c8aad0d [buddy] execute some of the tests during "make check" Alexandre Duret-Lutz 2021-11-04 15:18:59 +01:00
  • f99ddef787 bin: use regexes to detect shorthands, and add support for owl-21.0 Alexandre Duret-Lutz 2021-11-04 14:12:32 +01:00
  • 97046ea263 Synthesis decomposition: Add a new rewriting and tests Florian Renkin 2021-11-04 15:10:07 +01:00
  • 7947ffc930 ltlsynt: correct verbose when --aiger is used Florian Renkin 2021-11-04 10:20:48 +01:00
  • 553381bd6e aiger: improve parse errors and test them Alexandre Duret-Lutz 2021-11-03 23:00:18 +01:00
  • aff04c2207 Aiger parser: correct input and output names Florian Renkin 2021-11-03 12:03:19 +01:00
  • 8aa9da7fc8 Synthesis: rewrite bypass Florian Renkin 2021-10-29 17:03:28 +02:00
  • 3be79ea476 print_dot: improve aiger rendering Alexandre Duret-Lutz 2021-10-29 23:06:45 +02:00
  • 753d572e4d print_dot: improve the rendering of Mealy machines Alexandre Duret-Lutz 2021-10-29 16:45:35 +02:00
  • 09b361712d python: make sure swig also work with --disable-dependency-tracking Alexandre Duret-Lutz 2021-10-29 11:41:09 +02:00
  • 6464324a2c ltlsynt: fix a bug in split_2step_fast_here Alexandre Duret-Lutz 2021-10-24 22:34:06 +02:00
  • 1df5f0e2c7 synthesis: simplify split_2step_fast_here Alexandre Duret-Lutz 2021-10-23 01:23:24 +02:00
  • 074678416f ltlsynt: improve error message in case of missing --ins and --outs Alexandre Duret-Lutz 2021-10-22 17:46:21 +02:00
  • c43712682f synthesis: rename create_game() to ltl_to_game() Alexandre Duret-Lutz 2021-10-18 09:17:40 +02:00
  • 5fd4d94031 ltlsynt: replace some leftover throw by error() Alexandre Duret-Lutz 2021-10-09 21:36:17 +02:00
  • 1eb18f4b83 ltlsynt: fix --help output for common Input options Alexandre Duret-Lutz 2021-10-09 21:28:52 +02:00
  • 82d4fc8ed9 ltlsynt: report AP missing from --ins and --outs Alexandre Duret-Lutz 2021-10-09 21:18:21 +02:00
  • 0e5f2d4819 ltlsynt: --ins is optional but not its argument Alexandre Duret-Lutz 2021-10-09 20:50:38 +02:00
  • b9a39c5576 aiger: fix forcing of input properties Alexandre Duret-Lutz 2021-10-07 11:23:51 +02:00
  • 9b3956f892 zlktree: fix handling of automata with false acceptance Alexandre Duret-Lutz 2021-10-07 11:11:49 +02:00
  • 0ec1ee6de3 move parts of games.ipynb into synthesis.ipynb Alexandre Duret-Lutz 2021-10-07 10:48:02 +02:00
  • 7bc2c31043 game: teach solve_game to use solve_safety_game Alexandre Duret-Lutz 2021-10-07 09:25:01 +02:00
  • bdd20bd1a1 rename game_info to synthesis_info; move it with the synthesis code Alexandre Duret-Lutz 2021-10-06 22:51:10 +02:00