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);
80 mc_pair_reached_t new_pair = NULL;
81 new_pair = xbt_new0(s_mc_pair_reached_t, 1);
82 new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
83 new_pair->automaton_state = st;
84 new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
85 new_pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
86 MC_take_snapshot_liveness(new_pair->system_state);
88 /* Get values of propositional symbols */
91 unsigned int cursor = 0;
92 xbt_propositional_symbol_t ps = NULL;
93 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
94 f = (int_f_void_t)ps->function;
96 xbt_dynar_push_as(new_pair->prop_ato, int, res);
101 if(xbt_dynar_is_empty(reached_pairs) || !compare){
103 /* New pair reached */
104 xbt_dynar_push(reached_pairs, &new_pair);
113 mc_pair_reached_t pair_test = NULL;
115 xbt_dynar_foreach(reached_pairs, cursor, pair_test){
116 XBT_INFO("Pair reached #%d", pair_test->nb);
117 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
118 if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
119 if(snapshot_compare(pair_test->system_state, new_pair->system_state) == 0){
129 XBT_INFO("Different values of propositional symbols");
132 XBT_INFO("Different automaton state");
136 create_dump(xbt_dynar_length(reached_pairs));
138 /* New pair reached */
139 xbt_dynar_push(reached_pairs, &new_pair);
156 void set_pair_reached(xbt_state_t st){
158 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
162 mc_pair_reached_t pair = NULL;
163 pair = xbt_new0(s_mc_pair_reached_t, 1);
164 pair->nb = xbt_dynar_length(reached_pairs) + 1;
165 pair->automaton_state = st;
166 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
167 pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
168 MC_take_snapshot_liveness(pair->system_state);
170 /* Get values of propositional symbols */
171 unsigned int cursor = 0;
172 xbt_propositional_symbol_t ps = NULL;
176 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
177 f = (int_f_void_t)ps->function;
179 xbt_dynar_push_as(pair->prop_ato, int, res);
182 xbt_dynar_push(reached_pairs, &pair);
194 int reached_hash(xbt_state_t st){
196 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
198 if(xbt_dynar_is_empty(reached_pairs_hash)){
206 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
207 MC_take_snapshot_liveness(sn);
210 unsigned int hash_regions[sn->num_reg];
211 for(j=0; j<sn->num_reg; j++){
212 hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
216 /* Get values of propositional symbols */
217 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
218 unsigned int cursor = 0;
219 xbt_propositional_symbol_t ps = NULL;
223 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
224 f = (int_f_void_t)ps->function;
226 xbt_dynar_push_as(prop_ato, int, res);
229 mc_pair_reached_hash_t pair_test = NULL;
235 xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
237 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
238 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
239 for(j=0 ; j< sn->num_reg ; j++){
240 if(hash_regions[j] != pair_test->hash_regions[j]){
244 if(region_diff == 0){
245 MC_free_snapshot(sn);
246 xbt_dynar_reset(prop_ato);
257 XBT_INFO("Different snapshot");
260 XBT_INFO("Different values of propositional symbols");
263 XBT_INFO("Different automaton state");
269 MC_free_snapshot(sn);
270 xbt_dynar_reset(prop_ato);
284 void set_pair_reached_hash(xbt_state_t st){
286 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
290 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
291 MC_take_snapshot_liveness(sn);
293 mc_pair_reached_hash_t pair = NULL;
294 pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
295 pair->automaton_state = st;
296 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
297 pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
301 for(i=0 ; i< sn->num_reg ; i++){
302 pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
305 /* Get values of propositional symbols */
306 unsigned int cursor = 0;
307 xbt_propositional_symbol_t ps = NULL;
311 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
312 f = (int_f_void_t)ps->function;
314 xbt_dynar_push_as(pair->prop_ato, int, res);
317 xbt_dynar_push(reached_pairs_hash, &pair);
319 MC_free_snapshot(sn);
331 int visited(xbt_state_t st, int sc){
333 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
335 if(xbt_dynar_is_empty(visited_pairs)){
343 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
344 MC_take_snapshot_liveness(sn);
346 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
348 /* Get values of propositional symbols */
349 unsigned int cursor = 0;
350 xbt_propositional_symbol_t ps = NULL;
354 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
355 f = (int_f_void_t)ps->function;
357 xbt_dynar_push_as(prop_ato, int, res);
361 mc_pair_visited_t pair_test = NULL;
363 xbt_dynar_foreach(visited_pairs, cursor, pair_test){
364 if(pair_test->search_cycle == sc) {
365 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
366 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
367 if(snapshot_compare(pair_test->system_state, sn) == 0){
369 MC_free_snapshot(sn);
370 xbt_dynar_reset(prop_ato);
382 XBT_INFO("Different snapshot");
385 XBT_INFO("Different values of propositional symbols");
388 XBT_INFO("Different automaton state");
391 XBT_INFO("Different value of search_cycle");
396 MC_free_snapshot(sn);
397 xbt_dynar_reset(prop_ato);
412 int visited_hash(xbt_state_t st, int sc){
414 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
416 if(xbt_dynar_is_empty(visited_pairs_hash)){
424 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
425 MC_take_snapshot_liveness(sn);
428 unsigned int hash_regions[sn->num_reg];
429 for(j=0; j<sn->num_reg; j++){
430 hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
434 /* Get values of propositional symbols */
435 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
436 unsigned int cursor = 0;
437 xbt_propositional_symbol_t ps = NULL;
441 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
442 f = (int_f_void_t)ps->function;
444 xbt_dynar_push_as(prop_ato, int, res);
447 mc_pair_visited_hash_t pair_test = NULL;
452 xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
454 if(pair_test->search_cycle == sc) {
455 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
456 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
457 for(j=0 ; j< sn->num_reg ; j++){
458 if(hash_regions[j] != pair_test->hash_regions[j]){
462 if(region_diff == 0){
463 MC_free_snapshot(sn);
464 xbt_dynar_reset(prop_ato);
475 //XBT_INFO("Different snapshot");
478 //XBT_INFO("Different values of propositional symbols");
481 //XBT_INFO("Different automaton state");
484 //XBT_INFO("Different value of search_cycle");
490 MC_free_snapshot(sn);
491 xbt_dynar_reset(prop_ato);
505 void set_pair_visited_hash(xbt_state_t st, int sc){
507 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
511 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
512 MC_take_snapshot_liveness(sn);
514 mc_pair_visited_hash_t pair = NULL;
515 pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
516 pair->automaton_state = st;
517 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
518 pair->search_cycle = sc;
519 pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
523 for(i=0 ; i< sn->num_reg ; i++){
524 pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
527 /* Get values of propositional symbols */
528 unsigned int cursor = 0;
529 xbt_propositional_symbol_t ps = NULL;
533 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
534 f = (int_f_void_t)ps->function;
536 xbt_dynar_push_as(pair->prop_ato, int, res);
539 xbt_dynar_push(visited_pairs_hash, &pair);
541 MC_free_snapshot(sn);
552 void set_pair_visited(xbt_state_t st, int sc){
554 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
558 mc_pair_visited_t pair = NULL;
559 pair = xbt_new0(s_mc_pair_visited_t, 1);
560 pair->automaton_state = st;
561 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
562 pair->search_cycle = sc;
563 pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
564 MC_take_snapshot_liveness(pair->system_state);
567 /* Get values of propositional symbols */
568 unsigned int cursor = 0;
569 xbt_propositional_symbol_t ps = NULL;
573 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
574 f = (int_f_void_t)ps->function;
576 xbt_dynar_push_as(pair->prop_ato, int, res);
579 xbt_dynar_push(visited_pairs, &pair);
590 void MC_pair_delete(mc_pair_t pair){
591 xbt_free(pair->graph_state->proc_status);
592 xbt_free(pair->graph_state);
598 int MC_automaton_evaluate_label(xbt_exp_label_t l){
602 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
603 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
604 return (left_res || right_res);
607 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
608 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
609 return (left_res && right_res);
612 int res = MC_automaton_evaluate_label(l->u.exp_not);
616 unsigned int cursor = 0;
617 xbt_propositional_symbol_t p = NULL;
619 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
620 if(strcmp(p->pred, l->u.predicat) == 0){
621 f = (int_f_void_t)p->function;
636 /********************* Double-DFS stateless *******************/
638 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
639 xbt_free(pair->graph_state->proc_status);
640 xbt_free(pair->graph_state);
644 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
645 mc_pair_stateless_t p = NULL;
646 p = xbt_new0(s_mc_pair_stateless_t, 1);
647 p->automaton_state = st;
650 mc_stats_pair->expanded_pairs++;
654 void MC_ddfs_init(void){
656 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
658 XBT_INFO("**************************************************");
659 XBT_INFO("Double-DFS init");
660 XBT_INFO("**************************************************");
662 mc_pair_stateless_t mc_initial_pair = NULL;
663 mc_state_t initial_graph_state = NULL;
664 smx_process_t process;
667 MC_wait_for_requests();
671 initial_graph_state = MC_state_pair_new();
672 xbt_swag_foreach(process, simix_global->process_list){
673 if(MC_process_is_enabled(process)){
674 MC_state_interleave_process(initial_graph_state, process);
678 reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
679 //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
680 //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
681 //visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
682 successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
684 /* Save the initial state */
685 initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
686 MC_take_snapshot_liveness(initial_snapshot_liveness);
690 unsigned int cursor = 0;
693 xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
694 if(state->type == -1){
697 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
698 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
702 MC_restore_snapshot(initial_snapshot_liveness);
709 if(state->type == 2){
712 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
713 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
716 set_pair_reached(state);
717 //set_pair_reached_hash(state);
720 MC_restore_snapshot(initial_snapshot_liveness);
739 void MC_ddfs(int search_cycle){
741 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
743 smx_process_t process;
744 mc_pair_stateless_t current_pair = NULL;
746 if(xbt_fifo_size(mc_stack_liveness) == 0)
750 /* Get current pair */
751 current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
753 /* Update current state in buchi automaton */
754 _mc_property_automaton->current_state = current_pair->automaton_state;
757 XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
759 mc_stats_pair->visited_pairs++;
764 mc_state_t next_graph_state = NULL;
765 smx_simcall_t req = NULL;
768 xbt_transition_t transition_succ;
769 unsigned int cursor = 0;
772 mc_pair_stateless_t next_pair = NULL;
773 mc_pair_stateless_t pair_succ;
775 if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
777 //set_pair_visited(current_pair->automaton_state, search_cycle);
778 //set_pair_visited_hash(current_pair->automaton_state, search_cycle);
780 //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
781 //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
783 if(current_pair->requests > 0){
785 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
787 /* Debug information */
789 req_str = MC_request_to_string(req, value);
790 XBT_INFO("Execute: %s", req_str);
793 MC_state_set_executed_request(current_pair->graph_state, req, value);
795 /* Answer the request */
796 SIMIX_simcall_pre(req, value);
798 /* Wait for requests (schedules processes) */
799 MC_wait_for_requests();
804 /* Create the new expanded graph_state */
805 next_graph_state = MC_state_pair_new();
807 /* Get enabled process and insert it in the interleave set of the next graph_state */
808 xbt_swag_foreach(process, simix_global->process_list){
809 if(MC_process_is_enabled(process)){
810 MC_state_interleave_process(next_graph_state, process);
814 xbt_dynar_reset(successors);
820 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
822 res = MC_automaton_evaluate_label(transition_succ->label);
824 if(res == 1){ // enabled transition in automaton
826 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
827 xbt_dynar_push(successors, &next_pair);
835 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
837 res = MC_automaton_evaluate_label(transition_succ->label);
839 if(res == 2){ // true transition in automaton
841 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
842 xbt_dynar_push(successors, &next_pair);
850 xbt_dynar_foreach(successors, cursor, pair_succ){
852 if(search_cycle == 1){
854 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
856 if(reached(pair_succ->automaton_state)){
857 //if(reached_hash(pair_succ->automaton_state)){
859 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));
861 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
862 XBT_INFO("| ACCEPTANCE CYCLE |");
863 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
864 XBT_INFO("Counter-example that violates formula :");
865 MC_show_stack_liveness(mc_stack_liveness);
866 MC_dump_stack_liveness(mc_stack_liveness);
867 MC_print_statistics_pairs(mc_stats_pair);
872 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);
874 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
875 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
878 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
881 MC_ddfs(search_cycle);
887 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
888 //if(!visited(pair_succ->automaton_state, search_cycle)){
891 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
894 MC_ddfs(search_cycle);
898 XBT_INFO("Next pair already visited ! ");
906 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
908 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);
910 set_pair_reached(pair_succ->automaton_state);
911 //set_pair_reached_hash(pair_succ->automaton_state);
915 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
916 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
920 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
921 //if(!visited(pair_succ->automaton_state, search_cycle)){
924 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
927 MC_ddfs(search_cycle);
931 XBT_INFO("Next pair already visited ! ");
938 /* Restore system before checking others successors */
939 if(cursor != (xbt_dynar_length(successors) - 1))
940 MC_replay_liveness(mc_stack_liveness, 1);
945 if(MC_state_interleave_size(current_pair->graph_state) > 0){
946 XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
947 MC_replay_liveness(mc_stack_liveness, 0);
952 }else{ /*No request to execute, search evolution in Büchi automaton */
956 /* Create the new expanded graph_state */
957 next_graph_state = MC_state_pair_new();
959 xbt_dynar_reset(successors);
965 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
967 res = MC_automaton_evaluate_label(transition_succ->label);
969 if(res == 1){ // enabled transition in automaton
971 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
972 xbt_dynar_push(successors, &next_pair);
980 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
982 res = MC_automaton_evaluate_label(transition_succ->label);
984 if(res == 2){ // true transition in automaton
986 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
987 xbt_dynar_push(successors, &next_pair);
995 xbt_dynar_foreach(successors, cursor, pair_succ){
997 if(search_cycle == 1){
999 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
1001 if(reached(pair_succ->automaton_state)){
1002 //if(reached_hash(pair_succ->automaton_state)){
1004 XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
1006 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1007 XBT_INFO("| ACCEPTANCE CYCLE |");
1008 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1009 XBT_INFO("Counter-example that violates formula :");
1010 MC_show_stack_liveness(mc_stack_liveness);
1011 MC_dump_stack_liveness(mc_stack_liveness);
1012 MC_print_statistics_pairs(mc_stats_pair);
1017 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);
1019 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1020 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1023 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1026 MC_ddfs(search_cycle);
1032 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1033 //if(!visited(pair_succ->automaton_state, search_cycle)){
1036 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1039 MC_ddfs(search_cycle);
1043 XBT_INFO("Next pair already visited ! ");
1051 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1053 set_pair_reached(pair_succ->automaton_state);
1054 //set_pair_reached_hash(pair_succ->automaton_state);
1058 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1059 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1063 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1064 //if(!visited(pair_succ->automaton_state, search_cycle)){
1067 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1070 MC_ddfs(search_cycle);
1074 XBT_INFO("Next pair already visited ! ");
1080 /* Restore system before checking others successors */
1081 if(cursor != xbt_dynar_length(successors) - 1)
1082 MC_replay_liveness(mc_stack_liveness, 1);
1091 XBT_INFO("Max depth reached");
1095 if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
1096 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) );
1098 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) );
1103 xbt_fifo_shift(mc_stack_liveness);
1104 if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
1105 xbt_dynar_pop(reached_pairs, NULL);
1106 //xbt_dynar_pop(reached_pairs_hash, NULL);