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

Commit graph

  • ff43212e67 DVE2: Minor memory compaction. Alexandre Duret-Lutz 2011-05-02 14:46:01 +02:00
  • bf8becccea DVE2: Optionally use the new compression. Alexandre Duret-Lutz 2011-05-01 20:52:12 +02:00
  • a832eab156 Implement a new compression inspired from simple-9. Alexandre Duret-Lutz 2011-05-01 20:50:49 +02:00
  • 1d1872ab90 [buddy] Inline the "is bdd constant" check performed in copies/constructors. Alexandre Duret-Lutz 2011-04-30 13:37:53 +02:00
  • 2b58fb90c4 [buddy] Hint gcc about likely/unlikely branches. Alexandre Duret-Lutz 2011-04-30 13:30:05 +02:00
  • 24054605da [buddy] * src/pairs.c (bdd_pairalloc): Fix prototype. Alexandre Duret-Lutz 2011-04-30 13:22:27 +02:00
  • 21a28ca822 * src/misc/intvcomp.cc: Low-level fine-tuning. Alexandre Duret-Lutz 2011-04-15 16:35:14 +02:00
  • 445a785e10 Fix compression of large repetitions Alexandre Duret-Lutz 2011-04-13 11:31:36 +02:00
  • 1b447c3676 More interfaces to the int array compression routines. Alexandre Duret-Lutz 2011-04-12 11:44:53 +02:00
  • 3aa9c3bab6 * iface/dve2/dve2.cc: Typo when handling dead==true. Alexandre Duret-Lutz 2011-04-11 15:28:32 +02:00
  • e9396502f7 more files to ignore Alexandre Duret-Lutz 2011-04-10 22:14:12 +02:00
  • 2b6ea2279f Always pass --enable-devel or --disable-devel to BuDDy. Alexandre Duret-Lutz 2011-04-10 21:33:44 +02:00
  • e5f35dea48 [buddy] Fix some warnings reported by gcc. Alexandre Duret-Lutz 2011-04-10 21:30:31 +02:00
  • 35de7e9008 [buddy] Add support for --enable-devel and similar macros. Alexandre Duret-Lutz 2011-04-10 21:28:26 +02:00
  • cdede3d134 * src/misc/escape.hh: Fix Doxygen documentation. * src/misc/intvcomp.hh: Likewise. Alexandre Duret-Lutz 2011-04-10 09:25:10 +02:00
  • 4ec936387e Move the compression routines into their own *.cc file. Alexandre Duret-Lutz 2011-04-09 15:06:10 +02:00
  • ebb85c4da7 DVE2: Use mspool for compressed states. Alexandre Duret-Lutz 2011-04-09 14:18:11 +02:00
  • 56e487d468 Add a multiple-size memory pool implementation. Alexandre Duret-Lutz 2011-04-08 17:53:33 +02:00
  • cefedff192 * src/misc/fixpool.hh: Typo in comment. Alexandre Duret-Lutz 2011-04-08 17:53:03 +02:00
  • c938e652e4 DVE2: preliminary implementation of compressed states. Alexandre Duret-Lutz 2011-04-08 15:57:19 +02:00
  • bc1275455c Preliminary implementation of an int array compressor. Alexandre Duret-Lutz 2011-04-07 19:39:20 +02:00
  • 9ad062b247 Fix two spurious segfaults in test cases for the Python interface. Alexandre Duret-Lutz 2011-04-09 17:33:42 +02:00
  • 0caf51abd8 * HACKING: Add an example for using callgrind. Alexandre Duret-Lutz 2011-04-09 10:56:12 +02:00
  • 0368d653ca * iface/dve2/dve2check.cc (main): Catch out-of-memory errors during emptiness check or counterexample generation. Alexandre Duret-Lutz 2011-04-06 09:37:48 +02:00
  • 5fdfe28689 [buddy] Tag functions with attributes pure, const, or noreturn. Alexandre Duret-Lutz 2011-04-04 19:12:56 +02:00
  • 61d9e721a0 [buddy] Remove more sanity checks when NDEBUG is set. Alexandre Duret-Lutz 2011-04-04 19:10:06 +02:00
  • c44b60f08f * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc: Use a fixed-size memory pool for product_state instances. Alexandre Duret-Lutz 2011-04-03 21:00:11 +02:00
  • 5d12152449 * iface/dve2/dve2.cc: Use a fixed-size memory pool for dve2_state instances and their variables. Alexandre Duret-Lutz 2011-04-03 19:13:11 +02:00
  • 3396a03818 Add a fixed-size memory pool implementation. Alexandre Duret-Lutz 2011-04-03 19:05:11 +02:00
  • 050ea69f47 * HACKING (command): Some notes about link-time optimizations. Alexandre Duret-Lutz 2011-04-03 14:33:24 +02:00
  • 30f00584d4 [buddy] * src/kernel.h (CHECK, CHECKa, CHECKn): Disable if NDEBUG is set. Alexandre Duret-Lutz 2011-04-03 14:28:45 +02:00
  • 44aed5cda6 [buddy] Fix declaration of bddproduced. Alexandre Duret-Lutz 2011-04-03 13:54:01 +02:00
  • 87172f145d * configure.ac: Pass CXXFLAGS/CFLAGS/CPPFLAGS debug/optimization settings to sub configure. Alexandre Duret-Lutz 2011-04-03 10:51:32 +02:00
  • 197019ea62 [buddy] * buddy/src/kernel.c (bdd_addref, bdd_delref): Disable sanity checks when compiled with NDEBUG. Alexandre Duret-Lutz 2011-04-03 10:49:35 +02:00
  • 9f63bb6637 Introduct a down_cast macro. Alexandre Duret-Lutz 2011-03-31 19:39:44 +02:00
  • 12783ff784 Cosmetics. Alexandre Duret-Lutz 2011-03-31 10:19:59 +02:00
  • 36f7c648b6 Make state_explicit instances persistent objects. Alexandre Duret-Lutz 2011-03-30 19:47:18 +02:00
  • cd900a403b Remove tgba_reduc::format_state(). Alexandre Duret-Lutz 2011-03-30 16:19:31 +02:00
  • 29a908cc8f Protect the state destructor. Alexandre Duret-Lutz 2011-03-30 15:59:58 +02:00
  • 94ac863cfb Speedup tgba_product when one of the argument is a Kripke structure. Alexandre Duret-Lutz 2011-03-30 15:50:11 +02:00
  • 33732493fe * iface/dve2/dve2check.cc: Remove stray debug output. Alexandre Duret-Lutz 2011-03-30 15:43:28 +02:00
  • cc0a903a6e * src/tgba/tgbaproduct.hh: Do not include statebdd.hh. Alexandre Duret-Lutz 2011-03-30 10:25:58 +02:00
  • 35a0193781 Include <cstddef> in python modules to workaround Swig bug. Alexandre Duret-Lutz 2011-03-29 22:52:17 +02:00
  • 4ce06114d7 * THANKS: Add Michael Weber for his help on the DiVinE interface. Alexandre Duret-Lutz 2011-03-20 13:11:09 +01:00
  • a5a74481d9 * src/ltltest/genltl.cc (syntax): Typos in the help text. Alexandre Duret-Lutz 2011-03-18 17:02:30 +01:00
  • 1878bfd0fc Improve a reduction rule for "a M b". Alexandre Duret-Lutz 2011-03-17 11:55:56 +01:00
  • b51b7ab8b9 * NEWS: Mention recent changes to dotty_reachable. Alexandre Duret-Lutz 2011-03-11 10:20:47 +01:00
  • cb83e855a4 Add support for finite behaviors in the DVE interface. Alexandre Duret-Lutz 2011-03-10 22:37:44 +01:00
  • ef976c93d0 * iface/dve2/dve2.cc (convert_aps): Fix two typos while parsing >= and >, mistakenly registered as <= and <. Alexandre Duret-Lutz 2011-03-10 22:29:56 +01:00
  • 6d213e5e4c Remove the Nips interface. Alexandre Duret-Lutz 2011-03-07 14:03:53 +01:00
  • 8256ae9bfb Accept "P_0 == CS" as synonym for "P_0.CS" in the dve2 interface. Suggested by Yann Thierry-Mieg. Alexandre Duret-Lutz 2011-03-07 12:45:37 +01:00
  • 5318c1f966 Add some tests for the DVE2 interface. Alexandre Duret-Lutz 2011-03-07 11:08:12 +01:00
  • 0584d278d1 Clear the timer map to help valgrind. Alexandre Duret-Lutz 2011-03-07 10:47:27 +01:00
  • e75a73dfb1 Some documentation of about the dve2 interface. Alexandre Duret-Lutz 2011-03-07 10:01:21 +01:00
  • 76cfd57973 * iface/dve2/dve2.cc, iface/dve2/dve2check.cc: Cosmetic changes to please sanity checks. Alexandre Duret-Lutz 2011-03-06 21:12:40 +01:00
  • 51e6989d91 Call divine to compile dve models. Alexandre Duret-Lutz 2011-03-06 21:06:52 +01:00
  • 4a62224932 Allow atomic propositions and identifiers like `X.Y'. Alexandre Duret-Lutz 2011-03-06 19:12:24 +01:00
  • 8ce39e09b2 Augment dve2check to perform LTL model checking. Alexandre Duret-Lutz 2011-03-06 10:50:26 +01:00
  • 7b5879d26a Teach the DVE2 interface about enumerated types. Alexandre Duret-Lutz 2011-03-05 23:08:05 +01:00
  • 8136bd412d Teach the DVE2 interface about atomic propositions such as "a <= 10" or "b != 3". This only work for integer variables presently. Alexandre Duret-Lutz 2011-03-05 17:56:48 +01:00
  • 5a76a7bb05 Display states variables in the state label. Alexandre Duret-Lutz 2011-03-05 15:53:14 +01:00
  • 16b4c28859 We can now explore a divine2 compiled model, but the atomic properties are still missing. Alexandre Duret-Lutz 2011-03-05 15:25:39 +01:00
  • 155d76f4fb Setup libltdl in ltdl/, so we can use it in the dve2 interface. Alexandre Duret-Lutz 2011-03-05 11:52:55 +01:00
  • 3427f3bf0e Setup build system for a new dve2 interface. Alexandre Duret-Lutz 2011-03-05 11:00:56 +01:00
  • e1ef47d975 Using double borders for acceptance states in SBAs. Alexandre Duret-Lutz 2011-03-04 21:06:02 +01:00
  • 2c5bae3d37 * src/ltltest/genltl.cc (GF_n): Really use "op". Alexandre Duret-Lutz 2011-03-05 08:58:40 +01:00
  • 0792fb741d * wrap/python/ajax/spot.in: Use the degeneralized automaton if available while computing the emptiness check. Alexandre Duret-Lutz 2011-03-04 21:04:38 +01:00
  • de4166f4c9 Speedup build_result() called by minimize_dfa(). Alexandre Duret-Lutz 2011-03-04 11:50:52 +01:00
  • 4b75c9b8e6 * src/ltltest/genltl.cc: Add 10 more LTL formula classes. Alexandre Duret-Lutz 2011-03-01 18:15:13 +01:00
  • 8f5ecc14bf [buddy] * examples/cmilner/Makefile.am (cmilner_LDADD): Link with -lm, to find the pow() function. Alexandre Duret-Lutz 2011-02-27 15:24:22 +01:00
  • 774e20d8ee * src/tgba/bdddict.hh: Add more documentation. Alexandre Duret-Lutz 2011-02-21 22:11:57 +01:00
  • 428b21552f * src/misc/escape.hh: Correct documentation. Alexandre Duret-Lutz 2011-02-21 21:49:19 +01:00
  • 94d1c57ed4 Correct tgba_explicit::compute_support_conditions. Alexandre Duret-Lutz 2011-02-14 21:09:04 +01:00
  • 079747da23 more files to ignore Alexandre Duret-Lutz 2011-02-13 15:58:50 +01:00
  • 40e7350c80 Enable VERBOSE logs for nips, greatspn, and python tests. Alexandre Duret-Lutz 2011-02-10 12:58:16 +01:00
  • 0385f5b6c7 This should finally fix kv.test and dotty.test on the LIP6 buildfarm. Alexandre Duret-Lutz 2011-02-10 12:34:39 +01:00
  • e6be19cdf7 * HACKING (Running coverage tests): New section. Alexandre Duret-Lutz 2011-02-10 08:23:11 +01:00
  • ba564af08f Previous patch did not work on MacOS X, and I don't have shell access to that host. Alexandre Duret-Lutz 2011-02-09 22:44:05 +01:00
  • cb7b7d16f3 Avoid running "dot" when it is not installed... Alexandre Duret-Lutz 2011-02-09 21:09:54 +01:00
  • dd13bfa07b Add some tricks into HACKING. Alexandre Duret-Lutz 2011-02-08 12:23:34 +01:00
  • 964c2bed43 Adjust the WDBA test to count for sub-transitions. Alexandre Duret-Lutz 2011-02-08 12:21:36 +01:00
  • baf1288dc6 Fix a spurious g++ warning observed on Darwin builds. Alexandre Duret-Lutz 2011-02-08 10:53:06 +01:00
  • 9119ffe9bc * configure.ac: s/gnit/gnu so that we can use 0.7.1a as a version. Alexandre Duret-Lutz 2011-02-07 18:47:08 +01:00
  • e72f85a327 * NEWS: Typos. Alexandre Duret-Lutz 2011-02-07 18:30:21 +01:00
  • 6f43b997de * NEWS, configure.ac: Bump version to 0.7.1a Alexandre Duret-Lutz 2011-02-07 17:53:56 +01:00
  • 51bf0b18e3 Release Spot 0.7.1. Alexandre Duret-Lutz 2011-02-07 14:26:02 +01:00
  • 8b06edbc3b Generalize patch from 2011-02-03 by allowing guards like "! (...)". Alexandre Duret-Lutz 2011-02-07 00:06:18 +01:00
  • 0568eaf0ee Speedup scc_filter on tgba_explicit_number automata. Alexandre Duret-Lutz 2011-02-06 18:57:40 +01:00
  • caaf0a80c2 Document the new operators in the on-line tools. Alexandre Duret-Lutz 2011-02-06 17:36:26 +01:00
  • c019a44c49 Fix a segfault in WDBA minimization. Alexandre Duret-Lutz 2011-02-06 16:48:52 +01:00
  • 97df5b4285 Fix call to scc_filter in the CGI script. Alexandre Duret-Lutz 2011-02-05 14:26:51 +01:00
  • 08ee714760 * wrap/python/cgi-bin/ltl2tgba.in: Fix python error occurring only when the user did not make any error... Alexandre Duret-Lutz 2011-02-04 21:59:43 +01:00
  • 067a1a0b24 Prevent Spot from using an installed BuDDy version that does not have the latest function we added. Reported by Kristin Rozier. Alexandre Duret-Lutz 2011-02-04 21:28:17 +01:00
  • 30727074fd Add a way to count the number of sub-transitions. Alexandre Duret-Lutz 2011-02-04 00:17:53 +01:00
  • 91e51c4c3f Read guard of the form !(x) in neverclaims. Alexandre Duret-Lutz 2011-02-03 22:33:47 +01:00
  • 3278844c2a Recognize Goal's syntax for Boolean operators. Alexandre Duret-Lutz 2011-02-03 21:47:15 +01:00
  • 2fe5b3fb62 Minor fixes to ltl2tgba.html. Alexandre Duret-Lutz 2011-02-03 15:49:37 +01:00
  • 2452d9ff4a * NEWS, configure.ac: Bump version to 0.7a. Alexandre Duret-Lutz 2011-02-01 15:07:59 +01:00
  • ab73482581 Release Spot 0.7. Alexandre Duret-Lutz 2011-02-01 15:01:43 +01:00
  • f458eba1d7 * src/tgbatest/ltl2tgba.test: Fix previous test case. Alexandre Duret-Lutz 2011-02-01 13:12:24 +01:00