From 24427cccdbe3734d7f939fa6fbce97107dec302b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 7 Jul 2003 09:55:30 +0000 Subject: [PATCH] * configure.ac: Output iface/Makefile and iface/gspn/Makefile. * iface/Makefile.am, iface/gspn/Makefile.am: New files. * Makefile.am (SUBDIRS): Add iface. * iface/gspn/gspnlib.h: New file, from Yann and Souheib. --- ChangeLog | 7 +++- Makefile.am | 3 +- configure.ac | 2 + iface/Makefile.am | 1 + iface/gspn/Makefile.am | 6 +++ iface/gspn/gspnlib.h | 95 ++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 111 insertions(+), 3 deletions(-) create mode 100644 iface/Makefile.am create mode 100644 iface/gspn/Makefile.am create mode 100644 iface/gspn/gspnlib.h diff --git a/ChangeLog b/ChangeLog index 15d382649..7908650f3 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,8 +1,13 @@ 2003-07-07 Alexandre Duret-Lutz + * configure.ac: Output iface/Makefile and iface/gspn/Makefile. + * iface/Makefile.am, iface/gspn/Makefile.am: New files. + * Makefile.am (SUBDIRS): Add iface. + * iface/gspn/gspnlib.h: New file, from Yann and Souheib. + * src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::tgba_bdd_core_data, tgba_bdd_core_data::translate): Handle all_accepting_conditions. - * src/tgba/tgbabddconcretefactory.cc + * src/tgba/tgbabddconcretefactory.cc (tgba_bdd_concrete_factory::finish): Fill all_accepting_conditions. 2003-07-04 Alexandre Duret-Lutz diff --git a/Makefile.am b/Makefile.am index 965a181c0..a9a1e6eb1 100644 --- a/Makefile.am +++ b/Makefile.am @@ -2,8 +2,7 @@ if WITH_INCLUDED_BUDDY MAYBE_BUDDY = buddy endif WITH_INCLUDED_BUDDY -SUBDIRS = $(MAYBE_BUDDY) doc src wrap +SUBDIRS = $(MAYBE_BUDDY) doc src wrap iface ACLOCAL_AMFLAGS = -I m4 EXTRA_DIST = m4/gccwarn.m4 m4/pypath.m4 m4/buddy.m4 HACKING - diff --git a/configure.ac b/configure.ac index b4969cb8a..463b43d19 100644 --- a/configure.ac +++ b/configure.ac @@ -24,6 +24,8 @@ AC_CONFIG_FILES([ Makefile doc/Makefile doc/Doxyfile + iface/Makefile + iface/gspn/Makefile src/Makefile src/ltlenv/Makefile src/ltlast/Makefile diff --git a/iface/Makefile.am b/iface/Makefile.am new file mode 100644 index 000000000..c1f8b94aa --- /dev/null +++ b/iface/Makefile.am @@ -0,0 +1 @@ +SUBDIRS = gspn diff --git a/iface/gspn/Makefile.am b/iface/gspn/Makefile.am new file mode 100644 index 000000000..cc63b1307 --- /dev/null +++ b/iface/gspn/Makefile.am @@ -0,0 +1,6 @@ +AM_CPPFLAGS = -I$(top_srcdir)/src +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +lib_LTLIBRARIES = libspotgspn.la +libspotgspn_la_SOURCES = \ + gspnlib.h diff --git a/iface/gspn/gspnlib.h b/iface/gspn/gspnlib.h new file mode 100644 index 000000000..2f5bda099 --- /dev/null +++ b/iface/gspn/gspnlib.h @@ -0,0 +1,95 @@ +#ifndef __GSPN_LIB_H__ +#define __GSPN_LIB_H__ + +#include "stdlib.h" +g +/* Header file defining functions for Spot API */ + +/* -------------- 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 ); + + + + +#endif +