From aaeb297aedc78b3d3448c5119df5ee0079937465 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 7 Jul 2003 12:37:45 +0000 Subject: [PATCH] * iface/gspn/gspnlib.h: Fit 80 columns. [__cplusplus]: Wrap everything under extern "C". --- ChangeLog | 9 ++-- iface/gspn/gspnlib.h | 97 ++++++++++++++++++++++++-------------------- 2 files changed, 59 insertions(+), 47 deletions(-) diff --git a/ChangeLog b/ChangeLog index 232401a78..5a70dd684 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,10 +1,13 @@ 2003-07-07 Alexandre Duret-Lutz - * src/tgba/succiterconcrete.hh + * iface/gspn/gspnlib.h: Fit 80 columns. + [__cplusplus]: Wrap everything under extern "C". + + * src/tgba/succiterconcrete.hh (tgba_succ_iterator_concrete::current_acc_): New attribute. - * src/tgba/succiterconcrete.cc + * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Set current_acc_. - (tgba_succ_iterator_concrete::current_accepting_conditions): + (tgba_succ_iterator_concrete::current_accepting_conditions): Simply return it. * configure.ac: Output iface/Makefile and iface/gspn/Makefile. diff --git a/iface/gspn/gspnlib.h b/iface/gspn/gspnlib.h index 2f5bda099..33e183ef1 100644 --- a/iface/gspn/gspnlib.h +++ b/iface/gspn/gspnlib.h @@ -1,24 +1,28 @@ #ifndef __GSPN_LIB_H__ #define __GSPN_LIB_H__ -#include "stdlib.h" -g /* Header file defining functions for Spot API */ +#include + +#ifdef __cplusplus +extern "C" { +#endif + /* -------------- Interface type definitions -------------- */ -typedef unsigned long AtomicProp; +typedef unsigned long AtomicProp; typedef AtomicProp * pAtomicProp; -typedef enum {STATE_PROP,EVENT_PROP} AtomicPropKind; -typedef AtomicPropKind * pAtomicPropKind ; +typedef enum {STATE_PROP,EVENT_PROP} AtomicPropKind; +typedef AtomicPropKind * pAtomicPropKind; -typedef unsigned long State; -typedef State * pState ; +typedef unsigned long State; +typedef State * pState; typedef struct EventPropSucc { State s; - AtomicProp p; -} EventPropSucc ; + AtomicProp p; +} EventPropSucc; #define EVENT_TRUE 0 @@ -26,25 +30,25 @@ typedef struct EventPropSucc { /* ----------------- Utility Functions --------------------*/ /* Initialize data structures to work with model and properties - MANDATORY : should be called before any other function in this library + 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) ; +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" +/* Returns the index of the property given as "name" Non zero return = error codes */ -int prop_index (const char * name, pAtomicProp propindex) ; +int prop_index (const char * name, pAtomicProp propindex); -/* Returns the type of "prop" in "kind" - non zero return = error codes +/* Returns the type of "prop" in "kind" + non zero return = error codes */ -int prop_kind ( const AtomicProp prop, pAtomicPropKind kind) ; +int prop_kind (const AtomicProp prop, pAtomicPropKind kind); /* ------------------ State Space Exploration -----------------*/ @@ -52,44 +56,49 @@ int prop_kind ( const AtomicProp prop, pAtomicPropKind kind) ; /* 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); +/* 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). -/* free the "truth" vector allocated by satisfy + 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]} +/* 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 + 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, +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 +/* 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 +int succ_free (EventPropSucc * succ); +#ifdef __cplusplus +} +#endif /* __cplusplus */ +#endif /* __GSPN_LIB_H__ */