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

Commit graph

  • 0ac5bbc05d ltlsynt: replace -x minimization-lvl=N by --simplify Alexandre Duret-Lutz 2021-10-06 17:32:41 +02:00
  • af5474d791 ltlsynt: replace -x specification-decomposition by --decompose Alexandre Duret-Lutz 2021-10-06 10:50:41 +02:00
  • 5d722ca584 * doc/org/tut.org: Fix a title. Alexandre Duret-Lutz 2021-10-06 10:46:22 +02:00
  • 405f76f0a0 games, synthetis: improve Doxygen Alexandre Duret-Lutz 2021-10-03 19:13:15 +02:00
  • 188fee4756 * tests/core/ltlsynt.test: Test --aiger without option. Alexandre Duret-Lutz 2021-10-03 18:37:55 +02:00
  • 17070b6cee aiger: fix some typos and inconsistencies Alexandre Duret-Lutz 2021-10-03 18:33:57 +02:00
  • 590929fbcf ltlsynt: improve documentation Alexandre Duret-Lutz 2021-10-03 15:06:21 +02:00
  • ee83e8e4c2 tests: work around to compiler warnings Alexandre Duret-Lutz 2021-10-03 00:57:21 +02:00
  • 644342f5d4 simplify: fix some discrepancies between Intel and ARM Alexandre Duret-Lutz 2021-10-03 00:48:38 +02:00
  • 1b69ed96f9 ltlsynt: deduce --outs from --ins or vice-versa Alexandre Duret-Lutz 2021-10-02 18:16:39 +02:00
  • 60225fd139 acd: do not recompute identical subtrees Alexandre Duret-Lutz 2021-09-30 21:20:02 +02:00
  • 2c435c6c11 zlktree: simplify heuristic computation Alexandre Duret-Lutz 2021-09-30 17:05:18 +02:00
  • 88d0d2e112 org: cleanup tut40 Alexandre Duret-Lutz 2021-09-30 16:17:48 +02:00
  • 211e7d90d3 org: Add a pratical example for games Jerome Dubois 2021-02-09 17:03:40 +01:00
  • ee80849caf dtwasat: various fixes Alexandre Duret-Lutz 2021-09-29 16:47:03 +02:00
  • fea0be96c1 acd: add ORDER_HEURISTIC for state-based ACD-transform Alexandre Duret-Lutz 2021-09-24 20:39:47 +02:00
  • 70ede35702 acd: add support for state-based output Alexandre Duret-Lutz 2021-09-24 13:37:16 +02:00
  • 043a1dc394 acd: fix typeness checks, and add options for those Alexandre Duret-Lutz 2021-09-24 11:10:12 +02:00
  • 406bc8ed17 Remove do_simplify opt from split_2step Philipp Schlehuber 2021-09-22 12:52:03 +02:00
  • ddda68403f * spot/twa/twagraph.cc: Fixes #478. Alexandre Duret-Lutz 2021-09-21 11:20:14 +02:00
  • 3f606cdc35 Updated News Philipp 2021-09-21 11:03:31 +02:00
  • 8296079282 synthesis: aps_of uses a local cache Florian Renkin 2021-09-17 13:43:08 +02:00
  • cb3a833a8d ltlsynt: fix syntax error handling Alexandre Duret-Lutz 2021-09-17 13:25:28 +02:00
  • 4710577dfe build: fix multiple GCC warnings Alexandre Duret-Lutz 2021-09-16 22:52:43 +02:00
  • c973fcdf2d Improving handling of unused proposition for aig Philipp Schlehuber 2021-09-15 15:18:16 +02:00
  • 7c1230b484 synthesis: fix decomposition Florian Renkin 2021-09-14 11:08:55 +02:00
  • ad5203e77a synthesis: Fix segfault when there is no output Florian Renkin 2021-09-13 17:46:33 +02:00
  • 306a45f239 Aiger: Add a way to evaluate an input sequence (Python) Florian Renkin 2021-09-13 15:30:19 +02:00
  • b9ec16f9c2 Typos Florian Renkin 2021-09-13 15:28:39 +02:00
  • 7d908b9320 ltlsynt rewrite philipp 2021-09-03 00:40:42 +02:00
  • a5185c2123 Use new minterm enumeration in split_2step philipp 2021-08-30 15:59:43 +02:00
  • 98ab826255 Introducing formula split Florian Renkin 2021-08-13 16:26:13 +02:00
  • 4260b17fba New game api philipp 2021-08-13 14:50:16 +02:00
  • 786599ed20 Adding selective edge sorting and state merging philipp 2021-08-12 00:04:29 +02:00
  • 2c267dd894 Adding dot suppport for aiger class philipp 2021-08-10 23:58:26 +02:00
  • 17db582341 Making aiger a class philipp 2021-08-06 13:07:30 +02:00
  • 18948a96be Adding bdd_is_cube for python philipp 2021-08-06 13:06:25 +02:00
  • 3aef5f31c0 [buddy] Adding bdd_is_cube philipp 2021-08-03 11:37:48 +02:00
  • 5a0fbf6cb9 [buddy] introduce a bdd_satoneshortest() function Alexandre Duret-Lutz 2021-06-16 22:33:22 +02:00
  • 830f68b3b9 robin_hood: Update to version 3.11.3 Alexandre Duret-Lutz 2021-09-15 22:05:28 +02:00
  • 42ff02585b parseaut: convert short numbers without strtoul() Alexandre Duret-Lutz 2021-09-15 17:21:04 +02:00
  • 4c94e14f86 parseaut: replace std::map by robin_hood::unordered_flat_map Alexandre Duret-Lutz 2021-09-15 16:47:52 +02:00
  • ce1cf5507f parseaut: improve parsing of HOA labels Alexandre Duret-Lutz 2021-09-13 17:21:49 +02:00
  • 9539fbcf4c genem: implement the logic from the future journal version of ATVA19 Alexandre Duret-Lutz 2021-09-10 21:30:01 +02:00
  • 7fedb3dc61 acc: introduce fin_one_extract() Alexandre Duret-Lutz 2021-09-10 18:17:17 +02:00
  • 2d1cb0ddcd zlktree: replace std::vector<bool> by bitvect in ACD Alexandre Duret-Lutz 2021-09-10 14:07:26 +02:00
  • 6aa2079079 zlktree: speedup the construction of ACD nodes Alexandre Duret-Lutz 2021-09-10 11:47:44 +02:00
  • b6df1f8f92 bitvect: add a foreach_set_index(callback) function Alexandre Duret-Lutz 2021-09-10 11:46:26 +02:00
  • 850608a5fd zlktree: add a cheap unit-propagation Alexandre Duret-Lutz 2021-09-08 17:12:14 +02:00
  • cb1f6b1239 acc: introduce inf_unit() Alexandre Duret-Lutz 2021-09-08 16:44:57 +02:00
  • 4ed5160fb8 zlktree: fix a bug Alexandre Duret-Lutz 2021-09-08 15:15:08 +02:00
  • ceec447617 * tests/python/zlktree.ipynb: Fix the steps through the example. Alexandre Duret-Lutz 2021-09-07 13:54:43 +02:00
  • 170d839c4b acd: remove redundant nodes Alexandre Duret-Lutz 2021-09-05 16:56:54 +02:00
  • d5b641a7dc build: use 'jupyter nbconvert' instead of 'ipython nbconvert' Alexandre Duret-Lutz 2021-09-04 22:08:20 +02:00
  • 4d2ced1b07 * tests/Makefile.am: Fix location of zlktree.ipynb. Alexandre Duret-Lutz 2021-09-04 20:54:50 +02:00
  • 5c5790039b zlktree: cleanup the interface, and add interactive ACD Alexandre Duret-Lutz 2021-09-03 22:20:20 +02:00
  • dc17762e14 * doc/org/oaut.org (dot2tex): Acknowledge the 2.11 release. Alexandre Duret-Lutz 2021-09-02 22:54:45 +02:00
  • 4855d3c877 dot: add an option to output id= attributes Alexandre Duret-Lutz 2021-09-02 22:43:22 +02:00
  • d5bbeceeb2 * .gitlab-ci.yml (mingw-shared, mingw-static): Build from a tarball. Alexandre Duret-Lutz 2021-09-01 17:57:25 +02:00
  • d4e3b0bed4 tests: fix a gcc-snapshot warning Alexandre Duret-Lutz 2021-09-01 14:02:46 +02:00
  • 1de441e8e5 tests: work around issue #474 Alexandre Duret-Lutz 2021-09-01 12:27:21 +02:00
  • 86c22d98bc zlktree: remimplement zielonka_tree without BDDs Alexandre Duret-Lutz 2021-08-31 15:17:56 +02:00
  • 200ee0d204 style: better support if statement with initializer Alexandre Duret-Lutz 2021-09-01 11:59:54 +02:00
  • 49b5d570e7 zlktree: share bitvectors in ACD Alexandre Duret-Lutz 2021-08-30 11:07:53 +02:00
  • 26f2179805 zlktree: implement ACD and its transform Alexandre Duret-Lutz 2021-08-09 15:22:17 +02:00
  • 8c5bb6c2eb zlktree: add a paritization based on zielonka trees Alexandre Duret-Lutz 2021-08-04 11:30:19 +02:00
  • c924c63255 Merge branch 'master' into next Alexandre Duret-Lutz 2021-08-10 17:42:56 +02:00
  • 3c7a2c9b4a Bump version to 2.9.8.dev Alexandre Duret-Lutz 2021-08-10 17:38:54 +02:00
  • db0440f1fe Release Spot 2.9.8 Alexandre Duret-Lutz 2021-08-10 17:37:00 +02:00
  • 87022c23c6 * NEWS: Update for 2.9.8. Alexandre Duret-Lutz 2021-08-10 13:37:33 +02:00
  • d8a75518e4 twa: fix intersecting_run on weak automata Alexandre Duret-Lutz 2021-07-07 18:00:41 +02:00
  • c34192a77c twa_run: reduce now diagnoses rejecting runs Alexandre Duret-Lutz 2021-07-07 17:20:33 +02:00
  • eb3474d82b fix a gcc-snapshot -Wnoexcept diagnostic Alexandre Duret-Lutz 2021-07-05 16:00:57 +02:00
  • c0c76904da bitset: fix implementation of operator-() Alexandre Duret-Lutz 2021-07-05 14:12:58 +02:00
  • bb7426c0b9 org: we have a conda-forge package Alexandre Duret-Lutz 2021-06-29 11:54:17 +02:00
  • 487bbb63de work around a null pointer dereference error Alexandre Duret-Lutz 2021-06-21 11:42:36 +02:00
  • 77545824eb ltlfilt: fix a typo in the --help text Alexandre Duret-Lutz 2021-06-11 11:48:40 +02:00
  • 773939bebe typos: coma -> comma Alexandre Duret-Lutz 2021-06-11 11:46:55 +02:00
  • 2e14eb0c02 [buddy] typo coma -> comma Alexandre Duret-Lutz 2021-06-11 11:46:27 +02:00
  • eeccd5804d * spot/graph/graph.hh (chain_edges_): Typo in doc. Alexandre Duret-Lutz 2021-05-17 18:14:32 +02:00
  • c58e6f22ac mealy: work around spurious nullptr warning Alexandre Duret-Lutz 2021-08-02 09:28:14 +02:00
  • 3614cf34a8 use bdd_have_common_assignment in more places Alexandre Duret-Lutz 2021-07-30 12:05:21 +02:00
  • a6aa799a17 adjust for BuDDy change Alexandre Duret-Lutz 2021-07-30 11:18:57 +02:00
  • dfd168b048 [buddy] fix bdd_has_common_assignement Alexandre Duret-Lutz 2021-07-30 11:16:39 +02:00
  • af511707c0 introduce a zielonka_tree class Alexandre Duret-Lutz 2021-07-29 17:41:04 +02:00
  • 803f647dde acc: make the to_bdd() method public Alexandre Duret-Lutz 2021-07-29 16:17:49 +02:00
  • 31d6dc33e7 Improving efficiency of unsplit_2step philipp 2021-07-16 13:51:50 +02:00
  • 9669806cd0 Adding signature based minimization of mealy machines Florian Renkin 2021-07-11 00:11:04 +02:00
  • 3da41aa9a1 Improving hash performance for pairs of integral types philipp 2021-07-09 23:05:50 +02:00
  • f4776efb63 Adding sat-based minimization for mealy machines philipp 2021-06-23 12:23:05 +02:00
  • e8f5865fb8 Add setter and getter for synthesis-outputs philipp 2021-07-12 08:09:11 +02:00
  • 08113e0e04 Adding bdd_has_common_assignement philipp 2021-07-27 16:22:32 +02:00
  • 92239d8242 [buddy] Adding bdd_has_common_assignement philipp 2021-06-21 14:31:11 +02:00
  • 31e87aac11 mc: add missing <atomic> includes Alexandre Duret-Lutz 2021-07-13 11:31:53 +02:00
  • 4570c735f3 merge_states: don't call defrag_states if unnecessary Alexandre Duret-Lutz 2021-07-13 10:20:14 +02:00
  • d019ea61fe python: make sere twa::acc() survives its automaton Alexandre Duret-Lutz 2021-07-12 15:27:07 +02:00
  • b767411a82 twa_graph: work around swig-3 calling the wrong make_twa_graph copy Alexandre Duret-Lutz 2021-07-08 17:38:40 +02:00
  • 31a681c285 twa: implement a copy_named_properties_of() method Alexandre Duret-Lutz 2021-07-08 10:30:19 +02:00
  • 0cf2d285b6 python: implement twa_graph.__copy__ Alexandre Duret-Lutz 2021-07-08 09:33:57 +02:00
  • 0509263f82 twa: fix intersecting_run on weak automata Alexandre Duret-Lutz 2021-07-07 18:00:41 +02:00