1 /* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */
3 /* This program is free software; you can redistribute it and/or modify it
4 * under the terms of the license (GNU LGPL) which comes with this package. */
6 #include "mc_private.h"
10 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
11 "Logging specific to algorithms for liveness properties verification");
13 xbt_dynar_t reached_pairs;
14 xbt_dynar_t reached_pairs_hash;
15 xbt_dynar_t visited_pairs;
16 xbt_dynar_t visited_pairs_hash;
17 xbt_dynar_t successors;
19 xbt_dynar_t hosts_table;
22 /* fast implementation of djb2 algorithm */
23 unsigned int hash_region(char *str, int str_len){
26 register unsigned int hash = 5381;
30 hash = ((hash << 5) + hash) + c; /* hash * 33 + c */
37 int create_dump(int pair)
39 // Try to enable core dumps
40 struct rlimit core_limit;
41 core_limit.rlim_cur = RLIM_INFINITY;
42 core_limit.rlim_max = RLIM_INFINITY;
44 if(setrlimit(RLIMIT_CORE, &core_limit) < 0)
45 fprintf(stderr, "setrlimit: %s\nWarning: core dumps may be truncated or non-existant\n", strerror(errno));
50 // We are the child process -- run the actual program
55 // An error occurred, shouldn't happen
60 // We are the parent process -- wait for the child process to exit
63 if(WIFSIGNALED(status) && WCOREDUMP(status)){
64 char *core_name = malloc(20);
65 sprintf(core_name,"core_%d", pair);
66 rename("core", core_name);
74 int reached(xbt_state_t st){
76 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
78 if(xbt_dynar_is_empty(reached_pairs)){
86 mc_pair_reached_t new_pair = NULL;
87 new_pair = xbt_new0(s_mc_pair_reached_t, 1);
88 new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
89 new_pair->automaton_state = st;
90 new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
91 new_pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
92 MC_take_snapshot_liveness(new_pair->system_state);
94 /* Get values of propositional symbols */
97 unsigned int cursor = 0;
98 xbt_propositional_symbol_t ps = NULL;
99 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
100 f = (int_f_void_t)ps->function;
102 xbt_dynar_push_as(new_pair->prop_ato, int, res);
106 mc_pair_reached_t pair_test = NULL;
108 xbt_dynar_foreach(reached_pairs, cursor, pair_test){
109 XBT_INFO("Pair reached #%d", pair_test->nb);
110 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
111 if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
112 if(snapshot_compare(pair_test->system_state, new_pair->system_state) == 0){
122 XBT_INFO("Different values of propositional symbols");
125 XBT_INFO("Different automaton state");
129 /* New pair reached */
130 xbt_dynar_push(reached_pairs, &new_pair);
132 create_dump(xbt_dynar_length(reached_pairs));
147 void set_pair_reached(xbt_state_t st){
149 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
153 mc_pair_reached_t pair = NULL;
154 pair = xbt_new0(s_mc_pair_reached_t, 1);
155 pair->nb = xbt_dynar_length(reached_pairs) + 1;
156 pair->automaton_state = st;
157 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
158 pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
159 MC_take_snapshot_liveness(pair->system_state);
161 /* Get values of propositional symbols */
162 unsigned int cursor = 0;
163 xbt_propositional_symbol_t ps = NULL;
167 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
168 f = (int_f_void_t)ps->function;
170 xbt_dynar_push_as(pair->prop_ato, int, res);
173 xbt_dynar_push(reached_pairs, &pair);
185 int reached_hash(xbt_state_t st){
187 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
189 if(xbt_dynar_is_empty(reached_pairs_hash)){
197 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
198 MC_take_snapshot_liveness(sn);
201 unsigned int hash_regions[sn->num_reg];
202 for(j=0; j<sn->num_reg; j++){
203 hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
207 /* Get values of propositional symbols */
208 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
209 unsigned int cursor = 0;
210 xbt_propositional_symbol_t ps = NULL;
214 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
215 f = (int_f_void_t)ps->function;
217 xbt_dynar_push_as(prop_ato, int, res);
220 mc_pair_reached_hash_t pair_test = NULL;
226 xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
228 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
229 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
230 for(j=0 ; j< sn->num_reg ; j++){
231 if(hash_regions[j] != pair_test->hash_regions[j]){
235 if(region_diff == 0){
236 MC_free_snapshot(sn);
237 xbt_dynar_reset(prop_ato);
248 XBT_INFO("Different snapshot");
251 XBT_INFO("Different values of propositional symbols");
254 XBT_INFO("Different automaton state");
260 MC_free_snapshot(sn);
261 xbt_dynar_reset(prop_ato);
275 void set_pair_reached_hash(xbt_state_t st){
277 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
281 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
282 MC_take_snapshot_liveness(sn);
284 mc_pair_reached_hash_t pair = NULL;
285 pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
286 pair->automaton_state = st;
287 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
288 pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
292 for(i=0 ; i< sn->num_reg ; i++){
293 pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
296 /* Get values of propositional symbols */
297 unsigned int cursor = 0;
298 xbt_propositional_symbol_t ps = NULL;
302 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
303 f = (int_f_void_t)ps->function;
305 xbt_dynar_push_as(pair->prop_ato, int, res);
308 xbt_dynar_push(reached_pairs_hash, &pair);
310 MC_free_snapshot(sn);
322 int visited(xbt_state_t st, int sc){
324 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
326 if(xbt_dynar_is_empty(visited_pairs)){
334 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
335 MC_take_snapshot_liveness(sn);
337 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
339 /* Get values of propositional symbols */
340 unsigned int cursor = 0;
341 xbt_propositional_symbol_t ps = NULL;
345 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
346 f = (int_f_void_t)ps->function;
348 xbt_dynar_push_as(prop_ato, int, res);
352 mc_pair_visited_t pair_test = NULL;
354 xbt_dynar_foreach(visited_pairs, cursor, pair_test){
355 if(pair_test->search_cycle == sc) {
356 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
357 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
358 if(snapshot_compare(pair_test->system_state, sn) == 0){
360 MC_free_snapshot(sn);
361 xbt_dynar_reset(prop_ato);
373 XBT_INFO("Different snapshot");
376 XBT_INFO("Different values of propositional symbols");
379 XBT_INFO("Different automaton state");
382 XBT_INFO("Different value of search_cycle");
387 MC_free_snapshot(sn);
388 xbt_dynar_reset(prop_ato);
403 int visited_hash(xbt_state_t st, int sc){
405 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
407 if(xbt_dynar_is_empty(visited_pairs_hash)){
415 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
416 MC_take_snapshot_liveness(sn);
419 unsigned int hash_regions[sn->num_reg];
420 for(j=0; j<sn->num_reg; j++){
421 hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
425 /* Get values of propositional symbols */
426 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
427 unsigned int cursor = 0;
428 xbt_propositional_symbol_t ps = NULL;
432 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
433 f = (int_f_void_t)ps->function;
435 xbt_dynar_push_as(prop_ato, int, res);
438 mc_pair_visited_hash_t pair_test = NULL;
443 xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
445 if(pair_test->search_cycle == sc) {
446 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
447 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
448 for(j=0 ; j< sn->num_reg ; j++){
449 if(hash_regions[j] != pair_test->hash_regions[j]){
453 if(region_diff == 0){
454 MC_free_snapshot(sn);
455 xbt_dynar_reset(prop_ato);
466 //XBT_INFO("Different snapshot");
469 //XBT_INFO("Different values of propositional symbols");
472 //XBT_INFO("Different automaton state");
475 //XBT_INFO("Different value of search_cycle");
481 MC_free_snapshot(sn);
482 xbt_dynar_reset(prop_ato);
496 void set_pair_visited_hash(xbt_state_t st, int sc){
498 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
502 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
503 MC_take_snapshot_liveness(sn);
505 mc_pair_visited_hash_t pair = NULL;
506 pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
507 pair->automaton_state = st;
508 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
509 pair->search_cycle = sc;
510 pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
514 for(i=0 ; i< sn->num_reg ; i++){
515 pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
518 /* Get values of propositional symbols */
519 unsigned int cursor = 0;
520 xbt_propositional_symbol_t ps = NULL;
524 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
525 f = (int_f_void_t)ps->function;
527 xbt_dynar_push_as(pair->prop_ato, int, res);
530 xbt_dynar_push(visited_pairs_hash, &pair);
532 MC_free_snapshot(sn);
543 void set_pair_visited(xbt_state_t st, int sc){
545 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
549 mc_pair_visited_t pair = NULL;
550 pair = xbt_new0(s_mc_pair_visited_t, 1);
551 pair->automaton_state = st;
552 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
553 pair->search_cycle = sc;
554 pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
555 MC_take_snapshot_liveness(pair->system_state);
558 /* Get values of propositional symbols */
559 unsigned int cursor = 0;
560 xbt_propositional_symbol_t ps = NULL;
564 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
565 f = (int_f_void_t)ps->function;
567 xbt_dynar_push_as(pair->prop_ato, int, res);
570 xbt_dynar_push(visited_pairs, &pair);
581 void MC_pair_delete(mc_pair_t pair){
582 xbt_free(pair->graph_state->proc_status);
583 xbt_free(pair->graph_state);
589 int MC_automaton_evaluate_label(xbt_exp_label_t l){
593 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
594 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
595 return (left_res || right_res);
598 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
599 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
600 return (left_res && right_res);
603 int res = MC_automaton_evaluate_label(l->u.exp_not);
607 unsigned int cursor = 0;
608 xbt_propositional_symbol_t p = NULL;
610 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
611 if(strcmp(p->pred, l->u.predicat) == 0){
612 f = (int_f_void_t)p->function;
627 /********************* Double-DFS stateless *******************/
629 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
630 xbt_free(pair->graph_state->proc_status);
631 xbt_free(pair->graph_state);
635 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
636 mc_pair_stateless_t p = NULL;
637 p = xbt_new0(s_mc_pair_stateless_t, 1);
638 p->automaton_state = st;
641 mc_stats_pair->expanded_pairs++;
645 void MC_ddfs_init(void){
647 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
649 XBT_INFO("**************************************************");
650 XBT_INFO("Double-DFS init");
651 XBT_INFO("**************************************************");
653 mc_pair_stateless_t mc_initial_pair = NULL;
654 mc_state_t initial_graph_state = NULL;
655 smx_process_t process;
658 MC_wait_for_requests();
662 initial_graph_state = MC_state_pair_new();
663 xbt_swag_foreach(process, simix_global->process_list){
664 if(MC_process_is_enabled(process)){
665 MC_state_interleave_process(initial_graph_state, process);
669 reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
670 //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
671 //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
672 //visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
673 successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
675 /* Save the initial state */
676 initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
677 MC_take_snapshot_liveness(initial_snapshot_liveness);
681 unsigned int cursor = 0;
684 xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
685 if(state->type == -1){
688 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
689 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
693 MC_restore_snapshot(initial_snapshot_liveness);
700 if(state->type == 2){
703 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
704 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
707 set_pair_reached(state);
708 //set_pair_reached_hash(state);
711 MC_restore_snapshot(initial_snapshot_liveness);
730 void MC_ddfs(int search_cycle){
732 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
734 smx_process_t process;
735 mc_pair_stateless_t current_pair = NULL;
737 if(xbt_fifo_size(mc_stack_liveness) == 0)
741 /* Get current pair */
742 current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
744 /* Update current state in buchi automaton */
745 _mc_property_automaton->current_state = current_pair->automaton_state;
748 XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
750 mc_stats_pair->visited_pairs++;
755 mc_state_t next_graph_state = NULL;
756 smx_simcall_t req = NULL;
759 xbt_transition_t transition_succ;
760 unsigned int cursor = 0;
763 mc_pair_stateless_t next_pair = NULL;
764 mc_pair_stateless_t pair_succ;
766 if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
768 //set_pair_visited(current_pair->automaton_state, search_cycle);
769 //set_pair_visited_hash(current_pair->automaton_state, search_cycle);
771 //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
772 //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
774 if(current_pair->requests > 0){
776 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
778 /* Debug information */
780 req_str = MC_request_to_string(req, value);
781 XBT_INFO("Execute: %s", req_str);
784 MC_state_set_executed_request(current_pair->graph_state, req, value);
786 /* Answer the request */
787 SIMIX_simcall_pre(req, value);
789 /* Wait for requests (schedules processes) */
790 MC_wait_for_requests();
795 /* Create the new expanded graph_state */
796 next_graph_state = MC_state_pair_new();
798 /* Get enabled process and insert it in the interleave set of the next graph_state */
799 xbt_swag_foreach(process, simix_global->process_list){
800 if(MC_process_is_enabled(process)){
801 MC_state_interleave_process(next_graph_state, process);
805 xbt_dynar_reset(successors);
811 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
813 res = MC_automaton_evaluate_label(transition_succ->label);
815 if(res == 1){ // enabled transition in automaton
817 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
818 xbt_dynar_push(successors, &next_pair);
826 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
828 res = MC_automaton_evaluate_label(transition_succ->label);
830 if(res == 2){ // true transition in automaton
832 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
833 xbt_dynar_push(successors, &next_pair);
841 xbt_dynar_foreach(successors, cursor, pair_succ){
843 if(search_cycle == 1){
845 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
847 if(reached(pair_succ->automaton_state)){
848 //if(reached_hash(pair_succ->automaton_state)){
850 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));
852 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
853 XBT_INFO("| ACCEPTANCE CYCLE |");
854 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
855 XBT_INFO("Counter-example that violates formula :");
856 MC_show_stack_liveness(mc_stack_liveness);
857 MC_dump_stack_liveness(mc_stack_liveness);
858 MC_print_statistics_pairs(mc_stats_pair);
863 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);
865 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
866 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
869 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
872 MC_ddfs(search_cycle);
878 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
879 //if(!visited(pair_succ->automaton_state, search_cycle)){
882 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
885 MC_ddfs(search_cycle);
889 XBT_INFO("Next pair already visited ! ");
897 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
899 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);
901 set_pair_reached(pair_succ->automaton_state);
902 //set_pair_reached_hash(pair_succ->automaton_state);
906 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
907 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
911 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
912 //if(!visited(pair_succ->automaton_state, search_cycle)){
915 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
918 MC_ddfs(search_cycle);
922 XBT_INFO("Next pair already visited ! ");
929 /* Restore system before checking others successors */
930 if(cursor != (xbt_dynar_length(successors) - 1))
931 MC_replay_liveness(mc_stack_liveness, 1);
936 if(MC_state_interleave_size(current_pair->graph_state) > 0){
937 XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
938 MC_replay_liveness(mc_stack_liveness, 0);
943 }else{ /*No request to execute, search evolution in Büchi automaton */
947 /* Create the new expanded graph_state */
948 next_graph_state = MC_state_pair_new();
950 xbt_dynar_reset(successors);
956 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
958 res = MC_automaton_evaluate_label(transition_succ->label);
960 if(res == 1){ // enabled transition in automaton
962 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
963 xbt_dynar_push(successors, &next_pair);
971 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
973 res = MC_automaton_evaluate_label(transition_succ->label);
975 if(res == 2){ // true transition in automaton
977 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
978 xbt_dynar_push(successors, &next_pair);
986 xbt_dynar_foreach(successors, cursor, pair_succ){
988 if(search_cycle == 1){
990 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
992 if(reached(pair_succ->automaton_state)){
993 //if(reached_hash(pair_succ->automaton_state)){
995 XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
997 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
998 XBT_INFO("| ACCEPTANCE CYCLE |");
999 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1000 XBT_INFO("Counter-example that violates formula :");
1001 MC_show_stack_liveness(mc_stack_liveness);
1002 MC_dump_stack_liveness(mc_stack_liveness);
1003 MC_print_statistics_pairs(mc_stats_pair);
1008 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);
1010 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1011 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1014 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1017 MC_ddfs(search_cycle);
1023 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1024 //if(!visited(pair_succ->automaton_state, search_cycle)){
1027 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1030 MC_ddfs(search_cycle);
1034 XBT_INFO("Next pair already visited ! ");
1042 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1044 set_pair_reached(pair_succ->automaton_state);
1045 //set_pair_reached_hash(pair_succ->automaton_state);
1049 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1050 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1054 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1055 //if(!visited(pair_succ->automaton_state, search_cycle)){
1058 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1061 MC_ddfs(search_cycle);
1065 XBT_INFO("Next pair already visited ! ");
1071 /* Restore system before checking others successors */
1072 if(cursor != xbt_dynar_length(successors) - 1)
1073 MC_replay_liveness(mc_stack_liveness, 1);
1082 XBT_INFO("Max depth reached");
1086 if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
1087 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) );
1089 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) );
1094 xbt_fifo_shift(mc_stack_liveness);
1095 if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
1096 xbt_dynar_pop(reached_pairs, NULL);
1097 //xbt_dynar_pop(reached_pairs_hash, NULL);