[mc] Extend xbt_propositional_symbols

Add support for:

 * general callbacks with a `void*` argument (the `data` field);

 * as an optimisation, a simple pointer to a variable can be passed in
   the `data` field (this can be used in order to enable the MCer to
   fetch the data directly from the MCed memory without trigerring a
   MCed-side callback);

 * a callback function used to free the `data` field.

diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index b2ce355..cc1888e 100644 (file)
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -39,7 +39,7 @@ extern int _sg_mc_visited;
 #define MC_visited_reduction()          _sg_mc_visited
 
 XBT_PUBLIC(void) MC_assert(int);
 #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);
 XBT_PUBLIC(void *) MC_snapshot(void);
 XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2);
 XBT_PUBLIC(void) MC_cut(void);

diff --git a/include/xbt/automaton.h b/include/xbt/automaton.h
index c24453f..ade3328 100644 (file)
--- a/include/xbt/automaton.h
+++ b/include/xbt/automaton.h
@@ -57,10 +57,7 @@ typedef struct xbt_automaton_transition {
 typedef struct xbt_automaton_transition* xbt_automaton_transition_t;
 
 
 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;
 
 
 typedef struct xbt_automaton_propositional_symbol* xbt_automaton_propositional_symbol_t;
 


@@ -99,7 +96,11 @@ XBT_PUBLIC(void) xbt_automaton_display(xbt_automaton_t a);
 
 XBT_PUBLIC(void) xbt_automaton_exp_label_display(xbt_automaton_exp_label_t l);
 
 
 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);
 
 
 XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_get_current_state(xbt_automaton_t a);
 

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 27c83bd..9b29b4e 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -699,7 +699,7 @@ void MC_automaton_load(const char *file)
   mmalloc_set_current_heap(heap);
 }
 
   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);
 
 {
   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 3799185..d7f46a1 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -28,15 +28,12 @@ xbt_parmap_t parmap;
 
 static xbt_dynar_t get_atomic_propositions_values()
 {
 
 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) {
   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_dynar_push_as(values, int, res);
   }
 


@@ -185,7 +182,7 @@ static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l,
       xbt_automaton_propositional_symbol_t p = NULL;
       xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor,
                         p) {
       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);
       }
           return (int) xbt_dynar_get_as(atomic_propositions_values, cursor,
                                         int);
       }

diff --git a/src/xbt/automaton/automaton.c b/src/xbt/automaton/automaton.c
index 5c63609..43f389c 100644 (file)
--- a/src/xbt/automaton/automaton.c
+++ b/src/xbt/automaton/automaton.c
@@ -9,6 +9,30 @@
 #include "xbt/automaton.h"
 #include <stdio.h> /* printf */
 
 #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);
 xbt_automaton_t xbt_automaton_new(){
   xbt_automaton_t automaton = NULL;
   automaton = xbt_new0(struct xbt_automaton, 1);


@@ -197,11 +221,18 @@ xbt_automaton_state_t xbt_automaton_get_current_state(xbt_automaton_t a){
   return a->current_state;
 }
 
   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);
   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;
 }
   xbt_dynar_push(a->propositional_symbols, &prop_symb);
   return prop_symb;
 }


@@ -354,7 +385,11 @@ static void xbt_automaton_propositional_symbol_free(xbt_automaton_propositional_
 }
 
 void xbt_automaton_propositional_symbol_free_voidp(void *ps){
 }
 
 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){
 }
 
 void xbt_automaton_free(xbt_automaton_t a){