Commit graph

  • b521fef226 simulation: do not create scc_info Alexandre Duret-Lutz 2017-10-07 13:10:03 +02:00
  • da65479696 Bump version to 2.4.1.dev Alexandre Duret-Lutz 2017-10-18 14:45:21 +02:00
  • 308415f88a document the recent changes to implication rules Alexandre Duret-Lutz 2017-10-17 17:58:59 +02:00
  • fcccd5f425 ltlcross: add support for --reference translators Alexandre Duret-Lutz 2017-10-15 19:16:12 +02:00
  • 77c0e76258 org: fix the example for ltlcross --verbose Alexandre Duret-Lutz 2017-10-15 18:48:00 +02:00
  • ddaaf2c1c8 man: mention ltlsynt in spot(7) Alexandre Duret-Lutz 2017-10-15 11:21:13 +02:00
  • ba897bc3eb man: add missing crossrefs in spot(7) Alexandre Duret-Lutz 2017-10-15 11:15:53 +02:00
  • 183ec1fb4e ltlcross, autcross, ltldo: support --fail-on-timeout Alexandre Duret-Lutz 2017-10-15 10:44:26 +02:00
  • 0a2bca1377 simplify: improve the logic of some implication checks Alexandre Duret-Lutz 2017-10-11 21:47:31 +02:00
  • 689aa7fdc0 translate: add support for -x tls-impl=N Alexandre Duret-Lutz 2017-10-11 22:19:43 +02:00
  • 9b18729721 stutter: detect stutter-invariance at the state level Alexandre Duret-Lutz 2017-10-10 21:11:54 +02:00
  • b4963a7a6c genaut: fix ks_nca Alexandre Duret-Lutz 2017-10-11 14:35:23 +02:00
  • 4fa24a7ddd simulation: do not create scc_info Alexandre Duret-Lutz 2017-10-07 13:10:03 +02:00
  • 9ca5b8c2f1 scc_info: add ways to speedup scc_info Alexandre Duret-Lutz 2017-04-11 15:27:49 +02:00
  • 11704d31eb scc_info: improve split_on_sets Alexandre Duret-Lutz 2017-05-10 16:53:22 +02:00
  • 33af116fb8 ltldo: add support for -n Alexandre Duret-Lutz 2017-10-05 17:17:57 +02:00
  • 584430803d Merge branch 'master' into next Alexandre Duret-Lutz 2017-10-05 16:00:07 +02:00
  • 5c22db3c73 Release Spot 2.4.1 Alexandre Duret-Lutz 2017-10-05 15:49:43 +02:00
  • d2c4e596d1 org: fix the dot2tex example Alexandre Duret-Lutz 2017-10-05 15:44:14 +02:00
  • 89c312cb57 * HACKING, doc/tl/tl.tex, spot/tl/formula.hh: Typos Florian Perlié-Long 2017-10-03 08:57:42 +02:00
  • 7b6346d38d Typos Maximilien Colange 2017-10-02 10:58:30 +02:00
  • 0f023bd0fe * HACKING, doc/tl/tl.tex, spot/tl/formula.hh: Typos Florian Perlié-Long 2017-10-03 08:57:42 +02:00
  • d9d9288132 Typos Maximilien Colange 2017-10-02 10:58:30 +02:00
  • 7e394506b6 simulation: incorrect setting of non-deterministic property Alexandre Duret-Lutz 2017-09-28 20:38:13 +02:00
  • 7987d71ae8 * spot/twaalgos/totgba.cc: Typos in comment. Alexandre Duret-Lutz 2017-09-26 22:27:35 +02:00
  • bef58b4169 formula: fix building of {a->c[*]} Alexandre Duret-Lutz 2017-09-26 17:30:54 +02:00
  • 32087f29ad streett_to_generalized_buchi: fix incorrect algorithm Alexandre Duret-Lutz 2017-09-26 17:17:17 +02:00
  • cfa80ed842 tests: avoid some superfluous calls to remove_alternation() Alexandre Duret-Lutz 2017-09-25 10:54:09 +02:00
  • f45112a235 Fix a bug in scc_info, and clarify documentation Maximilien Colange 2017-09-25 14:12:12 +02:00
  • cdfe78f178 twa_graph: do not order BDDs by IDs in merge_edges() Alexandre Duret-Lutz 2017-09-24 16:06:41 +02:00
  • bd34f3c629 postproc: fix a comment Alexandre Duret-Lutz 2017-09-24 14:41:17 +02:00
  • 86560f6bd7 typos Alexandre GBAGUIDI AISSE 2017-05-12 22:48:11 +02:00
  • 697c94605f Fix: Remove SBAcc option in bin/ltlfilt Alexandre GBAGUIDI AISSE 2017-09-19 14:47:31 +01:00
  • f0dc9d44c9 tests: speed up two slow tests Alexandre Duret-Lutz 2017-09-29 10:50:58 +02:00
  • 900b344c9a degen: detect superfluous SCCs and remove them Alexandre Duret-Lutz 2017-09-28 21:54:49 +02:00
  • ce5e3b654f simulation: incorrect setting of non-deterministic property Alexandre Duret-Lutz 2017-09-28 20:38:13 +02:00
  • a13a4e7d23 remove universal transitions on the fly Thibaud Michaud 2017-02-15 00:34:33 +01:00
  • a0e89652b6 * NEWS: add tools for parity automata Laurent XU 2017-09-27 15:17:18 +02:00
  • c379acad8a * spot/twaalgos/totgba.cc: Typos in comment. Alexandre Duret-Lutz 2017-09-26 22:27:35 +02:00
  • a2cbf0af3a sanity: also check the 80-column limit in bin Alexandre Duret-Lutz 2017-09-26 21:46:42 +02:00
  • c473e4ca0b ltlsynt: handle --algo with XARGMATCH Alexandre Duret-Lutz 2017-09-26 21:44:37 +02:00
  • 69daf9c261 bin: make sure that all options are in a named section Alexandre Duret-Lutz 2017-09-26 21:28:16 +02:00
  • 002e6ed96b formula: fix building of {a->c[*]} Alexandre Duret-Lutz 2017-09-26 17:30:54 +02:00
  • f81fb31136 streett_to_generalized_buchi: fix incorrect algorithm Alexandre Duret-Lutz 2017-09-26 17:17:17 +02:00
  • 210046e8cd tests: avoid some superfluous calls to remove_alternation() Alexandre Duret-Lutz 2017-09-25 10:54:09 +02:00
  • 2697fcddbf Fix a bug in scc_info, and clarify documentation Maximilien Colange 2017-09-25 14:12:12 +02:00
  • d6ae7af5f5 ltlsynt: translate winning strategy to AIGER Thibaud Michaud 2017-09-14 17:02:21 +02:00
  • 601e1405de parity game: compute winning strategy Thibaud Michaud 2017-05-02 13:59:00 +02:00
  • f414e9f5f2 parity game: add Zielonka's recursive algorithm Thibaud Michaud 2017-09-10 22:54:24 +02:00
  • 0821c97eb8 add ltlsynt executable Thibaud Michaud 2017-09-10 22:47:50 +02:00
  • 7a11842613 parity: add spot::parity_product_or() Laurent XU 2016-07-04 19:22:47 +02:00
  • 192fb6c1e7 parity: merge states having same cleaned matrices in parity_product Laurent XU 2017-03-29 00:49:22 +02:00
  • cb7e43cb7d parity: remove history matrices in parity_product() Laurent XU 2016-07-07 18:13:45 +02:00
  • b92320cc33 parity: add spot::parity_product() Laurent XU 2017-02-15 00:25:11 +01:00
  • 3e650f18d9 parity: add spot::cleanup_parity_acceptance() Laurent XU 2017-02-15 00:16:35 +01:00
  • 0bf0a99d6d parity: add spot::colorize_parity() Laurent XU 2016-06-01 14:34:19 +02:00
  • 27982fb80f parity: add spot::change_parity() Laurent XU 2016-06-01 14:14:13 +02:00
  • b7ef7c55d7 misc: add spot::is_colored() Laurent XU 2017-03-22 18:01:37 +01:00
  • 5e5a69488e twa_graph: do not order BDDs by IDs in merge_edges() Alexandre Duret-Lutz 2017-09-24 16:06:41 +02:00
  • 2bca21f7f8 postproc: fix a comment Alexandre Duret-Lutz 2017-09-24 14:41:17 +02:00
  • 1689c08e09 genltl: add a new family from SYNTCOMP'2017 Maximilien Colange 2017-09-22 10:35:24 +02:00
  • 96974f7c97 bin/ltlfilt: Use is_persistence() and is_recurrence() Alexandre GBAGUIDI AISSE 2017-07-28 13:49:11 +02:00
  • c827f75c37 hierarchy: Add is_persistence() and make is_recurrence() use it Alexandre GBAGUIDI AISSE 2017-07-28 13:28:09 +02:00
  • e59274b609 hierarchy: Make is_recurrence() public Alexandre GBAGUIDI AISSE 2017-07-28 10:57:25 +02:00
  • 8cf542644c ltlfilt: Add %r and %R format options Alexandre GBAGUIDI AISSE 2017-07-24 17:35:39 +02:00
  • ad9bc644ba misc/timer: Gather handling of %r and %R options Alexandre GBAGUIDI AISSE 2017-07-24 17:27:23 +02:00
  • 302095ff9e typos Alexandre GBAGUIDI AISSE 2017-05-12 22:48:11 +02:00
  • 8ae10f744f twaalgos/cobuchi: Add dnf_to_dca() Alexandre GBAGUIDI AISSE 2017-06-17 22:16:22 +02:00
  • 5f6a71d27a twaalgos/cobuchi: Add breakpoint construction and nsa_to_dca() Alexandre GBAGUIDI AISSE 2017-06-17 22:04:21 +02:00
  • f2616069be twaalgos/cobuchi: Add dnf_to_nca() method Alexandre GBAGUIDI AISSE 2017-06-17 21:31:43 +02:00
  • 50e99cdca7 twaalgos/totgba: Add dnf_to_streett() method Alexandre GBAGUIDI AISSE 2017-06-17 21:06:31 +02:00
  • cf18c06940 twaalgos/cobuchi: Add nsa_to_nca() Alexandre GBAGUIDI AISSE 2017-06-17 19:33:26 +02:00
  • 37c1a19b39 twaalgos/scc_info: Add states_on_acc_cycle_of() method Alexandre GBAGUIDI AISSE 2017-06-17 19:27:10 +02:00
  • 0957317ad7 spot/twa: Add methods to set co-Büchi acceptance Alexandre GBAGUIDI AISSE 2017-06-17 19:23:38 +02:00
  • 75d9e5f624 Fix: Remove SBAcc option in bin/ltlfilt Alexandre GBAGUIDI AISSE 2017-09-19 14:47:31 +01:00
  • bd5c6920b1 Use clearer names for three methods of spot::scc_info Maximilien Colange 2017-09-14 10:32:36 +02:00
  • 7eb50bc1f8 genltl: add 4 new families from Müller & Sickert (GandALF'17) Alexandre Duret-Lutz 2017-09-15 21:47:58 +02:00
  • c704c3b019 bin: fix some --help typos Alexandre Duret-Lutz 2017-09-07 15:55:34 +02:00
  • 1941bac22c org: improve dot2tex conversion to png Alexandre Duret-Lutz 2017-09-06 11:18:34 +02:00
  • 86e61089ea * tests/core/dot2tex.test: Work around dot2tex 2.9.0. Alexandre Duret-Lutz 2017-09-06 11:10:22 +02:00
  • bfe5753bf9 * NEWS, configure.ac: Bump version to 2.4.0.dev. Alexandre Duret-Lutz 2017-09-06 11:05:34 +02:00
  • 80621557b2 Release Spot 2.4 Alexandre Duret-Lutz 2017-09-05 21:08:48 +02:00
  • f3ef225334 * NEWS: Add a missing entry. Alexandre Duret-Lutz 2017-09-05 19:08:51 +02:00
  • ad3588420c fix typos and indentation Clément Gillard 2017-04-18 15:19:38 +02:00
  • 552afb9d55 * NEWS: Some typos en cleanup. Alexandre Duret-Lutz 2017-09-05 11:23:23 +02:00
  • bc626788af dot: make 'x' compatible with 'b'/'r'/'R' Alexandre Duret-Lutz 2017-09-04 21:40:22 +02:00
  • 290d7b56fb * doc/org/oaut.org: Missing word. Alexandre Duret-Lutz 2017-09-04 19:57:40 +02:00
  • e452e09ff7 bin: make --stats and --format synonyms Alexandre Duret-Lutz 2017-09-04 17:42:13 +02:00
  • f726152ebd org: fix one example Alexandre Duret-Lutz 2017-09-04 17:23:07 +02:00
  • e7df182a30 gen: rename KS_COBUCHI to KS_NCA for consistency Alexandre Duret-Lutz 2017-09-03 15:36:08 +02:00
  • 6cd6802ace simplify: rewrite GF(a & Fb) as G(Fa & Fb) Alexandre Duret-Lutz 2017-09-02 19:54:07 +02:00
  • e8527d5ae9 Improve simplification of expr[*0..1] Alexandre Duret-Lutz 2017-09-02 16:35:18 +02:00
  • 190d4cfaf1 ltl2tgba_fm: implement a small optimization Alexandre Duret-Lutz 2017-09-02 14:48:52 +02:00
  • 42abcf8559 genltl: add --gxf-and and --fxg-or Alexandre Duret-Lutz 2017-09-02 11:51:54 +02:00
  • 646c5170ed simplify: some new simplification rules Alexandre Duret-Lutz 2017-09-02 09:30:26 +02:00
  • cd6f1c2c3e get rid of some unnecessary code Alexandre Duret-Lutz 2017-09-01 20:58:35 +02:00
  • 15cc7301cc remove_fin: apply Rabin conversion before Streett Alexandre Duret-Lutz 2017-09-01 20:51:42 +02:00
  • f7ba490898 streett_to_generalize_buchi: fix handling of SCCs without Fin Alexandre Duret-Lutz 2017-09-01 20:22:21 +02:00
  • 7b9cedc697 common_trans: leave the shell handle commands containing = in arg0 Alexandre Duret-Lutz 2017-09-01 20:20:36 +02:00
  • fbb9e4374e dot: add x option for dot2tex Alexandre Duret-Lutz 2017-08-31 18:56:53 +02:00