* iface/gspn/gspnlib.h: Fit 80 columns.
[__cplusplus]: Wrap everything under extern "C".
This commit is contained in:
Alexandre Duret-Lutz
parent
5f55663ad3
commit
aaeb297aed
2 changed files with 59 additions and 47 deletions
|
|
@ -1,10 +1,13 @@
|
|||
2003-07-07 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
||||
|
||||
* 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.
|
||||
|
|
|
|||
|
|
@ -1,24 +1,28 @@
|
|||
#ifndef __GSPN_LIB_H__
|
||||
#define __GSPN_LIB_H__
|
||||
|
||||
#include "stdlib.h"
|
||||
g
|
||||
/* Header file defining functions for Spot API */
|
||||
|
||||
#include <stdlib.h>
|
||||
|
||||
#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__ */
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue