From: Gabriel Corona Date: Tue, 10 Feb 2015 11:32:34 +0000 (+0100) Subject: [mc] Register symbols as pointers in the examples X-Git-Tag: v3_12~732^2~123 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/1a6e40bce6e758aa2e7afffbfd3c6b63063f1472 [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 5143623f2e..c5e9820a3b 100644 --- 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 d6beac0f42..25e2dedd2e 100644 --- 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 68a5ef4671..b92f4e3909 100644 --- 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 cc1888eca0..6ce5570b04 100644 --- 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 ade3328389..ef112fa2d0 100644 --- 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 9b29b4e0de..4b9cf0429e 100644 --- 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 43f389c2a5..b9308e63d7 100644 --- 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*/