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) || !compare){
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));
149 void set_pair_reached(xbt_state_t st){
151 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
155 mc_pair_reached_t pair = NULL;
156 pair = xbt_new0(s_mc_pair_reached_t, 1);
157 pair->nb = xbt_dynar_length(reached_pairs) + 1;
158 pair->automaton_state = st;
159 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
160 pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
161 MC_take_snapshot_liveness(pair->system_state);
163 /* Get values of propositional symbols */
164 unsigned int cursor = 0;
165 xbt_propositional_symbol_t ps = NULL;
169 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
170 f = (int_f_void_t)ps->function;
172 xbt_dynar_push_as(pair->prop_ato, int, res);
175 xbt_dynar_push(reached_pairs, &pair);
187 int reached_hash(xbt_state_t st){
189 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
191 if(xbt_dynar_is_empty(reached_pairs_hash)){
199 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
200 MC_take_snapshot_liveness(sn);
203 unsigned int hash_regions[sn->num_reg];
204 for(j=0; j<sn->num_reg; j++){
205 hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
209 /* Get values of propositional symbols */
210 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
211 unsigned int cursor = 0;
212 xbt_propositional_symbol_t ps = NULL;
216 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
217 f = (int_f_void_t)ps->function;
219 xbt_dynar_push_as(prop_ato, int, res);
222 mc_pair_reached_hash_t pair_test = NULL;
228 xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
230 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
231 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
232 for(j=0 ; j< sn->num_reg ; j++){
233 if(hash_regions[j] != pair_test->hash_regions[j]){
237 if(region_diff == 0){
238 MC_free_snapshot(sn);
239 xbt_dynar_reset(prop_ato);
250 XBT_INFO("Different snapshot");
253 XBT_INFO("Different values of propositional symbols");
256 XBT_INFO("Different automaton state");
262 MC_free_snapshot(sn);
263 xbt_dynar_reset(prop_ato);
277 void set_pair_reached_hash(xbt_state_t st){
279 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
283 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
284 MC_take_snapshot_liveness(sn);
286 mc_pair_reached_hash_t pair = NULL;
287 pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
288 pair->automaton_state = st;
289 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
290 pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
294 for(i=0 ; i< sn->num_reg ; i++){
295 pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
298 /* Get values of propositional symbols */
299 unsigned int cursor = 0;
300 xbt_propositional_symbol_t ps = NULL;
304 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
305 f = (int_f_void_t)ps->function;
307 xbt_dynar_push_as(pair->prop_ato, int, res);
310 xbt_dynar_push(reached_pairs_hash, &pair);
312 MC_free_snapshot(sn);
324 int visited(xbt_state_t st, int sc){
326 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
328 if(xbt_dynar_is_empty(visited_pairs)){
336 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
337 MC_take_snapshot_liveness(sn);
339 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
341 /* Get values of propositional symbols */
342 unsigned int cursor = 0;
343 xbt_propositional_symbol_t ps = NULL;
347 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
348 f = (int_f_void_t)ps->function;
350 xbt_dynar_push_as(prop_ato, int, res);
354 mc_pair_visited_t pair_test = NULL;
356 xbt_dynar_foreach(visited_pairs, cursor, pair_test){
357 if(pair_test->search_cycle == sc) {
358 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
359 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
360 if(snapshot_compare(pair_test->system_state, sn) == 0){
362 MC_free_snapshot(sn);
363 xbt_dynar_reset(prop_ato);
375 XBT_INFO("Different snapshot");
378 XBT_INFO("Different values of propositional symbols");
381 XBT_INFO("Different automaton state");
384 XBT_INFO("Different value of search_cycle");
389 MC_free_snapshot(sn);
390 xbt_dynar_reset(prop_ato);
405 int visited_hash(xbt_state_t st, int sc){
407 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
409 if(xbt_dynar_is_empty(visited_pairs_hash)){
417 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
418 MC_take_snapshot_liveness(sn);
421 unsigned int hash_regions[sn->num_reg];
422 for(j=0; j<sn->num_reg; j++){
423 hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
427 /* Get values of propositional symbols */
428 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
429 unsigned int cursor = 0;
430 xbt_propositional_symbol_t ps = NULL;
434 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
435 f = (int_f_void_t)ps->function;
437 xbt_dynar_push_as(prop_ato, int, res);
440 mc_pair_visited_hash_t pair_test = NULL;
445 xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
447 if(pair_test->search_cycle == sc) {
448 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
449 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
450 for(j=0 ; j< sn->num_reg ; j++){
451 if(hash_regions[j] != pair_test->hash_regions[j]){
455 if(region_diff == 0){
456 MC_free_snapshot(sn);
457 xbt_dynar_reset(prop_ato);
468 //XBT_INFO("Different snapshot");
471 //XBT_INFO("Different values of propositional symbols");
474 //XBT_INFO("Different automaton state");
477 //XBT_INFO("Different value of search_cycle");
483 MC_free_snapshot(sn);
484 xbt_dynar_reset(prop_ato);
498 void set_pair_visited_hash(xbt_state_t st, int sc){
500 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
504 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
505 MC_take_snapshot_liveness(sn);
507 mc_pair_visited_hash_t pair = NULL;
508 pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
509 pair->automaton_state = st;
510 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
511 pair->search_cycle = sc;
512 pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
516 for(i=0 ; i< sn->num_reg ; i++){
517 pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
520 /* Get values of propositional symbols */
521 unsigned int cursor = 0;
522 xbt_propositional_symbol_t ps = NULL;
526 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
527 f = (int_f_void_t)ps->function;
529 xbt_dynar_push_as(pair->prop_ato, int, res);
532 xbt_dynar_push(visited_pairs_hash, &pair);
534 MC_free_snapshot(sn);
545 void set_pair_visited(xbt_state_t st, int sc){
547 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
551 mc_pair_visited_t pair = NULL;
552 pair = xbt_new0(s_mc_pair_visited_t, 1);
553 pair->automaton_state = st;
554 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
555 pair->search_cycle = sc;
556 pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
557 MC_take_snapshot_liveness(pair->system_state);
560 /* Get values of propositional symbols */
561 unsigned int cursor = 0;
562 xbt_propositional_symbol_t ps = NULL;
566 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
567 f = (int_f_void_t)ps->function;
569 xbt_dynar_push_as(pair->prop_ato, int, res);
572 xbt_dynar_push(visited_pairs, &pair);
583 void MC_pair_delete(mc_pair_t pair){
584 xbt_free(pair->graph_state->proc_status);
585 xbt_free(pair->graph_state);
591 int MC_automaton_evaluate_label(xbt_exp_label_t l){
595 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
596 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
597 return (left_res || right_res);
600 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
601 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
602 return (left_res && right_res);
605 int res = MC_automaton_evaluate_label(l->u.exp_not);
609 unsigned int cursor = 0;
610 xbt_propositional_symbol_t p = NULL;
612 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
613 if(strcmp(p->pred, l->u.predicat) == 0){
614 f = (int_f_void_t)p->function;
629 /********************* Double-DFS stateless *******************/
631 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
632 xbt_free(pair->graph_state->proc_status);
633 xbt_free(pair->graph_state);
637 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
638 mc_pair_stateless_t p = NULL;
639 p = xbt_new0(s_mc_pair_stateless_t, 1);
640 p->automaton_state = st;
643 mc_stats_pair->expanded_pairs++;
647 void MC_ddfs_init(void){
649 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
651 XBT_INFO("**************************************************");
652 XBT_INFO("Double-DFS init");
653 XBT_INFO("**************************************************");
655 mc_pair_stateless_t mc_initial_pair = NULL;
656 mc_state_t initial_graph_state = NULL;
657 smx_process_t process;
660 MC_wait_for_requests();
664 initial_graph_state = MC_state_pair_new();
665 xbt_swag_foreach(process, simix_global->process_list){
666 if(MC_process_is_enabled(process)){
667 MC_state_interleave_process(initial_graph_state, process);
671 reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
672 //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
673 //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
674 //visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
675 successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
677 /* Save the initial state */
678 initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
679 MC_take_snapshot_liveness(initial_snapshot_liveness);
683 unsigned int cursor = 0;
686 xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
687 if(state->type == -1){
690 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
691 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
695 MC_restore_snapshot(initial_snapshot_liveness);
702 if(state->type == 2){
705 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
706 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
709 set_pair_reached(state);
710 //set_pair_reached_hash(state);
713 MC_restore_snapshot(initial_snapshot_liveness);
732 void MC_ddfs(int search_cycle){
734 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
736 smx_process_t process;
737 mc_pair_stateless_t current_pair = NULL;
739 if(xbt_fifo_size(mc_stack_liveness) == 0)
743 /* Get current pair */
744 current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
746 /* Update current state in buchi automaton */
747 _mc_property_automaton->current_state = current_pair->automaton_state;
750 XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
752 mc_stats_pair->visited_pairs++;
757 mc_state_t next_graph_state = NULL;
758 smx_simcall_t req = NULL;
761 xbt_transition_t transition_succ;
762 unsigned int cursor = 0;
765 mc_pair_stateless_t next_pair = NULL;
766 mc_pair_stateless_t pair_succ;
768 if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
770 //set_pair_visited(current_pair->automaton_state, search_cycle);
771 //set_pair_visited_hash(current_pair->automaton_state, search_cycle);
773 //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
774 //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
776 if(current_pair->requests > 0){
778 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
780 /* Debug information */
782 req_str = MC_request_to_string(req, value);
783 XBT_INFO("Execute: %s", req_str);
786 MC_state_set_executed_request(current_pair->graph_state, req, value);
788 /* Answer the request */
789 SIMIX_simcall_pre(req, value);
791 /* Wait for requests (schedules processes) */
792 MC_wait_for_requests();
797 /* Create the new expanded graph_state */
798 next_graph_state = MC_state_pair_new();
800 /* Get enabled process and insert it in the interleave set of the next graph_state */
801 xbt_swag_foreach(process, simix_global->process_list){
802 if(MC_process_is_enabled(process)){
803 MC_state_interleave_process(next_graph_state, process);
807 xbt_dynar_reset(successors);
813 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
815 res = MC_automaton_evaluate_label(transition_succ->label);
817 if(res == 1){ // enabled transition in automaton
819 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
820 xbt_dynar_push(successors, &next_pair);
828 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
830 res = MC_automaton_evaluate_label(transition_succ->label);
832 if(res == 2){ // true transition in automaton
834 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
835 xbt_dynar_push(successors, &next_pair);
843 xbt_dynar_foreach(successors, cursor, pair_succ){
845 if(search_cycle == 1){
847 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
849 if(reached(pair_succ->automaton_state)){
850 //if(reached_hash(pair_succ->automaton_state)){
852 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));
854 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
855 XBT_INFO("| ACCEPTANCE CYCLE |");
856 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
857 XBT_INFO("Counter-example that violates formula :");
858 MC_show_stack_liveness(mc_stack_liveness);
859 MC_dump_stack_liveness(mc_stack_liveness);
860 MC_print_statistics_pairs(mc_stats_pair);
865 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);
867 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
868 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
871 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
874 MC_ddfs(search_cycle);
880 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
881 //if(!visited(pair_succ->automaton_state, search_cycle)){
884 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
887 MC_ddfs(search_cycle);
891 XBT_INFO("Next pair already visited ! ");
899 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
901 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);
903 set_pair_reached(pair_succ->automaton_state);
904 //set_pair_reached_hash(pair_succ->automaton_state);
908 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
909 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
913 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
914 //if(!visited(pair_succ->automaton_state, search_cycle)){
917 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
920 MC_ddfs(search_cycle);
924 XBT_INFO("Next pair already visited ! ");
931 /* Restore system before checking others successors */
932 if(cursor != (xbt_dynar_length(successors) - 1))
933 MC_replay_liveness(mc_stack_liveness, 1);
938 if(MC_state_interleave_size(current_pair->graph_state) > 0){
939 XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
940 MC_replay_liveness(mc_stack_liveness, 0);
945 }else{ /*No request to execute, search evolution in Büchi automaton */
949 /* Create the new expanded graph_state */
950 next_graph_state = MC_state_pair_new();
952 xbt_dynar_reset(successors);
958 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
960 res = MC_automaton_evaluate_label(transition_succ->label);
962 if(res == 1){ // enabled transition in automaton
964 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
965 xbt_dynar_push(successors, &next_pair);
973 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
975 res = MC_automaton_evaluate_label(transition_succ->label);
977 if(res == 2){ // true transition in automaton
979 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
980 xbt_dynar_push(successors, &next_pair);
988 xbt_dynar_foreach(successors, cursor, pair_succ){
990 if(search_cycle == 1){
992 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
994 if(reached(pair_succ->automaton_state)){
995 //if(reached_hash(pair_succ->automaton_state)){
997 XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
999 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1000 XBT_INFO("| ACCEPTANCE CYCLE |");
1001 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1002 XBT_INFO("Counter-example that violates formula :");
1003 MC_show_stack_liveness(mc_stack_liveness);
1004 MC_dump_stack_liveness(mc_stack_liveness);
1005 MC_print_statistics_pairs(mc_stats_pair);
1010 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);
1012 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1013 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1016 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1019 MC_ddfs(search_cycle);
1025 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1026 //if(!visited(pair_succ->automaton_state, search_cycle)){
1029 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1032 MC_ddfs(search_cycle);
1036 XBT_INFO("Next pair already visited ! ");
1044 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1046 set_pair_reached(pair_succ->automaton_state);
1047 //set_pair_reached_hash(pair_succ->automaton_state);
1051 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1052 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1056 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1057 //if(!visited(pair_succ->automaton_state, search_cycle)){
1060 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1063 MC_ddfs(search_cycle);
1067 XBT_INFO("Next pair already visited ! ");
1073 /* Restore system before checking others successors */
1074 if(cursor != xbt_dynar_length(successors) - 1)
1075 MC_replay_liveness(mc_stack_liveness, 1);
1084 XBT_INFO("Max depth reached");
1088 if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
1089 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) );
1091 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) );
1096 xbt_fifo_shift(mc_stack_liveness);
1097 if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
1098 xbt_dynar_pop(reached_pairs, NULL);
1099 //xbt_dynar_pop(reached_pairs_hash, NULL);