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

Commit graph

  • 2c05a9fdb6 ltlast: move all accessor methods to headers to help the optimizer Alexandre Duret-Lutz 2014-02-12 10:39:38 +01:00
  • 9020ac8bef * doc/org/satmin.org: Reword last paragraph. Alexandre Duret-Lutz 2014-02-12 10:06:53 +01:00
  • be43c1e957 * NEWS, configure.ac: Bump version to 1.2.3a. Alexandre Duret-Lutz 2014-02-11 17:30:10 +01:00
  • 2a7d5f5f7f Release Spot 1.2.3 Alexandre Duret-Lutz 2014-02-11 16:23:40 +01:00
  • 327b7e18b2 * bench/dtgbasat/README: Update glucose URL. Alexandre Duret-Lutz 2014-02-11 17:16:51 +01:00
  • f567d88ff8 * NEWS: mention recent fixes. Alexandre Duret-Lutz 2014-02-11 10:45:15 +01:00
  • 58878cd405 Work around the clang version installed with MacOS X 10.9. Alexandre Duret-Lutz 2014-02-11 10:38:30 +01:00
  • 0b5f63c296 Add missing const. Alexandre Duret-Lutz 2014-02-11 10:05:57 +01:00
  • cb0b3d3c67 testsuite: find files when building in remote directory Alexandre Lewkowicz 2014-02-10 16:56:20 +01:00
  • eb778c569a sat: adjust SPOT_SATSOLVER default for glucose 3.0 Alexandre Duret-Lutz 2014-02-08 21:34:35 +01:00
  • fd4a963a26 * src/bin/common_setup.cc: Bump copyright year. Alexandre Duret-Lutz 2014-02-07 14:13:09 +01:00
  • 3c985a3235 sat: document the SPOT_SATLOG envvar Alexandre Duret-Lutz 2014-02-07 14:10:07 +01:00
  • 20824b96b9 timer: also consider the time spent in child processes Alexandre Duret-Lutz 2014-02-07 14:04:53 +01:00
  • 55ee18b96a sat-minimize: more statistics. Alexandre Duret-Lutz 2014-01-17 11:48:04 +01:00
  • 1319ec0bad sat-minimize: limit number of iterations Alexandre Duret-Lutz 2014-01-17 11:47:07 +01:00
  • e1be8e6e42 * bench/dtgbasat/README: Typo. Alexandre Duret-Lutz 2014-01-17 11:44:02 +01:00
  • 9c0021fac8 * src/tgbatest/satmin2.test, src/tgbatest/Makefile.am: New test. Alexandre Duret-Lutz 2013-12-17 16:08:34 +01:00
  • 7a26a4f1ec Revert "* src/tgbaalgos/dtbasat.cc: Better encoding for weak SCCs." Alexandre Duret-Lutz 2013-12-17 15:58:54 +01:00
  • b4d0b9ee42 sat: more debug. Alexandre Duret-Lutz 2013-12-17 15:55:23 +01:00
  • 9c98975c19 sat: factor the creation of temporary files Alexandre Duret-Lutz 2013-12-06 18:42:19 +01:00
  • 1853bdd53b sat: fix some non-determinism of the encoding Alexandre Duret-Lutz 2013-12-03 16:37:31 +01:00
  • e5874ee4c7 Call glucose with -verb=0. Alexandre Duret-Lutz 2013-12-03 14:32:37 +01:00
  • 977a6dfaee * src/tgbaalgos/dtbasat.cc: Better encoding for weak SCCs. Alexandre Duret-Lutz 2013-11-22 16:58:20 +01:00
  • 4334abdeed org: Fix UP links and center them on the page. Alexandre Duret-Lutz 2014-02-06 22:28:37 +01:00
  • c2195600b8 Fix spurious failre with Pandas 0.13. Alexandre Duret-Lutz 2014-02-06 01:31:19 +01:00
  • 38388748b0 * NEWS: Mention recent fixes. Alexandre Duret-Lutz 2014-02-06 00:45:18 +01:00
  • 50bdc24514 randltl: gracefully handle the absence of unary or binary operators. Alexandre Duret-Lutz 2014-02-05 18:10:48 +01:00
  • 4911e7dc1f Fix warning of Clang-3.5 against Doxygen comments. Alexandre Duret-Lutz 2014-02-05 15:07:10 +01:00
  • 17dd281b33 * doc/org/ltlfilt.org: Typo, reported by Fabrice Kordon. Alexandre Duret-Lutz 2014-02-04 07:58:52 +01:00
  • 494dbe2041 length: slight simplification Alexandre Duret-Lutz 2014-02-03 09:39:23 +01:00
  • 02334867da length_boolone: fix inconsistency Alexandre Lewkowicz 2014-01-15 00:43:19 +01:00
  • b6e5ce7e15 python: better support for Python 3 Alexandre Duret-Lutz 2014-02-02 15:33:11 +01:00
  • a6714119f9 * NEWS, configure.ac: Bump version to 1.2.2a. Alexandre Duret-Lutz 2014-01-24 12:19:58 +01:00
  • 35612f3626 Release Spot 1.2.2 Alexandre Duret-Lutz 2014-01-24 11:16:07 +01:00
  • 4f31a9bbed bitvect: fix block_count() on 0-sized bit-vectors Alexandre Duret-Lutz 2014-01-23 23:09:28 +01:00
  • 91789b9b12 * src/tgbaalgos/degen.cc: Do not copy the unicity table. Alexandre Duret-Lutz 2014-01-23 15:04:21 +01:00
  • bbf6a68228 Workaround another g++-4.0.1 bug on Darwin. Alexandre Duret-Lutz 2014-01-15 23:04:38 +01:00
  • ff816fbebb * NEWS: Update with recent fixes. Alexandre Duret-Lutz 2014-01-15 16:42:53 +01:00
  • 522373984c bitvect: fix some issues observed on 32bit architectures. Alexandre Duret-Lutz 2014-01-15 15:52:11 +01:00
  • 534edd4d1c bitvect: Fix compilation on 32-bits hosts. Alexandre Duret-Lutz 2014-01-15 14:40:27 +01:00
  • 9ccdef9cbd Workaround GCC 4.0.1 on the Darwin builds. Alexandre Duret-Lutz 2014-01-15 10:52:44 +01:00
  • e19e56fba3 * AUTHORS: Add Alexandre Lewkowicz Alexandre Duret-Lutz 2014-01-13 17:27:36 +01:00
  • d2e43c3b61 python: use new print syntax. Alexandre Lewkowicz 2014-01-13 13:32:04 +00:00
  • 72b616c8cc * src/eltlparse/eltlscan.ll (_atoi): Fix range checking. Alexandre Duret-Lutz 2014-01-12 15:42:47 +01:00
  • e2143c0313 ltlparse, eltlparse: avoid unnecessary calls to strlen(). Alexandre Duret-Lutz 2014-01-07 16:03:57 +01:00
  • 0c06844655 * src/taalgos/emptinessta.cc: Include <cstdlib> for abs(). Alexandre Duret-Lutz 2013-12-18 22:32:49 +01:00
  • 7a6af3aa0d Add missing #include. Alexandre Duret-Lutz 2013-12-18 16:44:05 +01:00
  • 51d6fa7347 Upgrade to gnulib 23eecb48e39afd0d267d64d40ba6bf97aa865e13. Alexandre Duret-Lutz 2013-12-17 23:03:52 +01:00
  • 7cfda699e6 Upgrade to gnulib 6b8f1dd1a21ce49319795391e21adf645b64db3c. Alexandre Duret-Lutz 2013-12-17 17:04:11 +01:00
  • 0afb9fe103 * src/tgba/tgbaunion.hh: Remove unused private member. Alexandre Duret-Lutz 2013-12-16 10:26:56 +01:00
  • 2febbd5929 * NEWS, configure.ac: Bump version to 1.2.1a Alexandre Duret-Lutz 2013-12-11 11:38:27 +01:00
  • 4d7638a269 Release Spot 1.2.1. Alexandre Duret-Lutz 2013-12-11 10:40:33 +01:00
  • f0bcab4add bin: support multi-line CSV fields. Alexandre Duret-Lutz 2013-12-06 13:45:55 +01:00
  • 6c21089599 ltlcross: end CSV lines with \n, not \r\n Alexandre Duret-Lutz 2013-12-06 11:29:31 +01:00
  • 846e33b9e5 ltl2tgba: Add a --csv-escape option and document CSV I/O. Alexandre Duret-Lutz 2013-11-29 18:46:02 +01:00
  • 0faea814da bin: add support for reading formulas from CSV files. Alexandre Duret-Lutz 2013-11-29 09:32:51 +01:00
  • 8c5875314c * doc/org/satmin.org: Typo Alexandre Duret-Lutz 2013-12-03 15:07:16 +01:00
  • 0fc189d186 * HACKING: Typos. Alexandre Duret-Lutz 2013-11-28 18:44:28 +01:00
  • d719c706f4 ltlcross: report statistics about Rabin and Streett automata Alexandre Duret-Lutz 2013-11-22 02:02:07 +01:00
  • 2b10745dfb ltlcross: support --products=+N Alexandre Duret-Lutz 2013-11-21 22:31:59 +01:00
  • 9577e5d528 * bench/dtgbasat/README: Do not mention VMCAI'14. Alexandre Duret-Lutz 2013-11-21 19:35:31 +01:00
  • 3e3d320de5 doc: add suggestions for bibliographic references Alexandre Duret-Lutz 2013-11-21 14:01:58 +01:00
  • f65c621a55 ltlcross: report exit_status and exit_code columns in CSV and JSON Alexandre Duret-Lutz 2013-11-19 23:22:29 +01:00
  • 686a45484d ltlcross: report missing input/output sequence Alexandre Duret-Lutz 2013-11-19 22:45:16 +01:00
  • cf91a23711 tests: add some missing "set -e" Alexandre Duret-Lutz 2013-11-19 19:20:50 +01:00
  • 7de25a32ef ltlcross: support short names Alexandre Duret-Lutz 2013-11-19 16:34:08 +01:00
  • 1c5536ea9c ltlcross: follow RFC 4180 for CSV output. Alexandre Duret-Lutz 2013-10-16 10:31:31 +02:00
  • 925a807f4f * doc/org/ltlcross.org: Show how to call ltl3dra and fix typos. Alexandre Duret-Lutz 2013-11-22 02:07:13 +01:00
  • 2cda03f8ce * doc/org/ltlcross.org: Typos, reported by František Blahoudek. Alexandre Duret-Lutz 2013-11-11 18:51:12 +01:00
  • d415a23804 * src/bin/ltl2tgta.cc: Simplify using spot::translator(). Alexandre Duret-Lutz 2013-10-22 17:55:29 +02:00
  • 9dd59f1974 * README: Document utf8/. Alexandre Duret-Lutz 2013-10-22 17:54:52 +02:00
  • fd80e944b5 * doc/tl/tl.tex: Typo. Alexandre Duret-Lutz 2013-10-17 05:08:49 +02:00
  • 54c01cfcdf * doc/org/ltlfilt.org: Typo. Alexandre Duret-Lutz 2013-10-11 17:52:37 +02:00
  • f38570138d * src/ltlvisit/relabel.cc: Add more comments. Alexandre Duret-Lutz 2013-10-01 18:32:57 +02:00
  • 65dc65b061 * NEWS, configure.ac: Bump version to 1.2a Alexandre Duret-Lutz 2013-10-01 13:48:40 +02:00
  • c0a845b274 Release Spot 1.2. Alexandre Duret-Lutz 2013-10-01 13:23:47 +02:00
  • f48b5e507c * HACKING: Update version requirements for Bison and SWIG. Alexandre Duret-Lutz 2013-10-01 11:02:33 +02:00
  • f3b87c85a2 Fix uninitialized variables in spot::postprocessor. Alexandre Duret-Lutz 2013-09-30 20:16:00 +02:00
  • c0851a9559 * iface/dve2/finite.test: Work around Darwin's wc. Alexandre Duret-Lutz 2013-09-30 20:15:40 +02:00
  • 3c943d836a Add support for Bison 3.0. Alexandre Duret-Lutz 2013-09-30 19:36:19 +02:00
  • 5663872083 Work around some configurations of latexmk. Alexandre Duret-Lutz 2013-09-30 11:50:52 +02:00
  • df109869eb Generalize implication-based simplifications for multops. Alexandre Duret-Lutz 2013-09-29 21:00:57 +02:00
  • c01909e3ff Sort comutative binops like we sort multops. Alexandre Duret-Lutz 2013-09-29 20:58:19 +02:00
  • 228121c963 Include lib/ and config.h in ltlast/. Alexandre Duret-Lutz 2013-09-28 09:25:10 +02:00
  • 87b65b9bce relabel: implement relabeling of Boolean subexpressions. Alexandre Duret-Lutz 2013-09-27 16:23:35 +02:00
  • 2efe52fab0 * src/ltlvisit/clone.cc: Use reserve() for multop. Alexandre Duret-Lutz 2013-09-27 16:09:15 +02:00
  • 1f1feb935d * src/tgbaalgos/randomgraph.hh: Two typos, reported by Akim. Alexandre Duret-Lutz 2013-09-27 14:38:03 +02:00
  • 536e45b342 Arrange multops so that Boolean arguments come first. Alexandre Duret-Lutz 2012-06-20 14:45:25 +02:00
  • 1f384c2c63 gnulib: Add module strverscmp. Alexandre Duret-Lutz 2013-09-23 11:36:15 +02:00
  • b486d4f1dc Fix compilation with g++-4.4.7. Alexandre Duret-Lutz 2013-09-26 13:30:58 +02:00
  • 9b582691b7 * src/ltlvisit/simplify.cc: Cosmetics. Alexandre Duret-Lutz 2012-06-20 17:31:03 +02:00
  • ce5ea829bd tools: Add a --format option Alexandre Duret-Lutz 2013-09-22 22:02:10 +02:00
  • 983feb5290 Add benchmark for our DTGBA SAT-minimization. Alexandre Duret-Lutz 2013-08-21 17:58:41 +02:00
  • 3076c3da4e org: document SAT-based minimization Alexandre Duret-Lutz 2013-09-15 22:37:55 +02:00
  • cda847e207 satdtba: optimize number of clauses of variables Alexandre Duret-Lutz 2013-09-13 10:51:00 +02:00
  • 77cef16ca0 dtgbasat: Improve handling of weaks SCC in the ref automaton Alexandre Duret-Lutz 2013-09-12 15:23:10 +02:00
  • 795c6e48d9 dtgbasat: get rid of the <q1,q1'>G variables Alexandre Duret-Lutz 2013-09-12 14:18:30 +02:00
  • b318b151c8 satmin: ignore (s,l,d2) if (s,l,d1) is already in result Alexandre Duret-Lutz 2013-09-11 14:36:08 +02:00
  • 90a466d6a3 degen: consider common outgoing acceptance only inside an SCC Alexandre Duret-Lutz 2013-09-11 10:49:49 +02:00
  • 073334dfd6 * src/tgbaalgos/dtbasat.cc: Skip clauses for trivial SCCs. Alexandre Duret-Lutz 2013-09-05 11:30:58 +02:00