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

Commit graph

  • 75e552fdac python: add bindings for BuDDy's minterms_of Alexandre Duret-Lutz 2024-03-11 17:38:52 +01:00
  • 0d4e93a4ec [buddy] add missing typedefs to minterm_iterator Alexandre Duret-Lutz 2024-03-11 17:38:13 +01:00
  • 1b81ecb80c dualize: should not call cleanup_acceptance_here Alexandre Duret-Lutz 2024-03-06 17:53:23 +01:00
  • 60f046a574 add intersection checks between words and automata Alexandre Duret-Lutz 2024-02-29 16:54:14 +01:00
  • 83cabfa6f9 ltlsynt: fix suggested references Alexandre Duret-Lutz 2024-02-19 11:11:17 +01:00
  • 82311c3e3b ltlsynt: fix the case where AP removal is disabled and decomp fails Alexandre Duret-Lutz 2024-02-17 16:57:31 +01:00
  • 15b876d368 ltlsynt: allow regular expressions in --ins/--outs Alexandre Duret-Lutz 2024-02-17 12:56:28 +01:00
  • 31462d84ba style: relax the else's body check Alexandre Duret-Lutz 2024-02-19 11:41:33 +01:00
  • bcfcea6272 * bin/spot-x.cc: Fix some typos. Alexandre Duret-Lutz 2024-02-16 12:10:14 +01:00
  • eff7966cef sccinfo: fix documentation for split_on_sets Alexandre Duret-Lutz 2024-02-11 22:43:04 +01:00
  • 3034e8fcc3 python: render <svg> via _repr_html_ Alexandre Duret-Lutz 2024-02-09 15:06:07 +01:00
  • 4cf7503fff org: fix many errors Alexandre Duret-Lutz 2024-02-09 12:16:52 +01:00
  • a6f79c6211 more doc handling of prop_universal for fused initial states Alexandre Duret-Lutz 2024-02-08 22:43:44 +01:00
  • a735c2b72d tl_simplifier: add more test cases Alexandre Duret-Lutz 2024-02-06 23:12:55 +01:00
  • ca739ce816 * NEWS: Fix some typos. Alexandre Duret-Lutz 2024-02-06 22:39:07 +01:00
  • db168f97e6 tl: fix detection of goto Alexandre Duret-Lutz 2024-02-06 22:37:34 +01:00
  • 94ab42612a work around some Swig 4.2 change Alexandre Duret-Lutz 2024-02-06 17:28:48 +01:00
  • 342360f8ca fix some preprocessor directive Alexandre Duret-Lutz 2024-02-06 14:11:42 +01:00
  • 27b8e5aa73 postproc: fix default for acd and interaction with colored Alexandre Duret-Lutz 2024-02-06 14:09:42 +01:00
  • dc5a569582 ltlsynt: fix --global-equiv Alexandre Duret-Lutz 2024-01-26 22:31:17 +01:00
  • 690e5a213d remove_alternation: option to return nullptr if too many sets needed Alexandre Duret-Lutz 2024-01-24 16:11:25 +01:00
  • 9957aa1a3a bump copyright to 2024 Alexandre Duret-Lutz 2024-01-13 12:53:54 +01:00
  • 69c8187330 * spot/twaalgos/aiger.cc: Work around gcc snapshot diagnostics. Alexandre Duret-Lutz 2023-12-18 10:04:15 +01:00
  • 55992b1ca2 * spot/bricks/brick-assert: include <cstdint>. Alexandre Duret-Lutz 2023-12-17 21:34:51 +01:00
  • 983964d037 strength: generalize is_safety_automaton to any type of automata Alexandre Duret-Lutz 2023-12-16 00:09:24 +01:00
  • e8c2b27ad2 * spot/tl/hierarchy.cc: Typo in comment. Alexandre Duret-Lutz 2023-12-15 11:31:55 +01:00
  • 3c638f2a88 python: add get_highlight_state and get_highlight_edge Alexandre Duret-Lutz 2023-12-06 16:38:56 +01:00
  • ba86dc6b18 twa: guard against highlighting of non-existing edges and states Alexandre Duret-Lutz 2023-12-04 17:59:09 +01:00
  • 444d4f773d twa: fix issue #555 better Alexandre Duret-Lutz 2023-12-03 22:26:12 +01:00
  • 3d05ecb4ac remove many useless includes Alexandre Duret-Lutz 2023-11-29 16:59:45 +01:00
  • c9d9c10cb2 * HACKING: Mention bear, to build compile_commands.json. Alexandre Duret-Lutz 2023-11-29 16:58:00 +01:00
  • cee2819a45 auts_to_aiger: Fix output name index Florian Renkin 2023-11-29 09:16:01 +00:00
  • 234ba2bb84 work around some gcc 9.4 warnings Alexandre Duret-Lutz 2023-11-28 17:50:28 +01:00
  • 738d62e0b9 hoa: do not output empty highlighting maps Alexandre Duret-Lutz 2023-11-23 20:37:25 +01:00
  • 55575a11e3 twagraph: fix highlight-edges in defrag_states Alexandre Duret-Lutz 2023-11-23 20:27:05 +01:00
  • 193fdd6f95 python: add easy ways to remove highlights Alexandre Duret-Lutz 2023-11-23 17:08:31 +01:00
  • 0dd623b358 hoa: improve the diagnostic for unregistered propositions Alexandre Duret-Lutz 2023-11-22 16:15:00 +01:00
  • d4827c5e00 acc: improve the "too many acceptance sets used" message Alexandre Duret-Lutz 2023-11-22 15:45:10 +01:00
  • 62fb0c354e stength: fix detection of terminal automata Alexandre Duret-Lutz 2023-11-21 16:40:33 +01:00
  • 63362d535f Upgrade the Copyright strings to point to AUTHORS and drop years Alexandre Duret-Lutz 2023-11-18 21:17:05 +01:00
  • 3be62a907c parity: don't change_parity to the same acceptance Alexandre Duret-Lutz 2023-11-17 23:06:09 +01:00
  • 205df01390 never iterate on the edge_vector() Alexandre Duret-Lutz 2023-11-17 22:07:40 +01:00
  • 313e43c84b translate: fix #551 Alexandre Duret-Lutz 2023-11-17 14:04:22 +01:00
  • f0928f2b52 translate: fix relabel-overlap setting Alexandre Duret-Lutz 2023-11-17 13:48:17 +01:00
  • 0e71dd70c1 sccfilter: some inherently-weak automata should have t acceptance Alexandre Duret-Lutz 2023-11-17 13:41:19 +01:00
  • 13377542cd autfilt: fix a typo in the --help output Alexandre Duret-Lutz 2023-11-16 10:52:55 +01:00
  • 5ed56c054b ltsmin: make it easier to find the README Alexandre Duret-Lutz 2023-11-15 17:00:19 +01:00
  • b7995fcc5d * .gitlab-ci.yml (rpm-pkg): Start from the make-dist tarball. Alexandre Duret-Lutz 2023-11-15 15:06:30 +01:00
  • 35fca49075 parseaut: allow false edges to not be dropped Alexandre Duret-Lutz 2023-11-14 22:21:52 +01:00
  • bed87c60a4 parseaut: update highlight-edges when edges are dropped/added Alexandre Duret-Lutz 2023-11-14 18:14:12 +01:00
  • b7a0a8c324 gfguarante: update citation Alexandre Duret-Lutz 2023-11-14 16:52:41 +01:00
  • 997f7ec7fb gfguarantee: fix handling of true/false languages Alexandre Duret-Lutz 2023-11-14 15:40:24 +01:00
  • 13f66e55af * tests/core/twacube.cc: Remove duplicate line. Alexandre Duret-Lutz 2023-11-10 23:00:19 +01:00
  • 5826a40063 add test case for issue #546 Alexandre Duret-Lutz 2023-11-09 23:19:39 +01:00
  • 67b5d2aa9a fix several algorithms that incorrectly preserved !weak Alexandre Duret-Lutz 2023-11-09 22:13:05 +01:00
  • ac05035267 product_susp: fix handling of unsatisfiable/universal acceptances Alexandre Duret-Lutz 2023-11-07 17:17:58 +01:00
  • 127cb89cad Remove binary integer literals Florian Renkin 2023-11-08 09:57:16 +01:00
  • 9bdc500013 powerset: speedup computation for singleton with single edge Alexandre Duret-Lutz 2023-10-26 17:58:12 +02:00
  • 75f3a5f2c5 Fix warnings with GCC 7 on Centos 7 Alexandre Duret-Lutz 2023-10-15 00:21:12 +02:00
  • 1a2746e182 sbacc: ignore false edges and unreachable states Alexandre Duret-Lutz 2023-10-12 16:05:27 +02:00
  • b04c4d7fd9 expansions: expose easy expansion in python am/psl2aa Antoine Martin 2023-10-12 15:04:40 +02:00
  • 49f3c18ae3 expansions: store as vector of pairs Antoine Martin 2023-10-12 15:04:06 +02:00
  • 0199ebd592 expansions: US order in pipeline configurable Antoine Martin 2023-09-27 11:36:17 +02:00
  • f2d034130a introduce realizability_simplifier to share more of ltlsynt's code Alexandre Duret-Lutz 2023-10-09 17:53:12 +02:00
  • 9e40a32fd1 * .gitlab-ci.yml: Add a centos7 build. Alexandre Duret-Lutz 2023-10-04 17:22:35 +02:00
  • 02f9f0a1c9 * .gitlab-ci.yml: Activate Raspbian again. Alexandre Duret-Lutz 2023-10-03 16:25:19 +02:00
  • 9bf1edd80d ltlsynt: add option --global-equivalence Alexandre Duret-Lutz 2023-10-02 14:11:45 +02:00
  • c016f561fa sccinfo: implement PROCESS_UNREACHABLE_STATES Alexandre Duret-Lutz 2023-10-02 11:54:34 +02:00
  • 70812046d2 ltlsynt: do a fixpoint around the polarity simplifications Alexandre Duret-Lutz 2023-09-26 17:10:05 +02:00
  • 6dc11b4715 notebooks: correction of typos Florian Renkin 2023-06-20 15:10:00 +02:00
  • de2025298e expansions: UniquePrefixSeenOpt Antoine Martin 2023-09-20 17:52:18 +02:00
  • 858629dd3a twagraph: fix merge_states() on automata without edges Alexandre Duret-Lutz 2023-09-20 00:00:15 +02:00
  • 202ab92d1d ltlsynt: detect APs with constant polarity Alexandre Duret-Lutz 2023-09-19 09:53:22 +02:00
  • abca0f7fd9 * spot/tl/formula.hh: Typo in comment. Alexandre Duret-Lutz 2023-09-15 11:25:48 +02:00
  • 6ac2416e5d forq: remove the "same AP set" restriction Alexandre Duret-Lutz 2023-09-13 17:46:48 +02:00
  • 6eff384fca forq: remove the relevance test Alexandre Duret-Lutz 2023-09-14 11:23:57 +02:00
  • 05d7622f8f forq: make it easier to select contains's version Alexandre Duret-Lutz 2023-09-07 17:36:09 +02:00
  • ca4e6c4b48 forq: swap arguments of contains_forq Alexandre Duret-Lutz 2023-09-07 16:01:46 +02:00
  • 3861c04581 forq: fix Buchi acceptance test Alexandre Duret-Lutz 2023-09-05 18:03:09 +02:00
  • 28a6471efb forq: fix bib entry and bind the doxygen doc to a group Alexandre Duret-Lutz 2023-09-05 11:39:13 +02:00
  • ad22eb3e65 add enviroment variables for FORQ algorithm Jonah Romero 2023-08-08 12:08:28 +02:00
  • d1c5b2efdf implement a FORQ-based inclusion check for SBAs Jonah Romero 2023-08-03 12:04:47 +02:00
  • c2832cabfc split: add a new split_edge variant Jonah Romero 2023-08-03 11:54:49 +02:00
  • d96796121a replace sprintf by snprintf Alexandre Duret-Lutz 2023-09-13 15:39:36 +02:00
  • 7149521f48 relabel_bse: rework to simplify more patterns Alexandre Duret-Lutz 2023-09-13 11:31:49 +02:00
  • cbb981ffd5 python: add bindings for set of unsigned int Alexandre Duret-Lutz 2023-09-08 12:02:42 +02:00
  • 538afeb73b * spot/twaalgos/aiger.hh: Add missing include. Alexandre Duret-Lutz 2023-09-06 10:30:19 +02:00
  • e2149fabf4 determinize: work around overflow in reachability matrix indices Alexandre Duret-Lutz 2023-09-04 17:51:26 +02:00
  • 110b052b7d translate: add a new relabel-overlap option Alexandre Duret-Lutz 2023-08-28 22:45:44 +02:00
  • 18478e663f relabel: introduce an overlapping relabeling version Alexandre Duret-Lutz 2023-08-28 15:42:19 +02:00
  • 14347cdc52 * tests/sanity/style.test: Don't use egrep. Alexandre Duret-Lutz 2023-08-03 11:49:08 +02:00
  • 93ded57e52 Merge branch 'master' into next Alexandre Duret-Lutz 2023-08-01 14:26:35 +02:00
  • 41751b80a1 * NEWS, configure.ac: Bump version to 2.11.6.dev. Alexandre Duret-Lutz 2023-08-01 14:22:32 +02:00
  • f4b397a2bf Release Spot 2.11.6 Alexandre Duret-Lutz 2023-08-01 12:19:47 +02:00
  • bb95705d52 mention the bug fixed in BuDDy Alexandre Duret-Lutz 2023-07-31 21:11:39 +02:00
  • e37bc9e1ae [buddy] fix cache index of bdd_forall Alexandre Duret-Lutz 2023-07-31 21:07:07 +02:00
  • de7d5a956f * .gitlab-ci.yml: temporary disable raspbian. Alexandre Duret-Lutz 2023-07-28 16:20:18 +02:00
  • 44d9e34e32 improve coverage of LaTeX/utf8 printers for SERE Alexandre Duret-Lutz 2023-07-27 14:28:15 +02:00
  • 15857385a5 bin: cover more tmpfile failure when running as root Alexandre Duret-Lutz 2023-07-27 10:23:33 +02:00
  • 3d412fbb78 tests: add some test to cover autcross' univ-edges removal Alexandre Duret-Lutz 2023-07-27 09:48:00 +02:00