X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/dda93e7e3c8844b68b25ce1172d9fe1b6fcb8d37..5ff7a0f00eab7d7005451ad66f517ac9c4bfd68a:/src/mc/mc_liveness.c diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index ae15bbfcef..08ee45f0f1 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -45,46 +45,44 @@ const char* get_memory_map_addr(void *addr){ if(fp == NULL) perror("fopen failed"); - if(addr == NULL) + if(addr == NULL){ + free(line); + fclose(fp); return "nil"; + } - char *lfields[6], *start, *end, *endptr; - int i; + xbt_dynar_t lfields = NULL; + xbt_dynar_t start_end = NULL; void *start_addr; void *end_addr; while ((read = getline(&line, &n, fp)) != -1) { - line[read - 1] = '\0'; + xbt_str_trim(line, NULL); + xbt_str_strip_spaces(line); + lfields = xbt_str_split(line,NULL); - lfields[0] = strtok(line, " "); - - for (i = 1; i < 6 && lfields[i - 1] != NULL; i++) { - lfields[i] = strtok(NULL, " "); - } + start_end = xbt_str_split(xbt_dynar_get_as(lfields, 0, char*), "-"); + start_addr = (void *) strtoul(xbt_dynar_get_as(start_end, 0, char*), NULL, 16); + end_addr = (void *) strtoul(xbt_dynar_get_as(start_end, 1, char*), NULL, 16); - start = strtok(lfields[0], "-"); - start_addr = (void *) strtoul(start, &endptr, 16); - - if(start_addr == std_heap) - lfields[5] = strdup("std_heap"); - if(start_addr == raw_heap) - lfields[5] = strdup("raw_heap"); - end = strtok(NULL, "-"); - end_addr = (void *) strtoul(end, &endptr, 16); - if((addr > start_addr) && ( addr < end_addr)){ free(line); fclose(fp); - if(lfields[5] != NULL){ - return lfields[5]; - }else{ + if(start_addr == std_heap) + return "std_heap"; + if(start_addr == raw_heap) + return "raw_heap"; + if(xbt_dynar_length(lfields) == 6) + return xbt_dynar_get_as(lfields, xbt_dynar_length(lfields) - 1, char*); + else return "Anonymous"; - } } - + } + free(line); + fclose(fp); return "Unknown area"; } @@ -93,18 +91,25 @@ int data_program_region_compare(void *d1, void *d2, size_t size){ int distance = 0; int pointer_align; int i; + char *pointed_address1 = NULL, *pointed_address2 = NULL; for(i=0; inum_reg != s2->num_reg){ - XBT_DEBUG("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg); + XBT_INFO("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg); return 1; } @@ -141,91 +153,51 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, void* s_heap, void* r_h for(i=0 ; i< s1->num_reg ; i++){ if(s1->regions[i]->type != s2->regions[i]->type){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different type of region"); + XBT_INFO("Different type of region"); errors++; - }else{ - return 1; - } } switch(s1->regions[i]->type){ case 0: if(s1->regions[i]->size != s2->regions[i]->size){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); - errors++; - }else{ - return 1; - } + XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); + errors++; } if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); - errors++; - }else{ - return 1; - } + XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + errors++; } if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data, s_heap, r_heap)){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different heap (mmalloc_compare)"); - errors++; - }else{ - return 1; - } + XBT_INFO("Different heap (mmalloc_compare)"); + errors++; } break; case 1 : if(s1->regions[i]->size != s2->regions[i]->size){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); - errors++; - }else{ - return 1; - } + XBT_INFO("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); + errors++; } if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); - errors++; - }else{ - return 1; - } + XBT_INFO("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + errors++; } - if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different memcmp for data in libsimgrid"); - errors++; - }else{ - return 1; - } + if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ + XBT_INFO("Different memcmp for data in libsimgrid"); + errors++; } break; case 2 : if(s1->regions[i]->size != s2->regions[i]->size){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); - errors++; - }else{ - return 1; - } + XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); + errors++; } if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); - errors++; - }else{ - return 1; - } + XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + errors++; } - if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different memcmp for data in libsimgrid"); - errors++; - }else{ - return 1; - } + if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ + XBT_INFO("Different memcmp for data in program"); + errors++; } break; default: @@ -270,28 +242,29 @@ int reached(xbt_state_t st){ //xbt_dict_t current_rdv_points = SIMIX_get_rdv_points(); xbt_dynar_foreach(reached_pairs, cursor, pair_test){ - XBT_DEBUG("Pair reached #%u", cursor+1); + XBT_INFO("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, prop_ato) == 0){ - //XBT_DEBUG("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points)); + //XBT_INFO("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points)); //if(xbt_dict_length(pair_test->rdv_points) == xbt_dict_length(current_rdv_points)){ //if(rdv_points_compare(pair_test->rdv_points, current_rdv_points) == 0){ if(snapshot_compare(pair_test->system_state, sn, std_heap, raw_heap) == 0){ - MC_free_snapshot(sn); - xbt_dynar_reset(prop_ato); - xbt_free(prop_ato); - MC_UNSET_RAW_MEM; - return 1; - } - /* } + + MC_free_snapshot(sn); + xbt_dynar_reset(prop_ato); + xbt_free(prop_ato); + MC_UNSET_RAW_MEM; + return 1; + } + /* } }else{ - XBT_DEBUG("Different size of rdv points (%d - %d)",xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points) ); + XBT_INFO("Different size of rdv points (%d - %d)",xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points) ); }*/ }else{ - XBT_DEBUG("Different values of propositional symbols"); + XBT_INFO("Different values of propositional symbols"); } }else{ - XBT_DEBUG("Different automaton state"); + XBT_INFO("Different automaton state"); } } @@ -321,15 +294,15 @@ int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = cu rdv1 = (smx_rdv_t)data; rdv2 = xbt_dict_get_or_null(d2, rdv1->name); if(rdv2 == NULL){ - XBT_DEBUG("Rdv point unknown"); + XBT_INFO("Rdv point unknown"); return 1; }else{ if(xbt_fifo_size(rdv1->comm_fifo) != xbt_fifo_size(rdv2->comm_fifo)){ - XBT_DEBUG("Different total of actions in mailbox \"%s\" (%d - %d)", rdv1->name, xbt_fifo_size(rdv1->comm_fifo),xbt_fifo_size(rdv2->comm_fifo) ); + XBT_INFO("Different total of actions in mailbox \"%s\" (%d - %d)", rdv1->name, xbt_fifo_size(rdv1->comm_fifo),xbt_fifo_size(rdv2->comm_fifo) ); return 1; }else{ - XBT_DEBUG("Total of actions in mailbox \"%s\" : %d", rdv1->name, xbt_fifo_size(rdv1->comm_fifo)); + XBT_INFO("Total of actions in mailbox \"%s\" : %d", rdv1->name, xbt_fifo_size(rdv1->comm_fifo)); item1 = xbt_fifo_get_first_item(rdv1->comm_fifo); item2 = xbt_fifo_get_first_item(rdv2->comm_fifo); @@ -339,17 +312,17 @@ int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = cu action2 = (smx_action_t) xbt_fifo_get_item_content(item2); if(action1->type != action2->type){ - XBT_DEBUG("Different type of action"); + XBT_INFO("Different type of action"); return 1; } if(action1->state != action2->state){ - XBT_DEBUG("Different state of action"); + XBT_INFO("Different state of action"); return 1; } if(xbt_fifo_size(action1->simcalls) != xbt_fifo_size(action2->simcalls)){ - XBT_DEBUG("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls)); + XBT_INFO("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls)); return 1; }else{ @@ -362,11 +335,11 @@ int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = cu req2 = (smx_simcall_t) xbt_fifo_get_item_content(item_req2); if(req1->call != req2->call){ - XBT_DEBUG("Different simcall call in simcalls of action (%d - %d)", (int)req1->call, (int)req2->call); + XBT_INFO("Different simcall call in simcalls of action (%d - %d)", (int)req1->call, (int)req2->call); return 1; } if(req1->issuer->pid != req2->issuer->pid){ - XBT_DEBUG("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid); + XBT_INFO("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid); return 1; } @@ -386,7 +359,7 @@ int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = cu case 2: /* comm */ if(action1->comm.type != action2->comm.type) return 1; - //XBT_DEBUG("Type of comm : %d", action1->comm.type); + //XBT_INFO("Type of comm : %d", action1->comm.type); switch(action1->comm.type){ case 0: /* SEND */ @@ -472,6 +445,7 @@ void set_pair_reached(xbt_state_t st){ mc_pair_reached_t pair = NULL; pair = xbt_new0(s_mc_pair_reached_t, 1); + pair->nb = xbt_dynar_length(reached_pairs) + 1; pair->automaton_state = st; pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); pair->system_state = xbt_new0(s_mc_snapshot_t, 1); @@ -506,9 +480,9 @@ void set_pair_reached(xbt_state_t st){ smx_action_t a = xbt_new0(s_smx_action_t, 1); memcpy(a, action, sizeof(s_smx_action_t)); xbt_fifo_push(new_rdv->comm_fifo, a); - XBT_DEBUG("New action (type = %d, state = %d) in mailbox \"%s\"", action->type, action->state, key); + XBT_INFO("New action (type = %d, state = %d) in mailbox \"%s\"", action->type, action->state, key); if(action->type==2) - XBT_DEBUG("Type of communication : %d, Ref count = %d", action->comm.type, action->comm.refcount); + XBT_INFO("Type of communication : %d, Ref count = %d", action->comm.type, action->comm.refcount); } //new_rdv->comm_fifo = xbt_fifo_copy(((smx_rdv_t)data)->comm_fifo); xbt_dict_set(pair->rdv_points, new_rdv->name, new_rdv, NULL); @@ -577,13 +551,13 @@ int reached_hash(xbt_state_t st){ MC_UNSET_RAW_MEM; return 1; }else{ - XBT_DEBUG("Different snapshot"); + XBT_INFO("Different snapshot"); } }else{ - XBT_DEBUG("Different values of propositional symbols"); + XBT_INFO("Different values of propositional symbols"); } }else{ - XBT_DEBUG("Different automaton state"); + XBT_INFO("Different automaton state"); } region_diff = 0; @@ -683,16 +657,16 @@ int visited(xbt_state_t st, int sc){ return 1; }else{ - XBT_DEBUG("Different snapshot"); + XBT_INFO("Different snapshot"); } }else{ - XBT_DEBUG("Different values of propositional symbols"); + XBT_INFO("Different values of propositional symbols"); } }else{ - XBT_DEBUG("Different automaton state"); + XBT_INFO("Different automaton state"); } }else{ - XBT_DEBUG("Different value of search_cycle"); + XBT_INFO("Different value of search_cycle"); } } @@ -763,16 +737,16 @@ int visited_hash(xbt_state_t st, int sc){ MC_UNSET_RAW_MEM; return 1; }else{ - //XBT_DEBUG("Different snapshot"); + //XBT_INFO("Different snapshot"); } }else{ - //XBT_DEBUG("Different values of propositional symbols"); + //XBT_INFO("Different values of propositional symbols"); } }else{ - //XBT_DEBUG("Different automaton state"); + //XBT_INFO("Different automaton state"); } }else{ - //XBT_DEBUG("Different value of search_cycle"); + //XBT_INFO("Different value of search_cycle"); } region_diff = 0; @@ -926,12 +900,9 @@ mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){ void MC_ddfs_init(void){ - XBT_DEBUG("**************************************************"); - XBT_DEBUG("Double-DFS init"); - XBT_DEBUG("**************************************************"); - - XBT_DEBUG("Std heap : %p", std_heap); - XBT_DEBUG("Raw heap : %p", raw_heap); + XBT_INFO("**************************************************"); + XBT_INFO("Double-DFS init"); + XBT_INFO("**************************************************"); mc_pair_stateless_t mc_initial_pair = NULL; mc_state_t initial_graph_state = NULL; @@ -1020,8 +991,8 @@ void MC_ddfs(int search_cycle){ automaton->current_state = current_pair->automaton_state; - XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), 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)); + XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle); + XBT_INFO("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++; @@ -1038,28 +1009,27 @@ void MC_ddfs(int search_cycle){ mc_pair_stateless_t next_pair = NULL; mc_pair_stateless_t pair_succ; - + if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){ //set_pair_visited(current_pair->automaton_state, search_cycle); set_pair_visited_hash(current_pair->automaton_state, search_cycle); - //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs)); - XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash)); + //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs)); + XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash)); if(current_pair->requests > 0){ while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ /* 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_free(req_str); - } + + req_str = MC_request_to_string(req, value); + XBT_INFO("Execute: %s", req_str); + xbt_free(req_str); MC_state_set_executed_request(current_pair->graph_state, req, value); - + /* Answer the request */ SIMIX_simcall_pre(req, value); @@ -1124,7 +1094,7 @@ void MC_ddfs(int search_cycle){ if(reached(pair_succ->automaton_state)){ //if(reached_hash(pair_succ->automaton_state)){ - XBT_DEBUG("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_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)); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); @@ -1137,13 +1107,13 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); set_pair_reached(pair_succ->automaton_state); //set_pair_reached_hash(pair_succ->automaton_state); - XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); - //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); + XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness, pair_succ); @@ -1166,7 +1136,7 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_DEBUG("Next pair already visited ! "); + XBT_INFO("Next pair already visited ! "); } @@ -1176,15 +1146,15 @@ void MC_ddfs(int search_cycle){ if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); set_pair_reached(pair_succ->automaton_state); //set_pair_reached_hash(pair_succ->automaton_state); search_cycle = 1; - XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); - //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); + XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); } @@ -1199,7 +1169,7 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_DEBUG("Next pair already visited ! "); + XBT_INFO("Next pair already visited ! "); } @@ -1214,7 +1184,7 @@ void MC_ddfs(int search_cycle){ } if(MC_state_interleave_size(current_pair->graph_state) > 0){ - XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness)); + XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness)); MC_replay_liveness(mc_stack_liveness, 0); } } @@ -1272,8 +1242,8 @@ void MC_ddfs(int search_cycle){ if(reached(pair_succ->automaton_state)){ //if(reached_hash(pair_succ->automaton_state)){ - XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1); - + XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1); + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); @@ -1285,13 +1255,13 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_DEBUG("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + XBT_INFO("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); set_pair_reached(pair_succ->automaton_state); //set_pair_reached_hash(pair_succ->automaton_state); - XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); - //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); + XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness, pair_succ); @@ -1314,7 +1284,7 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_DEBUG("Next pair already visited ! "); + XBT_INFO("Next pair already visited ! "); } } @@ -1329,8 +1299,8 @@ void MC_ddfs(int search_cycle){ search_cycle = 1; - XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); - //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); + XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); } @@ -1345,7 +1315,7 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_DEBUG("Next pair already visited ! "); + XBT_INFO("Next pair already visited ! "); } @@ -1362,14 +1332,14 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_DEBUG("Max depth reached"); + XBT_INFO("Max depth reached"); } if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){ - XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) ); + XBT_INFO("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) ); }else{ - XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) ); + XBT_INFO("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) ); }