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

Commit graph

  • 97665a584e hoa: detect colored automata Alexandre Duret-Lutz 2015-06-01 20:36:03 +02:00
  • a75a9c091c random: fix rounding in barand() Alexandre Duret-Lutz 2015-06-01 19:43:21 +02:00
  • eabed370bf bin: clear temporary files on termination signals Alexandre Duret-Lutz 2015-06-01 15:32:00 +02:00
  • 83364c636f * src/bin/common_trans.cc: Fix wording in error message. Alexandre Duret-Lutz 2015-06-01 12:23:24 +02:00
  • 1d9ceb8146 * src/bin/common_trans.cc: Use nullptr instead of 0. Alexandre Duret-Lutz 2015-06-01 12:15:51 +02:00
  • 0ac35a1591 randaut: rename -S as -Q for consistency Alexandre Duret-Lutz 2015-06-01 09:20:52 +02:00
  • a6ef24567e * doc/org/ltlcross.org: Typo. Alexandre Duret-Lutz 2015-05-30 13:05:11 +02:00
  • 6b28cc9170 org: document HOA support Alexandre Duret-Lutz 2015-05-30 00:22:05 +02:00
  • 3230b7c8aa hoaparse: fix errors observed with gcc-snapshot Alexandre Duret-Lutz 2015-05-27 08:25:39 +02:00
  • b87f24d7c4 * doc/org/randaut.org: Update for recent changes. Alexandre Duret-Lutz 2015-05-26 23:56:59 +02:00
  • 88141b2711 randaut: better generation of acceptance conditions Alexandre Duret-Lutz 2015-05-25 23:47:59 +02:00
  • d5598a9aaa * doc/org/ltlcross.org: Update. Alexandre Duret-Lutz 2015-05-25 17:56:05 +02:00
  • 7b6626d176 ltlcross: add a complete column Alexandre Duret-Lutz 2015-05-25 17:41:02 +02:00
  • ae0f0d5fc2 ltlcross: add --automata option Alexandre Duret-Lutz 2015-05-25 16:51:30 +02:00
  • 5d7f4464ea acc: Adjust generalition of parity acceptance Alexandre Duret-Lutz 2015-05-24 00:00:36 +02:00
  • 05ef316c23 * doc/org/satmin.org: Typo, reported by Joachim. Alexandre Duret-Lutz 2015-05-22 19:08:43 +02:00
  • 7b5c37d5a5 python: fix check of is_parity() Alexandre Duret-Lutz 2015-05-22 07:54:45 +02:00
  • 96e2da8666 sat-minimize: some documentation and associated fixes Alexandre Duret-Lutz 2015-05-21 19:05:48 +02:00
  • 7b28f1ffb5 acc: typo in parse_acc_code for generalized_co_buchi Alexandre Duret-Lutz 2015-05-21 17:27:38 +02:00
  • 8f2865070e * src/twaalgos/simulation.cc: Preserve the unambiguous flag. Alexandre Duret-Lutz 2015-05-21 14:30:44 +02:00
  • ef7f96a545 * doc/org/satmin.org: Missing name on dot output. Alexandre Duret-Lutz 2015-05-21 10:49:05 +02:00
  • e04b4eb9fb acc: better Rabin/Streett detection Alexandre Duret-Lutz 2015-05-21 08:07:13 +02:00
  • 04171207e6 acc: recognize parity acceptance Alexandre Duret-Lutz 2015-05-19 22:22:53 +02:00
  • 704eaf26c2 acc: add support for generating parity conditions Alexandre Duret-Lutz 2015-05-19 20:54:03 +02:00
  • d276f73eed hoa: output acc-name for several acceptance types Alexandre Duret-Lutz 2015-05-19 19:31:13 +02:00
  • 8e1c846984 acc: parse standard acceptance names Alexandre Duret-Lutz 2015-04-28 09:48:45 +02:00
  • 7880b25aae sat-minimize: add a max-states option Alexandre Duret-Lutz 2015-04-27 23:52:51 +02:00
  • 91f68ab1d8 sat-minimize: ignore silly histories Alexandre Duret-Lutz 2015-04-27 19:29:07 +02:00
  • 9480669e99 python: export the sat-minimization routines Alexandre Duret-Lutz 2015-04-27 17:22:08 +02:00
  • ec49398e84 * src/twa/acc.hh (mark_t::clear): New method. Alexandre Duret-Lutz 2015-04-27 17:20:23 +02:00
  • 6e32b65875 * src/twa/acc.cc: Fix BDD conversion in case of unused sets. Alexandre Duret-Lutz 2015-04-27 14:23:19 +02:00
  • 0ede968760 sat-minimize: allow different acceptances as input and output Alexandre Duret-Lutz 2015-04-16 00:10:56 +02:00
  • 3efeacb61b acc: preserve input order in parse_acc_code() Alexandre Duret-Lutz 2015-04-15 23:59:12 +02:00
  • b488157957 sat-minimize: omit impossible histories Alexandre Duret-Lutz 2015-03-26 19:39:47 +01:00
  • 0874980574 sat-minimize: generalize to any acceptance Alexandre Duret-Lutz 2015-03-03 14:44:28 +01:00
  • 19a273929c python: rewrite translate() to deal with unambiguous and sbacc Alexandre Duret-Lutz 2015-05-15 23:50:19 +02:00
  • 1ef3e5f3ff translate: remove arbitrary restriction on -U and -D Alexandre Duret-Lutz 2015-05-14 20:09:39 +02:00
  • 0786e068ae postproc: add a SBAcc option Alexandre Duret-Lutz 2015-05-14 20:04:50 +02:00
  • dd87bdf868 wdba: adjust to work on any TωA Alexandre Duret-Lutz 2015-05-14 17:25:36 +02:00
  • 8080813303 simulation: work on TωA Alexandre Duret-Lutz 2015-05-14 17:24:28 +02:00
  • 0e04b25342 ltldo: preserve generic acceptance Alexandre Duret-Lutz 2015-05-14 16:02:29 +02:00
  • 3d1ccdc45e autfilt: new --separate-sets option Alexandre Duret-Lutz 2015-05-14 13:21:09 +02:00
  • 5ed321fc19 * doc/org/ltlcross.org: document the ambiguous_aut column of --csv. Alexandre Duret-Lutz 2015-05-13 23:40:24 +02:00
  • f006f0df34 * src/twaalgos/isunamb.cc: Simplify. Alexandre Duret-Lutz 2015-05-13 23:23:11 +02:00
  • 8c32fba8b9 scc_info: determine accepting/rejecting-SCCs for any acceptance Alexandre Duret-Lutz 2015-05-13 23:16:26 +02:00
  • 07ee3d2dd0 allow scc_filter() and scc_filter_states() on any TωA Alexandre Duret-Lutz 2015-05-13 18:27:41 +02:00
  • 332694a485 document -U Alexandre Duret-Lutz 2015-05-13 12:44:07 +02:00
  • 5d76b9127b ltl2tgba_fm: produce unambiguous automata for PSL as well Alexandre Duret-Lutz 2015-05-12 20:18:42 +02:00
  • 778d8fe95b ltl2tgba_fm: make it easier to preserve state names Alexandre Duret-Lutz 2015-05-12 20:13:19 +02:00
  • 487a86d06a bin: add --check=unambiguous Alexandre Duret-Lutz 2015-05-10 17:39:26 +02:00
  • 98de84f3de Add an is_unambiguous() function, use it in ltlcross and autfilt Alexandre Duret-Lutz 2013-03-21 11:53:42 +01:00
  • 9f3a7a49de Add support for unambiguous automata Alexandre Duret-Lutz 2015-05-07 21:10:23 +02:00
  • f55211336e ltlgrind: fix two bugs related to PSL formulas Alexandre Duret-Lutz 2015-05-11 23:55:28 +02:00
  • 011a56846f org: document -0 Alexandre Duret-Lutz 2015-05-11 19:53:41 +02:00
  • 2749702e75 * src/bin/common_aoutput.cc: Remove duplicate include. Alexandre Duret-Lutz 2015-05-11 19:46:06 +02:00
  • 7b506a919c * src/twaalgos/stats.hh: Typo in comment. Alexandre Duret-Lutz 2015-05-11 19:45:43 +02:00
  • e026766219 bin: add -0 option for LTL output Alexandre Duret-Lutz 2015-05-11 17:17:15 +02:00
  • a44e1bf325 * NEWS: Mention recent change, and fix typos. Alexandre Duret-Lutz 2015-05-10 21:29:44 +02:00
  • 6bc2fa2431 hoa: add a stutter-sensitive property Alexandre Duret-Lutz 2015-05-10 16:54:44 +02:00
  • fe2fc88fc6 bin: add a --check option for automata outputs Alexandre Duret-Lutz 2015-05-10 16:30:12 +02:00
  • fa37bc5f72 postproc: do not simplify BA via transitions-based simulation Alexandre Duret-Lutz 2015-05-04 22:34:11 +02:00
  • e83bfd37a4 hoa: fix segfault when input has initial alternation Alexandre Duret-Lutz 2015-05-04 22:03:08 +02:00
  • a4b63e8e7f dot: heuristic to switch between circles and ellipses Alexandre Duret-Lutz 2015-04-28 18:22:08 +02:00
  • 8aa88c2951 dot: --dot=B to use bullets for all automata but Büchi and co-Büchi Alexandre Duret-Lutz 2015-04-28 17:27:22 +02:00
  • 51309cf742 dot: --dot=1 to ignore names and force numbered states Alexandre Duret-Lutz 2015-04-28 16:45:57 +02:00
  • b1cdab6f95 * src/twaalgos/remfin.cc: Fix comment. Alexandre Duret-Lutz 2015-04-27 17:21:26 +02:00
  • c0bbabc400 autfilt: -uc should count the number of non-isomorphic automata Alexandre Duret-Lutz 2015-04-28 16:12:13 +02:00
  • 5bfed246f9 hoaparse: make it possible to read from a string Alexandre Duret-Lutz 2015-04-27 00:11:29 +02:00
  • 528cc04cca Update documentation. Etienne Renault 2015-04-23 19:48:08 +02:00
  • 5f4b7e1f3f Remove all cvsignore files. Etienne Renault 2015-04-23 10:46:00 +02:00
  • a14518e103 Fix unused parameter. Etienne Renault 2015-04-23 11:07:10 +02:00
  • 66bd8f34db Merge kripketest, graphtest and ltltest into tests Etienne Renault 2015-04-23 10:08:45 +02:00
  • bd57f7a991 Rename tgbatest into tests. Etienne Renault 2015-04-23 09:46:49 +02:00
  • 8c4a3c0125 Ensure that all tests have different names. Etienne Renault 2015-04-22 21:47:52 +02:00
  • 7757d44ee9 bddprint: remove some never used functions Alexandre Duret-Lutz 2015-04-24 09:11:25 +02:00
  • 65c0cb48fc tmpfile: fix out-of-memory check Alexandre Duret-Lutz 2015-04-24 08:43:22 +02:00
  • 340557a12d remove some unused variables Alexandre Duret-Lutz 2015-04-24 08:39:23 +02:00
  • 967f9e8cf1 fix some cppcheck errors Alexandre Duret-Lutz 2015-04-23 23:45:36 +02:00
  • c829cbbadf get rid of tgta.cc Alexandre Duret-Lutz 2015-04-23 23:21:56 +02:00
  • a06ae1e97e get rid of the deprecated std::auto_ptr Alexandre Duret-Lutz 2015-04-23 18:20:06 +02:00
  • e201c3c9da ltsmin: do not install the library Alexandre Duret-Lutz 2015-04-23 17:27:22 +02:00
  • 7770572c89 debian: fix two lintian errors Alexandre Duret-Lutz 2015-04-23 17:12:27 +02:00
  • e07c70577a * NEWS: Update to mention TωA. Alexandre Duret-Lutz 2015-04-22 19:27:08 +02:00
  • 5e67d28c8f * HACKING: Update paragraph about LTO. Alexandre Duret-Lutz 2015-04-22 19:26:45 +02:00
  • de529df59f rename src/tgbaalgos/ as src/twaalgos/ Alexandre Duret-Lutz 2015-04-22 17:52:27 +02:00
  • 703fbd0e99 rename tgba files as twa Alexandre Duret-Lutz 2015-04-21 20:03:06 +02:00
  • 8839f50a0f rename Doxygen groups Alexandre Duret-Lutz 2015-04-21 19:55:37 +02:00
  • 03f78ee85a Rename tgba_mask and tgba_mask_keep as twa_mask and twa_mask_keep Alexandre Duret-Lutz 2015-04-21 19:52:35 +02:00
  • 5301fce3bf rename tgba_proxy into twa_proxy Alexandre Duret-Lutz 2015-04-21 19:50:48 +02:00
  • 2648ea170f rename tgba_graph_state and tgba_graph_trans_data as twa_... Alexandre Duret-Lutz 2015-04-21 19:41:09 +02:00
  • 8520c4c330 rename tgba_ptr into twa_ptr Alexandre Duret-Lutz 2015-04-21 19:38:09 +02:00
  • 5d9778474f rename tgba_succ_iterator as twa_succ_iterator Alexandre Duret-Lutz 2015-04-21 19:34:51 +02:00
  • c856933099 rename tgba_product as twa_product Alexandre Duret-Lutz 2015-04-21 19:24:49 +02:00
  • e0bd0ad4c0 rename tgba_digraph as twa_graph Alexandre Duret-Lutz 2015-04-21 19:13:55 +02:00
  • c2ae99e779 rename the spot::tgba class as spot::twa Alexandre Duret-Lutz 2015-04-21 18:58:22 +02:00
  • 8248072057 ltlfilt: add a --define option Alexandre Duret-Lutz 2015-04-22 13:54:06 +02:00
  • 65a729ab3d Add remove_fin Python binding. Etienne Renault 2015-04-20 20:28:10 +02:00
  • f067dd7871 Add setup method for spot. Etienne Renault 2015-04-20 11:28:04 +02:00
  • d55c15baf2 Use bdd dictionnary during translation. Etienne Renault 2015-04-20 11:24:39 +02:00
  • 0ab745be9c Ignore difference in graphviz versions. Etienne Renault 2015-04-20 11:18:33 +02:00