From 525f475f139a3cb313bf7eff204db8a4e38e6ed5 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Mon, 22 Aug 2011 11:27:09 +0200 Subject: [PATCH] model-checker : update ddfs stateful model checking for liveness properties, bug with stateless mode --- examples/msg/mc/example_automaton.c | 4 +- src/mc/mc_global.c | 4 +- src/mc/mc_liveness.c | 398 +++++++++++++++++++++------- src/mc/private.h | 4 +- 4 files changed, 301 insertions(+), 109 deletions(-) diff --git a/examples/msg/mc/example_automaton.c b/examples/msg/mc/example_automaton.c index a45c3f8f0f..69a5629573 100644 --- a/examples/msg/mc/example_automaton.c +++ b/examples/msg/mc/example_automaton.c @@ -14,7 +14,7 @@ extern xbt_automaton_t automaton; int p=1; -int r=0; +int r=1; int q=1; int e=1; int d=1; @@ -55,7 +55,7 @@ int server(int argc, char *argv[]) } MSG_task_receive(&task, "mymailbox"); count++; - //r=(r+1)%2; + r=(r+1)%2; //XBT_INFO("r (server) = %d", r); } diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index addfdbbcc4..556fa707fb 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -116,8 +116,8 @@ void MC_init_liveness_stateful(xbt_automaton_t a){ MC_UNSET_RAW_MEM; - //MC_vddfs_stateful_init(a); - MC_ddfs_stateful_init(a); + MC_vddfs_stateful_init(a); + //MC_ddfs_stateful_init(a); //MC_dpor2_init(a); //MC_dpor3_init(a); } diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 4fdd3d9788..65e780da44 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -182,19 +182,41 @@ void MC_vddfs_stateful_init(xbt_automaton_t a){ -> donnera les états initiaux de la propriété consistants avec l'état initial du système */ unsigned int cursor = 0; - unsigned int cursor2 = 0; + //unsigned int cursor2 = 0; xbt_state_t state = NULL; - int res; - xbt_transition_t transition_succ; - xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); - mc_pair_t pair_succ; + //int res; + //xbt_transition_t transition_succ; + //xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); + //mc_pair_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){ + + MC_SET_RAW_MEM; + + mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst); + xbt_dynar_push(successors, &mc_initial_pair); + + MC_UNSET_RAW_MEM; + + } + } + } + } + + cursor = 0; + cursor2 = 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) || (res == 2)){ + if(res == 2){ MC_SET_RAW_MEM; @@ -228,7 +250,6 @@ void MC_vddfs_stateful_init(xbt_automaton_t a){ MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ); - set_pair_visited(pair_succ, 0); MC_UNSET_RAW_MEM; @@ -237,7 +258,24 @@ void MC_vddfs_stateful_init(xbt_automaton_t a){ }else{ MC_vddfs_stateful(a, 0, 1); } - } + } */ + + cursor = 0; + xbt_dynar_foreach(a->states, cursor, state){ + if(state->type == -1){ + + MC_SET_RAW_MEM; + mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state); + xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair); + MC_UNSET_RAW_MEM; + + if(cursor == 0){ + MC_vddfs_stateful(a, 0, 0); + }else{ + MC_vddfs_stateful(a, 0, 1); + } + } + } } @@ -266,7 +304,7 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ } } - XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle); + XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle); XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state)); @@ -339,7 +377,22 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ MC_SET_RAW_MEM; - if((res == 1) || (res == 2)){ // enabled transition in automaton + if(res == 1){ + next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); + xbt_dynar_push(successors, &next_pair); + } + + MC_UNSET_RAW_MEM; + } + + 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; + + if(res == 2){ next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); xbt_dynar_push(successors, &next_pair); } @@ -347,6 +400,7 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ MC_UNSET_RAW_MEM; } + if(xbt_dynar_length(successors) == 0){ @@ -358,6 +412,8 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ } + //XBT_DEBUG("Successors length %lu", xbt_dynar_length(successors)); + cursor = 0; xbt_dynar_foreach(successors, cursor, pair_succ){ @@ -381,32 +437,37 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ); set_pair_visited(pair_succ, search_cycle); + //XBT_DEBUG("New pair (graph=%p, automaton=%p) in stack", pair_succ->graph_state, pair_succ->automaton_state); MC_UNSET_RAW_MEM; MC_vddfs_stateful(a, search_cycle, 0); - if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){ - - MC_restore_snapshot(current_pair->system_state); - MC_UNSET_RAW_MEM; - - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - MC_state_interleave_process(current_pair->graph_state, process); - } - } - - set_pair_reached(current_pair); - XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id); - MC_vddfs_stateful(a, 1, 1); - - } + //XBT_DEBUG("Pair (graph=%p, automaton=%p) expanded", pair_succ->graph_state, pair_succ->automaton_state); + }else{ XBT_DEBUG("Pair already visited !"); } } + + if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){ + + /*MC_restore_snapshot(current_pair->system_state); + MC_UNSET_RAW_MEM; + + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ + MC_state_interleave_process(current_pair->graph_state, process); + } + }*/ + + set_pair_reached(current_pair); + XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id); + MC_vddfs_stateful(a, 1, 1); + + } + if(MC_state_interleave_size(current_pair->graph_state) > 0){ @@ -417,10 +478,15 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ MC_SET_RAW_MEM; - xbt_fifo_shift(mc_stack_liveness_stateful); - XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state); + mc_pair_t top_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)); + if((top_pair->graph_state == current_pair->graph_state) && (top_pair->automaton_state == current_pair->automaton_state)){ + xbt_fifo_shift(mc_stack_liveness_stateful); + XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state); + } MC_UNSET_RAW_MEM; + + } @@ -462,19 +528,41 @@ void MC_ddfs_stateful_init(xbt_automaton_t a){ -> donnera les états initiaux de la propriété consistants avec l'état initial du système */ unsigned int cursor = 0; - unsigned int cursor2 = 0; + //unsigned int cursor2 = 0; xbt_state_t state = NULL; - int res; - xbt_transition_t transition_succ; - xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); - mc_pair_t pair_succ; + //int res; + //xbt_transition_t transition_succ; + //xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); + //mc_pair_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){ + + MC_SET_RAW_MEM; + + mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst); + xbt_dynar_push(successors, &mc_initial_pair); + + MC_UNSET_RAW_MEM; + + } + } + } + } + + cursor = 0; + cursor2 = 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) || (res == 2)){ + if(res == 2){ MC_SET_RAW_MEM; @@ -501,22 +589,24 @@ void MC_ddfs_stateful_init(xbt_automaton_t a){ MC_UNSET_RAW_MEM; } } - } + }*/ cursor = 0; - xbt_dynar_foreach(successors, cursor, pair_succ){ - MC_SET_RAW_MEM; - - xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ); - - MC_UNSET_RAW_MEM; + xbt_dynar_foreach(a->states, cursor, state){ + if(state->type == -1){ + + MC_SET_RAW_MEM; + mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state); + xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair); + MC_UNSET_RAW_MEM; - if(cursor == 0){ - MC_ddfs_stateful(a, 0, 0); - }else{ - MC_ddfs_stateful(a, 0, 1); + if(cursor == 0){ + MC_ddfs_stateful(a, 0, 0); + }else{ + MC_ddfs_stateful(a, 0, 1); + } } - } + } } @@ -545,9 +635,8 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ } } - XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle); + XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle); XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state)); - mc_stats_pair->visited_pairs++; @@ -579,7 +668,7 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ /* Debug information */ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ req_str = MC_request_to_string(req, value); - XBT_DEBUG("Execute: %s", req_str); + XBT_DEBUG("%u Execute: %s", search_cycle, req_str); xbt_free(req_str); } @@ -618,7 +707,22 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ MC_SET_RAW_MEM; - if((res == 1) || (res == 2)){ // enabled transition in automaton + if(res == 1){ // enabled transition in automaton + next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); + xbt_dynar_push(successors, &next_pair); + } + + MC_UNSET_RAW_MEM; + } + + 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; + + if(res == 2){ // enabled transition in automaton next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); xbt_dynar_push(successors, &next_pair); } @@ -636,6 +740,7 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ } + //XBT_DEBUG("Successors in automaton %lu", xbt_dynar_length(successors)); cursor = 0; xbt_dynar_foreach(successors, cursor, pair_succ){ @@ -660,10 +765,14 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ MC_UNSET_RAW_MEM; MC_ddfs_stateful(a, search_cycle, 0); + } + + if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){ - if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){ + set_pair_reached(current_pair); + XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id); - MC_restore_snapshot(current_pair->system_state); + /*MC_restore_snapshot(current_pair->system_state); MC_UNSET_RAW_MEM; xbt_swag_foreach(process, simix_global->process_list){ @@ -672,24 +781,32 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ } } - set_pair_reached(current_pair); - XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id); + mc_pair_t top_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)); + if((top_pair->graph_state != current_pair->graph_state) || (top_pair->automaton_state != current_pair->automaton_state)){ + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness_stateful, current_pair); + MC_UNSET_RAW_MEM; + }*/ + MC_ddfs_stateful(a, 1, 1); - } } - - + + if(MC_state_interleave_size(current_pair->graph_state) > 0){ MC_restore_snapshot(current_snapshot); MC_UNSET_RAW_MEM; } + } MC_SET_RAW_MEM; - xbt_fifo_shift(mc_stack_liveness_stateful); - XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state); + mc_pair_t top_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)); + if((top_pair->graph_state == current_pair->graph_state) && (top_pair->automaton_state == current_pair->automaton_state)){ + xbt_fifo_shift(mc_stack_liveness_stateful); + XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state); + } MC_UNSET_RAW_MEM; } @@ -715,7 +832,7 @@ mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){ } -int reached_stateless(mc_reached_pair_stateless_t pair){ +int reached_stateless(mc_pair_stateless_t pair){ char* hash_reached = malloc(sizeof(char)*160); unsigned int c= 0; @@ -736,16 +853,11 @@ int reached_stateless(mc_reached_pair_stateless_t pair){ void set_pair_stateless_reached(mc_pair_stateless_t pair){ - mc_reached_pair_stateless_t p = NULL; - p = xbt_new0(s_mc_reached_pair_stateless_t, 1); - p->pair = pair; - p->snapshot_system = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot(p->snapshot_system); + if(reached_stateless(pair) == 0){ - if(reached_stateless(p) == 0){ MC_SET_RAW_MEM; char *hash = malloc(sizeof(char)*160) ; - xbt_sha((char *)&p, hash); + xbt_sha((char *)&pair, hash); xbt_dynar_push(reached_pairs, &hash); MC_UNSET_RAW_MEM; } @@ -782,19 +894,42 @@ void MC_ddfs_stateless_init(xbt_automaton_t a){ -> donnera les états initiaux de la propriété consistants avec l'état initial du système */ unsigned int cursor = 0; - unsigned int cursor2 = 0; + //unsigned int cursor2 = 0; xbt_state_t state = NULL; - int res; - xbt_transition_t transition_succ; - xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); - mc_pair_stateless_t pair_succ; + //int res; + //xbt_transition_t transition_succ; + //xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); + //xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); + //mc_pair_stateless_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){ + + MC_SET_RAW_MEM; + + mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst); + xbt_dynar_push(successors, &mc_initial_pair); + + MC_UNSET_RAW_MEM; + + } + } + } + } + + cursor = 0; + cursor2 = 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) || (res == 2)){ + if(res == 2){ MC_SET_RAW_MEM; @@ -808,9 +943,10 @@ void MC_ddfs_stateless_init(xbt_automaton_t a){ } } + cursor = 0; - if(xbt_dynar_length(successors) == 0){ + if((xbt_dynar_length(successors) == 0) && (xbt_dynar_length(elses) == 0)){ xbt_dynar_foreach(a->states, cursor, state){ if(state->type == -1){ MC_SET_RAW_MEM; @@ -823,13 +959,13 @@ void MC_ddfs_stateless_init(xbt_automaton_t a){ } } + cursor = 0; xbt_dynar_foreach(successors, cursor, pair_succ){ MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); - /* Save the initial state */ initial_snapshot = xbt_new0(s_mc_snapshot_t, 1); MC_take_snapshot(initial_snapshot); @@ -840,25 +976,47 @@ void MC_ddfs_stateless_init(xbt_automaton_t a){ }else{ MC_ddfs_stateless(a, 0, 1); } - } -} + } */ + xbt_dynar_foreach(a->states, cursor, state){ + if(state->type == -1){ + + MC_SET_RAW_MEM; + mc_initial_pair = new_pair_stateless(initial_graph_state, state); + xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair); + + initial_snapshot = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot(initial_snapshot); + + MC_UNSET_RAW_MEM; + + if(cursor == 0){ + MC_ddfs_stateless(a, 0); + }else{ + MC_restore_snapshot(initial_snapshot); + MC_UNSET_RAW_MEM; + MC_ddfs_stateless(a, 0); + } + } + } +} -void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ - smx_process_t process = NULL; +void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle){ + smx_process_t process = NULL; if(xbt_fifo_size(mc_stack_liveness_stateless) == 0) return; + //XBT_DEBUG("Stack size before restore %u", xbt_fifo_size(mc_stack_liveness_stateless)); + /* Get current state */ mc_pair_stateless_t current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless)); XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle); XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state)); - mc_stats_pair->visited_pairs++; int value; @@ -874,15 +1032,22 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ xbt_dynar_t successors; mc_pair_stateless_t next_pair; - mc_snapshot_t snap; + mc_snapshot_t current_snap; + while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ - + + MC_SET_RAW_MEM; + current_snap = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot(current_snap); + MC_UNSET_RAW_MEM; + //XBT_DEBUG("Interleave size %u", MC_state_interleave_size(current_pair->graph_state)); /* Debug information */ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ req_str = MC_request_to_string(req, value); + XBT_DEBUG("-- Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state)); XBT_DEBUG("Execute: %s", req_str); xbt_free(req_str); } @@ -909,12 +1074,9 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ MC_state_interleave_process(next_graph_state, process); } } - + successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); - snap = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot(snap); - MC_UNSET_RAW_MEM; //xbt_dynar_reset(successors); @@ -927,7 +1089,23 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ MC_SET_RAW_MEM; - if((res == 1) || (res == 2)){ // enabled transition in automaton + if(res == 1){ // enabled transition in automaton + next_pair = new_pair_stateless(next_graph_state, transition_succ->dst); + xbt_dynar_push(successors, &next_pair); + } + + MC_UNSET_RAW_MEM; + } + + 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; + + if(res == 2){ // enabled transition in automaton next_pair = new_pair_stateless(next_graph_state, transition_succ->dst); xbt_dynar_push(successors, &next_pair); } @@ -946,15 +1124,11 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ } cursor = 0; + //XBT_DEBUG("Successors length %lu", xbt_dynar_length(successors)); xbt_dynar_foreach(successors, cursor, pair_succ){ - - mc_reached_pair_stateless_t p = NULL; - p = xbt_new0(s_mc_reached_pair_stateless_t, 1); - p->pair = pair_succ; - p->snapshot_system = snap; - if((search_cycle == 1) && (reached_stateless(p) == 1)){ + if((search_cycle == 1) && (reached_stateless(pair_succ) == 1)){ XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); @@ -971,29 +1145,47 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); MC_UNSET_RAW_MEM; - MC_ddfs_stateless(a, search_cycle, 0); + MC_ddfs_stateless(a, search_cycle); - if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){ + //XBT_DEBUG("Stack size %u", xbt_fifo_size(mc_stack_liveness_stateless)); + } + + //xbt_dynar_reset(successors); + + if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){ set_pair_stateless_reached(current_pair); XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id); - MC_replay_liveness(mc_stack_liveness_stateless); - MC_ddfs_stateless(a, 1, 1); + MC_restore_snapshot(current_snap); + MC_UNSET_RAW_MEM; - } + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ + MC_state_interleave_process(current_pair->graph_state, process); + } + } + + MC_ddfs_stateless(a, 1); } - + if(MC_state_interleave_size(current_pair->graph_state) > 0){ - XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless)); - MC_replay_liveness(mc_stack_liveness_stateless); + //XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless)); + //MC_replay_liveness(mc_stack_liveness_stateless); + MC_restore_snapshot(current_snap); + MC_UNSET_RAW_MEM; } + } MC_SET_RAW_MEM; - xbt_fifo_shift(mc_stack_liveness_stateless); - XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state); + mc_pair_stateless_t top_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless)); + if((top_pair->graph_state == current_pair->graph_state) && (top_pair->automaton_state == current_pair->automaton_state)){ + xbt_fifo_shift(mc_stack_liveness_stateless); + XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle); + } MC_UNSET_RAW_MEM; + //XBT_DEBUG("Stack size after shift %u", xbt_fifo_size(mc_stack_liveness_stateless)); } diff --git a/src/mc/private.h b/src/mc/private.h index 6439df43f7..ba7cc37114 100644 --- a/src/mc/private.h +++ b/src/mc/private.h @@ -239,8 +239,8 @@ extern xbt_fifo_t mc_stack_liveness_stateless; mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st); void MC_ddfs_stateless_init(xbt_automaton_t a); -void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay); -int reached_stateless(mc_reached_pair_stateless_t p); +void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle); +int reached_stateless(mc_pair_stateless_t p); void set_pair_stateless_reached(mc_pair_stateless_t p); void MC_show_stack_liveness_stateless(xbt_fifo_t stack); void MC_dump_stack_liveness_stateless(xbt_fifo_t stack); -- 2.20.1