Commit graph

  • f7c495ad12 debian: do not compress notebooks Alexandre Duret-Lutz 2016-02-16 20:52:51 +01:00
  • 9692d734a9 cleanup ltsmin bindings Alexandre Duret-Lutz 2016-02-16 19:08:28 +01:00
  • 9b5a763538 sanity: fix race conditions in the test suite Alexandre Duret-Lutz 2016-02-16 17:29:06 +01:00
  • 3a3913cf50 otf_product: fix deletion of iter_cache_ Alexandre Duret-Lutz 2016-02-16 17:22:36 +01:00
  • e86370f894 Turn on some new warnings from GCC 6.0 Alexandre Duret-Lutz 2016-02-16 16:04:03 +01:00
  • 7078ab0af9 satsolver: use precise fstream class for input or output Alexandre Duret-Lutz 2016-02-16 16:03:10 +01:00
  • 22af7aefdf python: report dot errors Alexandre Duret-Lutz 2016-02-16 14:34:57 +01:00
  • c093b7b78f python: move auxiliary functions in a separate module Alexandre Duret-Lutz 2016-02-16 12:56:20 +01:00
  • 5d272fd256 use more override and final keywords Alexandre Duret-Lutz 2016-02-15 22:43:23 +01:00
  • 1ae0600cae ltlcross: add option --determinize Alexandre Duret-Lutz 2016-02-15 18:37:45 +01:00
  • 26d7264717 org: fix two links Alexandre Duret-Lutz 2016-02-15 14:33:51 +01:00
  • 199e5fd2e0 autfilt: implement an --ap=RANGE option Alexandre Duret-Lutz 2016-02-15 14:29:00 +01:00
  • beb435ebd8 * tests/core/.gitignore: Ignore safra. Alexandre Duret-Lutz 2016-02-15 14:16:27 +01:00
  • 52bf1da3c2 ltlfilt: support --ap=RANGE instead of --ap=N Alexandre Duret-Lutz 2016-02-15 14:14:18 +01:00
  • 1b12df46fe ltlfilt: replace --[b]size-max/min by --[b]size Alexandre Duret-Lutz 2016-02-15 13:44:51 +01:00
  • a3e0c8624e remove twa::compute_support_conditions Alexandre Duret-Lutz 2016-02-15 10:45:05 +01:00
  • 39b95474f8 remove twa::transition_annotation Alexandre Duret-Lutz 2016-02-15 10:27:37 +01:00
  • e1f5eb1fd6 doc: improve the twa class documentation Alexandre Duret-Lutz 2016-02-15 08:18:28 +01:00
  • ea348d8e80 * spot/twa/twa.hh: Fix doxygen comments. Alexandre Duret-Lutz 2016-02-14 21:02:39 +01:00
  • ee2d3aac71 Force cast to please clang on OSX Etienne Renault 2016-02-14 17:44:51 +01:00
  • 091251b5b7 Provide support for %dve and %require Etienne Renault 2016-02-13 18:50:15 +01:00
  • 369c2c537d org: mention the determinization on the main page Alexandre Duret-Lutz 2016-02-13 15:54:27 +01:00
  • f7b5dcf47d autfilt: add support for --are-equivalent Alexandre Duret-Lutz 2016-02-12 19:53:52 +01:00
  • b59ebdc40c * NEWS: typo Alexandre Duret-Lutz 2016-02-12 19:50:37 +01:00
  • 021921f0c3 autfilt: add --included-in filter Alexandre Duret-Lutz 2016-02-12 17:42:57 +01:00
  • 9799a6455e autfilt: complement of non-deterministic automata as well Alexandre Duret-Lutz 2016-02-12 17:00:20 +01:00
  • 6a662a6d8e get read of twa_safra_complement Alexandre Duret-Lutz 2016-02-12 15:06:34 +01:00
  • df0f99410c * NEWS: Summarize recent changes. Alexandre Duret-Lutz 2016-02-12 14:27:48 +01:00
  • b066c6f3f2 postproc: add fine-tuning options for determinization Alexandre Duret-Lutz 2016-02-10 23:04:43 +01:00
  • 8feab7e2bb postproc: more documentation Alexandre Duret-Lutz 2016-02-10 22:06:10 +01:00
  • 1e52d2a7a8 doc: more doc about determinization Alexandre Duret-Lutz 2016-02-10 17:47:17 +01:00
  • 0288aaa304 determinize: add tests for the bug Alexandre L fixed Alexandre Duret-Lutz 2016-02-10 09:51:10 +01:00
  • 0d9019ea39 python: fix translate's doc string Alexandre Duret-Lutz 2016-02-09 18:28:31 +01:00
  • 8a5f652384 determinize: Correct scc optimisation Alexandre Lewkowicz 2016-02-08 19:21:37 +01:00
  • 8568c3b423 postproc: integrate tgba_determinize() Alexandre Duret-Lutz 2016-02-06 14:15:16 +01:00
  • 03d9a7512a determinize: do not work on deterministic automata Alexandre Duret-Lutz 2016-02-06 12:10:53 +01:00
  • c18ee329fb determinize: rename the main function Alexandre Duret-Lutz 2016-02-06 11:35:32 +01:00
  • 4635ce44a9 determinize: add some doc Alexandre Duret-Lutz 2016-02-06 09:50:48 +01:00
  • 2853c4ca04 * tests/core/safra.cc (help): Simplify. Alexandre Duret-Lutz 2016-02-05 23:33:40 +01:00
  • 8e26852a1b determinize: remove superfluous options Alexandre Duret-Lutz 2016-02-05 23:28:10 +01:00
  • e0c2452534 determinize: hide private data structures Alexandre Duret-Lutz 2016-02-05 23:14:28 +01:00
  • f9252aa703 safra: rename as determinize Alexandre Duret-Lutz 2016-02-05 23:07:31 +01:00
  • cd71286fb5 safra: Add stutter-invarience optimisation Alexandre Lewkowicz 2016-02-05 15:42:22 +01:00
  • 1d68decaca safra: Add compute_succ function Alexandre Lewkowicz 2016-02-04 16:38:25 +01:00
  • be0e6bffcf safra: Build safra-state after each AP Alexandre Lewkowicz 2016-02-04 16:20:56 +01:00
  • dbd7740874 safra: Iterate on APs to compute successors Alexandre Lewkowicz 2016-02-04 16:03:47 +01:00
  • 8068cfad93 safra: Add complete option and rename files Alexandre Lewkowicz 2016-01-14 16:54:08 +01:00
  • f88154e507 safra: Add bisimulation optimisation Alexandre Lewkowicz 2015-11-11 17:40:18 +01:00
  • d15b5f43a6 safra: Fix properties and use new API Alexandre Lewkowicz 2015-11-09 17:45:21 +01:00
  • bb93f6e9af safra: Nodes are grouped by SCC Alexandre Lewkowicz 2015-09-24 14:53:53 +02:00
  • b59b31f806 safra: Give more explicit names to types Alexandre Lewkowicz 2015-09-24 07:40:40 +02:00
  • 18396e5973 safra: SSC based construction Alexandre Lewkowicz 2015-09-23 21:08:09 +02:00
  • 0cf83d7cbc safra: Update pretty printer function Alexandre Lewkowicz 2015-09-23 18:56:36 +02:00
  • 3bd95c32e7 safra: Remove paths when leaving an SCC Alexandre Lewkowicz 2015-09-22 14:06:39 +02:00
  • e8c428d0a3 safra: Edges to accepting SCC are accepting Alexandre Lewkowicz 2015-09-22 08:33:48 +02:00
  • f29de22b8a safra: Add bisimulation option Alexandre Lewkowicz 2015-06-06 18:41:59 +02:00
  • 64b27a9a26 safra: Add pretty printer for states Alexandre Lewkowicz 2015-05-30 12:41:35 +02:00
  • 64cdd1adc7 safra: Fix the nesting comparision function Alexandre Lewkowicz 2015-05-28 19:11:02 +02:00
  • ebe03cf3d0 safra: Fix nesting comparision Alexandre Lewkowicz 2015-05-28 10:53:48 +02:00
  • 8362bf3a5f safra: Ensure parity min even acceptance Alexandre Lewkowicz 2015-05-27 16:42:19 +02:00
  • d0d42f86f9 safra: Use sub-transitions during determinization Alexandre Lewkowicz 2015-05-25 18:24:39 +02:00
  • 8b1f9d3712 safra: Ensure automata is degeneralized Alexandre Lewkowicz 2015-05-25 13:12:32 +02:00
  • 20fc8b0269 safra: Use std::map to represent macrostates Alexandre Lewkowicz 2015-05-21 16:24:35 +02:00
  • 3ecdba6094 safra: Add a couple of tests Alexandre Lewkowicz 2015-05-19 16:40:55 +02:00
  • ef3143f048 safra: Output parity acceptance sets Alexandre Lewkowicz 2015-05-19 16:32:00 +02:00
  • f2fa92004c safra: handle single accepting set Alexandre Lewkowicz 2015-05-13 19:43:11 +02:00
  • 496083b14a safra: implement powerset construction Alexandre Lewkowicz 2015-05-08 09:01:34 +02:00
  • 064ccd5c05 fix paths mentioning buddy/src/.libs Alexandre Duret-Lutz 2016-02-12 14:02:47 +01:00
  • fbdd146565 simplify: add missing recursion Alexandre Duret-Lutz 2016-02-11 23:37:41 +01:00
  • 992c97151c ltldo, ltl2tgba: support %< and %> Alexandre Duret-Lutz 2016-02-11 18:30:48 +01:00
  • 86646ac31f bin: fix destruction order of global variables Alexandre Duret-Lutz 2016-02-10 19:12:48 +01:00
  • bceb54c80e * spot/ltsmin/ltsmin.cc (format_state): Thinko. Alexandre Duret-Lutz 2016-02-09 14:44:52 +01:00
  • a31793960f * tests/ltsmin/modelcheck.cc: Typo when printing accepting run. Alexandre Duret-Lutz 2016-02-09 14:33:56 +01:00
  • e146527852 twa_run: add a highlight method Alexandre Duret-Lutz 2016-02-06 17:10:55 +01:00
  • 77b0b5b3fe dot: add option C(COLOR) Alexandre Duret-Lutz 2016-02-05 18:56:08 +01:00
  • 23c2cbf46a python: highlighting functions for edges and states Alexandre Duret-Lutz 2016-02-05 17:29:30 +01:00
  • be4418257e * spot/twaalgos/dot.cc: Rename a variable. Alexandre Duret-Lutz 2016-02-05 15:58:41 +01:00
  • 348f7cce0b parseaut, dot: install a highlighting framework Alexandre Duret-Lutz 2016-02-04 23:02:28 +01:00
  • 91bb93eeaa parse_acc: cleanup error reporting Alexandre Duret-Lutz 2016-02-04 10:48:40 +01:00
  • 30b996460c doc: run Doxygen twice to work around its bugs Alexandre Duret-Lutz 2016-02-03 22:30:51 +01:00
  • d5bf95c5cb do not build ikwiad, randtgba, and modelcheck by default Alexandre Duret-Lutz 2016-02-03 22:08:02 +01:00
  • 8880578e0d * bench/emptchk/pml2tgba.pl: Fix to work with recent Spin. Alexandre Duret-Lutz 2016-02-03 22:07:21 +01:00
  • 22345d0c67 rename parse_print_test as kripkecat Alexandre Duret-Lutz 2016-02-03 21:19:30 +01:00
  • 1ca4204ccd Remove obsolete ACLOCAL_AMFLAGS definition. Alexandre Duret-Lutz 2016-02-03 16:51:24 +01:00
  • af96cbca83 * tests/python/ltsmin.ipynb: Erase the model file. Alexandre Duret-Lutz 2016-02-03 08:51:37 +01:00
  • 35c8beaa3c dot, hoa: enable "k" also for fair_kripke Alexandre Duret-Lutz 2016-02-03 08:46:50 +01:00
  • 2c67c68766 org: adjust PYTHONPATH after recent python changes Alexandre Duret-Lutz 2016-02-02 17:38:58 +01:00
  • aebe6593f9 twa: make acc_ private Alexandre Duret-Lutz 2016-02-02 16:55:51 +01:00
  • 681bb82b8e * doc/Doxyfile.in: Tweak two options. Alexandre Duret-Lutz 2016-02-02 16:55:27 +01:00
  • df9a8ad0d1 Add missing documentation in twa.hh Alexandre Duret-Lutz 2016-02-02 16:53:03 +01:00
  • 02b5460b91 dot, hoa: default to "k" for kripke structure Alexandre Duret-Lutz 2016-02-01 18:49:09 +01:00
  • a9b4560f3d dot: add option "k" Alexandre Duret-Lutz 2016-02-01 08:36:59 +01:00
  • 5a5f83f468 python: add missing bindings for twa_word and twa_run Alexandre Duret-Lutz 2016-01-31 21:05:44 +01:00
  • eb0a0b6b34 dot: use circles if state names are all short Alexandre Duret-Lutz 2016-01-29 10:53:38 +01:00
  • b11c07b351 dot: add a <N option Alexandre Duret-Lutz 2016-01-28 17:45:50 +01:00
  • 4571d6dd3a copy: rewrite as a BFS without using reachiter Alexandre Duret-Lutz 2016-01-28 15:37:00 +01:00
  • 9b95b697a5 twa: introduce the state_map template alias Alexandre Duret-Lutz 2016-01-28 13:15:48 +01:00
  • 6230f320bf python: fix installation Alexandre Duret-Lutz 2016-01-28 10:46:55 +01:00
  • c968e7b856 ltl2tgba_fm: fix setting of unambiguous property Alexandre Duret-Lutz 2016-01-26 19:32:26 +01:00
  • a3c2691632 debian: add missing file Alexandre Duret-Lutz 2016-01-26 16:00:14 +01:00