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

Commit graph

  • 62914059f7 Fix a race condition on the CGI script. Alexandre Duret-Lutz 2012-02-15 11:57:13 +01:00
  • 547715463a Fix a segfault reported by Etienne Renault using dve2check. Alexandre Duret-Lutz 2012-01-24 19:09:07 +01:00
  • 4b5734d8ec * NEWS: Add missing dates. Alexandre Duret-Lutz 2012-01-20 14:17:53 +01:00
  • bc66974bf2 * configure.ac, NEWS: Bump version to 0.8.2a. Alexandre Duret-Lutz 2012-01-19 19:24:57 +01:00
  • b01ce51e65 Release Spot 0.8.2. Alexandre Duret-Lutz 2012-01-19 19:22:45 +01:00
  • 15c2a9473e Small speedup in safra_tree::compare(). Alexandre Duret-Lutz 2012-01-18 19:52:21 +01:00
  • a9669d3d17 * NEWS: Mention the last two changes. Alexandre Duret-Lutz 2012-01-18 17:44:58 +01:00
  • 75032c9fc4 Implement a unicity table for states created by tgba_tba_proxy. Alexandre Duret-Lutz 2012-01-18 10:13:57 +01:00
  • 578c5894f5 Minor speedups in tgba_safra_complement(). Alexandre Duret-Lutz 2012-01-17 18:07:47 +01:00
  • ebfec98e31 * src/eltlparse/eltlparse.yy (realias): Add a useless return to fix a g++ warning. Alexandre Duret-Lutz 2012-01-18 10:42:37 +01:00
  • b4ed47129d * bench/ltlclasses/run: Typo in comment. Alexandre Duret-Lutz 2012-01-18 10:39:16 +01:00
  • 4b0a3a7a37 Make it possible not to build Python bindings. Alexandre Duret-Lutz 2012-01-17 14:33:21 +01:00
  • ebc92d4688 Fix position of the Send button with WebKit. Alexandre Duret-Lutz 2012-01-17 14:02:15 +01:00
  • 7854283593 * wrap/python/ajax/spot.py: Add a required "None" second argument to utime(). Alexandre Duret-Lutz 2012-01-17 13:27:09 +01:00
  • a5787937ef minimize_wdba() failed to fully minimize some automata. Alexandre Duret-Lutz 2012-01-17 12:11:33 +01:00
  • 2952daf0ba * NEWS: Update with recent fixes. Alexandre Duret-Lutz 2012-01-13 15:23:37 +01:00
  • c21e716893 Fix a 'make check' failure when valgrind is not installed. Alexandre Duret-Lutz 2012-01-13 13:51:42 +01:00
  • 89279d9829 Do use of tr1::unordered_map with G++ 4.0.0. Alexandre Duret-Lutz 2012-01-12 18:40:40 +01:00
  • 253e38ae7d * lrde-upload.sh: Retrieve the package version from configure.ac. Alexandre Duret-Lutz 2012-01-06 11:35:52 +01:00
  • 0ca40d72d7 Fix detection of the last iteration of minimize_dfa(). Ala-Eddine Ben-Salem 2012-01-05 19:16:44 +01:00
  • 984c715cc6 Fix computation of length of LTL formulas. Alexandre Duret-Lutz 2012-01-05 18:34:23 +01:00
  • 93f1009b75 * configure.ac, NEWS: Bump version to 0.8.1a. Alexandre Duret-Lutz 2011-12-18 13:38:38 +01:00
  • 64e0c65c7e Release Spot 0.8.1. Alexandre Duret-Lutz 2011-12-18 12:49:09 +01:00
  • e27a7899a3 * NEWS: Summarize recent fixes. Alexandre Duret-Lutz 2011-12-18 11:34:37 +01:00
  • 28b7c0858b Fix VPATH builds, now that hash.hh include _config.h Alexandre Duret-Lutz 2011-12-18 11:29:14 +01:00
  • e531da8d92 Perform WDBA minimization before degeneralization. Alexandre Duret-Lutz 2011-12-16 12:56:22 +01:00
  • 9679032510 Don't rely on the g++ version to include tr1/unordered_map and co. Alexandre Duret-Lutz 2011-12-14 16:51:35 +01:00
  • a804c88e1b Fix mkdir error in ajax/spot.in. Alexandre Duret-Lutz 2011-12-01 12:33:20 +01:00
  • 1e7cda5e05 Fix build on MacOS X. Alexandre Duret-Lutz 2011-11-29 20:32:08 +01:00
  • e5196a5943 * AUTHORS: Sort alphabetically. Alexandre Duret-Lutz 2011-11-28 18:40:37 +01:00
  • 6acf30b2ab Remove the old CGI interface. Alexandre Duret-Lutz 2011-11-28 18:17:50 +01:00
  • 6794b8570a Undocument `.' from the web interface. Alexandre Duret-Lutz 2011-11-28 17:56:46 +01:00
  • c905a71ab8 * NEWS, configure.ac: Bump version to 0.8a. Alexandre Duret-Lutz 2011-11-28 17:36:52 +01:00
  • d6959b4a46 Release Spot 0.8. Alexandre Duret-Lutz 2011-11-28 14:32:08 +01:00
  • 6b503d43a9 Remove spotref.pdf. Alexandre Duret-Lutz 2011-11-28 13:49:56 +01:00
  • 799ab14300 Fix some Doxygen errors. Alexandre Duret-Lutz 2011-11-28 13:37:14 +01:00
  • 11bb4c7789 Add more nodes when resizing BDD table. Alexandre Duret-Lutz 2011-11-13 13:14:39 +01:00
  • 5f689b5139 * NEWS: Mention the Kripke I/O. Alexandre Duret-Lutz 2011-11-28 10:38:54 +01:00
  • 9c4adf1eb4 Don't flush the stream on each new line, when writing automata. Alexandre Duret-Lutz 2011-11-27 23:35:31 +01:00
  • ba3108f98d Add an ltl2tgba option to read Kripke structure. Alexandre Duret-Lutz 2011-11-27 21:05:01 +01:00
  • 172ce2d7fd * AUTHORS: Add Thomas Badie. Alexandre Duret-Lutz 2011-11-27 20:59:17 +01:00
  • bb5949f6de Add text I/O for Kripke structures. Thomas Badie 2011-11-24 22:47:41 +01:00
  • 71d1a4fe25 Fix bench/emptchk/pml2tgba.pl for more recent Spin version. Alexandre Duret-Lutz 2011-11-24 22:07:09 +01:00
  • fdf8878db3 Update formulae.ltl not to use uncommon operators. Alexandre Duret-Lutz 2011-11-24 21:50:36 +01:00
  • fd98345c17 More documentation. Alexandre Duret-Lutz 2011-11-23 10:57:29 +01:00
  • 3010d7051b Display transition annotations in dotty output. Alexandre Duret-Lutz 2011-11-17 18:36:23 +01:00
  • d573eb9b8d * NEWS: Add an entry for the previous fix. Alexandre Duret-Lutz 2011-11-17 18:47:45 +01:00
  • ea6a1ffc22 Fully quote guards used by neverclaims. Alexandre Duret-Lutz 2011-11-16 14:24:34 +01:00
  • 2b5956c2d4 Fix a g++-4.7 warning about a variable used only in an assert(). Alexandre Duret-Lutz 2011-11-11 22:36:38 +01:00
  • 9130d6f58c Allow neverclaim guards of the form !(x)' or ! (x)'. Alexandre Duret-Lutz 2011-11-08 11:59:45 +01:00
  • 2422b63a36 Better documentation for print_tgba_run. Alexandre Duret-Lutz 2011-10-26 19:05:55 +02:00
  • 053b1ebc8e * iface/dve2/finite.test: Swap -e and -E after change from 2011-07-26. Alexandre Duret-Lutz 2011-10-24 07:11:29 +02:00
  • 8549eb9d16 * NEWS: Update with recent fixes. Alexandre Duret-Lutz 2011-10-24 06:56:02 +02:00
  • a4d1e18bf3 Safra: Fix usage of multiple acceptance conditions and fix text output. Alexandre Duret-Lutz 2011-10-23 23:06:35 +02:00
  • ff3c02f51d * src/tgba/tgbasafracomplement.cc: Fix two asserts. Alexandre Duret-Lutz 2011-10-23 22:02:19 +02:00
  • 73d9f65d2c Improve the print_safra_automaton output. Alexandre Duret-Lutz 2011-10-23 22:01:40 +02:00
  • 101b18b24b Fix errors reported by clang++-2.9. Alexandre Duret-Lutz 2011-08-28 10:35:36 +02:00
  • 92ef9d6e07 * examples/adder/adder.cxx (test_vector): Add parentheses to remove a clang++-2.9 warning. Alexandre Duret-Lutz 2011-08-28 10:13:36 +02:00
  • 24be6076f6 * src/bddop.c (bdd_support): Speedup using a cache. Alexandre Duret-Lutz 2011-08-27 19:08:16 +02:00
  • d9fc75e94e Improve SCC simplification by removing implied acceptance conditions. Alexandre Duret-Lutz 2011-08-27 18:55:13 +02:00
  • 9d232af82f Refine yesterday's change to the degeneralization. Alexandre Duret-Lutz 2011-08-26 10:39:00 +02:00
  • bc416fdb2f Make sure the degeneralization is idempotent (up to renaming of states). Alexandre Duret-Lutz 2011-08-25 18:42:00 +02:00
  • bf7b94e1cd Fix escaping of state name in save_reachable()'s output. Alexandre Duret-Lutz 2011-08-25 18:29:46 +02:00
  • d8ba172e6d Running ltl2tgba -R1q -R1t -N would degeneralize before and after the simulation-reduction. Alexandre Duret-Lutz 2011-08-25 16:53:40 +02:00
  • 1c2450f609 Please GCC 4.6. Alexandre Duret-Lutz 2011-08-17 16:27:40 +02:00
  • 03aabf9a3a Fix a nondeterministic behavior of the degeneralization algorithm. Alexandre Duret-Lutz 2011-08-17 15:27:39 +02:00
  • 7760b459e7 * src/tgbatest/ltl2tgba.cc (syntax): -N implies -DS, not -D. Alexandre Duret-Lutz 2011-08-17 14:00:39 +02:00
  • cdb4e36121 * iface/dve2/dve2check.cc: Add option -W and simplify formulae. Alexandre Duret-Lutz 2011-07-26 18:55:19 +02:00
  • 1719287b1e -e means we expect an accepting run. Alexandre Duret-Lutz 2011-07-26 18:44:18 +02:00
  • 7aefc190c9 Add some "drop shadow" in ltl2tgba.html. Alexandre Duret-Lutz 2011-06-26 18:26:20 +02:00
  • 1a823fea96 Revamp the ltl2tgba benchmark. Alexandre Duret-Lutz 2011-06-25 23:29:16 +02:00
  • 3fecb250a2 * src/ltlvisit/tostring.cc (to_spin_string_visitor): Add missing break. Alexandre Duret-Lutz 2011-06-16 15:13:49 +02:00
  • fb3edb47e0 [buddy] * src/bddop.c (apply_rec, appquant_rec): Improve caching by reordering operands of commutative operators. Alexandre Duret-Lutz 2011-06-10 18:39:28 +02:00
  • c42d55e6b1 * wrap/python/ajax/spot.in: Touch the directory containing the cached result for the requests. So that it survives the browser's cache. (finish): Prune the cache only once per hour, and only eraes files that are older than 2 hours. Alexandre Duret-Lutz 2011-06-10 11:12:05 +02:00
  • 8059047b21 * wrap/python/ajax/ltl2tgba.html: Add focus on the formula field on page load. Alexandre Duret-Lutz 2011-06-09 14:51:45 +02:00
  • d3ccaa7cb9 [buddy] Remove some valgrind warnings about uninitialized memory when BddCache_lookup return an entry from a Not operation. Alexandre Duret-Lutz 2011-06-09 11:56:02 +02:00
  • a0ca684dc6 more files to ignore Alexandre Duret-Lutz 2011-06-08 17:24:22 +02:00
  • d26a7f7e48 * NEWS: Update with recent changes. Alexandre Duret-Lutz 2011-06-08 17:12:06 +02:00
  • 3216494cf6 Implement cache pruning in the CGI script. Alexandre Duret-Lutz 2011-06-08 16:39:04 +02:00
  • 155ba42c90 Cache dot sources in the CGI script. Alexandre Duret-Lutz 2011-06-08 14:29:38 +02:00
  • 0d2ac81a8c Output a "Cache-Control:" header in the CGI script. Alexandre Duret-Lutz 2011-06-08 11:43:01 +02:00
  • b8f8441167 Cache results of the spot.py CGI script. Alexandre Duret-Lutz 2011-06-08 11:36:45 +02:00
  • b535741a90 [buddy] * examples/cmilner/cmilner.c (A, transitions, initial_state) (reachable_states, has_deadlocks): Declare as static functions, to suppress a GCC warning. Alexandre Duret-Lutz 2011-06-07 14:50:07 +02:00
  • f4ecb34275 * src/ltltest/genltl.cc (X_n): Fix assertion. Alexandre Duret-Lutz 2011-06-07 07:26:43 +02:00
  • 0b11fc2e11 * src/ltlvisit/dotty.cc (dotty_visitor): Reorder attributes. Alexandre Duret-Lutz 2011-06-06 19:25:27 +02:00
  • bb06db7c1b * src/ltltest/genltl.cc (fair_response): Typo. Alexandre Duret-Lutz 2011-06-06 19:02:03 +02:00
  • d47aa1d8b2 DVE2: Do not display state variables with only one possible value. Alexandre Duret-Lutz 2011-06-06 18:19:11 +02:00
  • 866af2a715 Remove Kristin Rozier's LTLcounter.pl scripts, now that we can generate these formulae with "genltl". Alexandre Duret-Lutz 2011-06-06 17:57:55 +02:00
  • 4087d37fe5 Better layout of the LTL formula parse tree. Alexandre Duret-Lutz 2011-06-06 17:04:49 +02:00
  • 625b9362c8 Add more formula families to genltl. Alexandre Duret-Lutz 2011-06-06 15:58:15 +02:00
  • 67ff9f203f Install a misc/_config.h to hide all the defines that clutter the built output. Alexandre Duret-Lutz 2011-06-03 18:05:06 +02:00
  • 78f932081b Document the protocol used between ltl2tgba.html and spot.py. Alexandre Duret-Lutz 2011-06-03 17:13:53 +02:00
  • 23334e7e25 * iface/dve2/README: Document state compression. Alexandre Duret-Lutz 2011-06-02 19:37:20 +02:00
  • f3bae53e5b Update jQuery and jQuery-UI. Alexandre Duret-Lutz 2011-06-02 13:54:12 +02:00
  • bf2b44c6de * iface/dve2/dve2.cc: Kill a spurious warning. Alexandre Duret-Lutz 2011-05-30 12:00:58 +02:00
  • 1eb0464afc * bench/wdba/README: Typos. Alexandre Duret-Lutz 2011-05-30 09:11:40 +02:00
  • 290b825a3a Some intvcomp2 speedups. Alexandre Duret-Lutz 2011-05-18 19:00:53 +02:00
  • ced733e4da * src/misc/intvcomp.hh, src/misc/intvcmp2.hh: Include stddef.h for size_t. Alexandre Duret-Lutz 2011-05-16 16:18:49 +02:00
  • 3752c3918e * src/misc/intvcmp2.cc: Cosmetics to please sanity checks. Alexandre Duret-Lutz 2011-05-05 15:06:41 +02:00
  • fea61e9f51 Fix compilation error with g++ <= 4.3. Alexandre Duret-Lutz 2011-05-05 12:10:08 +02:00