1. 10 Apr, 2011 3 commits
    • Alexandre Duret-Lutz's avatar
      [buddy] · e5f35dea
      Alexandre Duret-Lutz authored
      Fix some warnings reported by gcc.
      * buddy/src/kernel.c (errorstrings): Mark these as const.
      * buddy/src/reorder.c (reorder_gbc): Fix prototype.
      (siftTestCmp): Add missing const in cast.
      (bdd_reorder_auto): Actually call bdd_reorder_ready().
    • Alexandre Duret-Lutz's avatar
      [buddy] · 35de7e90
      Alexandre Duret-Lutz authored
      Add support for --enable-devel and similar macros.
      * m4/debug.m4: Rename to ...
      * m4/bdebug.m4: ... this.
      * m4/debug.m4, m4/devel.m4, m4/gccoptim.m4, m4/ndebug.m4: New file.
      * m4/gccwarns.m4: Fix usage of cache variable.  Fix shell
      syntax.  Do not check for -Waggregate-return.  Update CFLAGS.
      * configure.ac: Adjust to handle --enable-devel and similar macros
      in the same way as Spot.
    • Alexandre Duret-Lutz's avatar
      * src/misc/escape.hh: Fix Doxygen documentation. · cdede3d1
      Alexandre Duret-Lutz authored
      * src/misc/intvcomp.hh: Likewise.
  2. 09 Apr, 2011 8 commits
  3. 06 Apr, 2011 1 commit
  4. 05 Apr, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      [buddy] · 5fdfe286
      Alexandre Duret-Lutz authored
      Tag functions with attributes pure, const, or noreturn.
      * src/bdd.h (__purefn, __constfn, __noreturnfn): Define
      new macros.
      * src/bdd.h, src/bddio.c, src/bvec.h, src/imatrix.h: Use them
      to tag many functions as suggested by -Wsuggest-attribute=pure,
      -Wsuggest-attribute=const, -Wsuggest-attribute=noreturn.
  5. 04 Apr, 2011 2 commits
  6. 03 Apr, 2011 7 commits
  7. 31 Mar, 2011 3 commits
    • Alexandre Duret-Lutz's avatar
      Introduct a down_cast macro. · 9f63bb66
      Alexandre Duret-Lutz authored
      * src/misc/casts.hh: New file.
      * src/misc/Makefile.am: Add it.
      * iface/dve2/dve2.cc, iface/gspn/gspn.cc, iface/gspn/ssp.cc,
      src/evtgba/explicit.cc, src/evtgba/product.cc, src/misc/casts.hh,
      src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/taatgba.cc,
      src/tgba/taatgba.hh, src/tgba/tgbabddconcrete.cc,
      src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
      src/tgba/tgbakvcomplement.cc, src/tgba/tgbaproduct.cc,
      src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc,
      src/tgba/tgbatba.cc, src/tgba/tgbaunion.cc, src/tgba/wdbacomp.cc,
      src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/reductgba_sim.cc,
      src/tgbaalgos/reductgba_sim_del.cc: Use down_cast when
    • Alexandre Duret-Lutz's avatar
      Cosmetics. · 12783ff7
      Alexandre Duret-Lutz authored
      * src/sanity/style.test: Catch some binary operators not
      delimited with spaces.
      * src/tgbaalgos/bfssteps.cc, src/tgbaalgos/magic.cc,
      src/tgbaalgos/reducerun.cc, src/tgbaalgos/se05.cc,
      src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Fix these.
    • Alexandre Duret-Lutz's avatar
      Make state_explicit instances persistent objects. · 36f7c648
      Alexandre Duret-Lutz authored
      * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Merge
      state_explicit and tgba_explicit::state.  In the past,
      state_explicit was a small object encapsulating a pointer to the
      persistent tgba_explicit::state; and we used to clone() and
      destroy() a lot of state_explicit instance.  Now state_explicit is
      persistent, and clone() and destroy() have no effects.
      * src/tgba/tgbareduce.cc: Adjust, since this inherits from
      tgbaexplicit and uses the internals of state_explicit.
      * src/tgbatest/reductgba.cc: Fix deletion order for automata.
      * src/tgba/tgba.hh (last_support_conditions_input_,
      last_support_variables_input_): Make these protected, so
      they can be zeroed by tgba_explicit.
  8. 30 Mar, 2011 5 commits
  9. 29 Mar, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Include <cstddef> in python modules to workaround Swig bug. · 35a01937
      Alexandre Duret-Lutz authored
      * wrap/python/spot.i, wrap/python/buddy.i: Include <cstddef>
      because Swig 2.0.2 uses ptrdiff_t and does not do the include
      itself.  In g++ most libstdc++ standard headers have been changed
      to no longer include <cstddef> as an implementation detail, so
      the difference shows.
  10. 21 Mar, 2011 2 commits
  11. 17 Mar, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Improve a reduction rule for "a M b". · 1878bfd0
      Alexandre Duret-Lutz authored
      * src/ltlvisit/reduce.cc (reduce_visitor): Always reduce "a M b"
      to "a & b" if "a" is a pure eventual formula, remove the
      constraint on "b".
      * src/ltltest/reduccmp.test: Add two tests.
  12. 11 Mar, 2011 1 commit
  13. 10 Mar, 2011 2 commits
    • Alexandre Duret-Lutz's avatar
      Add support for finite behaviors in the DVE interface. · cb83e855
      Alexandre Duret-Lutz authored
      * iface/dve2/dve2.hh (load_dve2): Take a "dead" argument.
      * iface/dve2/dve2.cc (callback_context): Add a destructor
      to simplify...
      (dve2_succ_iterator::~dve2_succ_iterator) ... this one.
      (convert_aps): Skip the dead proposition.
      (dve2_kripke::dve2_kripke): Take a dead argument, and
      setup alive_prop and dead_prop.
      (compute_state_condition, get_succ): Use a cache for the
      conditions and successor of the last state, to share
      some work between these two function.  Add loops on dead
      (load_dve2): Pass dead to dve2_kripke and convert_aps.
      * iface/dve2/dve2check.cc: Add a -dDEAD option.
      * iface/dve2/finite.test, iface/dve2/finite.dve: New file.
      * iface/dve2/Makefile.am: Declare them.
    • Alexandre Duret-Lutz's avatar
      * iface/dve2/dve2.cc (convert_aps): Fix two typos while · ef976c93
      Alexandre Duret-Lutz authored
      parsing >= and >, mistakenly registered as <= and <.
  14. 07 Mar, 2011 3 commits