From a919469a2cba34e8d082b652f03b33182d27fa5d Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Fri, 29 Apr 2011 10:31:48 +0200 Subject: [PATCH] =?utf8?q?d=C3=A9tection=20de=20cycle=20d'acceptation=20ok?= =?utf8?q?=20mais=20boucle=20infinie=20en=20cas=20d'absence=20de=20cycle?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit --- examples/msg/mc/example_automaton.c | 2 + src/mc/mc_dfs.c | 485 ++++++++++++++++++---------- src/mc/mc_global.c | 4 +- src/mc/private.h | 15 +- 4 files changed, 332 insertions(+), 174 deletions(-) diff --git a/examples/msg/mc/example_automaton.c b/examples/msg/mc/example_automaton.c index 6f5e019ee9..67f5f87182 100644 --- a/examples/msg/mc/example_automaton.c +++ b/examples/msg/mc/example_automaton.c @@ -39,6 +39,8 @@ int server(int argc, char *argv[]) } MSG_task_receive(&task, "mymailbox"); count++; + //e++; + //e=e%2; } //MC_assert(atoi(MSG_task_get_name(task)) == 3); diff --git a/src/mc/mc_dfs.c b/src/mc/mc_dfs.c index 6f7102d6a7..6108d49bc6 100644 --- a/src/mc/mc_dfs.c +++ b/src/mc/mc_dfs.c @@ -1,15 +1,16 @@ #include "private.h" +#include "unistd.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; +xbt_dynar_t visited_pairs = NULL; mc_pairs_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){ mc_pairs_t p = NULL; @@ -17,39 +18,72 @@ mc_pairs_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){ p->system_state = sn; p->automaton_state = st; p->graph_state = sg; - p->visited = 0; p->num = max_pair; + p->pairs_reached = xbt_dynar_new(sizeof(int), NULL); max_pair++; return p; } -void set_pair_visited(mc_pairs_t p){ - p->visited = 1; +void set_pair_visited(int np, int sc){ + mc_visited_pairs_t p = NULL; + p = xbt_new0(s_mc_visited_pairs_t, 1); + p->num_pair = np; + p->search_cycle = sc; + + xbt_dynar_push(visited_pairs, &p); + //XBT_DEBUG("New visited pair , length of visited pairs : %lu", xbt_dynar_length(visited_pairs)); } -int pair_reached(xbt_dynar_t p, int num_pair){ +int pair_reached(xbt_dynar_t lpr, int num_pair){ + + //XBT_DEBUG("Search pair reached"); + //XBT_DEBUG("Lpr length : %lu", xbt_dynar_length(lpr)); + int n; unsigned int cursor = 0; - xbt_dynar_foreach(p, cursor, n){ - if(n == num_pair) + + xbt_dynar_foreach(lpr, cursor, n){ + if(n == num_pair){ + return 1; + } + } + return 0; +} + +int visited(int np, int sc){ + unsigned int c = 0; + mc_visited_pairs_t p = NULL; + + //XBT_DEBUG("Length of visited pairs : %lu", xbt_dynar_length(visited_pairs)); + + xbt_dynar_foreach(visited_pairs, c, p){ + //sleep(2); + //XBT_DEBUG("Visited pair : %p", p); + if((p->num_pair == np) && (p->search_cycle == sc)){ 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; - + smx_process_t process; + + + MC_wait_for_requests(); MC_SET_RAW_MEM; + //XBT_DEBUG("Taking initial snapshot"); + 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)){ @@ -58,24 +92,29 @@ void MC_dfs_init(xbt_automaton_t a){ } list_pairs_reached = xbt_dynar_new(sizeof(int), NULL); + visited_pairs = xbt_dynar_new(sizeof(mc_visited_pairs_t), NULL); - MC_UNSET_RAW_MEM; + MC_take_snapshot(initial_snapshot); + 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 + + /* 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; + xbt_state_t state = NULL; 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_transition_t transition_succ; + xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL); + xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL); + // int enabled_transition = 0; + mc_pairs_t pair_succ; 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){ @@ -83,43 +122,289 @@ void MC_dfs_init(xbt_automaton_t a){ 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); + xbt_dynar_push(successors, &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); + + MC_SET_RAW_MEM; + + mc_initial_pair = new_pair(initial_snapshot, initial_graph_state, transition_succ->dst); + xbt_dynar_push(elses, &mc_initial_pair); + + MC_UNSET_RAW_MEM; } } } } } - if(enabled_transition == 0){ - cursor2 = 0; - xbt_dynar_foreach(elses, cursor, transition_succ){ - + if(xbt_dynar_length(successors) > 0){ + + cursor = 0; + xbt_dynar_foreach(successors, cursor, pair_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); + xbt_fifo_unshift(mc_snapshot_stack, pair_succ); + + MC_UNSET_RAW_MEM; + + set_pair_visited(pair_succ->num, 0); + + if(cursor == 0) + MC_dfs(a, 0, 0); + else + MC_dfs(a, 0, 1); + + } + + }else{ + + if(xbt_dynar_length(elses) > 0){ + cursor = 0; + xbt_dynar_foreach(elses, cursor, pair_succ){ + MC_SET_RAW_MEM; + + xbt_fifo_unshift(mc_snapshot_stack, pair_succ); + //XBT_DEBUG("New initial pair from elses"); + + MC_UNSET_RAW_MEM; + + set_pair_visited(pair_succ->num, 0); + + if(cursor == 0) + MC_dfs(a, 0, 0); + else + MC_dfs(a, 0, 1); + } + }else{ + + XBT_DEBUG("No initial state !"); + + return; + } + } + +} + + + +void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ + + + if(xbt_fifo_size(mc_snapshot_stack) == 0) + return; + + //XBT_DEBUG("Lpr length before snapshot: %lu", xbt_dynar_length(lpr)); + + if(restore == 1){ + MC_restore_snapshot(((mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state); + MC_UNSET_RAW_MEM; + } + + //XBT_DEBUG("Lpr length after restore snapshot: %lu", xbt_dynar_length(lpr)); + + /* 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, mc_snapshot_stack size=%d",current_pair, MC_state_interleave_size(current_pair->graph_state), xbt_fifo_size(mc_snapshot_stack)); + //XBT_DEBUG("Restore : %d", restore); + + + /* Update statistics */ + mc_stats->visited_states++; + + //sleep(1); + + smx_process_t process = NULL; + int value; + mc_state_t next_graph_state = NULL; + smx_req_t req = NULL; + char *req_str; + + mc_pairs_t pair_succ; + xbt_transition_t transition_succ; + unsigned int cursor; + int res; + //int enabled_transition = 0; + + xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL); + xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL); + + mc_pairs_t next_pair; + mc_snapshot_t next_snapshot; + mc_snapshot_t current_snapshot = xbt_new0(s_mc_snapshot_t, 1); + + while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ + + XBT_DEBUG("Current pair : %p (%u interleave)", current_pair, MC_state_interleave_size(current_pair->graph_state)+1); + + MC_SET_RAW_MEM; + MC_take_snapshot(current_snapshot); + MC_UNSET_RAW_MEM; + + + /* 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_reset(elses); + xbt_dynar_reset(successors); + cursor = 0; + xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ + + res = MC_automaton_evaluate_label(a, transition_succ->label); + + MC_SET_RAW_MEM; + + next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); + + //XBT_DEBUG("Next pair : %p", next_pair); + + if(res == 1){ // enabled transition in automaton + xbt_dynar_push(successors, &next_pair); + //XBT_DEBUG("New Successors length : %lu", xbt_dynar_length(successors)); + }else{ + if(res == 2){ + xbt_dynar_push(elses, &next_pair); + //XBT_DEBUG("New Elses length : %lu", xbt_dynar_length(elses)); + } + } + MC_UNSET_RAW_MEM; + } + + + if((xbt_dynar_length(successors) == 0) && (xbt_dynar_length(elses) == 0) ){ + + MC_SET_RAW_MEM; + + next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state); + xbt_dynar_push(successors, &next_pair); + + MC_UNSET_RAW_MEM; + + } + + //XBT_DEBUG("Successors length : %lu", xbt_dynar_length(successors)); + //XBT_DEBUG("Elses length : %lu", xbt_dynar_length(elses)); + + if(xbt_dynar_length(successors) >0){ + + cursor = 0; + xbt_dynar_foreach(successors, cursor, pair_succ){ + + //XBT_DEBUG("Pair succ from successors : %p", pair_succ); + + MC_SET_RAW_MEM; + + if(visited(pair_succ->num, search_cycle) == 0){ + xbt_fifo_unshift(mc_snapshot_stack, pair_succ); + set_pair_visited(pair_succ->num, search_cycle); + MC_dfs(a, search_cycle, 0); + + if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){ + xbt_fifo_unshift(mc_snapshot_stack, pair_succ); + xbt_dynar_push(pair_succ->pairs_reached, &(pair_succ->num)); + XBT_DEBUG("Acceptance state : %p (automaton state : %p)", pair_succ, pair_succ->automaton_state); + MC_dfs(a, 1, 0); + } + } + + MC_UNSET_RAW_MEM; + + } - MC_dfs(a, 0); + }else{ + + cursor = 0; + xbt_dynar_foreach(elses, cursor, pair_succ){ + + //XBT_DEBUG("Pair succ from elses : %p", pair_succ); + + MC_SET_RAW_MEM; + + if(visited(pair_succ->num, search_cycle) == 0){ + //XBT_DEBUG("Pair not visited"); + xbt_fifo_unshift(mc_snapshot_stack, pair_succ); + set_pair_visited(pair_succ->num, search_cycle); + MC_dfs(a, search_cycle, 0); + + if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){ + xbt_fifo_unshift(mc_snapshot_stack, pair_succ); + xbt_dynar_push(pair_succ->pairs_reached, &(pair_succ->num)); + XBT_DEBUG("Acceptance state : %p (automaton state : %p)", pair_succ, pair_succ->automaton_state); + MC_dfs(a, 1, 0); + } + } + + MC_UNSET_RAW_MEM; + + } + } + + + + XBT_DEBUG("Restoring snapshot"); + + MC_restore_snapshot(current_snapshot); + MC_UNSET_RAW_MEM; + + } + + if((search_cycle == 1) && (pair_reached(current_pair->pairs_reached, current_pair->num) == 1)){ + XBT_DEBUG("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_DEBUG("| ACCEPTANCE CYCLE |"); + XBT_DEBUG("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + // afficher chemin menant au cycle d'acceptation + exit(0); } + + MC_SET_RAW_MEM; + xbt_fifo_shift(mc_snapshot_stack); + MC_UNSET_RAW_MEM; + + XBT_DEBUG("Shift state in snapshot_stack, mc_snapshot_stack size=%d", xbt_fifo_size(mc_snapshot_stack)); + } + int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){ switch(l->type){ @@ -237,137 +522,3 @@ int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){ 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 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)) != NULL){ - - /* 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_global.c b/src/mc/mc_global.c index 8c3f1718c8..203b7aa8c7 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -65,13 +65,13 @@ void MC_init_with_automaton(xbt_automaton_t a){ mc_stats = xbt_new0(s_mc_stats_t, 1); mc_stats->state_size = 1; + XBT_DEBUG("Creating snapshot_stack"); + /* Create exploration stack */ mc_snapshot_stack = xbt_fifo_new(); MC_UNSET_RAW_MEM; - XBT_DEBUG("---------- Avant dfs init -----------"); - MC_dfs_init(a); } diff --git a/src/mc/private.h b/src/mc/private.h index 6bfc90a4c9..88d4e7dc12 100644 --- a/src/mc/private.h +++ b/src/mc/private.h @@ -175,16 +175,21 @@ typedef struct s_mc_pairs{ mc_snapshot_t system_state; mc_state_t graph_state; xbt_state_t automaton_state; - int visited; + xbt_dynar_t pairs_reached; int num; }s_mc_pairs_t, *mc_pairs_t; +typedef struct s_mc_visited_pairs{ + int num_pair; + int search_cycle; +}s_mc_visited_pairs_t, *mc_visited_pairs_t; + void MC_dfs_init(xbt_automaton_t a); -void MC_dfs(xbt_automaton_t automaton, int search_cycle); +void MC_dfs(xbt_automaton_t automaton, int search_cycle, int restore); 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); - +void set_pair_visited(int num_pair, int search_cycle); +int visited(int num_pair, int search_cycle); +int pair_reached(xbt_dynar_t pairs_reached, int num_pair); #endif -- 2.20.1