From 4ac192ac1eb0392e44b3f364aa622cb753707cd8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 16 Jul 2003 12:56:38 +0000 Subject: [PATCH] * m4/gspnlib.m4: New file. * configure.ac: Call AX_CHECK_GSPNLIB. * Makefile.am (EXTRA_DIST): Add m4/gspnlib.m4. * iface/gspn/Makefile.am (AM_CPPFLAGS): Add $(LIBGSPN_CPPFLAGS). (libspotgspn_la_LIBADD, check_PROGRAMS, dottygspn_SOURCES, dottygspn_LDADD): New variables. * iface/gspn/gspn.hh (gspn_interface): New class. (gspn_exeption): Take a string argument and adjust all callers. (operator<<): Define for gspn_exeption. * iface/gspn/gspn.cc (gspn_interface::gspn_interface, gspn_interface::~gspn_interface): New. * iface/gspn/gspnlib.h: Delete, it belongs to GSPN. * iface/gspn/dottygspn.cc: New file. --- ChangeLog | 16 +++++++ Makefile.am | 8 +++- configure.ac | 1 + iface/gspn/Makefile.am | 8 +++- iface/gspn/dottygspn.cc | 26 ++++++++++ iface/gspn/gspn.cc | 34 +++++++++---- iface/gspn/gspn.hh | 31 ++++++++++-- iface/gspn/gspnlib.h | 104 ---------------------------------------- m4/gspnlin.m4 | 29 +++++++++++ 9 files changed, 137 insertions(+), 120 deletions(-) create mode 100644 iface/gspn/dottygspn.cc delete mode 100644 iface/gspn/gspnlib.h create mode 100644 m4/gspnlin.m4 diff --git a/ChangeLog b/ChangeLog index b512840f6..3ac9b346f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,19 @@ +2003-07-16 Alexandre Duret-Lutz + + * m4/gspnlib.m4: New file. + * configure.ac: Call AX_CHECK_GSPNLIB. + * Makefile.am (EXTRA_DIST): Add m4/gspnlib.m4. + * iface/gspn/Makefile.am (AM_CPPFLAGS): Add $(LIBGSPN_CPPFLAGS). + (libspotgspn_la_LIBADD, check_PROGRAMS, dottygspn_SOURCES, + dottygspn_LDADD): New variables. + * iface/gspn/gspn.hh (gspn_interface): New class. + (gspn_exeption): Take a string argument and adjust all callers. + (operator<<): Define for gspn_exeption. + * iface/gspn/gspn.cc (gspn_interface::gspn_interface, + gspn_interface::~gspn_interface): New. + * iface/gspn/gspnlib.h: Delete, it belongs to GSPN. + * iface/gspn/dottygspn.cc: New file. + 2003-07-15 Alexandre Duret-Lutz * m4/lbtt.m4 (AX_CHECK_LBTT): Set LBTT and LBTT_TRANSLATE diff --git a/Makefile.am b/Makefile.am index 168bbc1a1..9e58f5283 100644 --- a/Makefile.am +++ b/Makefile.am @@ -8,4 +8,10 @@ endif WITH_INCLUDED_LBTT SUBDIRS = $(MAYBE_BUDDY) $(MAYBE_LBTT) doc src wrap iface ACLOCAL_AMFLAGS = -I m4 -EXTRA_DIST = m4/gccwarn.m4 m4/pypath.m4 m4/buddy.m4 m4/lbtt.m4 HACKING +EXTRA_DIST = \ + m4/gccwarn.m4 \ + m4/pypath.m4 \ + m4/buddy.m4 \ + m4/lbtt.m4 \ + m4/gspnlib.m4 \ + HACKING diff --git a/configure.ac b/configure.ac index 7591ff11b..763ff71a7 100644 --- a/configure.ac +++ b/configure.ac @@ -14,6 +14,7 @@ AC_LANG(C++) AX_CHECK_BUDDY AX_CHECK_LBTT +AX_CHECK_GSPNLIB AC_PROG_LIBTOOL diff --git a/iface/gspn/Makefile.am b/iface/gspn/Makefile.am index 6b2a6803b..71808c134 100644 --- a/iface/gspn/Makefile.am +++ b/iface/gspn/Makefile.am @@ -1,8 +1,14 @@ -AM_CPPFLAGS = -I$(top_srcdir)/src $(BUDDY_CPPFLAGS) +AM_CPPFLAGS = -I$(top_srcdir)/src $(BUDDY_CPPFLAGS) $(LIBGSPN_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) lib_LTLIBRARIES = libspotgspn.la +libspotgspn_la_LIBADD = $(top_builddir)/src/libspot.la libspotgspn_la_SOURCES = \ gspn.hh \ gspn.cc \ gspnlib.h + +check_PROGRAMS = dottygspn + +dottygspn_SOURCES = dottygspn.cc +dottygspn_LDADD = libspotgspn.la $(LIBGSPN_LDFLAGS) diff --git a/iface/gspn/dottygspn.cc b/iface/gspn/dottygspn.cc new file mode 100644 index 000000000..4821d48a2 --- /dev/null +++ b/iface/gspn/dottygspn.cc @@ -0,0 +1,26 @@ +#include "gspn.hh" +#include "tgbaalgos/dotty.hh" + +int +main(int argc, char **argv) + try + { + spot::gspn_interface gspn(argc, argv); + + spot::gspn_environment env; + env.declare("obs"); + + spot::bdd_dict* dict = new spot::bdd_dict(); + + spot::tgba_gspn a(dict, env); + + spot::dotty_reachable(std::cout, &a); + + delete dict; + } + catch (spot::gspn_exeption e) + { + std::cerr << e << std::endl; + throw; + } + diff --git a/iface/gspn/gspn.cc b/iface/gspn/gspn.cc index a230563fc..c192f3879 100644 --- a/iface/gspn/gspn.cc +++ b/iface/gspn/gspn.cc @@ -8,6 +8,21 @@ namespace spot { + gspn_interface::gspn_interface(int argc, char **argv) + { + int res = initialize(argc, argv); + if (res) + throw gspn_exeption("initialize()", res); + } + + gspn_interface::~gspn_interface() + { + int res = finalize(); + if (res) + throw gspn_exeption("finalize()", res); + } + + // tgba_gspn_private_ ////////////////////////////////////////////////////////////////////// @@ -36,11 +51,11 @@ namespace spot AtomicProp index; int err = prop_index(i->first.c_str(), &index); if (err) - throw gspn_exeption(err); + throw gspn_exeption("prop_index()", err); AtomicPropKind kind; err = prop_kind(index, &kind); if (err) - throw gspn_exeption(err); + throw gspn_exeption("prop_kind()", err); prop_dict[index] = ab_pair(kind, bdd_ithvar(var)); } @@ -97,7 +112,8 @@ namespace spot { const state_gspn* o = dynamic_cast(other); assert(o); - return o->get_state() - get_state(); + return reinterpret_cast(o->get_state()) + - reinterpret_cast(get_state()); } virtual state_gspn* clone() const @@ -130,11 +146,9 @@ namespace spot current_(0), data_(data) { - AtomicProp want[] = { EVENT_TRUE }; - int res = succ(state, want, sizeof(want) / sizeof(*want), - &successors_, &size_); + int res = succ(state, &successors_, &size_); if (res) - throw res; + throw gspn_exeption("succ()", res); assert(successors_); // GSPN is expected to return a looping "dead" transition where // there is no successor, @@ -188,7 +202,7 @@ namespace spot private: bdd state_conds_; /// All conditions known on STATE. EventPropSucc* successors_; /// array of successors - size_t size_; /// size of successors_ + size_t size_; /// size of successors_ size_t current_; /// current position in successors_ tgba_gspn_private_* data_; }; // tgba_succ_iterator_gspn @@ -278,7 +292,7 @@ namespace spot State s; int err = initial_state(&s); if (err) - throw gspn_exeption(err); + throw gspn_exeption("initial_state()", err); return new state_gspn(s); } @@ -293,7 +307,7 @@ namespace spot int res = satisfy(s->get_state(), data_->all_indexes, &cube, data_->index_count); if (res) - throw res; + throw gspn_exeption("satisfy()", res); assert(cube); bdd state_conds = bddtrue; for (size_t i = 0; i < data_->index_count; ++i) diff --git a/iface/gspn/gspn.hh b/iface/gspn/gspn.hh index 0be9967f2..7e84be871 100644 --- a/iface/gspn/gspn.hh +++ b/iface/gspn/gspn.hh @@ -4,6 +4,7 @@ // Try not to include gspnlib.h here, or it will polute the user's // namespace with internal C symbols. +# include # include # include "tgba/tgba.hh" # include "ltlast/atomic_prop.hh" @@ -12,24 +13,46 @@ namespace spot { + class gspn_interface + { + public: + gspn_interface(int argc, char **argv); + ~gspn_interface(); + tgba* get_automata(); + }; + + /// An exeption used to forward GSPN errors. class gspn_exeption { public: - gspn_exeption(int err) - : err(err) + gspn_exeption(const std::string& where, int err) + : err_(err), where_(where) { } int get_err() const { - return err; + return err_; } + + std::string + get_where() const + { + return where_; + } + private: - int err; + int err_; + std::string where_; }; + std::ostream& operator<<(std::ostream& os, const gspn_exeption& e) + { + os << e.get_where() << " exited with " << e.get_err(); + return os; + } class gspn_environment : public ltl::environment { diff --git a/iface/gspn/gspnlib.h b/iface/gspn/gspnlib.h deleted file mode 100644 index 62c7696ad..000000000 --- a/iface/gspn/gspnlib.h +++ /dev/null @@ -1,104 +0,0 @@ -#ifndef __GSPN_LIB_H__ -#define __GSPN_LIB_H__ - -/* Header file defining functions for Spot API */ - -#include - -#ifdef __cplusplus -extern "C" { -#endif - -/* -------------- Interface type definitions -------------- */ - -typedef unsigned long AtomicProp; -typedef AtomicProp * pAtomicProp; -typedef enum {STATE_PROP,EVENT_PROP} AtomicPropKind; -typedef AtomicPropKind * pAtomicPropKind; - -typedef unsigned long State; -typedef State * pState; - -typedef struct EventPropSucc { - State s; - AtomicProp p; -} EventPropSucc; - -#define EVENT_TRUE 0 - - -/* ----------------- Utility Functions --------------------*/ - -/* Initialize data structures to work with model and properties - MANDATORY : should be called before any other function in this library - Non 0 return correspond to errors in initialization - Call with arguments similar to WNRG/WNSRG/WNERG -*/ -int initialize (int argc, char **argv); -/* Close and cleanup after using the library */ -int finalize (void); - - -/* ----------------- Property related Functions ----------------*/ - -/* Returns the index of the property given as "name" - Non zero return = error codes */ -int prop_index (const char * name, pAtomicProp propindex); - -/* Returns the type of "prop" in "kind" - non zero return = error codes -*/ -int prop_kind (const AtomicProp prop, pAtomicPropKind kind); - - -/* ------------------ State Space Exploration -----------------*/ - -/* Returns the identifier of the initial marking state */ -int initial_state (pState M0); - -/* Given a state "s" and a list of "props_size" property indexes - "props" checks the truth value of every atomic property in "props" - and returns in "truth" the truth value of these properties in the - same order as the input, ONE CHAR PER TRUTH VALUE - (i.e. sizeof(truth[]) = props_size). - - NB : the vector "truth" is allocated in this function -*/ -int satisfy (const State s, const AtomicProp props [], - unsigned char ** truth, size_t props_size); - -/* free the "truth" vector allocated by satisfy - !!! NB: Don't forget to call me, or you will get a memory leak !!! -*/ -int satisfy_free (unsigned char * truth); - - -/* Calculates successors of a state "s" that can be reached by - verifying at least one event property specified in - "enabled_events". In our first implementation enabled events is - discarded, and ALL successors will be returned. This behavior is - also obtained by giving "TRUE" in the list of enabled events. Each - successor is returned in a struct that gives the Event property - verified by the transition fired to reach this marking; If a - marking is reached by firing a transition observed by more than one - event property, it will be returned in many copies: i.e. E1 and E2 - observe different firngs of transition t1; M1 is reached from M0 - by firing t1 with a binding observable by both E1 and E2 : succ - (M0, [E1,E2] , ...) will return {[M1,E1],[M1,E2]} - - NB : "succ" vector is allocated in the function, use succ_free for - memory release -*/ -int succ (const State s, - const AtomicProp enabled_events [], size_t enabled_events_size, - EventPropSucc ** succ, size_t * succ_size); - -/* free the "succ" vector allocated by succ - !!! NB: Don't forget to call me, or you will get a memory leak !!! -*/ -int succ_free (EventPropSucc * succ); - -#ifdef __cplusplus -} -#endif /* __cplusplus */ -#endif /* __GSPN_LIB_H__ */ diff --git a/m4/gspnlin.m4 b/m4/gspnlin.m4 new file mode 100644 index 000000000..f6e4fe891 --- /dev/null +++ b/m4/gspnlin.m4 @@ -0,0 +1,29 @@ +AC_DEFUN([AX_CHECK_GSPNLIB], [ + AC_ARG_WITH([gspn], + [AC_HELP_STRING([--with-gpsn=/root/of/greatspn], + [build interface with GreadSPN])]) + if test x${with_gspn-no} != xno; then + ax_tmp_LDFLAGS=$LDFLAGS + ax_tmp_LIBS=$LIBS + LIBGSPN_LDFLAGS= + 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.])]) + 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_MSG_ERROR([Cannot find libgspnRG. Check --with-gspn's argument.])], [-lm -lfl]) + LIBGSPN_LDFLAGS="$LIBGSPN_LDFLAGS -lgspnRG -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]) +])