[mc] Register symbols as pointers in the examples

diff --git a/examples/msg/mc/bugged1_liveness.c b/examples/msg/mc/bugged1_liveness.c
index 5143623..c5e9820 100644 (file)
--- a/examples/msg/mc/bugged1_liveness.c
+++ b/examples/msg/mc/bugged1_liveness.c
@@ -26,14 +26,6 @@ XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages");
 int r=0; 
 int cs=0;
 
-int predR(){
-  return r;
-}
-
-int predCS(){
-  return cs;
-}
-
 #ifdef GARBAGE_STACK
 /** Do not use a clean stack */
 static void garbage_stack(void) {
@@ -165,8 +157,8 @@ int main(int argc, char *argv[])
   char **options = &argv[1];
 
   MSG_config("model-check/property","promela_bugged1_liveness");
-  MC_automaton_new_propositional_symbol("r", &predR);
-  MC_automaton_new_propositional_symbol("cs", &predCS);
+  MC_automaton_new_propositional_symbol_pointer("r", &r);
+  MC_automaton_new_propositional_symbol_pointer("cs", &cs);
 
   const char* platform_file = options[0];
   const char* application_file = options[1];

diff --git a/examples/msg/mc/bugged2_liveness.c b/examples/msg/mc/bugged2_liveness.c
index d6beac0..25e2ded 100644 (file)
--- a/examples/msg/mc/bugged2_liveness.c
+++ b/examples/msg/mc/bugged2_liveness.c
@@ -19,11 +19,6 @@ XBT_LOG_NEW_DEFAULT_CATEGORY(bugged3, "my log messages");
  
 int cs = 0;
 
-int predCS(){
-  return cs;
-}
-
-
 int coordinator(int argc, char **argv);
 int client(int argc, char **argv);
 
@@ -103,7 +98,7 @@ int main(int argc, char *argv[])
   MSG_init(&argc, argv);
 
   MSG_config("model-check/property","promela_bugged2_liveness");
-  MC_automaton_new_propositional_symbol("cs", &predCS);
+  MC_automaton_new_propositional_symbol_pointer("cs", &cs);
   
   MSG_create_environment("../msg_platform.xml");
   MSG_function_register("coordinator", coordinator);

diff --git a/examples/smpi/mc/bugged1_liveness.c b/examples/smpi/mc/bugged1_liveness.c
index 68a5ef4..b92f4e3 100644 (file)
--- a/examples/smpi/mc/bugged1_liveness.c
+++ b/examples/smpi/mc/bugged1_liveness.c
@@ -23,15 +23,6 @@
 
 int r, cs;
 
-static int predR(){
-  return r;
-}
-
-static int predCS(){
-  return cs;
-}
-
-
 int main(int argc, char **argv){
 
   int err, size, rank;
@@ -47,8 +38,8 @@ int main(int argc, char **argv){
     exit(1);
   }
 
-  MC_automaton_new_propositional_symbol("r", &predR);
-  MC_automaton_new_propositional_symbol("cs", &predCS);
+  MC_automaton_new_propositional_symbol_pointer("r", &r);
+  MC_automaton_new_propositional_symbol_pointer("cs", &cs);
 
   MC_ignore(&(status.count), sizeof(status.count));
 

diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index cc1888e..6ce5570 100644 (file)
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -40,6 +40,7 @@ extern int _sg_mc_visited;
 
 XBT_PUBLIC(void) MC_assert(int);
 XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, int(*fct)(void));
+XBT_PUBLIC(void) MC_automaton_new_propositional_symbol_pointer(const char *id, int* value);
 XBT_PUBLIC(void *) MC_snapshot(void);
 XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2);
 XBT_PUBLIC(void) MC_cut(void);
@@ -52,6 +53,7 @@ XBT_PUBLIC(void) MC_ignore(void *addr, size_t size);
 
 #define MC_assert(a)                    xbt_assert(a)
 #define MC_automaton_new_propositional_symbol(a, b) ((void)0)
+#define MC_automaton_new_propositional_symbol_pointer(a, b) ((void)0)
 #define MC_snapshot()                   ((void*)0)
 #define MC_compare_snapshots(a, b)      0
 #define MC_cut()                        ((void)0)

diff --git a/include/xbt/automaton.h b/include/xbt/automaton.h
index ade3328..ef112fa 100644 (file)
--- a/include/xbt/automaton.h
+++ b/include/xbt/automaton.h
@@ -98,6 +98,12 @@ 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, int(*fct)(void));
 
+XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new_pointer(xbt_automaton_t a, const char* id, int* value);
+
+XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new_callback(
+  xbt_automaton_t a, const char* id,
+  int(*callback)(void*), void* data, void (*free_function)(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);

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 9b29b4e..4b9cf04 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -710,6 +710,15 @@ void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void))
   mmalloc_set_current_heap(heap);
 }
 
+void MC_automaton_new_propositional_symbol_pointer(const char *id, int* value)
+{
+  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+  if (_mc_property_automaton == NULL)
+    _mc_property_automaton = xbt_automaton_new();
+  xbt_automaton_propositional_symbol_new_pointer(_mc_property_automaton, id, value);
+  mmalloc_set_current_heap(heap);
+}
+
 void MC_dump_stacks(FILE* file)
 {
   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);

diff --git a/src/xbt/automaton/automaton.c b/src/xbt/automaton/automaton.c
index 43f389c..b9308e6 100644 (file)
--- a/src/xbt/automaton/automaton.c
+++ b/src/xbt/automaton/automaton.c
@@ -237,6 +237,32 @@ xbt_automaton_propositional_symbol_t xbt_automaton_propositional_symbol_new(xbt_
   return prop_symb;
 }
 
+XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new_pointer(xbt_automaton_t a, const char* id, int* value)
+{
+  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 = NULL;
+  prop_symb->data = value;
+  prop_symb->free_function = NULL;
+  xbt_dynar_push(a->propositional_symbols, &prop_symb);
+  return prop_symb;
+}
+
+XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new_callback(
+  xbt_automaton_t a, const char* id,
+  int(*callback)(void*), void* data, void (*free_function)(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 = callback;
+  prop_symb->data = data;
+  prop_symb->free_function = free_function;
+  xbt_dynar_push(a->propositional_symbols, &prop_symb);
+  return prop_symb;
+}
+
 int xbt_automaton_state_compare(xbt_automaton_state_t s1, xbt_automaton_state_t s2){
 
   /* single id for each state, id and type sufficient for comparison*/