#define MC_visited_reduction() _sg_mc_visited
XBT_PUBLIC(void) MC_assert(int);
-XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, void* fct);
+XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, int(*fct)(void));
XBT_PUBLIC(void *) MC_snapshot(void);
XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2);
XBT_PUBLIC(void) MC_cut(void);
typedef struct xbt_automaton_transition* xbt_automaton_transition_t;
-typedef struct xbt_automaton_propositional_symbol{
- char* pred;
- void* function;
-} s_xbt_automaton_propositional_symbol;
+typedef struct xbt_automaton_propositional_symbol s_xbt_automaton_propositional_symbol;
typedef struct xbt_automaton_propositional_symbol* xbt_automaton_propositional_symbol_t;
XBT_PUBLIC(void) xbt_automaton_exp_label_display(xbt_automaton_exp_label_t l);
-XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, void* fct);
+XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, int(*fct)(void));
+
+XBT_PUBLIC(int) xbt_automaton_propositional_symbol_evaluate(xbt_automaton_propositional_symbol_t symbol);
+
+char* xbt_automaton_propositional_symbol_get_name(xbt_automaton_propositional_symbol_t symbol);
XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_get_current_state(xbt_automaton_t a);
mmalloc_set_current_heap(heap);
}
-void MC_automaton_new_propositional_symbol(const char *id, void *fct)
+void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void))
{
xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
static xbt_dynar_t get_atomic_propositions_values()
{
- int res;
- int_f_void_t f;
unsigned int cursor = 0;
xbt_automaton_propositional_symbol_t ps = NULL;
xbt_dynar_t values = xbt_dynar_new(sizeof(int), NULL);
// FIXME, cross-process support
xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps) {
- f = (int_f_void_t) ps->function;
- res = f();
+ int res = xbt_automaton_propositional_symbol_evaluate(ps);
xbt_dynar_push_as(values, int, res);
}
xbt_automaton_propositional_symbol_t p = NULL;
xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor,
p) {
- if (strcmp(p->pred, l->u.predicat) == 0)
+ if (strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0)
return (int) xbt_dynar_get_as(atomic_propositions_values, cursor,
int);
}
#include "xbt/automaton.h"
#include <stdio.h> /* printf */
+struct xbt_automaton_propositional_symbol{
+ char* pred;
+ /** Callback used to evaluate the value of the symbol */
+ int (*function)(void*);
+ /** Additional data for the callback.
+ Alternatively it can be used as a pointer to the data. */
+ void* data;
+ //** Optional callback used to free the data field */
+ void (*free_function)(void*);
+};
+
+int xbt_automaton_propositional_symbol_evaluate(xbt_automaton_propositional_symbol_t symbol)
+{
+ if (symbol->function)
+ return (symbol->function)(symbol->data);
+ else
+ return *(int*) symbol->data;
+}
+
+char* xbt_automaton_propositional_symbol_get_name(xbt_automaton_propositional_symbol_t symbol)
+{
+ return symbol->pred;
+}
+
xbt_automaton_t xbt_automaton_new(){
xbt_automaton_t automaton = NULL;
automaton = xbt_new0(struct xbt_automaton, 1);
return a->current_state;
}
-xbt_automaton_propositional_symbol_t xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, void* fct){
+static int call_simple_function(void* function)
+{
+ return ((int (*)(void)) function)();
+}
+
+xbt_automaton_propositional_symbol_t xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, int(*fct)(void)){
xbt_automaton_propositional_symbol_t prop_symb = NULL;
prop_symb = xbt_new0(struct xbt_automaton_propositional_symbol, 1);
prop_symb->pred = strdup(id);
- prop_symb->function = fct;
+ prop_symb->function = call_simple_function;
+ prop_symb->data = fct;
+ prop_symb->free_function = NULL;
xbt_dynar_push(a->propositional_symbols, &prop_symb);
return prop_symb;
}
}
void xbt_automaton_propositional_symbol_free_voidp(void *ps){
- xbt_automaton_propositional_symbol_free((xbt_automaton_propositional_symbol_t) * (void **) ps);
+ xbt_automaton_propositional_symbol_t symbol = (xbt_automaton_propositional_symbol_t) * (void **) ps;
+ if (symbol->free_function)
+ symbol->free_function(symbol->data);
+ xbt_free(symbol->pred);
+ xbt_automaton_propositional_symbol_free(symbol);
}
void xbt_automaton_free(xbt_automaton_t a){