4 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
5 "Logging specific to algorithms for liveness properties verification");
7 xbt_dynar_t reached_pairs;
8 xbt_dynar_t reached_pairs_hash;
9 xbt_dynar_t visited_pairs;
10 xbt_dynar_t visited_pairs_hash;
11 xbt_dynar_t successors;
13 /* fast implementation of djb2 algorithm */
14 unsigned int hash_region(char *str, int str_len){
17 register unsigned int hash = 5381;
21 hash = ((hash << 5) + hash) + c; /* hash * 33 + c */
28 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
31 if(s1->num_reg != s2->num_reg){
32 //XBT_DEBUG("Different num_reg (s1 = %d, s2 = %d)", s1->num_reg, s2->num_reg);
38 for(i=0 ; i< s1->num_reg ; i++){
40 if(s1->regions[i]->type != s2->regions[i]->type){
41 //XBT_DEBUG("Different type of region");
45 switch(s1->regions[i]->type){
47 if(s1->regions[i]->size != s2->regions[i]->size){
48 //XBT_DEBUG("Different size of heap (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
51 if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
52 //XBT_DEBUG("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
55 if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){
56 //XBT_DEBUG("Different heap (mmalloc_compare)");
61 if(s1->regions[i]->size != s2->regions[i]->size){
62 //XBT_DEBUG("Different size of libsimgrid (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
65 if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
66 //XBT_DEBUG("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
69 if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
70 //XBT_DEBUG("Different memcmp for data in libsimgrid");
75 if(s1->regions[i]->size != s2->regions[i]->size){
76 //XBT_DEBUG("Different size of program (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
79 if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
80 //XBT_DEBUG("Different start addr of program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
83 if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
84 //XBT_DEBUG("Different memcmp for data in program");
89 if(s1->regions[i]->size != s2->regions[i]->size){
90 //XBT_DEBUG("Different size of stack (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
93 if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
94 //XBT_DEBUG("Different start addr of stack (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
97 if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
98 //XBT_DEBUG("Different memcmp for data in stack");
109 int reached(xbt_state_t st){
112 if(xbt_dynar_is_empty(reached_pairs)){
120 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
121 MC_take_snapshot_liveness(sn);
123 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
127 /* Get values of propositional symbols */
128 unsigned int cursor = 0;
129 xbt_propositional_symbol_t ps = NULL;
130 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
133 xbt_dynar_push_as(prop_ato, int, res);
137 mc_pair_reached_t pair_test = NULL;
140 xbt_dynar_foreach(reached_pairs, cursor, pair_test){
141 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
142 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
143 if(snapshot_compare(pair_test->system_state, sn) == 0){
144 MC_free_snapshot(sn);
145 xbt_dynar_reset(prop_ato);
154 MC_free_snapshot(sn);
155 xbt_dynar_reset(prop_ato);
163 void set_pair_reached(xbt_state_t st){
168 mc_pair_reached_t pair = NULL;
169 pair = xbt_new0(s_mc_pair_reached_t, 1);
170 pair->automaton_state = st;
171 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
172 pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
173 MC_take_snapshot_liveness(pair->system_state);
175 /* Get values of propositional symbols */
176 unsigned int cursor = 0;
177 xbt_propositional_symbol_t ps = NULL;
181 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
184 xbt_dynar_push_as(pair->prop_ato, int, res);
187 xbt_dynar_push(reached_pairs, &pair);
193 int reached_hash(xbt_state_t st){
196 if(xbt_dynar_is_empty(reached_pairs_hash)){
204 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
205 MC_take_snapshot_liveness(sn);
208 unsigned int hash_regions[sn->num_reg];
209 for(j=0; j<sn->num_reg; j++){
210 hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
214 /* Get values of propositional symbols */
215 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
216 unsigned int cursor = 0;
217 xbt_propositional_symbol_t ps = NULL;
221 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
224 xbt_dynar_push_as(prop_ato, int, res);
227 mc_pair_reached_hash_t pair_test = NULL;
233 xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
235 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
236 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
237 for(j=0 ; j< sn->num_reg ; j++){
238 if(hash_regions[j] != pair_test->hash_regions[j]){
242 if(region_diff == 0){
243 MC_free_snapshot(sn);
244 xbt_dynar_reset(prop_ato);
256 MC_free_snapshot(sn);
257 xbt_dynar_reset(prop_ato);
265 void set_pair_reached_hash(xbt_state_t st){
269 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
270 MC_take_snapshot_liveness(sn);
272 mc_pair_reached_hash_t pair = NULL;
273 pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
274 pair->automaton_state = st;
275 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
276 pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
280 for(i=0 ; i< sn->num_reg ; i++){
281 pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
284 /* Get values of propositional symbols */
285 unsigned int cursor = 0;
286 xbt_propositional_symbol_t ps = NULL;
290 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
293 xbt_dynar_push_as(pair->prop_ato, int, res);
296 xbt_dynar_push(reached_pairs_hash, &pair);
298 MC_free_snapshot(sn);
305 int visited(xbt_state_t st, int sc){
308 if(xbt_dynar_is_empty(visited_pairs)){
316 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
317 MC_take_snapshot_liveness(sn);
319 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
321 /* Get values of propositional symbols */
322 unsigned int cursor = 0;
323 xbt_propositional_symbol_t ps = NULL;
327 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
330 xbt_dynar_push_as(prop_ato, int, res);
334 mc_pair_visited_t pair_test = NULL;
336 xbt_dynar_foreach(visited_pairs, cursor, pair_test){
337 if(pair_test->search_cycle == sc) {
338 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
339 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
340 if(snapshot_compare(pair_test->system_state, sn) == 0){
342 MC_free_snapshot(sn);
343 xbt_dynar_reset(prop_ato);
356 MC_free_snapshot(sn);
357 xbt_dynar_reset(prop_ato);
366 int visited_hash(xbt_state_t st, int sc){
369 if(xbt_dynar_is_empty(visited_pairs_hash)){
377 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
378 MC_take_snapshot_liveness(sn);
381 unsigned int hash_regions[sn->num_reg];
382 for(j=0; j<sn->num_reg; j++){
383 hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
387 /* Get values of propositional symbols */
388 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
389 unsigned int cursor = 0;
390 xbt_propositional_symbol_t ps = NULL;
394 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
397 xbt_dynar_push_as(prop_ato, int, res);
400 mc_pair_visited_hash_t pair_test = NULL;
405 xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
407 if(pair_test->search_cycle == sc) {
408 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
409 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
410 for(j=0 ; j< sn->num_reg ; j++){
411 if(hash_regions[j] != pair_test->hash_regions[j]){
415 if(region_diff == 0){
416 MC_free_snapshot(sn);
417 xbt_dynar_reset(prop_ato);
429 MC_free_snapshot(sn);
430 xbt_dynar_reset(prop_ato);
438 void set_pair_visited_hash(xbt_state_t st, int sc){
442 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
443 MC_take_snapshot_liveness(sn);
445 mc_pair_visited_hash_t pair = NULL;
446 pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
447 pair->automaton_state = st;
448 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
449 pair->search_cycle = sc;
450 pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
454 for(i=0 ; i< sn->num_reg ; i++){
455 pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
458 /* Get values of propositional symbols */
459 unsigned int cursor = 0;
460 xbt_propositional_symbol_t ps = NULL;
464 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
467 xbt_dynar_push_as(pair->prop_ato, int, res);
470 xbt_dynar_push(visited_pairs_hash, &pair);
472 MC_free_snapshot(sn);
478 void set_pair_visited(xbt_state_t st, int sc){
483 mc_pair_visited_t pair = NULL;
484 pair = xbt_new0(s_mc_pair_visited_t, 1);
485 pair->automaton_state = st;
486 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
487 pair->search_cycle = sc;
488 pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
489 MC_take_snapshot_liveness(pair->system_state);
492 /* Get values of propositional symbols */
493 unsigned int cursor = 0;
494 xbt_propositional_symbol_t ps = NULL;
498 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
501 xbt_dynar_push_as(pair->prop_ato, int, res);
504 xbt_dynar_push(visited_pairs, &pair);
511 void MC_pair_delete(mc_pair_t pair){
512 xbt_free(pair->graph_state->proc_status);
513 xbt_free(pair->graph_state);
519 int MC_automaton_evaluate_label(xbt_exp_label_t l){
523 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
524 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
525 return (left_res || right_res);
529 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
530 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
531 return (left_res && right_res);
535 int res = MC_automaton_evaluate_label(l->u.exp_not);
540 unsigned int cursor = 0;
541 xbt_propositional_symbol_t p = NULL;
543 xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){
544 if(strcmp(p->pred, l->u.predicat) == 0){
565 /********************* Double-DFS stateless *******************/
567 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
568 xbt_free(pair->graph_state->proc_status);
569 xbt_free(pair->graph_state);
573 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
574 mc_pair_stateless_t p = NULL;
575 p = xbt_new0(s_mc_pair_stateless_t, 1);
576 p->automaton_state = st;
579 mc_stats_pair->expanded_pairs++;
583 void MC_ddfs_stateless_init(){
585 XBT_DEBUG("**************************************************");
586 XBT_DEBUG("Double-DFS stateless init");
587 XBT_DEBUG("**************************************************");
589 mc_pair_stateless_t mc_initial_pair = NULL;
590 mc_state_t initial_graph_state = NULL;
591 smx_process_t process;
593 MC_wait_for_requests();
597 initial_graph_state = MC_state_pair_new();
598 xbt_swag_foreach(process, simix_global->process_list){
599 if(MC_process_is_enabled(process)){
600 MC_state_interleave_process(initial_graph_state, process);
604 //reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
605 reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
606 //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
607 visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
608 successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
610 /* Save the initial state */
611 initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
612 MC_take_snapshot_to_restore_liveness(initial_snapshot_liveness);
616 unsigned int cursor = 0;
619 xbt_dynar_foreach(automaton->states, cursor, state){
620 if(state->type == -1){
623 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
624 xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
628 MC_restore_snapshot(initial_snapshot_liveness);
632 MC_ddfs_stateless(0);
635 if(state->type == 2){
638 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
639 xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
642 //set_pair_reached(state);
643 set_pair_reached_hash(state);
646 MC_restore_snapshot(initial_snapshot_liveness);
650 MC_ddfs_stateless(1);
659 void MC_ddfs_stateless(int search_cycle){
661 smx_process_t process;
662 mc_pair_stateless_t current_pair = NULL;
664 if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
668 /* Get current pair */
669 current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
671 /* Update current state in buchi automaton */
672 automaton->current_state = current_pair->automaton_state;
675 XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
676 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));
678 mc_stats_pair->visited_pairs++;
683 mc_state_t next_graph_state = NULL;
684 smx_req_t req = NULL;
687 xbt_transition_t transition_succ;
688 unsigned int cursor = 0;
691 mc_pair_stateless_t next_pair = NULL;
692 mc_pair_stateless_t pair_succ;
694 if(xbt_fifo_size(mc_stack_liveness_stateless) < MAX_DEPTH_LIVENESS){
696 //set_pair_visited(current_pair->automaton_state, search_cycle);
697 set_pair_visited_hash(current_pair->automaton_state, search_cycle);
699 //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
700 XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
702 if(current_pair->requests > 0){
704 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
706 /* Debug information */
707 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
708 req_str = MC_request_to_string(req, value);
709 XBT_DEBUG("Execute: %s", req_str);
713 MC_state_set_executed_request(current_pair->graph_state, req, value);
715 /* Answer the request */
716 SIMIX_request_pre(req, value);
718 /* Wait for requests (schedules processes) */
719 MC_wait_for_requests();
724 /* Create the new expanded graph_state */
725 next_graph_state = MC_state_pair_new();
727 /* Get enabled process and insert it in the interleave set of the next graph_state */
728 xbt_swag_foreach(process, simix_global->process_list){
729 if(MC_process_is_enabled(process)){
730 MC_state_interleave_process(next_graph_state, process);
734 xbt_dynar_reset(successors);
740 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
742 res = MC_automaton_evaluate_label(transition_succ->label);
744 if(res == 1){ // enabled transition in automaton
746 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
747 xbt_dynar_push(successors, &next_pair);
755 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
757 res = MC_automaton_evaluate_label(transition_succ->label);
759 if(res == 2){ // true transition in automaton
761 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
762 xbt_dynar_push(successors, &next_pair);
770 xbt_dynar_foreach(successors, cursor, pair_succ){
772 if(search_cycle == 1){
774 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
776 //if(reached(pair_succ->automaton_state)){
777 if(reached_hash(pair_succ->automaton_state)){
779 XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1, MC_state_interleave_size(pair_succ->graph_state));
781 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
782 XBT_INFO("| ACCEPTANCE CYCLE |");
783 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
784 XBT_INFO("Counter-example that violates formula :");
785 MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
786 MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
787 MC_print_statistics_pairs(mc_stats_pair);
792 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
794 //set_pair_reached(pair_succ->automaton_state);
795 set_pair_reached_hash(pair_succ->automaton_state);
797 //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
798 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
801 xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
804 MC_ddfs_stateless(search_cycle);
810 if(!visited_hash(pair_succ->automaton_state, search_cycle)){
811 //if(!visited(pair_succ->automaton_state, search_cycle)){
814 xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
817 MC_ddfs_stateless(search_cycle);
821 XBT_DEBUG("Next pair already visited ! ");
829 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
831 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
833 //set_pair_reached(pair_succ->automaton_state);
834 set_pair_reached_hash(pair_succ->automaton_state);
838 //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
839 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
843 if(!visited_hash(pair_succ->automaton_state, search_cycle)){
844 //if(!visited(pair_succ->automaton_state, search_cycle)){
847 xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
850 MC_ddfs_stateless(search_cycle);
854 XBT_DEBUG("Next pair already visited ! ");
861 /* Restore system before checking others successors */
862 if(cursor != (xbt_dynar_length(successors) - 1))
863 MC_replay_liveness(mc_stack_liveness_stateless, 1);
868 if(MC_state_interleave_size(current_pair->graph_state) > 0){
869 XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
870 MC_replay_liveness(mc_stack_liveness_stateless, 0);
875 }else{ /*No request to execute, search evolution in Büchi automaton */
879 /* Create the new expanded graph_state */
880 next_graph_state = MC_state_pair_new();
882 xbt_dynar_reset(successors);
888 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
890 res = MC_automaton_evaluate_label(transition_succ->label);
892 if(res == 1){ // enabled transition in automaton
894 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
895 xbt_dynar_push(successors, &next_pair);
903 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
905 res = MC_automaton_evaluate_label(transition_succ->label);
907 if(res == 2){ // true transition in automaton
909 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
910 xbt_dynar_push(successors, &next_pair);
918 xbt_dynar_foreach(successors, cursor, pair_succ){
920 if(search_cycle == 1){
922 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
924 //if(reached(pair_succ->automaton_state)){
925 if(reached_hash(pair_succ->automaton_state)){
927 XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1);
929 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
930 XBT_INFO("| ACCEPTANCE CYCLE |");
931 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
932 XBT_INFO("Counter-example that violates formula :");
933 MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
934 MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
935 MC_print_statistics_pairs(mc_stats_pair);
940 XBT_DEBUG("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
942 //set_pair_reached(pair_succ->automaton_state);
943 set_pair_reached_hash(pair_succ->automaton_state);
945 //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
946 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
949 xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
952 MC_ddfs_stateless(search_cycle);
958 if(!visited_hash(pair_succ->automaton_state, search_cycle)){
959 //if(!visited(pair_succ->automaton_state, search_cycle)){
962 xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
965 MC_ddfs_stateless(search_cycle);
969 XBT_DEBUG("Next pair already visited ! ");
977 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
979 //set_pair_reached(pair_succ->automaton_state);
980 set_pair_reached_hash(pair_succ->automaton_state);
984 //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
985 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
989 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
990 if(!visited(pair_succ->automaton_state, search_cycle)){
993 xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
996 MC_ddfs_stateless(search_cycle);
1000 XBT_DEBUG("Next pair already visited ! ");
1006 /* Restore system before checking others successors */
1007 if(cursor != xbt_dynar_length(successors) - 1)
1008 MC_replay_liveness(mc_stack_liveness_stateless, 1);
1017 XBT_DEBUG("Max depth reached");
1021 if(xbt_fifo_size(mc_stack_liveness_stateless) == MAX_DEPTH_LIVENESS ){
1022 XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness_stateless) );
1024 XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness_stateless) );
1029 xbt_fifo_shift(mc_stack_liveness_stateless);
1030 if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
1031 //xbt_dynar_pop(reached_pairs, NULL);
1032 xbt_dynar_pop(reached_pairs_hash, NULL);