diff --git a/ChangeLog b/ChangeLog index a113e88ed..aa3dfdb71 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2003-07-22 Alexandre Duret-Lutz + + * m4/gspnlib.m4: Check for libgspnRG.a and libgspnSRG.a. + Define LIBGSPNRG_LDFLAGS and LIBGSPNSRG_LDFLAGS, not + LIBGSPN_LDFLAGS. + * iface/gspn/Makefile.am: Adjust, build dottygspn-rg and + dottygspn-srg instead of dottygspn. + * iface/gspn/gspn.cc (EVENT_TRUE): Undefine. + (tgba_gspn_private_::~tgba_gspn_private_): Free all_indexes. + * iface/gspn/dottygspn.cc (main): Destroy the automaton before + its dictionnary. + 2003-07-17 Alexandre Duret-Lutz Now succ_iter() can fetch extra information from @@ -22,7 +34,7 @@ (tgba_explicit::compute_support_conditions, tgba_explicit::compute_support_variables): Implement them. * src/tgba/tgbaexplicit.hh: Adjust. - * src/tgba/tgbaproduct.cc (tgba_product::succ_iter): Handle the + * src/tgba/tgbaproduct.cc (tgba_product::succ_iter): Handle the two new arguments. (tgba_product::compute_support_conditions, tgba_product::compute_support_variables): Implement them. diff --git a/iface/gspn/Makefile.am b/iface/gspn/Makefile.am index 71808c134..9576c96cc 100644 --- a/iface/gspn/Makefile.am +++ b/iface/gspn/Makefile.am @@ -8,7 +8,10 @@ libspotgspn_la_SOURCES = \ gspn.cc \ gspnlib.h -check_PROGRAMS = dottygspn +check_PROGRAMS = dottygspn-rg dottygspn-srg -dottygspn_SOURCES = dottygspn.cc -dottygspn_LDADD = libspotgspn.la $(LIBGSPN_LDFLAGS) +dottygspn_rg_SOURCES = dottygspn.cc +dottygspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS) + +dottygspn_srg_SOURCES = dottygspn.cc +dottygspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS) diff --git a/iface/gspn/dottygspn.cc b/iface/gspn/dottygspn.cc index 5d079328b..f64077209 100644 --- a/iface/gspn/dottygspn.cc +++ b/iface/gspn/dottygspn.cc @@ -12,9 +12,11 @@ main(int argc, char **argv) spot::bdd_dict* dict = new spot::bdd_dict(); - spot::tgba_gspn a(dict, env); + { + spot::tgba_gspn a(dict, env); - spot::dotty_reachable(std::cout, &a); + spot::dotty_reachable(std::cout, &a); + } delete dict; } diff --git a/iface/gspn/gspn.cc b/iface/gspn/gspn.cc index c68c913f1..16c1be95e 100644 --- a/iface/gspn/gspn.cc +++ b/iface/gspn/gspn.cc @@ -5,11 +5,6 @@ #include "gspn.hh" #include "ltlvisit/destroy.hh" -// FIXME: Override signed definition of EVENT_TRUE until this is fixed -// in gspnlib.h. -#undef EVENT_TRUE -#define EVENT_TRUE 0U - namespace spot { @@ -87,7 +82,7 @@ namespace spot tgba_gspn_private_(bdd_dict* dict, const gspn_environment& env) - : refs(0), dict(dict), last_state_conds_input(0) + : refs(1), dict(dict), all_indexes(0), last_state_conds_input(0) { const gspn_environment::prop_map& p = env.get_prop_map(); @@ -130,6 +125,8 @@ namespace spot dict->unregister_all_my_variables(this); if (last_state_conds_input) delete last_state_conds_input; + if (all_indexes) + delete[] all_indexes; } bdd index_to_bdd(AtomicProp index) const @@ -149,7 +146,7 @@ namespace spot { // Build the BDD of the conditions available on this state. unsigned char* cube = 0; - // This is temporary. We ought to ask only what we need. + // FIXME: This is temporary. We ought to ask only what we need. AtomicProp* want = all_indexes; size_t count = index_count; int res = satisfy(s->get_state(), want, &cube, count); @@ -192,7 +189,7 @@ namespace spot throw gspn_exeption("succ()", res); assert(successors_); // GSPN is expected to return a looping "dead" transition where - // there is no successor, + // there is no successor. assert(size_> 0); } diff --git a/m4/gspnlib.m4 b/m4/gspnlib.m4 index f6e4fe891..be3a62661 100644 --- a/m4/gspnlib.m4 +++ b/m4/gspnlib.m4 @@ -9,21 +9,27 @@ AC_DEFUN([AX_CHECK_GSPNLIB], [ if test x${with_gspn-yes} != xyes; then # Try to locate the headers and libraries. gspn_version_sh=$with_gspn/SOURCES/contrib/version.sh; - AC_CHECK_FILE($gspn_version_sh,, - [AC_MSG_ERROR( - [Cannot find $gspn_version_sh. Check --with-gspn's argument.])]) + AC_CHECK_FILE($gspn_version_sh,, + [AC_MSG_ERROR( + [Cannot find $gspn_version_sh. Check --with-gspn's argument.])]) gspn_version=`$gspn_version_sh` LIBGSPN_LDFLAGS="-L$with_gspn/$gspn_version/2bin/lib" LIBGSPN_CPPFLAGS="-I$with_gspn/SOURCES/WN/INCLUDE" fi LDFLAGS="$LDFLAGS $LIBGSPN_LDFLAGS" - AC_CHECK_LIB([gspnRG], [initialize], [], + AC_CHECK_LIB([gspnRG], [initialize], [], [AC_MSG_ERROR([Cannot find libgspnRG. Check --with-gspn's argument.])], [-lm -lfl]) - LIBGSPN_LDFLAGS="$LIBGSPN_LDFLAGS -lgspnRG -lm -lfl" + LIBGSPNRG_LDFLAGS="$LIBGSPN_LDFLAGS -lgspnRG -lm -lfl" + + LDFLAGS="$LDFLAGS $LIBGSPN_LDFLAGS" + AC_CHECK_LIB([gspnSRG], [initialize], [], + [AC_MSG_ERROR([Cannot find libgspnSRG. Check --with-gspn's argument.])], [-lm -lfl]) + LIBGSPNSRG_LDFLAGS="$LIBGSPN_LDFLAGS -lgspnSRG -lm -lfl" LDFLAGS="$ax_tmp_LDFLAGS" LIBS="$ax_tmp_LIBS" fi AM_CONDITIONAL([WITH_GSPN], [test x${with_gspn+set} = xset]) AC_SUBST([LIBGSPN_CPPFLAGS]) - AC_SUBST([LIBGSPN_LDFLAGS]) -]) + AC_SUBST([LIBGSPNRG_LDFLAGS])] + AC_SUBST([LIBGSPNSRG_LDFLAGS]) +)