From cd794f9367d030c421a5bcbd9e9ceba8a232e4ce Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 19 May 2011 17:41:45 +0200 Subject: [PATCH] model checker : dfs algorithm corrected --- examples/msg/mc/example_automaton.c | 46 ++- examples/msg/mc/example_automaton.h | 7 +- examples/msg/mc/result_parse | 28 +- examples/msg/mc/result_parse2 | 28 ++ src/mc/mc_dfs.c | 504 ++++++++++++++++++++-------- src/mc/mc_global.c | 6 +- 6 files changed, 448 insertions(+), 171 deletions(-) create mode 100644 examples/msg/mc/result_parse2 diff --git a/examples/msg/mc/example_automaton.c b/examples/msg/mc/example_automaton.c index fbf546a6b0..8780f17d5c 100644 --- a/examples/msg/mc/example_automaton.c +++ b/examples/msg/mc/example_automaton.c @@ -13,22 +13,37 @@ XBT_LOG_NEW_DEFAULT_CATEGORY(example, "Example with automaton"); extern xbt_automaton_t automaton; -int d=1; -int r=0; +int p=1; +int r=1; +int q=1; int e=1; +int d=1; -int predD(){ - return d; + +int predP(){ + return p; } int predR(){ return r; } +int predQ(){ + return q; +} + + +int predD(){ + return d; +} + + int predE(){ return e; } + + int server(int argc, char *argv[]) { m_task_t task = NULL; @@ -40,7 +55,9 @@ int server(int argc, char *argv[]) } MSG_task_receive(&task, "mymailbox"); count++; - //r=(r+1)%4; + r=(r+1)%3; + //d=(d+1)%2; + XBT_INFO("r (server) = %d", r); } MC_assert_pair(atoi(MSG_task_get_name(task)) == 3); @@ -59,7 +76,10 @@ int client(int argc, char *argv[]) MSG_task_send(task, "mymailbox"); XBT_INFO("Sent!"); - //r=(r+1)%4; + + //r=(r+1)%3; + XBT_INFO("r (client) = %d", r); + return 0; } @@ -69,10 +89,12 @@ int main(int argc, char **argv){ init(); yyparse(); automaton = get_automaton(); - xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"d", &predD); - ps = xbt_new_propositional_symbol(automaton,"e", &predE); + xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"p", &predP); + ps = xbt_new_propositional_symbol(automaton,"q", &predQ); ps = xbt_new_propositional_symbol(automaton,"r", &predR); - + ps = xbt_new_propositional_symbol(automaton,"e", &predE); + ps = xbt_new_propositional_symbol(automaton,"d", &predD); + //display_automaton(); MSG_global_init(&argc, argv); @@ -83,8 +105,10 @@ int main(int argc, char **argv){ MSG_function_register("client", client); - MSG_launch_application("deploy_bugged1.xml"); - + MSG_launch_application("deploy_bugged1.xml"); + + XBT_INFO("r=%d", r); + MSG_main_with_automaton(automaton); MSG_clean(); diff --git a/examples/msg/mc/example_automaton.h b/examples/msg/mc/example_automaton.h index 745762ce50..1ff4c9982b 100644 --- a/examples/msg/mc/example_automaton.h +++ b/examples/msg/mc/example_automaton.h @@ -5,10 +5,15 @@ int yyparse(void); int yywrap(void); int yylex(void); -int predD(void); +int predP(void); int predR(void); +int predQ(void); +int predD(void); int predE(void); + + + int server(int argc, char *argv[]); int client(int argc, char *argv[]); diff --git a/examples/msg/mc/result_parse b/examples/msg/mc/result_parse index 43f7fc5e8f..92702b12e2 100644 --- a/examples/msg/mc/result_parse +++ b/examples/msg/mc/result_parse @@ -1,29 +1,17 @@ -never { /* []<>e->[](d-><>r) */ - +never { /* !([]<>p->[](q-><>r)) */ T0_init: if - :: (!d) || (r) -> goto accept_S1 - :: (1) -> goto T1_S4 - :: (1) -> goto T0_S2 - :: (!e) -> goto accept_S3 + :: (1) -> goto T0_init + :: (!r && q) -> goto T1_S4 fi; T1_S4: if - :: (1) -> goto T1_S4 - :: (r) -> goto accept_S1 + :: (!r) -> goto T1_S4 + :: (!r && p) -> goto accept_S4 fi; -accept_S1: +accept_S4: if - :: (!d) || (r) -> goto accept_S1 - :: (1) -> goto T1_S4 - fi; -T0_S2: - if - :: (1) -> goto T0_S2 - :: (!e) -> goto accept_S3 - fi; -accept_S3: - if - :: (!e) -> goto accept_S3 + :: (!r) -> goto T1_S4 + :: (!r && p) -> goto accept_S4 fi; } diff --git a/examples/msg/mc/result_parse2 b/examples/msg/mc/result_parse2 new file mode 100644 index 0000000000..2d0a31203d --- /dev/null +++ b/examples/msg/mc/result_parse2 @@ -0,0 +1,28 @@ +never { +T0_init: + if + :: (!d) || (r) -> goto accept_S1 + :: (1) -> goto T1_S4 + :: (1) -> goto T0_S2 + :: (!e) -> goto accept_S3 + fi; +T1_S4: + if + :: (1) -> goto T1_S4 + :: (r) -> goto accept_S1 + fi; +accept_S1: + if + :: (!d) || (r) -> goto accept_S1 + :: (1) -> goto T1_S4 + fi; +T0_S2: + if + :: (1) -> goto T0_S2 + :: (!e) -> goto accept_S3 + fi; +accept_S3: + if + :: (!e) -> goto accept_S3 + fi; +} diff --git a/src/mc/mc_dfs.c b/src/mc/mc_dfs.c index 246b21b3a3..fa9ec05c14 100644 --- a/src/mc/mc_dfs.c +++ b/src/mc/mc_dfs.c @@ -13,7 +13,7 @@ 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->automaton_state = st; p->graph_state = sg; p->num = max_pair; max_pair++; @@ -23,17 +23,16 @@ mc_pairs_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){ void set_pair_visited(mc_state_t gs, xbt_state_t as, int sc){ - if(visited(gs, as, sc) == 0){ - //XBT_DEBUG("New visited pair : graph=%p, automaton=%p", gs, as); - MC_SET_RAW_MEM; - mc_visited_pairs_t p = NULL; - p = xbt_new0(s_mc_visited_pairs_t, 1); - p->graph_state = gs; - p->automaton_state = as; - p->search_cycle = sc; - xbt_dynar_push(visited_pairs, &p); - MC_UNSET_RAW_MEM; - } + //XBT_DEBUG("New visited pair : graph=%p, automaton=%p", gs, as); + MC_SET_RAW_MEM; + mc_visited_pairs_t p = NULL; + p = xbt_new0(s_mc_visited_pairs_t, 1); + p->graph_state = gs; + p->automaton_state = as; + 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)); + MC_UNSET_RAW_MEM; //XBT_DEBUG("New visited pair , length of visited pairs : %lu", xbt_dynar_length(visited_pairs)); } @@ -50,14 +49,17 @@ int reached(mc_state_t gs, xbt_state_t as ){ if(rp->automaton_state == as){ different_process=0; for(i=0; i < gs->max_pid; i++){ - if(gs->proc_status[i].state != rp->graph_state->proc_status[i].state){ - different_process++; - } + if(gs->proc_status[i].state != rp->graph_state->proc_status[i].state){ + different_process++; + } } if(different_process==0){ - MC_UNSET_RAW_MEM; - return 1; + MC_UNSET_RAW_MEM; + XBT_DEBUG("Pair (graph=%p, automaton=%p, interleave=%d) already reached (graph=%p)!", gs, as, MC_state_interleave_size(gs), rp->graph_state); + return 1; } + /* XBT_DEBUG("Pair (graph=%p, automaton=%p(%s)) already reached !", gs, as, as->id); */ + /* return 1; */ } } MC_UNSET_RAW_MEM; @@ -66,6 +68,7 @@ int reached(mc_state_t gs, xbt_state_t as ){ void set_pair_reached(mc_state_t gs, xbt_state_t as){ + //XBT_DEBUG("Set pair (graph=%p, automaton=%p) reached ", gs, as); if(reached(gs, as) == 0){ MC_SET_RAW_MEM; mc_reached_pairs_t p = NULL; @@ -73,7 +76,7 @@ void set_pair_reached(mc_state_t gs, xbt_state_t as){ p->graph_state = gs; p->automaton_state = as; xbt_dynar_push(reached_pairs, &p); - //XBT_DEBUG("New reached pair : graph=%p, automaton=%p", gs, as); + XBT_DEBUG("New reached pair : graph=%p, automaton=%p(%s)", gs, as, as->id); MC_UNSET_RAW_MEM; } @@ -85,8 +88,12 @@ int visited(mc_state_t gs, xbt_state_t as, int sc){ unsigned int i; int different_process; + //XBT_DEBUG("Visited pair length : %lu", xbt_dynar_length(visited_pairs)); + MC_SET_RAW_MEM; xbt_dynar_foreach(visited_pairs, c, p){ + //XBT_DEBUG("Test pair visited"); + //sleep(1); if((p->automaton_state == as) && (p->search_cycle == sc)){ different_process=0; for(i=0; i < gs->max_pid; i++){ @@ -136,6 +143,33 @@ void MC_dfs_init(xbt_automaton_t a){ MC_UNSET_RAW_MEM; + /* unsigned int cursor = 0; */ + /* xbt_state_t state = NULL; */ + /* int nb_init_state = 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_snapshot_stack, mc_initial_pair); */ + + /* XBT_DEBUG("**************************************************"); */ + /* XBT_DEBUG("Initial state=%p ", mc_initial_pair); */ + + /* MC_UNSET_RAW_MEM; */ + + /* set_pair_visited(mc_initial_pair->graph_state, mc_initial_pair->automaton_state, 0); */ + + /* if(nb_init_state == 0) */ + /* MC_dfs(a, 0, 0); */ + /* else */ + /* MC_dfs(a, 0, 1); */ + + /* nb_init_state++; */ + /* } */ + /* } */ /* 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 */ @@ -153,32 +187,32 @@ void MC_dfs_init(xbt_automaton_t a){ 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); + res = MC_automaton_evaluate_label(a, transition_succ->label); - if(res == 1){ + if(res == 1){ - MC_SET_RAW_MEM; + 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_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst); + xbt_dynar_push(successors, &mc_initial_pair); - //XBT_DEBUG("New initial successor"); + //XBT_DEBUG("New initial successor"); - MC_UNSET_RAW_MEM; + MC_UNSET_RAW_MEM; - }else{ - if(res == 2){ + }else{ + if(res == 2){ - MC_SET_RAW_MEM; + MC_SET_RAW_MEM; - mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst); - xbt_dynar_push(elses, &mc_initial_pair); + mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst); + xbt_dynar_push(elses, &mc_initial_pair); - //XBT_DEBUG("New initial successor"); + //XBT_DEBUG("New initial successor"); - MC_UNSET_RAW_MEM; - } - } + MC_UNSET_RAW_MEM; + } + } } } } @@ -194,52 +228,75 @@ void MC_dfs_init(xbt_automaton_t a){ XBT_DEBUG("**************************************************"); XBT_DEBUG("Initial state=%p ", pair_succ); - MC_UNSET_RAW_MEM; + MC_UNSET_RAW_MEM; set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0); - - if(cursor == 0) - MC_dfs(a, 0, 0); - else - MC_dfs(a, 0, 1); - - } - }else{ + if(cursor == 0){ + MC_dfs(a, 0, 0); + if(pair_succ->automaton_state->type == 1){ + set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state); + MC_dfs(a, 1, 0); + } + }else{ + MC_dfs(a, 0, 1); + if(pair_succ->automaton_state->type == 1){ + MC_dfs(a, 1, 1); + } + } - if(xbt_dynar_length(elses) > 0){ - cursor = 0; - xbt_dynar_foreach(elses, cursor, pair_succ){ - MC_SET_RAW_MEM; + /* if(cursor == 0) */ + /* MC_dfs(a, 0, 0); */ + /* else */ + /* MC_dfs(a, 0, 1); */ + + } - xbt_fifo_unshift(mc_snapshot_stack, pair_succ); + } + + if(xbt_dynar_length(elses) > 0){ + cursor = 0; + xbt_dynar_foreach(elses, cursor, pair_succ){ + MC_SET_RAW_MEM; - XBT_DEBUG("**************************************************"); - XBT_DEBUG("Initial state=%p ", pair_succ); + xbt_fifo_unshift(mc_snapshot_stack, pair_succ); - MC_UNSET_RAW_MEM; + XBT_DEBUG("**************************************************"); + XBT_DEBUG("Initial state=%p ", pair_succ); - set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0); + MC_UNSET_RAW_MEM; - if(cursor == 0) - MC_dfs(a, 0, 0); - else - MC_dfs(a, 0, 1); - } - }else{ + set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0); - XBT_DEBUG("No initial state !"); + if(cursor == 0){ + MC_dfs(a, 0, 0); + if(pair_succ->automaton_state->type == 1){ + set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state); + MC_dfs(a, 1, 0); + } + }else{ + MC_dfs(a, 0, 1); + if(pair_succ->automaton_state->type == 1){ + MC_dfs(a, 1, 1); + } + } - return; + /* if(cursor == 0) */ + /* MC_dfs(a, 0, 0); */ + /* else */ + /* MC_dfs(a, 0, 1); */ + + } } } - void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ + smx_process_t process = NULL; + if(xbt_fifo_size(mc_snapshot_stack) == 0) return; @@ -249,24 +306,28 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ MC_UNSET_RAW_MEM; } - //XBT_DEBUG("Lpv length after restore snapshot: %lu", xbt_dynar_length(visited_pairs)); /* 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 : graph=%p, automaton=%p, %u interleave, stack size=%d", current_pair->graph_state, current_pair->automaton_state, MC_state_interleave_size(current_pair->graph_state), xbt_fifo_size(mc_snapshot_stack)); + if(restore==1){ + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ + //XBT_DEBUG("Pid : %lu", process->pid); + MC_state_interleave_process(current_pair->graph_state, process); + } + } + } + + XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle); + XBT_DEBUG("State : 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("Restore : %d", restore); - - /* Update statistics */ - //mc_stats->visited_states++; - //set_pair_visited(current_pair->graph_state, current_pair->automaton_state, search_cycle); + //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); //sleep(1); - smx_process_t process = NULL; int value; mc_state_t next_graph_state = NULL; smx_req_t req = NULL; @@ -278,18 +339,15 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ 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); + 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; + 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); - //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs)); - MC_SET_RAW_MEM; current_snapshot = xbt_new0(s_mc_snapshot_t, 1); MC_take_snapshot(current_snapshot); @@ -307,7 +365,7 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ //mc_stats->executed_transitions++; /* Answer the request */ - SIMIX_request_pre(req, value); + SIMIX_request_pre(req, value); /* Wait for requests (schedules processes) */ MC_wait_for_requests(); @@ -321,6 +379,7 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ /* Get 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)){ + //XBT_DEBUG("Pid : %lu", process->pid); MC_state_interleave_process(next_graph_state, process); } } @@ -330,7 +389,6 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ MC_UNSET_RAW_MEM; - xbt_dynar_reset(elses); xbt_dynar_reset(successors); cursor = 0; @@ -343,21 +401,15 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ //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)); - } + if((res == 1) || (res == 2)){ // enabled transition in automaton + xbt_dynar_push(successors, &next_pair); } MC_UNSET_RAW_MEM; } - if((xbt_dynar_length(successors) == 0) && (xbt_dynar_length(elses) == 0) ){ + if(xbt_dynar_length(successors) == 0){ MC_SET_RAW_MEM; next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state); @@ -366,7 +418,7 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ } - //XBT_DEBUG("Successors length : %lu", xbt_dynar_length(successors)); + // XBT_DEBUG("Successors length : %lu", xbt_dynar_length(successors)); //XBT_DEBUG("Elses length : %lu", xbt_dynar_length(elses)); if(xbt_dynar_length(successors) >0){ @@ -375,9 +427,21 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ xbt_dynar_foreach(successors, cursor, pair_succ){ //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state); + + if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){ + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("| ACCEPTANCE CYCLE |"); + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("Counter-example that violates formula :"); + MC_show_snapshot_stack(mc_snapshot_stack); + MC_dump_snapshot_stack(mc_snapshot_stack); + exit(0); + } if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){ + //XBT_DEBUG("Unvisited pair !"); + MC_SET_RAW_MEM; xbt_fifo_unshift(mc_snapshot_stack, pair_succ); MC_UNSET_RAW_MEM; @@ -385,73 +449,41 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle); MC_dfs(a, search_cycle, 0); - if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){ + 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)){ + //XBT_DEBUG("Pid : %lu", process->pid); + MC_state_interleave_process(current_pair->graph_state, process); + } + } - set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state); - XBT_DEBUG("Acceptance state : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state); - MC_dfs(a, 1, 0); + set_pair_reached(current_pair->graph_state, current_pair->automaton_state); + XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id); + MC_dfs(a, 1, 1); } - }else{ - //XBT_DEBUG("Pair (graph=%p, automaton=%p) already visited !", pair_succ->graph_state, pair_succ->automaton_state ); - set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle); } - } - }else{ - - cursor = 0; - xbt_dynar_foreach(elses, cursor, pair_succ){ - - //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state); - - if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){ - - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_snapshot_stack, pair_succ); - MC_UNSET_RAW_MEM; - - set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle); - MC_dfs(a, search_cycle, 0); - - if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){ - - set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state); - XBT_DEBUG("Acceptance state : graph state=%p, automaton state=%p",pair_succ->graph_state, pair_succ->automaton_state); - MC_dfs(a, 1, 0); + } - } - }else{ - //XBT_DEBUG("Pair (graph=%p, automaton=%p) already visited !", pair_succ->graph_state, pair_succ->automaton_state ); - /* Different graph_state */ - set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle); - } - } - - } - if(MC_state_interleave_size(current_pair->graph_state) > 0){ MC_restore_snapshot(current_snapshot); MC_UNSET_RAW_MEM; //XBT_DEBUG("Snapshot restored"); - } + } } - if((search_cycle == 1) && (reached(current_pair->graph_state, current_pair->automaton_state) == 1)){ - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("| ACCEPTANCE CYCLE |"); - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("Counter-example that violates formula :"); - MC_show_snapshot_stack(mc_snapshot_stack); - MC_dump_snapshot_stack(mc_snapshot_stack); - exit(0); - } MC_SET_RAW_MEM; + //remove_pair_reached(current_pair->graph_state); xbt_fifo_shift(mc_snapshot_stack); - //XBT_DEBUG("State shifted in snapshot_stack, mc_snapshot_stack size=%d", xbt_fifo_size(mc_snapshot_stack)); + XBT_DEBUG("State (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state); MC_UNSET_RAW_MEM; } @@ -609,3 +641,203 @@ 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, int restore){ */ + + +/* if(xbt_fifo_size(mc_snapshot_stack) == 0) */ +/* return; */ + +/* 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("Lpv length after restore snapshot: %lu", xbt_dynar_length(visited_pairs)); */ + +/* /\* 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("************************************************** ( search_cycle = %d )", search_cycle); */ +/* XBT_DEBUG("State : 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("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); */ + +/* //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); */ +/* xbt_dynar_reset(all_successors); */ + +/* mc_pairs_t next_pair; */ +/* mc_snapshot_t next_snapshot; */ +/* mc_snapshot_t current_snapshot; */ + +/* 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); */ +/* //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs)); */ + +/* MC_SET_RAW_MEM; */ +/* current_snapshot = xbt_new0(s_mc_snapshot_t, 1); */ +/* 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 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){ */ +/* MC_SET_RAW_MEM; */ +/* xbt_dynar_push(all_successors, &pair_succ); */ +/* MC_UNSET_RAW_MEM; */ +/* } */ + +/* }else{ */ + +/* cursor = 0; */ +/* xbt_dynar_foreach(elses, cursor, pair_succ){ */ +/* MC_SET_RAW_MEM; */ +/* xbt_dynar_push(all_successors, &pair_succ); */ +/* MC_UNSET_RAW_MEM; */ +/* } */ + +/* } */ + +/* MC_restore_snapshot(current_snapshot); */ +/* MC_UNSET_RAW_MEM; */ + +/* } */ + +/* //XBT_DEBUG("All successors : %lu", xbt_dynar_length(all_successors)); */ + +/* cursor = 0; */ + +/* xbt_dynar_foreach(all_successors, cursor, pair_succ){ */ + +/* if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){ */ +/* XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); */ +/* XBT_INFO("| ACCEPTANCE CYCLE |"); */ +/* XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); */ +/* XBT_INFO("Counter-example that violates formula :"); */ +/* MC_show_snapshot_stack(mc_snapshot_stack); */ +/* MC_dump_snapshot_stack(mc_snapshot_stack); */ +/* exit(0); */ +/* } */ + +/* if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){ */ + +/* //XBT_DEBUG("New pair in stack"); */ + +/* MC_SET_RAW_MEM; */ +/* xbt_fifo_unshift(mc_snapshot_stack, pair_succ); */ +/* MC_UNSET_RAW_MEM; */ + +/* set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle); */ +/* MC_dfs(a, search_cycle, 1); */ + +/* if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){ */ + +/* set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state); */ +/* XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); */ +/* MC_dfs(a, 1, 1); */ + +/* } */ +/* } */ + +/* } */ + +/* MC_SET_RAW_MEM; */ +/* //remove_pair_reached(current_pair->graph_state); */ +/* xbt_fifo_shift(mc_snapshot_stack); */ +/* XBT_DEBUG("State (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state); */ +/* MC_UNSET_RAW_MEM; */ + +/* } */ diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 85770eabc1..508ef2803f 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -273,9 +273,9 @@ void MC_assert_pair(int prop){ XBT_INFO("**************************"); XBT_INFO("*** PROPERTY NOT VALID ***"); XBT_INFO("**************************"); - XBT_INFO("Counter-example execution trace:"); - MC_show_snapshot_stack(mc_snapshot_stack); - MC_dump_snapshot_stack(mc_snapshot_stack); + //XBT_INFO("Counter-example execution trace:"); + //MC_show_snapshot_stack(mc_snapshot_stack); + //MC_dump_snapshot_stack(mc_snapshot_stack); //MC_print_statistics(mc_stats); xbt_abort(); } -- 2.20.1