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

Commit graph

  • 9f6924ccfb twaalgos: add many guards against alternation Alexandre Duret-Lutz 2016-12-24 18:31:19 +01:00
  • 87c9d6f039 ltlcross: add support for alternating automata Alexandre Duret-Lutz 2016-12-23 15:27:39 +01:00
  • 543e0db9a0 stats: add a variant for twa_graph_ptr Alexandre Duret-Lutz 2016-12-22 19:39:03 +01:00
  • 64fa6c0026 remfin: ignore unreachable states in remove_fin_weak() Alexandre Duret-Lutz 2016-12-22 18:47:46 +01:00
  • 326431fd28 * NEWS: Describe experimental alternation support. Alexandre Duret-Lutz 2016-12-22 14:01:13 +01:00
  • fa06cfa303 alternation: implement remove_alternation() for weak alt automata Alexandre Duret-Lutz 2016-12-02 17:56:47 +01:00
  • 582d455c23 twa: add support for very-weak property Alexandre Duret-Lutz 2016-12-01 18:27:54 +01:00
  • a4ce999402 sccinfo: adjust to work with alternating automata Alexandre Duret-Lutz 2016-12-01 16:05:27 +01:00
  • d2f471da06 parseaut: handle alternating automata with many universal init states Alexandre Duret-Lutz 2016-11-28 11:23:01 +01:00
  • 27ab631cdc alternation: add a states_and algorithm Alexandre Duret-Lutz 2016-11-27 22:14:11 +01:00
  • 48c812a595 twa_graph: add support for universal initial states Alexandre Duret-Lutz 2016-11-30 14:22:44 +01:00
  • d5c9c34514 dot: add support for alternating automata Alexandre Duret-Lutz 2016-11-25 17:17:22 +01:00
  • e620368696 parseaut: preliminary support for reading alternating automata Alexandre Duret-Lutz 2016-11-24 21:49:30 +01:00
  • 56df459c75 print_hoa: add support for universal branches Alexandre Duret-Lutz 2016-11-24 21:13:13 +01:00
  • 6aad559c29 twa_graph: add basic support for alternation Alexandre Duret-Lutz 2016-11-24 17:56:59 +01:00
  • 4903f086e3 graph: replace the existing "alternating" interface Alexandre Duret-Lutz 2016-11-23 21:08:11 +01:00
  • dcd21aaabf org: call set_init_state() in tut22 Alexandre Duret-Lutz 2016-12-25 12:14:17 +01:00
  • 34ac6f08cc org: ltlcross supports any acceptance condition Alexandre Duret-Lutz 2016-12-22 21:18:57 +01:00
  • 8e8c6a8cea org: support org >= 8.3 Alexandre Duret-Lutz 2016-12-23 15:26:34 +01:00
  • 2f02911e1a copy: improve documentation Alexandre Duret-Lutz 2016-12-24 18:29:13 +01:00
  • f5a76baa33 strength: improve doc Alexandre Duret-Lutz 2016-12-16 13:43:28 +01:00
  • f1922325ed * AUTHORS: Add Maximilien. Alexandre Duret-Lutz 2016-12-16 08:09:20 +01:00
  • 975ec6ff81 Merge branch 'master' into next Alexandre Duret-Lutz 2016-12-16 07:03:18 +01:00
  • f8f7c9a537 bump version number Alexandre Duret-Lutz 2016-12-16 06:58:46 +01:00
  • 574f47c366 Release Spot 2.2.2 Alexandre Duret-Lutz 2016-12-16 06:50:59 +01:00
  • 38fdb40eaf spotcgi: correctly kill ltl3ba on timeout Alexandre Duret-Lutz 2016-12-15 13:35:20 +01:00
  • cd34827510 spotcgi: correctly kill ltl3ba on timeout Alexandre Duret-Lutz 2016-12-15 13:35:20 +01:00
  • 55eae0d8bc * spot/twa/twa.hh (twa_succ_iterable): Mark move ctor as noexcept. Alexandre Duret-Lutz 2016-12-15 11:11:59 +01:00
  • 05f8333e76 Add an option to enable C++14. Maximilien Colange 2016-12-13 17:42:07 +01:00
  • 878649c823 [buddy] Add an option to enable C++14. Maximilien Colange 2016-12-13 17:40:55 +01:00
  • 114f7f1200 Default emptiness check is the new version of Couvreur. Maximilien Colange 2016-11-25 13:42:47 +01:00
  • 1a08eca840 Add a new, parameterized, version of the Couvreur emptiness check. Maximilien Colange 2016-11-25 11:52:11 +01:00
  • f0416b3f3c ltsmin: workaround spurious gcc-snapshot warning Alexandre Duret-Lutz 2016-12-10 20:21:29 +01:00
  • 15709084b8 ltlf: ensure alive holds initially Alexandre Duret-Lutz 2016-12-09 21:37:15 +01:00
  • 413eab1d32 ltlf: ensure alive holds initially Alexandre Duret-Lutz 2016-12-09 21:37:15 +01:00
  • 7824005d3e install back the safety check of includes.test Alexandre Duret-Lutz 2016-12-02 13:39:04 +01:00
  • 0ab8dc06c4 install back the safety check of includes.test Alexandre Duret-Lutz 2016-12-02 13:39:04 +01:00
  • 2198543a7a parseaut: diagnose invalid acceptance terms Alexandre Duret-Lutz 2016-12-01 15:51:55 +01:00
  • 38b82dba9b ltsmin: use any installed libltdl Alexandre Duret-Lutz 2016-11-28 17:32:40 +01:00
  • 3d726fccb2 parseaut: diagnose invalid acceptance terms Alexandre Duret-Lutz 2016-12-01 15:51:55 +01:00
  • f3b95a8a11 tests: recognize ./run jupyter Alexandre Duret-Lutz 2016-12-01 15:21:43 +01:00
  • e8a3f62491 Fix a sanity check. Maximilien Colange 2016-12-01 11:51:49 +01:00
  • 9a1e411502 Properly time computations of accepting runs in randtgba. Maximilien Colange 2016-12-01 10:49:18 +01:00
  • 2b07326217 twa_graph: simplify two precondition checks Alexandre Duret-Lutz 2016-11-29 22:26:35 +01:00
  • 034620c521 graph: fix internal iterator constness Alexandre Duret-Lutz 2016-11-23 21:06:42 +01:00
  • 5841af026a sccinfo: simplify initial code Alexandre Duret-Lutz 2016-11-30 14:25:35 +01:00
  • 5ca1281e36 tests: speed up recuc.test and reducpsl.test Alexandre Duret-Lutz 2016-11-29 15:54:08 +01:00
  • 7e5b336f16 tests: divide the run time of parse.test by 20 Alexandre Duret-Lutz 2016-11-29 11:51:34 +01:00
  • ad51525608 tests: divide the run time of tostring.test by 40 Alexandre Duret-Lutz 2016-11-29 11:33:56 +01:00
  • b3ee68310f Automata with no state are no longer allowed. Maximilien Colange 2016-11-25 13:42:13 +01:00
  • da6fc955a3 debian: add lintian-overrides for the Doxygen doc Alexandre Duret-Lutz 2016-11-28 18:00:38 +01:00
  • 51a683c23f debian: depend on libjs-jquery Alexandre Duret-Lutz 2016-11-28 17:45:15 +01:00
  • b1f9081761 ltsmin: use any installed libltdl Alexandre Duret-Lutz 2016-11-28 17:32:40 +01:00
  • 341eeb2ba1 strength: fix is_terminal() Alexandre Duret-Lutz 2016-11-28 16:19:05 +01:00
  • 9bc978a90f strength: fix is_terminal() Alexandre Duret-Lutz 2016-11-28 16:19:05 +01:00
  • 2fbc75f439 New macro to downcast shared pointers. Maximilien Colange 2016-11-24 16:24:29 +01:00
  • 5952392494 Use the [[deprecated]] standard attribute when possible. Maximilien Colange 2016-11-24 15:06:46 +01:00
  • 22292e6058 sanity: do not check source files in *.dir/* Alexandre Duret-Lutz 2016-11-24 20:48:28 +01:00
  • 1afb76a630 split ltsmin/check.test in three files Alexandre Duret-Lutz 2016-11-24 10:52:37 +01:00
  • f868e0cea6 scc_filter: remove left-over print Alexandre Duret-Lutz 2016-11-24 07:31:32 +01:00
  • e1d0c07d4b * NEWS, configure.ac: Bump version number. Alexandre Duret-Lutz 2016-11-21 11:09:51 +01:00
  • dc4a477172 lts-min: fix loading of spins models Alexandre Duret-Lutz 2016-11-24 10:26:46 +01:00
  • e2b0b9d989 scc_filter: remove left-over print Alexandre Duret-Lutz 2016-11-24 07:31:32 +01:00
  • fd2f79200f Improve error messages when loading compiled models. * spot/ltsmin/ltsmin.cc: Improve error messages. Maximilien Colange 2016-11-22 10:46:49 +01:00
  • c9aabcddab Add support to load GAL models. * spot/ltsmin/ltsmin.cc: Handle GAL models. * tests/Makefile.am: Test the new feature. * tests/ltsmin/check.test: Also check GAL. * tests/ltsmin/beem-peterson.4.gal: A new GAL model for tests. * tests/ltsmin/finite.gal: A new GAL model for tests. * tests/ltsmin/finite3.test: A new test for GAL. Maximilien Colange 2016-11-22 10:44:20 +01:00
  • ec83e60bb9 bitvec: remove useless methods Etienne Renault 2016-11-22 11:35:47 +01:00
  • 43ec36cda7 Prefer emplace_back to push_back Etienne Renault 2016-11-22 10:21:08 +01:00
  • ef214b2c42 * NEWS, configure.ac: Bump version number. Alexandre Duret-Lutz 2016-11-21 11:09:51 +01:00
  • 9cf8535578 Release Spot 2.2.1 Alexandre Duret-Lutz 2016-11-21 09:00:51 +01:00
  • 4e1c8dfd74 add test-case for bdd_noderesize Alexandre Duret-Lutz 2016-11-19 14:49:46 +01:00
  • 38c4fc8812 [buddy] fix bdd_noderesize Alexandre Duret-Lutz 2016-11-19 14:48:18 +01:00
  • 88a8a3efbe * NEWS: Typo. Alexandre Duret-Lutz 2016-11-14 20:39:35 +01:00
  • 5376466f43 * configure.ac, NEWS: Bump version number. Alexandre Duret-Lutz 2016-11-14 10:15:38 +01:00
  • dd960dc71c Release Spot 2.2 Alexandre Duret-Lutz 2016-11-14 06:02:13 +01:00
  • 4bd04fc65c * doc/org/oaut.org: Shorten a long line. Alexandre Duret-Lutz 2016-11-13 21:58:37 +01:00
  • e91073a9f1 org: document %r and %R Alexandre Duret-Lutz 2016-11-13 14:30:12 +01:00
  • c225747749 twa: introduce intersects() and friends Alexandre Duret-Lutz 2016-11-13 11:23:12 +01:00
  • bdad288c70 * spot/twa/twa.hh: Typos. Alexandre Duret-Lutz 2016-11-13 09:36:06 +01:00
  • 937011692c * NEWS: Update for upcoming release. Alexandre Duret-Lutz 2016-11-12 10:10:50 +01:00
  • dce83a649b improve doc for purge_unreachable_states and purge_dead_states Alexandre Duret-Lutz 2016-11-11 15:38:25 +01:00
  • ee85cf7759 * tests/python/ipnbdoctest.py: Ignore more SVG differences. Alexandre Duret-Lutz 2016-11-11 15:27:36 +01:00
  • 85f6e0e158 scc_filter: preserve state names and highlighted states Alexandre Duret-Lutz 2016-11-11 15:17:34 +01:00
  • dd706d7847 twa: do not set prop_state_acc in set_acceptance Alexandre Duret-Lutz 2016-11-11 14:05:58 +01:00
  • a70589fe13 remfin: fix handling of weak automata Alexandre Duret-Lutz 2016-11-11 12:30:13 +01:00
  • 49266dee7f parseaut: do not close fd or stdin Alexandre Duret-Lutz 2016-11-11 12:24:15 +01:00
  • a0956d25b6 tests: do not hide stderr in ipnbdoctest Alexandre Duret-Lutz 2016-11-10 23:18:57 +01:00
  • 0ac14e9ca2 [buddy] avoid costly calls to setjmp() when BDD_REORDER_NONE Alexandre Duret-Lutz 2016-11-09 11:03:24 +01:00
  • 2e6297c26a ltl2tgba_fm: simplify three bdd operations Alexandre Duret-Lutz 2016-11-09 07:29:59 +01:00
  • 84b16aa6bd [buddy] consolidate shortcuts for binary operation Alexandre Duret-Lutz 2016-11-09 07:16:47 +01:00
  • 75c33defb3 attempt to mitigate our Debian build failures Alexandre Duret-Lutz 2016-11-08 19:07:12 +01:00
  • 5a862295d3 [buddy] improve initialization of bddnode Alexandre Duret-Lutz 2016-11-08 12:00:24 +01:00
  • 278b41f4bb ltldo: rename %R as %# Alexandre Duret-Lutz 2016-11-08 14:56:38 +01:00
  • 600b1f7e5c bin: adjust %R to work with Mingw Alexandre Duret-Lutz 2016-11-08 14:23:18 +01:00
  • 6ed380709d spot: Add %R, %[..]R common option. Alexandre GBAGUIDI AISSE 2016-10-24 17:46:26 +02:00
  • 3eafbc823c debian: update build-depends for new Jupyter version Alexandre Duret-Lutz 2016-11-06 09:59:23 +01:00
  • 939e713e09 tests: update to work with Jupyter 4.2 Alexandre Duret-Lutz 2016-11-05 23:14:21 +01:00
  • 0b7b03c7d2 parsetl: flush the errors Alexandre Duret-Lutz 2016-11-05 19:28:22 +01:00
  • 2e69e04583 from_ltlf: new LTL transformation. Alexandre Duret-Lutz 2016-11-05 17:52:38 +01:00
  • fe1f754d2e * doc/tl/tl.tex: Typo. Alexandre Duret-Lutz 2016-11-05 12:11:00 +01:00
  • 3f64e9723f determinize: call bdd_implies less often Alexandre Duret-Lutz 2016-11-01 09:08:05 +01:00