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

* m4/gspnlib.m4: Check for libgspnRG.a and libgspnSRG.a.

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2003-07-22 13:11:32 +00:00
parent 44993317ea
commit 94a9543f38
5 changed files with 41 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

12
ChangeLog
View file

@ -1,3 +1,15 @@
2003-07-22 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* 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 <aduret@src.lip6.fr> 2003-07-17 Alexandre Duret-Lutz <aduret@src.lip6.fr>
Now succ_iter() can fetch extra information from Now succ_iter() can fetch extra information from

9
iface/gspn/Makefile.am
View file

@ -8,7 +8,10 @@ libspotgspn_la_SOURCES = \
gspn.cc \ gspn.cc \
gspnlib.h gspnlib.h
check_PROGRAMS = dottygspn check_PROGRAMS = dottygspn-rg dottygspn-srg
dottygspn_SOURCES = dottygspn.cc dottygspn_rg_SOURCES = dottygspn.cc
dottygspn_LDADD = libspotgspn.la $(LIBGSPN_LDFLAGS) dottygspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS)
dottygspn_srg_SOURCES = dottygspn.cc
dottygspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS)

6
iface/gspn/dottygspn.cc
View file

@ -12,9 +12,11 @@ main(int argc, char **argv)
spot::bdd_dict* dict = new spot::bdd_dict(); 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; delete dict;
} }

13
iface/gspn/gspn.cc
View file

@ -5,11 +5,6 @@
#include "gspn.hh" #include "gspn.hh"
#include "ltlvisit/destroy.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 namespace spot
{ {
@ -87,7 +82,7 @@ namespace spot
tgba_gspn_private_(bdd_dict* dict, const gspn_environment& env) 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(); const gspn_environment::prop_map& p = env.get_prop_map();
@ -130,6 +125,8 @@ namespace spot
dict->unregister_all_my_variables(this); dict->unregister_all_my_variables(this);
if (last_state_conds_input) if (last_state_conds_input)
delete last_state_conds_input; delete last_state_conds_input;
if (all_indexes)
delete[] all_indexes;
} }
bdd index_to_bdd(AtomicProp index) const bdd index_to_bdd(AtomicProp index) const
@ -149,7 +146,7 @@ namespace spot
{ {
// Build the BDD of the conditions available on this state. // Build the BDD of the conditions available on this state.
unsigned char* cube = 0; 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; AtomicProp* want = all_indexes;
size_t count = index_count; size_t count = index_count;
int res = satisfy(s->get_state(), want, &cube, count); int res = satisfy(s->get_state(), want, &cube, count);
@ -192,7 +189,7 @@ namespace spot
throw gspn_exeption("succ()", res); throw gspn_exeption("succ()", res);
assert(successors_); assert(successors_);
// GSPN is expected to return a looping "dead" transition where // GSPN is expected to return a looping "dead" transition where
// there is no successor, // there is no successor.
assert(size_> 0); assert(size_> 0);
} }

16
m4/gspnlib.m4
View file

@ -10,8 +10,8 @@ AC_DEFUN([AX_CHECK_GSPNLIB], [
# Try to locate the headers and libraries. # Try to locate the headers and libraries.
gspn_version_sh=$with_gspn/SOURCES/contrib/version.sh; gspn_version_sh=$with_gspn/SOURCES/contrib/version.sh;
AC_CHECK_FILE($gspn_version_sh,, AC_CHECK_FILE($gspn_version_sh,,
[AC_MSG_ERROR( [AC_MSG_ERROR(
[Cannot find $gspn_version_sh. Check --with-gspn's argument.])]) [Cannot find $gspn_version_sh. Check --with-gspn's argument.])])
gspn_version=`$gspn_version_sh` gspn_version=`$gspn_version_sh`
LIBGSPN_LDFLAGS="-L$with_gspn/$gspn_version/2bin/lib" LIBGSPN_LDFLAGS="-L$with_gspn/$gspn_version/2bin/lib"
LIBGSPN_CPPFLAGS="-I$with_gspn/SOURCES/WN/INCLUDE" LIBGSPN_CPPFLAGS="-I$with_gspn/SOURCES/WN/INCLUDE"
@ -19,11 +19,17 @@ AC_DEFUN([AX_CHECK_GSPNLIB], [
LDFLAGS="$LDFLAGS $LIBGSPN_LDFLAGS" 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]) [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" LDFLAGS="$ax_tmp_LDFLAGS"
LIBS="$ax_tmp_LIBS" LIBS="$ax_tmp_LIBS"
fi fi
AM_CONDITIONAL([WITH_GSPN], [test x${with_gspn+set} = xset]) AM_CONDITIONAL([WITH_GSPN], [test x${with_gspn+set} = xset])
AC_SUBST([LIBGSPN_CPPFLAGS]) AC_SUBST([LIBGSPN_CPPFLAGS])
AC_SUBST([LIBGSPN_LDFLAGS]) AC_SUBST([LIBGSPNRG_LDFLAGS])]
]) AC_SUBST([LIBGSPNSRG_LDFLAGS])
)