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

Commit graph

  • 062045eb45 Speedup reduc.test by not spawning one process per formula. Alexandre Duret-Lutz 2010-01-21 14:54:36 +01:00
  • 7262dff0d9 Move the last test from emptchk.test to emptchke.test. Alexandre Duret-Lutz 2010-01-21 13:50:25 +01:00
  • 79cb3ff512 Fix a memory leak in Cou99 statistics. Alexandre Duret-Lutz 2010-01-21 11:57:44 +01:00
  • 99884e8e0f Fix a longstanding bug in our implementation of GV04. Alexandre Duret-Lutz 2010-01-21 11:30:03 +01:00
  • 04827ef4a1 When iterating a hash_map, be careful not to delete i->first before doing ++i to avoid memory issues. Damien Lefortier 2010-01-20 17:37:25 +01:00
  • 0d6fd3225a Minor fixes to compile with GCC 3.3 Damien Lefortier 2010-01-20 17:09:06 +01:00
  • dcf7eed11f Remove some non-determinism in random_graph() Alexandre Duret-Lutz 2010-01-20 15:23:32 +01:00
  • 9fb8701667 * src/tgbaalgos/ltl2taa.cc: Fix the previous patch. Damien Lefortier 2010-01-19 10:43:43 +01:00
  • 9cebcdc124 * src/tgba/taatgba.cc, src/tgba/taatgba.hh: Fix memory issues occuring when labels are pointers. * src/tgbaalgos/ltl2taa.cc: Fix a bug. * src/tgbatest/ltl2tgba.cc: Fix a bug. Damien Lefortier 2010-01-18 12:11:31 +01:00
  • be78c82e44 * src/saba/sabacomplementtgba.cc: Fix a bug. Guillaume Sadegh 2010-01-16 23:21:26 +01:00
  • 1f19198d2d [LBTT] Add a missing include. Guillaume Sadegh 2010-01-16 23:17:47 +01:00
  • beb3744581 Use taa_tgba_formula instead of taa_tgba_string in ltl_to_taa to speed up a little the translation. Damien Lefortier 2010-01-16 13:33:04 +01:00
  • 7c20d8ae5d Introduce taa_tgba_labelled<label> so that we can build taa_tgba instances labelled by other objects than strings in the same way Alexandre did for tgba_explicit. Damien Lefortier 2010-01-16 11:48:21 +01:00
  • 88df8c0a1d Fix a longstanding bug reported by Guillaume Sadegh. Damien Lefortier 2010-01-06 09:37:05 +01:00
  • 830e482836 Merge eltl2tgba.cc into ltl2tgba.cc. Damien Lefortier 2010-01-05 19:28:17 +01:00
  • 1aa10e1395 * src/tgba/tgbabddcoredata.cc (delete_unaccepting_scc): Fix a bug. * src/tgbatest/spotlbtt.test: Use the above function with LaCIM for ELTL which greatly reduce the size of the automata! Damien Lefortier 2009-12-18 12:19:07 +01:00
  • 2a94402e82 * src/misc/timer.hh (timer::timer): Initialize running... Alexandre Duret-Lutz 2009-12-11 11:38:20 +01:00
  • 57c41de5f0 * src/Makefile.am (SUBDIRS): Fix missing ".", mistakenly removed by previous patch. Alexandre Duret-Lutz 2009-12-09 14:09:00 +01:00
  • d462f50b59 [buddy] Inline bdd_addref() and bdd_delref() to speedup BDD operations. Alexandre Duret-Lutz 2009-12-09 14:05:08 +01:00
  • d659001f0e An algorithm to complement TGBA into SABA. Guillaume Sadegh 2009-11-30 23:52:37 +01:00
  • 7cb6ff331d Add a new type of automata: State-labeled Alternating Büchi Automata (SABA). Guillaume Sadegh 2009-11-30 23:22:13 +01:00
  • f00aa49dc3 Rename the class taa as taa_tgba. Guillaume Sadegh 2009-11-27 23:17:38 +01:00
  • d362e752d1 * src/tgbatest/ltl2tgba.cc (main): Fix typo to re-enable reductions by simulation. Alexandre Duret-Lutz 2009-11-26 17:40:21 +01:00
  • deff1a5ca7 * m4/buddy.m4 (AX_CHECK_BUDDY): Check for bdd_satprefix, the latest function added to BuDDy. Alexandre Duret-Lutz 2009-11-26 16:47:16 +01:00
  • 3cbd681c6d [lbtt] Fix generation of random formulae on 64bits systems. Alexandre Duret-Lutz 2009-11-26 15:51:01 +01:00
  • c95eb21ecf [lbtt] * src/Configuration.cc (registerAlgorithm): Do not complain about a missing path for disabled algorithms. Alexandre Duret-Lutz 2009-11-25 18:07:55 +01:00
  • 1e19aa3a5f * src/tgbatest/ltl2tgba.cc (main): Stop the SCC timer. I mean really stop it! Alexandre Duret-Lutz 2009-11-25 18:06:46 +01:00
  • b796bb3d0a Detect running timers, and stop a timer in ltl2tgba. Alexandre Duret-Lutz 2009-11-24 11:47:42 +01:00
  • ab02ee60fe * src/tgbaalgos/sccfilter.cc (create_transition): Do not clone the same node twice when dealing with loops. Alexandre Duret-Lutz 2009-11-23 22:24:55 +01:00
  • 9a14d28a06 Use bdd_satprefix() to speedup minato on BDDs that are almost cubes. Alexandre Duret-Lutz 2009-11-23 21:47:25 +01:00
  • 253ee35030 [buddy] Introduce bdd_satprefix, to speedup spot::minato(). Alexandre Duret-Lutz 2009-11-23 21:32:13 +01:00
  • 81e0872b5d Specialize scc_filter when handling tgba_explicit_formula automata. Alexandre Duret-Lutz 2009-11-23 10:19:38 +01:00
  • dfb9c6622b Strip useless acceptance conditions in scc_filter(). Alexandre Duret-Lutz 2009-11-20 19:21:12 +01:00
  • 5d427f6d15 * src/tgbaalgos/sccfilter.cc (scc_filter): Merge transitions after removing acceptance conditions. Alexandre Duret-Lutz 2009-11-20 15:33:40 +01:00
  • 7ac3c5e70c Remove prune_scc(), prune_acc(), and related fonctions. Alexandre Duret-Lutz 2009-11-18 18:20:11 +01:00
  • 7ea51cc65f Replace prune_scc() by scc_filter(). Alexandre Duret-Lutz 2009-11-18 15:40:37 +01:00
  • 74f620d192 Quick implementation of a "useless SCC" filter using scc_map. Alexandre Duret-Lutz 2009-11-18 15:36:35 +01:00
  • 99981153e6 Fix acceptance check in scc_map: trivial SCCs are not accepting. Also compute useless SCCs. Alexandre Duret-Lutz 2009-11-18 15:18:40 +01:00
  • ac5dda1032 Make it easy to filter states while iterating over an automaton. Alexandre Duret-Lutz 2009-11-18 14:54:53 +01:00
  • 38148f87f8 * src/tgbaalgos/cutscc.cc (cut_scc): Pass `s' by reference instead of by pointer. * src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh: Fix copyright header. Alexandre Duret-Lutz 2009-11-17 16:48:42 +01:00
  • f2be64dd2c Replace the hash key construction of LTL formulae by a simple counter updated each time we create a new (unique) formula. Alexandre Duret-Lutz 2009-11-13 18:13:59 +01:00
  • 8cdc196719 Use -l wherever we where expecting ltl2tgba to default to LaCIM. Alexandre Duret-Lutz 2009-11-12 16:46:04 +01:00
  • c9b65cff71 Cleanup the help of ltl2tgba. Alexandre Duret-Lutz 2009-11-12 16:22:06 +01:00
  • 8ccc2b81c1 * src/tgbatest/ltl2tgba.cc (-l): New option to select the lacim translation. It still is the default translation. (opt_fm, opt_taa): Replace these two variables by ... (translation): ... this enum. And use a switch to call the correct translation. Alexandre Duret-Lutz 2009-11-12 15:30:55 +01:00
  • 49d1abbda7 Remove python bindings for ltl::clone and ltl::destroy. Alexandre Duret-Lutz 2009-11-11 11:13:00 +01:00
  • 7c946878e4 Typo from a previous patch. Alexandre Duret-Lutz 2009-11-11 00:01:14 +01:00
  • 8c6a2b33d9 Do not comment states in the never claim by default. It takes too much time when the formula is large, and it is useless when the purpose is model-checking with Spin. Alexandre Duret-Lutz 2009-11-10 17:45:41 +01:00
  • 1d8b115b83 * src/tgba/taa.cc, src/tgba/taa.hh: Fix it. * src/tgbaalgos/ltl2taa.cc: Do NOT use the same bdd_dict for both the translation and the language containment checker. * src/tgbatest/spotlbtt.test: Update TAA related tests. Damien Lefortier 2009-11-10 16:45:29 +01:00
  • 007e2bd0b9 Use tgba_explicit_formula instead of tgba_explicit_string in FM. Alexandre Duret-Lutz 2009-11-10 16:57:08 +01:00
  • 32a4647d03 Ease debugging of LTL formulae leaks. Alexandre Duret-Lutz 2009-11-10 15:10:46 +01:00
  • 4e22bb8b09 Introduce tgba_explicit_labelled<label> so that we can build tgba_explicit instances labelled by other objects than strings. Alexandre Duret-Lutz 2009-11-10 12:16:33 +01:00
  • d3dcecc6c3 Do not use the Boost macro from the Autoconf macro archive. Alexandre Duret-Lutz 2009-11-09 17:02:40 +01:00
  • 39912aa51e * src/tgbatest/ltlcounter.test (run): Do not run with n=12, as the test case might become too slow for the autobuilder. Alexandre Duret-Lutz 2009-11-09 16:10:58 +01:00
  • 3ce1627251 Add a benchmark using Kristin Y. Rozier's LTLcounter scripts. Alexandre Duret-Lutz 2009-11-06 16:45:11 +01:00
  • e539226e13 Use a timer to clock the different phases of the translation. Alexandre Duret-Lutz 2009-11-06 15:57:24 +01:00
  • 77df39b4dd Deprecate ltl::destroy(f) in favor of f->destroy() Alexandre Duret-Lutz 2009-11-09 06:54:52 +01:00
  • 48fb19ea44 Deprecate ltl::clone(f) in favor of f->clone(). Alexandre Duret-Lutz 2009-11-08 19:41:40 +01:00
  • e44f1b8997 Make it possible to clone const formulae. Alexandre Duret-Lutz 2009-11-08 19:36:35 +01:00
  • b0888257f8 Rename formula::ref and formula::unref as formula::clone and formula::destroy. Alexandre Duret-Lutz 2009-11-08 11:41:46 +01:00
  • 8e4e692e7f Change the way references are counted to speedup cloning. Alexandre Duret-Lutz 2009-11-07 02:56:45 +01:00
  • 631f4b5bea Make it easier to debug reference counts in LTL nodes. Alexandre Duret-Lutz 2009-11-07 02:41:32 +01:00
  • 3488bf45e0 Better types for instance maps. Alexandre Duret-Lutz 2009-11-07 02:23:19 +01:00
  • f2e941cd07 Add missing instance_count() in automatop and eltl2tgba. Alexandre Duret-Lutz 2009-11-07 02:20:53 +01:00
  • 09bba54b5f * src/tgba/taa.cc, src/tgbatest/taa.cc: Adjust. Damien Lefortier 2009-11-07 19:20:16 +01:00
  • 11ecdf2b86 * src/tgba/taa.cc, src/tgba/taa.hh: Speed up the cartesian product in taa_succ_iterator and allow multiple initial states in taa. * src/tgba/ltl2taa.cc: Remove temporary printing. Damien Lefortier 2009-11-07 15:50:45 +01:00
  • eab1261437 Fix ltlcounter.test for VPATH builds and n > 2. Alexandre Duret-Lutz 2009-11-05 21:22:12 +01:00
  • b57fdcb684 * src/tgbatest/ltlcounter.test (run): Only construct small formulae (i.e. n<=2) under valgrind. The test case is too slow otherwise. Alexandre Duret-Lutz 2009-11-05 14:12:47 +01:00
  • 24527d6f99 Fix spurious failure of style.test. Alexandre Duret-Lutz 2009-11-04 18:10:48 +01:00
  • 6fb7e9faff Fix a longstanding bug reported by Kristin Y. Rozier.. Alexandre Duret-Lutz 2009-11-04 18:05:48 +01:00
  • 24b78fde34 Fix the help text of ltl2tgba. Alexandre Duret-Lutz 2009-11-03 16:16:48 +01:00
  • cb6b74f5ec * src/tgba/tgbacomplement.cc (state_complement): Remove the copy constructor. It does the same thing as the default copy constructor, and g++ 4.2.3 complained that the copy constructor of spot::state was not called. Reported by Denis Poitrenaud. Alexandre Duret-Lutz 2009-10-28 14:42:51 +01:00
  • 8901d0d5be * src/ltlast/formula_tree.cc (instanciate, arity): Add a useless return 0 at the end to prevent g++ 4.2.3 from complaining about a missing return. Reported by Denis Poitrenaud. Alexandre Duret-Lutz 2009-10-28 14:24:26 +01:00
  • 802754c60a * src/tgbatest/kv.test: Don't run valgrind on dot! Alexandre Duret-Lutz 2009-10-23 14:32:39 +02:00
  • 913637a7ae Escape labels in -KV output. Alexandre Duret-Lutz 2009-10-16 10:07:26 +02:00
  • 4d8239e855 * src/tgbaalgos/ltl2tgba_fm.cc: Typos. Alexandre Duret-Lutz 2009-10-16 01:34:39 +02:00
  • 7ce27ef994 Improve ltl_to_taa. Damien Lefortier 2009-10-22 14:37:30 +02:00
  • 9f47dde5a7 Fix make check in sanity. Damien Lefortier 2009-10-17 13:47:59 +02:00
  • 84060b49e5 Minor fixes. Damien Lefortier 2009-10-16 17:00:46 +02:00
  • 627b667712 Add a new algorithm (from Tauriainen) to translate LTL formulae to TGBA which uses TAA as an intermediate representation. This is a basic version, optimizations and enhancements will come later. Damien Lefortier 2009-10-16 16:49:24 +02:00
  • 20c1f01e48 Add a class to represent Transition-based Alternating Automata (TAA). Damien Lefortier 2009-10-04 14:49:00 +02:00
  • 98215ed9a4 more authors Alexandre Duret-Lutz 2009-10-07 18:04:43 +02:00
  • b7db0c3085 [buddy] Fix the previous patch in reorder.c Alexandre Duret-Lutz 2009-10-01 13:33:16 +02:00
  • 44ab903b86 The sgba proxy adds an acceptance condition to every states when the original automaton has no acceptance condition. Guillaume Sadegh 2009-10-01 00:25:06 +02:00
  • 6d18623e4b * src/tgba/tgbacomplement.cc: Move functions related to shared_ptr on states... * src/tgba/state.hh: ... here. * src/tgbatest/complementation.test: Do not apply some tests on the new algorithm because it takes to much time to run. Guillaume Sadegh 2009-09-30 17:19:06 +02:00
  • d6e22c0674 A new complementation construction based on ranking. Guillaume Sadegh 2009-09-29 15:16:26 +02:00
  • d037008cdc * src/ltltest/randltl.cc, src/ltltest/reduc.test, src/tgbatest/dfs.test: Adjust headers to 80 columns. Guillaume Sadegh 2009-09-29 14:56:43 +02:00
  • 8f5f0354ad A wrapper around tgba to produce state-labeled automata. Guillaume Sadegh 2009-09-24 12:44:45 +02:00
  • 9775dd9701 Rename files related to Safra complementation. Guillaume Sadegh 2009-09-21 11:53:07 +02:00
  • 1208365b8c Fix previous patch. Alexandre Duret-Lutz 2009-09-28 15:29:31 +02:00
  • fd0de04d24 Optimize previous patch. Alexandre Duret-Lutz 2009-09-18 10:39:07 +02:00
  • fa8dd7f160 Have scc_map keep track of APs that are reachable from a SCC. Alexandre Duret-Lutz 2009-09-17 17:56:35 +02:00
  • b3486965a0 Have scc_map keep track of APs that are occurring in a SCC. Alexandre Duret-Lutz 2009-09-17 15:06:30 +02:00
  • ada681d813 [buddy] Fix some issues reported by LLVM/Clang's static analyser. Alexandre Duret-Lutz 2009-09-07 17:42:04 +02:00
  • 995335618a Fix some memory leaks. Damien Lefortier 2009-09-07 16:41:18 +02:00
  • 4964c9a1a4 Fix a memory leak in reduce_tau03(). Alexandre Duret-Lutz 2009-09-07 16:10:40 +02:00
  • 058bb83c6d Fix a memory leak in randltl. Alexandre Duret-Lutz 2009-09-07 14:34:07 +02:00
  • edd4b2b532 Add an algorithm (from Couvreur) working on BDDs to reduce the size of TGBAs represented as BDDs by deleting unaccepting SCCs. Damien Lefortier 2009-09-04 21:29:29 +02:00
  • dc8cb56b67 Fix path to libtool in test suites. Alexandre Duret-Lutz 2009-09-01 18:13:35 +02:00
  • 1098c62de2 Use Automake 1.11's parallel-tests feature. Alexandre Duret-Lutz 2009-08-31 16:08:16 +02:00
  • 1f7aa90d74 more files to ignore Alexandre Duret-Lutz 2009-08-31 15:50:38 +02:00