From 3a54b6d1aef3110883b46f912b3a4eeb5c9fb087 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 19 Mar 2013 13:41:22 +0100 Subject: [PATCH] model-checker : cleanups - remove (a part of) redundant code - rename structs and variables - update headers --- buildtools/Cmake/DefinePackages.cmake | 1 + include/xbt/automaton.h | 84 +++---- src/mc/mc_checkpoint.c | 2 +- src/mc/mc_compare.c | 15 +- src/mc/mc_dpor.c | 26 +-- src/mc/mc_global.c | 53 ++--- src/mc/mc_liveness.c | 254 ++++++++------------- src/mc/mc_memory.c | 2 +- src/mc/mc_pair.c | 24 ++ src/mc/mc_private.h | 93 +++----- src/mc/mc_request.c | 2 +- src/mc/mc_state.c | 14 +- src/mc/memory_map.c | 2 +- src/xbt/automaton/automaton.c | 146 ++++++------ src/xbt/automaton/automatonparse_promela.c | 36 +-- src/xbt/automaton/parserPromela.tab.hacc | 2 +- src/xbt/automaton/parserPromela.yacc | 2 +- 17 files changed, 337 insertions(+), 421 deletions(-) create mode 100644 src/mc/mc_pair.c diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake index 930c233cf5..2ff4816baa 100644 --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@ -423,6 +423,7 @@ set(MC_SRC src/mc/mc_request.c src/mc/mc_state.c src/mc/memory_map.c + src/mc/mc_pair.c ) set(headers_to_install diff --git a/include/xbt/automaton.h b/include/xbt/automaton.h index 9f577477f2..0cdf31f64c 100644 --- a/include/xbt/automaton.h +++ b/include/xbt/automaton.h @@ -9,111 +9,111 @@ SG_BEGIN_DECL() -typedef struct xbt_state { +typedef struct xbt_automaton_state { char* id; int type; /* -1 = init, 0 = inter, 1 = final */ xbt_dynar_t in; xbt_dynar_t out; -} s_xbt_state; +} s_xbt_automaton_state; -typedef struct xbt_state* xbt_state_t; +typedef struct xbt_automaton_state* xbt_automaton_state_t; typedef struct xbt_automaton { xbt_dynar_t propositional_symbols; xbt_dynar_t transitions; xbt_dynar_t states; - xbt_state_t current_state; + xbt_automaton_state_t current_state; } s_xbt_automaton; typedef struct xbt_automaton* xbt_automaton_t; -typedef struct xbt_exp_label{ +typedef struct xbt_automaton_exp_label{ enum{or=0, and=1, not=2, predicat=3, one=4} type; union{ struct{ - struct xbt_exp_label* left_exp; - struct xbt_exp_label* right_exp; + struct xbt_automaton_exp_label* left_exp; + struct xbt_automaton_exp_label* right_exp; }or_and; - struct xbt_exp_label* exp_not; + struct xbt_automaton_exp_label* exp_not; char* predicat; }u; -} s_xbt_exp_label; +} s_xbt_automaton_exp_label; -typedef struct xbt_exp_label* xbt_exp_label_t; +typedef struct xbt_automaton_exp_label* xbt_automaton_exp_label_t; -typedef struct xbt_transition { - xbt_state_t src; - xbt_state_t dst; - xbt_exp_label_t label; -} s_xbt_transition; +typedef struct xbt_automaton_transition { + xbt_automaton_state_t src; + xbt_automaton_state_t dst; + xbt_automaton_exp_label_t label; +} s_xbt_automaton_transition; -typedef struct xbt_transition* xbt_transition_t; +typedef struct xbt_automaton_transition* xbt_automaton_transition_t; -typedef struct xbt_propositional_symbol{ +typedef struct xbt_automaton_propositional_symbol{ char* pred; void* function; -} s_xbt_propositional_symbol; +} s_xbt_automaton_propositional_symbol; -typedef struct xbt_propositional_symbol* xbt_propositional_symbol_t; +typedef struct xbt_automaton_propositional_symbol* xbt_automaton_propositional_symbol_t; XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new(void); XBT_PUBLIC(void) xbt_automaton_load(xbt_automaton_t automaton, const char *file); -XBT_PUBLIC(xbt_state_t) xbt_automaton_new_state(xbt_automaton_t a, int type, char* id); +XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_state_new(xbt_automaton_t a, int type, char* id); -XBT_PUBLIC(xbt_transition_t) xbt_automaton_new_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst, xbt_exp_label_t label); +XBT_PUBLIC(xbt_automaton_transition_t) xbt_automaton_transition_new(xbt_automaton_t a, xbt_automaton_state_t src, xbt_automaton_state_t dst, xbt_automaton_exp_label_t label); -XBT_PUBLIC(xbt_exp_label_t) xbt_automaton_new_label(int type, ...); +XBT_PUBLIC(xbt_automaton_exp_label_t) xbt_automaton_exp_label_new(int type, ...); XBT_PUBLIC(xbt_dynar_t) xbt_automaton_get_states(xbt_automaton_t a); XBT_PUBLIC(xbt_dynar_t) xbt_automaton_get_transitions(xbt_automaton_t a); -XBT_PUBLIC(xbt_transition_t) xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst); +XBT_PUBLIC(xbt_automaton_transition_t) xbt_automaton_get_transition(xbt_automaton_t a, xbt_automaton_state_t src, xbt_automaton_state_t dst); -XBT_PUBLIC(xbt_state_t) xbt_automaton_transition_get_source(xbt_transition_t t); +XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_transition_get_source(xbt_automaton_transition_t t); -XBT_PUBLIC(xbt_state_t) xbt_automaton_transition_get_destination(xbt_transition_t t); +XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_transition_get_destination(xbt_automaton_transition_t t); -XBT_PUBLIC(void) xbt_automaton_transition_set_source(xbt_transition_t t, xbt_state_t src); +XBT_PUBLIC(void) xbt_automaton_transition_set_source(xbt_automaton_transition_t t, xbt_automaton_state_t src); -XBT_PUBLIC(void) xbt_automaton_transition_set_destination(xbt_transition_t t, xbt_state_t dst); +XBT_PUBLIC(void) xbt_automaton_transition_set_destination(xbt_automaton_transition_t t, xbt_automaton_state_t dst); -XBT_PUBLIC(xbt_dynar_t) xbt_automaton_state_get_out_transitions(xbt_state_t s); +XBT_PUBLIC(xbt_dynar_t) xbt_automaton_state_get_out_transitions(xbt_automaton_state_t s); -XBT_PUBLIC(xbt_dynar_t) xbt_automaton_state_get_in_transitions(xbt_state_t s); +XBT_PUBLIC(xbt_dynar_t) xbt_automaton_state_get_in_transitions(xbt_automaton_state_t s); -XBT_PUBLIC(xbt_state_t) xbt_automaton_state_exists(xbt_automaton_t a, char *id); +XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_state_exists(xbt_automaton_t a, char *id); XBT_PUBLIC(void) xbt_automaton_display(xbt_automaton_t a); -XBT_PUBLIC(void) xbt_automaton_display_exp(xbt_exp_label_t l); +XBT_PUBLIC(void) xbt_automaton_exp_label_display(xbt_automaton_exp_label_t l); -XBT_PUBLIC(xbt_propositional_symbol_t) xbt_new_propositional_symbol(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, void* fct); -XBT_PUBLIC(xbt_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); -XBT_PUBLIC(int) automaton_state_compare(xbt_state_t s1, xbt_state_t s2); +XBT_PUBLIC(int) xbt_automaton_state_compare(xbt_automaton_state_t s1, xbt_automaton_state_t s2); -XBT_PUBLIC(int) propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2); +XBT_PUBLIC(int) xbt_automaton_propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2); -XBT_PUBLIC(int) automaton_transition_compare(const void *t1, const void *t2); +XBT_PUBLIC(int) xbt_automaton_transition_compare(const void *t1, const void *t2); -XBT_PUBLIC(int) automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2); +XBT_PUBLIC(int) xbt_automaton_exp_label_compare(xbt_automaton_exp_label_t l1, xbt_automaton_exp_label_t l2); -XBT_PUBLIC(void) xbt_state_free_voidp(void *s); +XBT_PUBLIC(void) xbt_automaton_state_free_voidp(void *s); -XBT_PUBLIC(void) xbt_state_free(xbt_state_t s); +XBT_PUBLIC(void) xbt_automaton_state_free(xbt_automaton_state_t s); -XBT_PUBLIC(void) xbt_transition_free_voidp(void *t); +XBT_PUBLIC(void) xbt_automaton_transition_free_voidp(void *t); -XBT_PUBLIC(void) xbt_exp_label_free_voidp(void *e); +XBT_PUBLIC(void) xbt_automaton_exp_label_free_voidp(void *e); -XBT_PUBLIC(void) xbt_propositional_symbol_free_voidp(void *ps); +XBT_PUBLIC(void) xbt_automaton_propositional_symbol_free_voidp(void *ps); XBT_PUBLIC(void) xbt_automaton_free(xbt_automaton_t a); diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index cc87fe8644..9b0650a961 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 693bcae9d9..73886842c9 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */ +/* Copyright (c) 2012-2013 Da SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ @@ -41,7 +41,7 @@ static size_t heap_ignore_size(void *address){ return 0; } -static int compare_global_variables(int region_type, void *d1, void *d2){ +static int compare_global_variables(int region_type, void *d1, void *d2){ /* region_type = 1 -> libsimgrid, region_type = 2 -> binary */ unsigned int cursor = 0; size_t offset; @@ -192,7 +192,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ #ifdef MC_VERBOSE XBT_VERB("Different number of processes : %d - %d", s1->nb_processes, s2->nb_processes); #endif - + xbt_os_timer_free(timer); xbt_os_timer_stop(global_timer); mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer); @@ -261,7 +261,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ #ifdef MC_VERBOSE XBT_VERB("Different size used in stacks : %zu - %zu", size_used1, size_used2); #endif - + xbt_os_timer_free(timer); xbt_os_timer_stop(global_timer); mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer); @@ -294,7 +294,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ #ifdef MC_VERBOSE XBT_VERB("Different hash of global variables : %s - %s", s1->hash_global, s2->hash_global); #endif - + xbt_os_timer_free(timer); xbt_os_timer_stop(global_timer); mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer); @@ -324,7 +324,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ #ifdef MC_VERBOSE XBT_VERB("Different hash of local variables : %s - %s", s1->hash_local, s2->hash_local); #endif - + xbt_os_timer_free(timer); xbt_os_timer_stop(global_timer); mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer); @@ -357,7 +357,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ #ifdef MC_VERBOSE XBT_VERB("Different global variables in binary"); #endif - + reset_heap_information(); xbt_os_timer_free(timer); xbt_os_timer_stop(global_timer); @@ -600,6 +600,7 @@ static int compare_local_variables(char *s1, char *s2){ #ifdef MC_DEBUG XBT_DEBUG("Different local variable : %s (%s - %s)", var_name, xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *)); #endif + xbt_dynar_free(&s_tokens1); xbt_dynar_free(&s_tokens2); xbt_dynar_free(&tokens1); diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index c52988b0ad..06e03d9735 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2012. Da SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-2013. Da SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ @@ -11,10 +11,10 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc, xbt_dynar_t visited_states; static int is_visited_state(void); -static void visited_state_free(mc_safety_visited_state_t state); +static void visited_state_free(mc_visited_state_t state); static void visited_state_free_voidp(void *s); -static void visited_state_free(mc_safety_visited_state_t state){ +static void visited_state_free(mc_visited_state_t state){ if(state){ MC_free_snapshot(state->system_state); xbt_free(state); @@ -22,7 +22,7 @@ static void visited_state_free(mc_safety_visited_state_t state){ } static void visited_state_free_voidp(void *s){ - visited_state_free((mc_safety_visited_state_t) * (void **) s); + visited_state_free((mc_visited_state_t) * (void **) s); } static int is_visited_state(){ @@ -34,8 +34,8 @@ static int is_visited_state(){ MC_SET_RAW_MEM; - mc_safety_visited_state_t new_state = NULL; - new_state = xbt_new0(s_mc_safety_visited_state_t, 1); + mc_visited_state_t new_state = NULL; + new_state = xbt_new0(s_mc_visited_state_t, 1); new_state->system_state = MC_take_snapshot(); new_state->num = mc_stats->expanded_states; @@ -63,13 +63,13 @@ static int is_visited_state(){ int start = 0; int end = xbt_dynar_length(visited_states) - 1; - mc_safety_visited_state_t state_test = NULL; + mc_visited_state_t state_test = NULL; size_t bytes_used_test; int same_bytes_not_found = 1; while(start <= end && same_bytes_not_found){ cursor = (start + end) / 2; - state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t); + state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t); bytes_used_test = state_test->system_state->heap_bytes_used; if(bytes_used_test < current_bytes_used) start = cursor + 1; @@ -90,7 +90,7 @@ static int is_visited_state(){ /* Search another state with same number of bytes used */ previous_cursor = cursor - 1; while(previous_cursor >= 0){ - state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_safety_visited_state_t); + state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_visited_state_t); bytes_used_test = state_test->system_state->heap_bytes_used; if(bytes_used_test != current_bytes_used) break; @@ -108,7 +108,7 @@ static int is_visited_state(){ } next_cursor = cursor + 1; while(next_cursor < xbt_dynar_length(visited_states)){ - state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_safety_visited_state_t); + state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_visited_state_t); bytes_used_test = state_test->system_state->heap_bytes_used; if(bytes_used_test != current_bytes_used) break; @@ -128,7 +128,7 @@ static int is_visited_state(){ } } - state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t); + state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t); bytes_used_test = state_test->system_state->heap_bytes_used; if(bytes_used_test < current_bytes_used) @@ -174,7 +174,7 @@ void MC_dpor_init() MC_SET_RAW_MEM; initial_state = MC_state_new(); - visited_states = xbt_dynar_new(sizeof(mc_safety_visited_state_t), visited_state_free_voidp); + visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); MC_UNSET_RAW_MEM; @@ -322,8 +322,6 @@ void MC_dpor(void) } - - xbt_fifo_unshift(mc_stack_safety, next_state); MC_UNSET_RAW_MEM; diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index b04debeb25..970ef80e3f 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ @@ -95,16 +95,15 @@ char mc_replay_mode = FALSE; double *mc_time = NULL; mc_comparison_times_t mc_comp_times = NULL; double mc_snapshot_comparison_time; +mc_stats_t mc_stats = NULL; /* Safety */ xbt_fifo_t mc_stack_safety = NULL; -mc_stats_t mc_stats = NULL; mc_global_t initial_state_safety = NULL; /* Liveness */ -mc_stats_pair_t mc_stats_pair = NULL; xbt_fifo_t mc_stack_liveness = NULL; mc_global_t initial_state_liveness = NULL; int compare; @@ -310,13 +309,15 @@ void MC_modelcheck_liveness(){ MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double)); MC_SET_RAW_MEM; - + /* Initialize statistics */ - mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1); + mc_stats = xbt_new0(s_mc_stats_t, 1); + mc_stats->state_size = 1; /* Create exploration stack */ mc_stack_liveness = xbt_fifo_new(); + /* Create the initial state */ initial_state_liveness = xbt_new0(s_mc_global_t, 1); MC_UNSET_RAW_MEM; @@ -324,7 +325,7 @@ void MC_modelcheck_liveness(){ MC_ddfs_init(); /* We're done */ - MC_print_statistics_pairs(mc_stats_pair); + MC_print_statistics(mc_stats); xbt_free(mc_time); if(raw_mem_set) @@ -477,7 +478,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) smx_simcall_t req = NULL, saved_req = NULL; xbt_fifo_item_t item; mc_state_t state; - mc_pair_stateless_t pair; + mc_pair_t pair; int depth = 1; XBT_DEBUG("**** Begin Replay ****"); @@ -496,7 +497,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) while(depth <= xbt_fifo_size(stack)){ - pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item); + pair = (mc_pair_t) xbt_fifo_get_item_content(item); state = (mc_state_t) pair->graph_state; if(pair->requests > 0){ @@ -526,7 +527,8 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) depth++; /* Update statistics */ - mc_stats_pair->visited_pairs++; + mc_stats->visited_states++; + mc_stats->executed_transitions++; item = xbt_fifo_get_prev_item(item); } @@ -538,7 +540,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) item != xbt_fifo_get_first_item(stack); item = xbt_fifo_get_prev_item(item)) { - pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item); + pair = (mc_pair_t) xbt_fifo_get_item_content(item); state = (mc_state_t) pair->graph_state; if(pair->requests > 0){ @@ -568,7 +570,8 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) depth++; /* Update statistics */ - mc_stats_pair->visited_pairs++; + mc_stats->visited_states++; + mc_stats->executed_transitions++; } } @@ -649,13 +652,13 @@ void MC_show_deadlock(smx_simcall_t req) void MC_show_stack_liveness(xbt_fifo_t stack){ int value; - mc_pair_stateless_t pair; + mc_pair_t pair; xbt_fifo_item_t item; smx_simcall_t req; char *req_str = NULL; for (item = xbt_fifo_get_last_item(stack); - (item ? (pair = (mc_pair_stateless_t) (xbt_fifo_get_item_content(item))) + (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item))) : (NULL)); item = xbt_fifo_get_prev_item(item)) { req = MC_state_get_executed_request(pair->graph_state, &value); if(req){ @@ -674,11 +677,11 @@ void MC_dump_stack_liveness(xbt_fifo_t stack){ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); - mc_pair_stateless_t pair; + mc_pair_t pair; MC_SET_RAW_MEM; - while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL) - pair_stateless_free(pair); + while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL) + MC_pair_delete(pair); MC_UNSET_RAW_MEM; if(raw_mem_set) @@ -699,18 +702,6 @@ void MC_print_statistics(mc_stats_t stats) (double)stats->expanded_states / stats->state_size); */ } -void MC_print_statistics_pairs(mc_stats_pair_t stats) -{ - XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs); - XBT_INFO("Visited pairs = %lu", stats->visited_pairs); - //XBT_INFO("Executed transitions = %lu", stats->executed_transitions); - XBT_INFO("Expanded / Visited = %lf", - (double) stats->visited_pairs / stats->expanded_pairs); - - if(mmalloc_get_current_heap() == raw_heap) - MC_UNSET_RAW_MEM; -} - void MC_assert(int prop) { if (MC_is_active() && !prop){ @@ -732,7 +723,7 @@ static void MC_assert_pair(int prop){ //XBT_INFO("Counter-example execution trace:"); MC_show_stack_liveness(mc_stack_liveness); //MC_dump_snapshot_stack(mc_snapshot_stack); - MC_print_statistics_pairs(mc_stats_pair); + MC_print_statistics(mc_stats); xbt_abort(); } } @@ -781,7 +772,7 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) { if (_mc_property_automaton == NULL) _mc_property_automaton = xbt_automaton_new(); - xbt_new_propositional_symbol(_mc_property_automaton,id,fct); + xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct); MC_UNSET_RAW_MEM; @@ -865,7 +856,7 @@ void MC_remove_ignore_heap(void *address, size_t size){ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; - + unsigned int cursor = 0; int start = 0; int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1; diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 06265cb6e0..ac9b74d62e 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */ +/* Copyright (c) 2011-2013 Da SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ @@ -10,56 +10,24 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification"); -xbt_dynar_t reached_pairs; +/********* Global variables *********/ + +xbt_dynar_t acceptance_pairs; xbt_dynar_t visited_pairs; xbt_dynar_t successors; -int create_dump(int pair) -{ - // Try to enable core dumps - struct rlimit core_limit; - core_limit.rlim_cur = RLIM_INFINITY; - core_limit.rlim_max = RLIM_INFINITY; - - if(setrlimit(RLIMIT_CORE, &core_limit) < 0) - fprintf(stderr, "setrlimit: %s\nWarning: core dumps may be truncated or non-existant\n", strerror(errno)); - - int status; - switch(fork()){ - case 0: - // We are the child process -- run the actual program - xbt_abort(); - break; - - case -1: - // An error occurred, shouldn't happen - perror("fork"); - return -1; - - default: - // We are the parent process -- wait for the child process to exit - if(wait(&status) < 0) - perror("wait"); - if(WIFSIGNALED(status) && WCOREDUMP(status)){ - char *core_name = xbt_malloc(20); - sprintf(core_name,"core_%d", pair); - rename("core", core_name); - free(core_name); - } - } - return 0; -} +/********* Static functions *********/ -int reached(xbt_state_t st){ +static int is_reached_acceptance_pair(xbt_automaton_state_t st){ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; - mc_pair_reached_t new_pair = NULL; - new_pair = xbt_new0(s_mc_pair_reached_t, 1); - new_pair->nb = xbt_dynar_length(reached_pairs) + 1; + mc_acceptance_pair_t new_pair = NULL; + new_pair = xbt_new0(s_mc_acceptance_pair_t, 1); + new_pair->num = xbt_dynar_length(acceptance_pairs) + 1; new_pair->automaton_state = st; new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); new_pair->system_state = MC_take_snapshot(); @@ -68,7 +36,7 @@ int reached(xbt_state_t st){ int res; int_f_void_t f; unsigned int cursor = 0; - xbt_propositional_symbol_t ps = NULL; + xbt_automaton_propositional_symbol_t ps = NULL; xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){ f = (int_f_void_t)ps->function; res = f(); @@ -77,11 +45,11 @@ int reached(xbt_state_t st){ MC_UNSET_RAW_MEM; - if(xbt_dynar_is_empty(reached_pairs)/* || !compare*/){ + if(xbt_dynar_is_empty(acceptance_pairs)){ MC_SET_RAW_MEM; - /* New pair reached */ - xbt_dynar_push(reached_pairs, &new_pair); + /* New acceptance pair */ + xbt_dynar_push(acceptance_pairs, &new_pair); MC_UNSET_RAW_MEM; if(raw_mem_set) @@ -94,13 +62,13 @@ int reached(xbt_state_t st){ MC_SET_RAW_MEM; cursor = 0; - mc_pair_reached_t pair_test = NULL; + mc_acceptance_pair_t pair_test = NULL; - xbt_dynar_foreach(reached_pairs, cursor, pair_test){ + xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) - XBT_DEBUG("****** Pair reached #%d ******", pair_test->nb); - if(automaton_state_compare(pair_test->automaton_state, st) == 0){ - if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){ + XBT_DEBUG("****** Pair reached #%d ******", pair_test->num); + if(xbt_automaton_state_compare(pair_test->automaton_state, st) == 0){ + if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){ if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){ if(raw_mem_set) @@ -118,8 +86,8 @@ int reached(xbt_state_t st){ } } - /* New pair reached */ - xbt_dynar_push(reached_pairs, &new_pair); + /* New acceptance pair */ + xbt_dynar_push(acceptance_pairs, &new_pair); MC_UNSET_RAW_MEM; @@ -134,22 +102,22 @@ int reached(xbt_state_t st){ } -void set_pair_reached(xbt_state_t st){ +static void set_acceptance_pair_reached(xbt_automaton_state_t st){ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; - mc_pair_reached_t pair = NULL; - pair = xbt_new0(s_mc_pair_reached_t, 1); - pair->nb = xbt_dynar_length(reached_pairs) + 1; + mc_acceptance_pair_t pair = NULL; + pair = xbt_new0(s_mc_acceptance_pair_t, 1); + pair->num = xbt_dynar_length(acceptance_pairs) + 1; pair->automaton_state = st; pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); pair->system_state = MC_take_snapshot(); /* Get values of propositional symbols */ unsigned int cursor = 0; - xbt_propositional_symbol_t ps = NULL; + xbt_automaton_propositional_symbol_t ps = NULL; int res; int_f_void_t f; @@ -159,7 +127,7 @@ void set_pair_reached(xbt_state_t st){ xbt_dynar_push_as(pair->prop_ato, int, res); } - xbt_dynar_push(reached_pairs, &pair); + xbt_dynar_push(acceptance_pairs, &pair); MC_UNSET_RAW_MEM; @@ -168,7 +136,7 @@ void set_pair_reached(xbt_state_t st){ } -int visited(xbt_state_t st){ +static int is_visited_pair(xbt_automaton_state_t st){ if(_sg_mc_visited == 0) return 0; @@ -177,8 +145,8 @@ int visited(xbt_state_t st){ MC_SET_RAW_MEM; - mc_pair_visited_t new_pair = NULL; - new_pair = xbt_new0(s_mc_pair_visited_t, 1); + mc_visited_pair_t new_pair = NULL; + new_pair = xbt_new0(s_mc_visited_pair_t, 1); new_pair->automaton_state = st; new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); new_pair->system_state = MC_take_snapshot(); @@ -187,7 +155,7 @@ int visited(xbt_state_t st){ int res; int_f_void_t f; unsigned int cursor = 0; - xbt_propositional_symbol_t ps = NULL; + xbt_automaton_propositional_symbol_t ps = NULL; xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){ f = (int_f_void_t)ps->function; res = f(); @@ -213,13 +181,13 @@ int visited(xbt_state_t st){ MC_SET_RAW_MEM; cursor = 0; - mc_pair_visited_t pair_test = NULL; + mc_visited_pair_t pair_test = NULL; xbt_dynar_foreach(visited_pairs, cursor, pair_test){ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) XBT_DEBUG("****** Pair visited #%d ******", cursor + 1); - if(automaton_state_compare(pair_test->automaton_state, st) == 0){ - if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){ + if(xbt_automaton_state_compare(pair_test->automaton_state, st) == 0){ + if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){ if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){ if(raw_mem_set) MC_SET_RAW_MEM; @@ -253,15 +221,7 @@ int visited(xbt_state_t st){ } } -void MC_pair_delete(mc_pair_t pair){ - xbt_free(pair->graph_state->proc_status); - xbt_free(pair->graph_state); - xbt_free(pair); -} - - - -int MC_automaton_evaluate_label(xbt_exp_label_t l){ +static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l){ switch(l->type){ case 0 : { @@ -280,7 +240,7 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){ } case 3 : { unsigned int cursor = 0; - xbt_propositional_symbol_t p = NULL; + xbt_automaton_propositional_symbol_t p = NULL; int_f_void_t f; xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){ if(strcmp(p->pred, l->u.predicat) == 0){ @@ -299,9 +259,9 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){ } -/********************* Double-DFS stateless *******************/ +/********* Free functions *********/ -void pair_visited_free(mc_pair_visited_t pair){ +static void visited_pair_free(mc_visited_pair_t pair){ if(pair){ xbt_dynar_free(&(pair->prop_ato)); MC_free_snapshot(pair->system_state); @@ -309,32 +269,11 @@ void pair_visited_free(mc_pair_visited_t pair){ } } -void pair_visited_free_voidp(void *p){ - pair_visited_free((mc_pair_visited_t) * (void **) p); +static void visited_pair_free_voidp(void *p){ + visited_pair_free((mc_visited_pair_t) * (void **) p); } -void pair_stateless_free(mc_pair_stateless_t pair){ - xbt_free(pair->graph_state->system_state); - xbt_free(pair->graph_state->proc_status); - xbt_free(pair->graph_state); - xbt_free(pair); -} - -void pair_stateless_free_voidp(void *p){ - pair_stateless_free((mc_pair_stateless_t) * (void **) p); -} - -mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){ - mc_pair_stateless_t p = NULL; - p = xbt_new0(s_mc_pair_stateless_t, 1); - p->automaton_state = st; - p->graph_state = sg; - p->requests = r; - mc_stats_pair->expanded_pairs++; - return p; -} - -void pair_reached_free(mc_pair_reached_t pair){ +static void acceptance_pair_free(mc_acceptance_pair_t pair){ if(pair){ xbt_dynar_free(&(pair->prop_ato)); MC_free_snapshot(pair->system_state); @@ -342,10 +281,14 @@ void pair_reached_free(mc_pair_reached_t pair){ } } -void pair_reached_free_voidp(void *p){ - pair_reached_free((mc_pair_reached_t) * (void **) p); +static void acceptance_pair_free_voidp(void *p){ + acceptance_pair_free((mc_acceptance_pair_t) * (void **) p); } + +/********* DDFS Algorithm *********/ + + void MC_ddfs_init(void){ initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap); @@ -354,7 +297,7 @@ void MC_ddfs_init(void){ XBT_DEBUG("Double-DFS init"); XBT_DEBUG("**************************************************"); - mc_pair_stateless_t mc_initial_pair = NULL; + mc_pair_t mc_initial_pair = NULL; mc_state_t initial_graph_state = NULL; smx_process_t process; @@ -363,16 +306,16 @@ void MC_ddfs_init(void){ MC_SET_RAW_MEM; - initial_graph_state = MC_state_pair_new(); + initial_graph_state = MC_state_new(); xbt_swag_foreach(process, simix_global->process_list){ if(MC_process_is_enabled(process)){ MC_state_interleave_process(initial_graph_state, process); } } - reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), pair_reached_free_voidp); - visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), pair_visited_free_voidp); - successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); + acceptance_pairs = xbt_dynar_new(sizeof(mc_acceptance_pair_t), acceptance_pair_free_voidp); + visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), visited_pair_free_voidp); + successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); /* Save the initial state */ initial_state_liveness->snapshot = MC_take_snapshot(); @@ -380,13 +323,13 @@ void MC_ddfs_init(void){ MC_UNSET_RAW_MEM; unsigned int cursor = 0; - xbt_state_t state; + xbt_automaton_state_t automaton_state; - xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){ - if(state->type == -1){ + xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){ + if(automaton_state->type == -1){ MC_SET_RAW_MEM; - mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state)); + mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state)); xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair); MC_UNSET_RAW_MEM; @@ -398,14 +341,14 @@ void MC_ddfs_init(void){ MC_ddfs(0); }else{ - if(state->type == 2){ + if(automaton_state->type == 2){ MC_SET_RAW_MEM; - mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state)); + mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state)); xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair); MC_UNSET_RAW_MEM; - set_pair_reached(state); + set_acceptance_pair_reached(automaton_state); if(cursor != 0){ MC_restore_snapshot(initial_state_liveness->snapshot); @@ -429,17 +372,15 @@ void MC_ddfs_init(void){ void MC_ddfs(int search_cycle){ - //initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap); - smx_process_t process; - mc_pair_stateless_t current_pair = NULL; + mc_pair_t current_pair = NULL; if(xbt_fifo_size(mc_stack_liveness) == 0) return; /* Get current pair */ - current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness)); + current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness)); /* Update current state in buchi automaton */ _mc_property_automaton->current_state = current_pair->automaton_state; @@ -447,24 +388,22 @@ void MC_ddfs(int search_cycle){ XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle); - mc_stats_pair->visited_pairs++; - - //sleep(1); + mc_stats->visited_states++; int value; mc_state_t next_graph_state = NULL; smx_simcall_t req = NULL; char *req_str; - xbt_transition_t transition_succ; + xbt_automaton_transition_t transition_succ; unsigned int cursor = 0; int res; - mc_pair_stateless_t next_pair = NULL; - mc_pair_stateless_t pair_succ; + mc_pair_t next_pair = NULL; + mc_pair_t pair_succ; - mc_pair_stateless_t remove_pair; - mc_pair_reached_t remove_pair_reached; + mc_pair_t pair_to_remove; + mc_acceptance_pair_t acceptance_pair_to_remove; if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){ @@ -491,7 +430,7 @@ void MC_ddfs(int search_cycle){ MC_SET_RAW_MEM; /* Create the new expanded graph_state */ - next_graph_state = MC_state_pair_new(); + next_graph_state = MC_state_new(); /* Get enabled process and insert it in the interleave set of the next graph_state */ xbt_swag_foreach(process, simix_global->process_list){ @@ -518,7 +457,7 @@ void MC_ddfs(int search_cycle){ if(res == 1){ // enabled transition in automaton MC_SET_RAW_MEM; - next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); + next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); xbt_dynar_push(successors, &next_pair); MC_UNSET_RAW_MEM; } @@ -533,7 +472,7 @@ void MC_ddfs(int search_cycle){ if(res == 2){ // true transition in automaton MC_SET_RAW_MEM; - next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); + next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); xbt_dynar_push(successors, &next_pair); MC_UNSET_RAW_MEM; } @@ -548,7 +487,7 @@ void MC_ddfs(int search_cycle){ if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ - if(reached(pair_succ->automaton_state)){ + if(is_reached_acceptance_pair(pair_succ->automaton_state)){ XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state)); @@ -558,12 +497,12 @@ void MC_ddfs(int search_cycle){ XBT_INFO("Counter-example that violates formula :"); MC_show_stack_liveness(mc_stack_liveness); MC_dump_stack_liveness(mc_stack_liveness); - MC_print_statistics_pairs(mc_stats_pair); + MC_print_statistics(mc_stats); xbt_abort(); }else{ - if(visited(pair_succ->automaton_state)){ + if(is_visited_pair(pair_succ->automaton_state)){ XBT_DEBUG("Next pair already visited !"); break; @@ -572,7 +511,7 @@ void MC_ddfs(int search_cycle){ XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id); - XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs)); MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness, pair_succ); @@ -586,7 +525,7 @@ void MC_ddfs(int search_cycle){ }else{ - if(visited(pair_succ->automaton_state)){ + if(is_visited_pair(pair_succ->automaton_state)){ XBT_DEBUG("Next pair already visited !"); break; @@ -604,7 +543,7 @@ void MC_ddfs(int search_cycle){ }else{ - if(visited(pair_succ->automaton_state)){ + if(is_visited_pair(pair_succ->automaton_state)){ XBT_DEBUG("Next pair already visited !"); break; @@ -615,11 +554,11 @@ void MC_ddfs(int search_cycle){ XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id); - set_pair_reached(pair_succ->automaton_state); + set_acceptance_pair_reached(pair_succ->automaton_state); search_cycle = 1; - XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs)); } @@ -653,7 +592,7 @@ void MC_ddfs(int search_cycle){ MC_SET_RAW_MEM; /* Create the new expanded graph_state */ - next_graph_state = MC_state_pair_new(); + next_graph_state = MC_state_new(); xbt_dynar_reset(successors); @@ -667,7 +606,7 @@ void MC_ddfs(int search_cycle){ if(res == 1){ // enabled transition in automaton MC_SET_RAW_MEM; - next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); + next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); xbt_dynar_push(successors, &next_pair); MC_UNSET_RAW_MEM; } @@ -682,7 +621,7 @@ void MC_ddfs(int search_cycle){ if(res == 2){ // true transition in automaton MC_SET_RAW_MEM; - next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); + next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); xbt_dynar_push(successors, &next_pair); MC_UNSET_RAW_MEM; } @@ -697,7 +636,7 @@ void MC_ddfs(int search_cycle){ if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ - if(reached(pair_succ->automaton_state)){ + if(is_reached_acceptance_pair(pair_succ->automaton_state)){ XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1); @@ -707,12 +646,12 @@ void MC_ddfs(int search_cycle){ XBT_INFO("Counter-example that violates formula :"); MC_show_stack_liveness(mc_stack_liveness); MC_dump_stack_liveness(mc_stack_liveness); - MC_print_statistics_pairs(mc_stats_pair); + MC_print_statistics(mc_stats); xbt_abort(); }else{ - if(visited(pair_succ->automaton_state)){ + if(is_visited_pair(pair_succ->automaton_state)){ XBT_DEBUG("Next pair already visited !"); break; @@ -721,7 +660,7 @@ void MC_ddfs(int search_cycle){ XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id); - XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs)); MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness, pair_succ); @@ -735,7 +674,7 @@ void MC_ddfs(int search_cycle){ }else{ - if(visited(pair_succ->automaton_state)){ + if(is_visited_pair(pair_succ->automaton_state)){ XBT_DEBUG("Next pair already visited !"); break; @@ -755,7 +694,7 @@ void MC_ddfs(int search_cycle){ }else{ - if(visited(pair_succ->automaton_state)){ + if(is_visited_pair(pair_succ->automaton_state)){ XBT_DEBUG("Next pair already visited !"); break; @@ -764,11 +703,11 @@ void MC_ddfs(int search_cycle){ if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - set_pair_reached(pair_succ->automaton_state); + set_acceptance_pair_reached(pair_succ->automaton_state); search_cycle = 1; - XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs)); } @@ -793,7 +732,7 @@ void MC_ddfs(int search_cycle){ }else{ XBT_WARN("/!\\ Max depth reached ! /!\\ "); - if(current_pair->requests > 0){ + if(MC_state_interleave_size(current_pair->graph_state) > 0){ XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ "); XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value."); } @@ -808,17 +747,14 @@ void MC_ddfs(int search_cycle){ MC_SET_RAW_MEM; - remove_pair = xbt_fifo_shift(mc_stack_liveness); - xbt_fifo_remove(mc_stack_liveness, remove_pair); - remove_pair = NULL; + pair_to_remove = xbt_fifo_shift(mc_stack_liveness); + xbt_fifo_remove(mc_stack_liveness, pair_to_remove); + pair_to_remove = NULL; if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){ - remove_pair_reached = xbt_dynar_pop_as(reached_pairs, mc_pair_reached_t); - pair_reached_free(remove_pair_reached); - remove_pair_reached = NULL; + acceptance_pair_to_remove = xbt_dynar_pop_as(acceptance_pairs, mc_acceptance_pair_t); + acceptance_pair_free(acceptance_pair_to_remove); + acceptance_pair_to_remove = NULL; } MC_UNSET_RAW_MEM; - /*if(initial_state_liveness->raw_mem_set) - MC_SET_RAW_MEM;*/ - } diff --git a/src/mc/mc_memory.c b/src/mc/mc_memory.c index f104773658..82b4b51b0b 100644 --- a/src/mc/mc_memory.c +++ b/src/mc/mc_memory.c @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ diff --git a/src/mc/mc_pair.c b/src/mc/mc_pair.c new file mode 100644 index 0000000000..9e8ff3ed88 --- /dev/null +++ b/src/mc/mc_pair.c @@ -0,0 +1,24 @@ +/* Copyright (c) 2013 Da SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "mc_private.h" + +mc_pair_t MC_pair_new(mc_state_t gs, xbt_automaton_state_t as, int r){ + mc_pair_t p = NULL; + p = xbt_new0(s_mc_pair_t, 1); + p->automaton_state = as; + p->graph_state = gs; + p->system_state = NULL; + p->requests = r; + return p; +} + +void MC_pair_delete(mc_pair_t p){ + p->automaton_state = NULL; + if(p->system_state) + MC_free_snapshot(p->system_state); + MC_state_delete(p->graph_state); + xbt_free(p); +} diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index b2f9a1b3eb..6a46fd6106 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -1,4 +1,4 @@ -/* Copyright (c) 2007-2012 Da SimGrid Team. All rights reserved. */ +/* Copyright (c) 2007-2013 Da SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ @@ -63,6 +63,7 @@ void snapshot_stack_free_voidp(void *s); int is_stack_ignore_variable(char *frame, char *var_name); /********************************* MC Global **********************************/ + extern double *mc_time; extern FILE *dot_output; extern const char* colors[10]; @@ -78,7 +79,9 @@ void MC_init(void); void MC_init_dot_output(void); int SIMIX_pre_mc_random(smx_simcall_t simcall); + /********************************* Requests ***********************************/ + int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2); char* MC_request_to_string(smx_simcall_t req, int value); unsigned int MC_request_testany_fail(smx_simcall_t req); @@ -91,6 +94,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value); /******************************** States **************************************/ + /* Possible exploration status of a process in a state */ typedef enum { MC_NOT_INTERLEAVE=0, /* Do not interleave (do not execute) */ @@ -130,7 +134,9 @@ smx_simcall_t MC_state_get_internal_request(mc_state_t state); smx_simcall_t MC_state_get_request(mc_state_t state, int *value); void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process); + /****************************** Statistics ************************************/ + typedef struct mc_stats { unsigned long state_size; unsigned long visited_states; @@ -138,18 +144,10 @@ typedef struct mc_stats { unsigned long executed_transitions; } s_mc_stats_t, *mc_stats_t; -typedef struct mc_stats_pair { - //unsigned long pair_size; - unsigned long visited_pairs; - unsigned long expanded_pairs; - unsigned long executed_transitions; -} s_mc_stats_pair_t, *mc_stats_pair_t; - extern mc_stats_t mc_stats; -extern mc_stats_pair_t mc_stats_pair; void MC_print_statistics(mc_stats_t); -void MC_print_statistics_pairs(mc_stats_pair_t); + /********************************** MEMORY ******************************/ /* The possible memory modes for the modelchecker are standard and raw. */ @@ -175,6 +173,7 @@ extern void *raw_heap; #define MC_SET_RAW_MEM mmalloc_set_current_heap(raw_heap) #define MC_UNSET_RAW_MEM mmalloc_set_current_heap(std_heap) + /******************************* MEMORY MAPPINGS ***************************/ /* These functions and data structures implements a binary interface for */ /* the proc maps ascii interface */ @@ -201,6 +200,8 @@ typedef struct s_memory_map { } s_memory_map_t, *memory_map_t; + +void MC_init_memory_map_info(void); memory_map_t get_memory_map(void); void free_memory_map(memory_map_t map); void get_libsimgrid_plt_section(void); @@ -221,6 +222,7 @@ extern void *end_got_plt_libsimgrid; extern void *start_got_plt_binary; extern void *end_got_plt_binary; + /********************************** Snapshot comparison **********************************/ typedef struct s_mc_comparison_times{ @@ -243,9 +245,11 @@ int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall, mc_snapshot_t s1, mc_s void print_comparison_times(void); //#define MC_DEBUG 1 -//#define MC_VERBOSE 1 +#define MC_VERBOSE 1 + + +/********************************** DPOR for safety property **************************************/ -/********************************** DPOR for safety **************************************/ typedef enum { e_mc_reduce_unset, e_mc_reduce_none, @@ -254,17 +258,18 @@ typedef enum { extern e_mc_reduce_t mc_reduce_kind; extern mc_global_t initial_state_safety; +extern xbt_fifo_t mc_stack_safety; void MC_dpor_init(void); void MC_dpor(void); -typedef struct s_mc_safety_visited_state{ +typedef struct s_mc_visited_state{ mc_snapshot_t system_state; int num; -}s_mc_safety_visited_state_t, *mc_safety_visited_state_t; +}s_mc_visited_state_t, *mc_visited_state_t; -/********************************** Double-DFS for liveness property**************************************/ +/********************************** Double-DFS for liveness property **************************************/ extern xbt_fifo_t mc_stack_liveness; extern mc_global_t initial_state_liveness; @@ -273,66 +278,37 @@ extern int compare; extern xbt_dynar_t mc_stack_comparison_ignore; extern xbt_dynar_t mc_data_bss_comparison_ignore; - typedef struct s_mc_pair{ mc_snapshot_t system_state; mc_state_t graph_state; - xbt_state_t automaton_state; + xbt_automaton_state_t automaton_state; + int requests; }s_mc_pair_t, *mc_pair_t; -typedef struct s_mc_pair_reached{ - int nb; - xbt_state_t automaton_state; +typedef struct s_mc_acceptance_pair{ + int num; + xbt_automaton_state_t automaton_state; xbt_dynar_t prop_ato; mc_snapshot_t system_state; -}s_mc_pair_reached_t, *mc_pair_reached_t; +}s_mc_acceptance_pair_t, *mc_acceptance_pair_t; -typedef struct s_mc_pair_visited{ - xbt_state_t automaton_state; +typedef struct s_mc_visited_pair{ + xbt_automaton_state_t automaton_state; xbt_dynar_t prop_ato; mc_snapshot_t system_state; -}s_mc_pair_visited_t, *mc_pair_visited_t; - -int MC_automaton_evaluate_label(xbt_exp_label_t l); - -int reached(xbt_state_t st); -void set_pair_reached(xbt_state_t st); -int visited(xbt_state_t st); - -void MC_pair_delete(mc_pair_t pair); -mc_state_t MC_state_pair_new(void); -void pair_reached_free(mc_pair_reached_t pair); -void pair_reached_free_voidp(void *p); -void pair_visited_free(mc_pair_visited_t pair); -void pair_visited_free_voidp(void *p); -void MC_init_memory_map_info(void); - -int get_heap_region_index(mc_snapshot_t s); - -/* **** Double-DFS stateless **** */ + int num; +}s_mc_visited_pair_t, *mc_visited_pair_t; -typedef struct s_mc_pair_stateless{ - mc_state_t graph_state; - xbt_state_t automaton_state; - int requests; -}s_mc_pair_stateless_t, *mc_pair_stateless_t; +mc_pair_t MC_pair_new(mc_state_t sg, xbt_automaton_state_t st, int r); +void MC_pair_delete(mc_pair_t); -mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r); void MC_ddfs_init(void); void MC_ddfs(int search_cycle); void MC_show_stack_liveness(xbt_fifo_t stack); void MC_dump_stack_liveness(xbt_fifo_t stack); -void pair_stateless_free(mc_pair_stateless_t pair); -void pair_stateless_free_voidp(void *p); -/********************************** Configuration of MC **************************************/ -extern xbt_fifo_t mc_stack_safety; - -/****** Core dump ******/ -int create_dump(int pair); - -/****** Local variables with DWARF ******/ +/********************************** Local variables with DWARF **********************************/ typedef enum { e_dw_loclist, @@ -431,7 +407,8 @@ void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_ void print_local_variables(xbt_dict_t list); xbt_dict_t MC_get_location_list(const char *elf_file); -/**** Global variables ****/ + +/********************************** Global variables with objdump **********************************/ typedef struct s_global_variable{ char *name; diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index 2bf890d1b3..c25a0bc400 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c index a78a72e8cf..59cca4e6cc 100644 --- a/src/mc/mc_state.c +++ b/src/mc/mc_state.c @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ @@ -23,18 +23,6 @@ mc_state_t MC_state_new() return state; } -mc_state_t MC_state_pair_new(void) -{ - mc_state_t state = NULL; - - state = xbt_new0(s_mc_state_t, 1); - state->max_pid = simix_process_maxpid; - state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid); - - //mc_stats->expanded_states++; - return state; -} - /** * \brief Deletes a state data structure * \param trans The state to be deleted diff --git a/src/mc/memory_map.c b/src/mc/memory_map.c index 1606b2d4b0..b4315233c4 100644 --- a/src/mc/memory_map.c +++ b/src/mc/memory_map.c @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ diff --git a/src/xbt/automaton/automaton.c b/src/xbt/automaton/automaton.c index 8824c52df9..7e0916ad8e 100644 --- a/src/xbt/automaton/automaton.c +++ b/src/xbt/automaton/automaton.c @@ -11,26 +11,26 @@ xbt_automaton_t xbt_automaton_new(){ xbt_automaton_t automaton = NULL; automaton = xbt_new0(struct xbt_automaton, 1); - automaton->states = xbt_dynar_new(sizeof(xbt_state_t), xbt_state_free_voidp); - automaton->transitions = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp); - automaton->propositional_symbols = xbt_dynar_new(sizeof(xbt_propositional_symbol_t), xbt_propositional_symbol_free_voidp); + automaton->states = xbt_dynar_new(sizeof(xbt_automaton_state_t), xbt_automaton_state_free_voidp); + automaton->transitions = xbt_dynar_new(sizeof(xbt_automaton_transition_t), xbt_automaton_transition_free_voidp); + automaton->propositional_symbols = xbt_dynar_new(sizeof(xbt_automaton_propositional_symbol_t), xbt_automaton_propositional_symbol_free_voidp); return automaton; } -xbt_state_t xbt_automaton_new_state(xbt_automaton_t a, int type, char* id){ - xbt_state_t state = NULL; - state = xbt_new0(struct xbt_state, 1); +xbt_automaton_state_t xbt_automaton_state_new(xbt_automaton_t a, int type, char* id){ + xbt_automaton_state_t state = NULL; + state = xbt_new0(struct xbt_automaton_state, 1); state->type = type; state->id = strdup(id); - state->in = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp); - state->out = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp); + state->in = xbt_dynar_new(sizeof(xbt_automaton_transition_t), xbt_automaton_transition_free_voidp); + state->out = xbt_dynar_new(sizeof(xbt_automaton_transition_t), xbt_automaton_transition_free_voidp); xbt_dynar_push(a->states, &state); return state; } -xbt_transition_t xbt_automaton_new_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst, xbt_exp_label_t label){ - xbt_transition_t transition = NULL; - transition = xbt_new0(struct xbt_transition, 1); +xbt_automaton_transition_t xbt_automaton_transition_new(xbt_automaton_t a, xbt_automaton_state_t src, xbt_automaton_state_t dst, xbt_automaton_exp_label_t label){ + xbt_automaton_transition_t transition = NULL; + transition = xbt_new0(struct xbt_automaton_transition, 1); if(src != NULL){ xbt_dynar_push(src->out, &transition); transition->src = src; @@ -44,30 +44,30 @@ xbt_transition_t xbt_automaton_new_transition(xbt_automaton_t a, xbt_state_t src return transition; } -xbt_exp_label_t xbt_automaton_new_label(int type, ...){ - xbt_exp_label_t label = NULL; - label = xbt_new0(struct xbt_exp_label, 1); +xbt_automaton_exp_label_t xbt_automaton_exp_label_new(int type, ...){ + xbt_automaton_exp_label_t label = NULL; + label = xbt_new0(struct xbt_automaton_exp_label, 1); label->type = type; va_list ap; va_start(ap, type); switch(type){ case 0 : { - xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t); - xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t); + xbt_automaton_exp_label_t left = va_arg(ap, xbt_automaton_exp_label_t); + xbt_automaton_exp_label_t right = va_arg(ap, xbt_automaton_exp_label_t); label->u.or_and.left_exp = left; label->u.or_and.right_exp = right; break; } case 1 : { - xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t); - xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t); + xbt_automaton_exp_label_t left = va_arg(ap, xbt_automaton_exp_label_t); + xbt_automaton_exp_label_t right = va_arg(ap, xbt_automaton_exp_label_t); label->u.or_and.left_exp = left; label->u.or_and.right_exp = right; break; } case 2 : { - xbt_exp_label_t exp_not = va_arg(ap, xbt_exp_label_t); + xbt_automaton_exp_label_t exp_not = va_arg(ap, xbt_automaton_exp_label_t); label->u.exp_not = exp_not; break; } @@ -90,8 +90,8 @@ xbt_dynar_t xbt_automaton_get_transitions(xbt_automaton_t a){ return a->transitions; } -xbt_transition_t xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst){ - xbt_transition_t transition; +xbt_automaton_transition_t xbt_automaton_get_transition(xbt_automaton_t a, xbt_automaton_state_t src, xbt_automaton_state_t dst){ + xbt_automaton_transition_t transition; unsigned int cursor; xbt_dynar_foreach(src->out, cursor, transition){ if((transition->src == src) && (transition->dst == dst)) @@ -100,34 +100,34 @@ xbt_transition_t xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src return NULL; } -xbt_state_t xbt_automaton_transition_get_source(xbt_transition_t t){ +xbt_automaton_state_t xbt_automaton_transition_get_source(xbt_automaton_transition_t t){ return t->src; } -xbt_state_t xbt_automaton_transition_get_destination(xbt_transition_t t){ +xbt_automaton_state_t xbt_automaton_transition_get_destination(xbt_automaton_transition_t t){ return t->dst; } -void xbt_automaton_transition_set_source(xbt_transition_t t, xbt_state_t src){ +void xbt_automaton_transition_set_source(xbt_automaton_transition_t t, xbt_automaton_state_t src){ t->src = src; xbt_dynar_push(src->out,&t); } -void xbt_automaton_transition_set_destination(xbt_transition_t t, xbt_state_t dst){ +void xbt_automaton_transition_set_destination(xbt_automaton_transition_t t, xbt_automaton_state_t dst){ t->dst = dst; xbt_dynar_push(dst->in,&t); } -xbt_dynar_t xbt_automaton_state_get_out_transitions(xbt_state_t s){ +xbt_dynar_t xbt_automaton_state_get_out_transitions(xbt_automaton_state_t s){ return s->out; } -xbt_dynar_t xbt_automaton_state_get_in_transitions(xbt_state_t s){ +xbt_dynar_t xbt_automaton_state_get_in_transitions(xbt_automaton_state_t s){ return s->in; } -xbt_state_t xbt_automaton_state_exists(xbt_automaton_t a, char *id){ - xbt_state_t state = NULL; +xbt_automaton_state_t xbt_automaton_state_exists(xbt_automaton_t a, char *id){ + xbt_automaton_state_t state = NULL; unsigned int cursor = 0; xbt_dynar_foreach(a->states, cursor, state){ if(strcmp(state->id, id)==0) @@ -136,9 +136,9 @@ xbt_state_t xbt_automaton_state_exists(xbt_automaton_t a, char *id){ return NULL; } -void xbt_automaton_display(xbt_automaton_t a){ +void xbt_automaton_display(xbt_automaton_t a){ unsigned int cursor = 0; - xbt_state_t state = NULL; + xbt_automaton_state_t state = NULL; printf("\n\nEtat courant : %s\n", a->current_state->id); @@ -150,36 +150,36 @@ void xbt_automaton_display(xbt_automaton_t a){ } cursor=0; - xbt_transition_t transition = NULL; + xbt_automaton_transition_t transition = NULL; printf("\nListe des transitions : %lu\n\n", xbt_dynar_length(a->transitions)); xbt_dynar_foreach(a->transitions, cursor, transition){ printf("label :"); - xbt_automaton_display_exp(transition->label); + xbt_automaton_exp_label_display(transition->label); printf(", %s -> %s\n", transition->src->id, transition->dst->id); } } -void xbt_automaton_display_exp(xbt_exp_label_t label){ +void xbt_automaton_exp_label_display(xbt_automaton_exp_label_t label){ switch(label->type){ case 0 : printf("("); - xbt_automaton_display_exp(label->u.or_and.left_exp); + xbt_automaton_exp_label_display(label->u.or_and.left_exp); printf(" || "); - xbt_automaton_display_exp(label->u.or_and.right_exp); + xbt_automaton_exp_label_display(label->u.or_and.right_exp); printf(")"); break; case 1 : printf("("); - xbt_automaton_display_exp(label->u.or_and.left_exp); + xbt_automaton_exp_label_display(label->u.or_and.left_exp); printf(" && "); - xbt_automaton_display_exp(label->u.or_and.right_exp); + xbt_automaton_exp_label_display(label->u.or_and.right_exp); printf(")"); break; case 2 : printf("(!"); - xbt_automaton_display_exp(label->u.exp_not); + xbt_automaton_exp_label_display(label->u.exp_not); printf(")"); break; case 3 : @@ -192,20 +192,20 @@ void xbt_automaton_display_exp(xbt_exp_label_t label){ } -xbt_state_t xbt_automaton_get_current_state(xbt_automaton_t a){ +xbt_automaton_state_t xbt_automaton_get_current_state(xbt_automaton_t a){ return a->current_state; } -xbt_propositional_symbol_t xbt_new_propositional_symbol(xbt_automaton_t a, const char* id, void* fct){ - xbt_propositional_symbol_t prop_symb = NULL; - prop_symb = xbt_new0(struct xbt_propositional_symbol, 1); +xbt_automaton_propositional_symbol_t xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, void* fct){ + 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; xbt_dynar_push(a->propositional_symbols, &prop_symb); return prop_symb; } -int automaton_state_compare(xbt_state_t s1, xbt_state_t s2){ +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*/ @@ -219,22 +219,22 @@ int automaton_state_compare(xbt_state_t s1, xbt_state_t s2){ } -int automaton_transition_compare(const void *t1, const void *t2){ +int xbt_automaton_transition_compare(const void *t1, const void *t2){ - if(automaton_state_compare(((xbt_transition_t)t1)->src, ((xbt_transition_t)t2)->src)) + if(xbt_automaton_state_compare(((xbt_automaton_transition_t)t1)->src, ((xbt_automaton_transition_t)t2)->src)) return 1; - if(automaton_state_compare(((xbt_transition_t)t1)->dst, ((xbt_transition_t)t2)->dst)) + if(xbt_automaton_state_compare(((xbt_automaton_transition_t)t1)->dst, ((xbt_automaton_transition_t)t2)->dst)) return 1; - if(automaton_label_transition_compare(((xbt_transition_t)t1)->label,((xbt_transition_t)t2)->label)) + if(xbt_automaton_exp_label_compare(((xbt_automaton_transition_t)t1)->label,((xbt_automaton_transition_t)t2)->label)) return 1; return 0; } -int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){ +int xbt_automaton_exp_label_compare(xbt_automaton_exp_label_t l1, xbt_automaton_exp_label_t l2){ if(l1->type != l2->type) return 1; @@ -243,14 +243,14 @@ int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){ case 0 : // OR case 1 : // AND - if(automaton_label_transition_compare(l1->u.or_and.left_exp, l2->u.or_and.left_exp)) + if(xbt_automaton_exp_label_compare(l1->u.or_and.left_exp, l2->u.or_and.left_exp)) return 1; else - return automaton_label_transition_compare(l1->u.or_and.right_exp, l2->u.or_and.right_exp); + return xbt_automaton_exp_label_compare(l1->u.or_and.right_exp, l2->u.or_and.right_exp); break; case 2 : // NOT - return automaton_label_transition_compare(l1->u.exp_not, l2->u.exp_not); + return xbt_automaton_exp_label_compare(l1->u.exp_not, l2->u.exp_not); break; case 3 : // predicat @@ -270,7 +270,7 @@ int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){ } -int propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2){ +int xbt_automaton_propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2){ int *iptr1, *iptr2; unsigned int cursor; @@ -288,11 +288,11 @@ int propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2){ /************ Free functions ****************/ -static void xbt_transition_free(xbt_transition_t t); -static void xbt_exp_label_free(xbt_exp_label_t e); -static void xbt_propositional_symbol_free(xbt_propositional_symbol_t ps); +static void xbt_automaton_transition_free(xbt_automaton_transition_t t); +static void xbt_automaton_exp_label_free(xbt_automaton_exp_label_t e); +static void xbt_automaton_propositional_symbol_free(xbt_automaton_propositional_symbol_t ps); -void xbt_state_free(xbt_state_t s){ +void xbt_automaton_state_free(xbt_automaton_state_t s){ if(s){ xbt_free(s->id); xbt_dynar_free(&(s->in)); @@ -302,32 +302,32 @@ void xbt_state_free(xbt_state_t s){ } } -void xbt_state_free_voidp(void *s){ - xbt_state_free((xbt_state_t) * (void **) s); +void xbt_automaton_state_free_voidp(void *s){ + xbt_automaton_state_free((xbt_automaton_state_t) * (void **) s); } -static void xbt_transition_free(xbt_transition_t t){ +static void xbt_automaton_transition_free(xbt_automaton_transition_t t){ if(t){ - xbt_exp_label_free(t->label); + xbt_automaton_exp_label_free(t->label); xbt_free(t); t = NULL; } } -void xbt_transition_free_voidp(void *t){ - xbt_transition_free((xbt_transition_t) * (void **) t); +void xbt_automaton_transition_free_voidp(void *t){ + xbt_automaton_transition_free((xbt_automaton_transition_t) * (void **) t); } -static void xbt_exp_label_free(xbt_exp_label_t e){ +static void xbt_automaton_exp_label_free(xbt_automaton_exp_label_t e){ if(e){ switch(e->type){ case 0: case 1: - xbt_exp_label_free(e->u.or_and.left_exp); - xbt_exp_label_free(e->u.or_and.right_exp); + xbt_automaton_exp_label_free(e->u.or_and.left_exp); + xbt_automaton_exp_label_free(e->u.or_and.right_exp); break; case 2: - xbt_exp_label_free(e->u.exp_not); + xbt_automaton_exp_label_free(e->u.exp_not); break; case 3: xbt_free(e->u.predicat); @@ -340,11 +340,11 @@ static void xbt_exp_label_free(xbt_exp_label_t e){ } } -void xbt_exp_label_free_voidp(void *e){ - xbt_exp_label_free((xbt_exp_label_t) * (void **) e); +void xbt_automaton_exp_label_free_voidp(void *e){ + xbt_automaton_exp_label_free((xbt_automaton_exp_label_t) * (void **) e); } -static void xbt_propositional_symbol_free(xbt_propositional_symbol_t ps){ +static void xbt_automaton_propositional_symbol_free(xbt_automaton_propositional_symbol_t ps){ if(ps){ xbt_free(ps->pred); xbt_free(ps); @@ -352,8 +352,8 @@ static void xbt_propositional_symbol_free(xbt_propositional_symbol_t ps){ } } -void xbt_propositional_symbol_free_voidp(void *ps){ - xbt_propositional_symbol_free((xbt_propositional_symbol_t) * (void **) ps); +void xbt_automaton_propositional_symbol_free_voidp(void *ps){ + xbt_automaton_propositional_symbol_free((xbt_automaton_propositional_symbol_t) * (void **) ps); } void xbt_automaton_free(xbt_automaton_t a){ @@ -361,7 +361,7 @@ void xbt_automaton_free(xbt_automaton_t a){ xbt_dynar_free(&(a->propositional_symbols)); xbt_dynar_free(&(a->transitions)); xbt_dynar_free(&(a->states)); - xbt_state_free(a->current_state); + xbt_automaton_state_free(a->current_state); xbt_free(a); a = NULL; } diff --git a/src/xbt/automaton/automatonparse_promela.c b/src/xbt/automaton/automatonparse_promela.c index 9736dd122e..34dcbc597e 100644 --- a/src/xbt/automaton/automatonparse_promela.c +++ b/src/xbt/automaton/automatonparse_promela.c @@ -25,10 +25,10 @@ static void new_state(char* id, int src){ } } - xbt_state_t state = NULL; + xbt_automaton_state_t state = NULL; state = xbt_automaton_state_exists(parsed_automaton, id_state); if(state == NULL){ - state = xbt_automaton_new_state(parsed_automaton, type, id_state); + state = xbt_automaton_state_new(parsed_automaton, type, id_state); } if(type==-1) @@ -39,48 +39,48 @@ static void new_state(char* id, int src){ } -static void new_transition(char* id, xbt_exp_label_t label){ +static void new_transition(char* id, xbt_automaton_exp_label_t label){ char* id_state = strdup(id); - xbt_state_t state_dst = NULL; + xbt_automaton_state_t state_dst = NULL; new_state(id, 0); state_dst = xbt_automaton_state_exists(parsed_automaton, id_state); - xbt_state_t state_src = xbt_automaton_state_exists(parsed_automaton, state_id_src); + xbt_automaton_state_t state_src = xbt_automaton_state_exists(parsed_automaton, state_id_src); //xbt_transition_t trans = NULL; - xbt_automaton_new_transition(parsed_automaton, state_src, state_dst, label); + xbt_automaton_transition_new(parsed_automaton, state_src, state_dst, label); } -static xbt_exp_label_t new_label(int type, ...){ - xbt_exp_label_t label = NULL; +static xbt_automaton_exp_label_t new_label(int type, ...){ + xbt_automaton_exp_label_t label = NULL; va_list ap; va_start(ap,type); switch(type){ case 0 : { - xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t); - xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t); - label = xbt_automaton_new_label(type, left, right); + xbt_automaton_exp_label_t left = va_arg(ap, xbt_automaton_exp_label_t); + xbt_automaton_exp_label_t right = va_arg(ap, xbt_automaton_exp_label_t); + label = xbt_automaton_exp_label_new(type, left, right); break; } case 1 : { - xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t); - xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t); - label = xbt_automaton_new_label(type, left, right); + xbt_automaton_exp_label_t left = va_arg(ap, xbt_automaton_exp_label_t); + xbt_automaton_exp_label_t right = va_arg(ap, xbt_automaton_exp_label_t); + label = xbt_automaton_exp_label_new(type, left, right); break; } case 2 : { - xbt_exp_label_t exp_not = va_arg(ap, xbt_exp_label_t); - label = xbt_automaton_new_label(type, exp_not); + xbt_automaton_exp_label_t exp_not = va_arg(ap, xbt_automaton_exp_label_t); + label = xbt_automaton_exp_label_new(type, exp_not); break; } case 3 : { char* p = va_arg(ap, char*); - label = xbt_automaton_new_label(type, p); + label = xbt_automaton_exp_label_new(type, p); break; } case 4 : { - label = xbt_automaton_new_label(type); + label = xbt_automaton_exp_label_new(type); break; } } diff --git a/src/xbt/automaton/parserPromela.tab.hacc b/src/xbt/automaton/parserPromela.tab.hacc index 51a4ae6cfb..676dd599a4 100644 --- a/src/xbt/automaton/parserPromela.tab.hacc +++ b/src/xbt/automaton/parserPromela.tab.hacc @@ -72,7 +72,7 @@ typedef union YYSTYPE double real; int integer; char* string; - xbt_exp_label_t label; + xbt_automaton_exp_label_t label; diff --git a/src/xbt/automaton/parserPromela.yacc b/src/xbt/automaton/parserPromela.yacc index f88ac53087..c74d2ce67c 100644 --- a/src/xbt/automaton/parserPromela.yacc +++ b/src/xbt/automaton/parserPromela.yacc @@ -11,7 +11,7 @@ void yyerror(const char *s); double real; int integer; char* string; - xbt_exp_label_t label; + xbt_automaton_exp_label_t label; } %token NEVER -- 2.20.1