From 692266ba967fb41cb41084539bdb2df5f9f29192 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 21 Apr 2011 10:25:50 +0200 Subject: [PATCH] new dfs algorithm with automaton of LTL formula --- src/include/mc/mc.h | 2 + src/mc/mc_dfs.c | 372 ++++++++++++++++++++++++++++++++++++++++++++ src/mc/mc_dpor.c | 2 +- src/mc/mc_global.c | 30 ++++ src/mc/private.h | 18 +++ 5 files changed, 423 insertions(+), 1 deletion(-) create mode 100644 src/mc/mc_dfs.c diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index d4c01ffd6b..401ce5b4a5 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -16,6 +16,7 @@ #include "mc/datatypes.h" #include "simix/datatypes.h" #include "gras_config.h" /* Definition of HAVE_MC */ +#include "xbt/automaton.h" #ifdef HAVE_MC extern int _surf_do_model_check; @@ -31,6 +32,7 @@ XBT_PUBLIC(void) MC_init(void); XBT_PUBLIC(void) MC_exit(void); XBT_PUBLIC(void) MC_assert(int); XBT_PUBLIC(void) MC_modelcheck(void); +XBT_PUBLIC(void) MC_modelcheck_with_automaton(xbt_automaton_t a); XBT_PUBLIC(int) MC_random(int, int); XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double); XBT_PUBLIC(double) MC_process_clock_get(smx_process_t); diff --git a/src/mc/mc_dfs.c b/src/mc/mc_dfs.c new file mode 100644 index 0000000000..1c443d10b4 --- /dev/null +++ b/src/mc/mc_dfs.c @@ -0,0 +1,372 @@ +#include "private.h" + +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dfs, mc, + "Logging specific to MC DFS algorithm"); + + +extern xbt_fifo_t mc_snapshot_stack; +mc_pairs_t mc_reached = NULL; +xbt_dynar_t initial_pairs = NULL; +int max_pair = 0; +xbt_dynar_t list_pairs_reached = NULL; +extern mc_snapshot_t initial_snapshot; + +mc_pairs_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){ + mc_pairs_t p = NULL; + p = xbt_new0(s_mc_pairs_t, 1); + p->system_state = sn; + p->automaton_state = st; + p->graph_state = sg; + p->visited = 0; + p->num = max_pair; + max_pair++; + return p; + +} + +void set_pair_visited(mc_pairs_t p){ + p->visited = 1; +} + +int pair_reached(xbt_dynar_t p, int num_pair){ + int n; + unsigned int cursor = 0; + xbt_dynar_foreach(p, cursor, n){ + if(n == num_pair) + return 1; + } + return 0; +} + +void MC_dfs_init(xbt_automaton_t a){ + + mc_pairs_t mc_initial_pair = NULL; + mc_state_t initial_graph_state = NULL; + smx_process_t process; + + MC_wait_for_requests(); + + MC_SET_RAW_MEM; + + initial_snapshot = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot(initial_snapshot); + 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); + } + } + + list_pairs_reached = xbt_dynar_new(sizeof(int), NULL); + + MC_UNSET_RAW_MEM; + + + //regarder dans l'automate toutes les transitions activables grâce à l'état initial du système -> donnera les états initiaux de la propriété consistants avec l'état initial du système + + unsigned int cursor = 0; + xbt_state_t state = NULL; + unsigned int cursor2 = 0; + int res; + xbt_transition_t transition_succ = NULL; + xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL); + int enabled_transition = 0; + + xbt_dynar_foreach(a->states, cursor, state){ + if(state->type == -1){ + xbt_dynar_foreach(state->out, cursor2, transition_succ){ + + res = MC_automaton_evaluate_label(a, transition_succ->label); + + if(res == 1){ + + MC_SET_RAW_MEM; + + mc_initial_pair = new_pair(initial_snapshot, initial_graph_state, transition_succ->dst); + xbt_fifo_unshift(mc_snapshot_stack, mc_initial_pair); + set_pair_visited(mc_initial_pair); + + MC_UNSET_RAW_MEM; + + enabled_transition = 1; + + XBT_DEBUG(" ++++++++++++++++++ new initial pair +++++++++++++++++++"); + + MC_dfs(a, 0); + }else{ + if(res == 2){ + xbt_dynar_push(elses,&transition_succ); + } + } + } + } + } + + if(enabled_transition == 0){ + cursor2 = 0; + xbt_dynar_foreach(elses, cursor, transition_succ){ + + MC_SET_RAW_MEM; + + mc_initial_pair = new_pair(initial_snapshot, initial_graph_state, transition_succ->dst); + xbt_fifo_unshift(mc_snapshot_stack, mc_initial_pair); + set_pair_visited(mc_initial_pair); + + MC_UNSET_RAW_MEM; + + MC_dfs(a, 0); + } + } + +} + +int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){ + + switch(l->type){ + case 0 : { + int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp); + int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp); + return (left_res || right_res); + break; + } + case 1 : { + int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp); + int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp); + return (left_res && right_res); + break; + } + case 2 : { + int res = MC_automaton_evaluate_label(a, l->u.exp_not); + return (!res); + break; + } + case 3 : { + unsigned int cursor = 0; + xbt_propositional_symbol_t p = NULL; + xbt_dynar_foreach(a->propositional_symbols, cursor, p){ + if(strcmp(p->pred, l->u.predicat) == 0){ + int (*f)() = p->function; + return (*f)(); + } + } + return -1; + break; + } + case 4 : { + return 2; + break; + } + } +} + +/*void MC_dfs(xbt_automaton_t a, int search_cycle){ + + xbt_state_t current_state = (xbt_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(stack_automaton_dfs)); + xbt_transition_t transition_succ = NULL; + xbt_state_t successor = NULL; + unsigned int cursor = 0; + xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL); + int res; + + //printf("++ current state : %s\n", current_state->id); + + xbt_dynar_foreach(current_state->out, cursor, transition_succ){ + successor = transition_succ->dst; + res = MC_automaton_evaluate_label(a, transition_succ->label); + //printf("-- state : %s, transition_label : %d, res = %d\n", successor->id, transition_succ->label->type, res); + if(res == 1){ + if(search_cycle == 1 && reached_dfs != NULL){ + if(strcmp(reached_dfs->id, successor->id) == 0){ + xbt_dynar_push(state_automaton_visited_dfs, &successor); + printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n"); + printf("Visited states : \n"); + unsigned int cursor2 = 0; + xbt_state_t visited_state = NULL; + xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){ + printf("State : %s\n", visited_state->id); + } + exit(1); + } + } + if(successor->visited == 0){ + successor->visited = 1; + xbt_fifo_unshift(stack_automaton_dfs, successor); + xbt_dynar_push(state_automaton_visited_dfs, &successor); + MC_dfs(a, search_cycle); + if(search_cycle == 0 && successor->type == 1){ + reached_dfs = successor; + MC_dfs(a, 1); + } + } + }else{ + if(res == 2){ + xbt_dynar_push(elses,&transition_succ); + } + } + } + + cursor = 0; + xbt_dynar_foreach(elses, cursor, transition_succ){ + successor = transition_succ->dst; + if(search_cycle == 1 && reached_dfs != NULL){ + if(strcmp(reached_dfs->id, successor->id) == 0){ + xbt_dynar_push(state_automaton_visited_dfs, &successor); + printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n"); + printf("Visited states : \n"); + unsigned int cursor2 = 0; + xbt_state_t visited_state = NULL; + xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){ + printf("State : %s\n", visited_state->id); + } + exit(1); + } + } + if(successor->visited == 0){ + successor->visited = 1; + xbt_fifo_unshift(stack_automaton_dfs, successor); + xbt_dynar_push(state_automaton_visited_dfs, &successor); + MC_dfs(a, search_cycle); + if(search_cycle == 0 && successor->type == 1){ + reached_dfs = successor; + MC_dfs(a, 1); + } + } + } + + xbt_fifo_shift(stack_automaton_dfs); + }*/ + + +void MC_dfs(xbt_automaton_t a, int search_cycle){ + + smx_process_t process = NULL; + int value; + mc_state_t state = NULL; + mc_state_t next_graph_state = NULL; + smx_req_t req = NULL; + char *req_str; + + xbt_transition_t transition_succ = NULL; + xbt_state_t successor = NULL; + unsigned int cursor = 0; + xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL); + int res; + int enabled_transition = 0; + + mc_pairs_t next_pair = NULL; + mc_snapshot_t next_snapshot = NULL; + + + /* Get current state */ + mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)); + + XBT_DEBUG("**************************************************"); + XBT_DEBUG("State=%p, %u interleave",current_pair->graph_state,MC_state_interleave_size(current_pair->graph_state)); + + /* Update statistics */ + mc_stats->visited_states++; + + MC_restore_snapshot(current_pair->system_state); + MC_UNSET_RAW_MEM; + + //FIXME : vérifier condition permettant d'avoir tous les successeurs possibles dans le graph + + while(req = MC_state_get_request(current_pair->graph_state, &value)){ + + /* Debug information */ + if(XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_debug)){ + req_str = MC_request_to_string(req, value); + XBT_DEBUG("Execute: %s", req_str); + xbt_free(req_str); + } + + MC_state_set_executed_request(current_pair->graph_state, req, value); + mc_stats->executed_transitions++; + + /* Answer the request */ + SIMIX_request_pre(req, value); + + /* Wait for requests (schedules processes) */ + MC_wait_for_requests(); + + + /* Create the new expanded graph_state */ + MC_SET_RAW_MEM; + + next_graph_state = MC_state_new(); + + /* Get an enabled process and insert it in the interleave set of the next graph_state */ + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ + MC_state_interleave_process(next_graph_state, process); + } + } + + next_snapshot = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot(next_snapshot); + + MC_UNSET_RAW_MEM; + + xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ + successor = transition_succ->dst; + res = MC_automaton_evaluate_label(a, transition_succ->label); + if(res == 1){ // enabled transition + + MC_SET_RAW_MEM; + next_pair = new_pair(next_snapshot, next_graph_state, successor); + + if((search_cycle == 1) && (pair_reached(list_pairs_reached, next_pair->num) == 1)){ + printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n"); + // afficher chemin menant au cycle d'acceptation + exit(1); + } + if(next_pair->visited == 0){ // FIXME : tester avec search_cycle ? + xbt_fifo_unshift(mc_snapshot_stack, next_pair); + set_pair_visited(next_pair); + MC_dfs(a, search_cycle); + if((search_cycle == 0) && (next_pair->automaton_state->type == 1)){ + xbt_dynar_push(list_pairs_reached, &next_pair->num); + MC_dfs(a, 1); + } + } + + MC_UNSET_RAW_MEM; + enabled_transition = 1; + }else{ + if(res == 2){ + xbt_dynar_push(elses,&transition_succ); + } + } + } + + if(enabled_transition == 0){ + cursor = 0; + xbt_dynar_foreach(elses, cursor, transition_succ){ + successor = transition_succ->dst; + MC_SET_RAW_MEM; + next_pair = new_pair(next_snapshot, next_graph_state, successor); + + if((search_cycle == 1) && (pair_reached(list_pairs_reached, next_pair->num) == 1)){ + printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n"); + // afficher chemin menant au cycle d'acceptation + exit(1); + } + if(next_pair->visited == 0){ // FIXME : tester avec search_cycle ? + xbt_fifo_unshift(mc_snapshot_stack, next_pair); + set_pair_visited(next_pair); + MC_dfs(a, search_cycle); + if((search_cycle == 0) && (next_pair->automaton_state->type == 1)){ + xbt_dynar_push(list_pairs_reached, &next_pair->num); + MC_dfs(a, 1); + } + } + + MC_UNSET_RAW_MEM; + } + } + + } + + xbt_fifo_shift(mc_snapshot_stack); + +} diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index 074570b916..48de38fc30 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -65,7 +65,7 @@ void MC_dpor(void) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); XBT_DEBUG("**************************************************"); - XBT_DEBUG("Exploration detph=%d (state=%p)(%u interleave)", + XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)", xbt_fifo_size(mc_stack), state, MC_state_interleave_size(state)); diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 1142da7c2a..8c3f1718c8 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -18,6 +18,8 @@ mc_stats_t mc_stats = NULL; mc_state_t mc_current_state = NULL; char mc_replay_mode = FALSE; double *mc_time = NULL; +xbt_fifo_t mc_snapshot_stack = NULL; + /** * \brief Initialize the model-checker data structures */ @@ -51,6 +53,29 @@ void MC_init(void) MC_UNSET_RAW_MEM; } +void MC_init_with_automaton(xbt_automaton_t a){ + + mc_time = xbt_new0(double, simix_process_maxpid); + + /* Initialize the data structures that must be persistent across every + iteration of the model-checker (in RAW memory) */ + MC_SET_RAW_MEM; + + /* Initialize statistics */ + mc_stats = xbt_new0(s_mc_stats_t, 1); + mc_stats->state_size = 1; + + /* Create exploration stack */ + mc_snapshot_stack = xbt_fifo_new(); + + MC_UNSET_RAW_MEM; + + XBT_DEBUG("---------- Avant dfs init -----------"); + + MC_dfs_init(a); +} + + void MC_modelcheck(void) { MC_init(); @@ -58,6 +83,11 @@ void MC_modelcheck(void) MC_exit(); } +void MC_modelcheck_with_automaton(xbt_automaton_t a){ + MC_init_with_automaton(a); + MC_exit(); +} + void MC_exit(void) { MC_print_statistics(mc_stats); diff --git a/src/mc/private.h b/src/mc/private.h index 1adc99aa82..6bfc90a4c9 100644 --- a/src/mc/private.h +++ b/src/mc/private.h @@ -18,6 +18,7 @@ #include "xbt/function_types.h" #include "xbt/mmalloc.h" #include "../simix/private.h" +#include "xbt/automaton.h" /****************************** Snapshots ***********************************/ @@ -168,5 +169,22 @@ typedef struct s_memory_map { memory_map_t get_memory_map(void); +/********************************** DFS **************************************/ + +typedef struct s_mc_pairs{ + mc_snapshot_t system_state; + mc_state_t graph_state; + xbt_state_t automaton_state; + int visited; + int num; +}s_mc_pairs_t, *mc_pairs_t; + +void MC_dfs_init(xbt_automaton_t a); +void MC_dfs(xbt_automaton_t automaton, int search_cycle); +int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l); +mc_pairs_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st); +void set_pair_visited(mc_pairs_t p); +int pair_reached(xbt_dynar_t p, int num_pair); + #endif -- 2.20.1