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_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
87 MC_take_snapshot_liveness(sn);
89 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
93 /* Get values of propositional symbols */
94 unsigned int cursor = 0;
95 xbt_propositional_symbol_t ps = NULL;
96 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
97 f = (int_f_void_t)ps->function;
99 xbt_dynar_push_as(prop_ato, int, res);
103 mc_pair_reached_t pair_test = NULL;
105 xbt_dynar_foreach(reached_pairs, cursor, pair_test){
106 XBT_INFO("Pair reached #%d", pair_test->nb);
107 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
108 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
109 if(snapshot_compare(pair_test->system_state, sn) == 0){
111 MC_free_snapshot(sn);
112 xbt_dynar_reset(prop_ato);
124 XBT_INFO("Different values of propositional symbols");
127 XBT_INFO("Different automaton state");
131 MC_free_snapshot(sn);
132 xbt_dynar_reset(prop_ato);
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 //pair->rdv_points = xbt_dict_new();
160 MC_take_snapshot_liveness(pair->system_state);
162 /* Get values of propositional symbols */
163 unsigned int cursor = 0;
164 xbt_propositional_symbol_t ps = NULL;
168 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
169 f = (int_f_void_t)ps->function;
171 xbt_dynar_push_as(pair->prop_ato, int, res);
174 xbt_dynar_push(reached_pairs, &pair);
176 create_dump(xbt_dynar_length(reached_pairs));
188 int reached_hash(xbt_state_t st){
190 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
192 if(xbt_dynar_is_empty(reached_pairs_hash)){
200 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
201 MC_take_snapshot_liveness(sn);
204 unsigned int hash_regions[sn->num_reg];
205 for(j=0; j<sn->num_reg; j++){
206 hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
210 /* Get values of propositional symbols */
211 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
212 unsigned int cursor = 0;
213 xbt_propositional_symbol_t ps = NULL;
217 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
218 f = (int_f_void_t)ps->function;
220 xbt_dynar_push_as(prop_ato, int, res);
223 mc_pair_reached_hash_t pair_test = NULL;
229 xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
231 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
232 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
233 for(j=0 ; j< sn->num_reg ; j++){
234 if(hash_regions[j] != pair_test->hash_regions[j]){
238 if(region_diff == 0){
239 MC_free_snapshot(sn);
240 xbt_dynar_reset(prop_ato);
251 XBT_INFO("Different snapshot");
254 XBT_INFO("Different values of propositional symbols");
257 XBT_INFO("Different automaton state");
263 MC_free_snapshot(sn);
264 xbt_dynar_reset(prop_ato);
278 void set_pair_reached_hash(xbt_state_t st){
280 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
284 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
285 MC_take_snapshot_liveness(sn);
287 mc_pair_reached_hash_t pair = NULL;
288 pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
289 pair->automaton_state = st;
290 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
291 pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
295 for(i=0 ; i< sn->num_reg ; i++){
296 pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
299 /* Get values of propositional symbols */
300 unsigned int cursor = 0;
301 xbt_propositional_symbol_t ps = NULL;
305 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
306 f = (int_f_void_t)ps->function;
308 xbt_dynar_push_as(pair->prop_ato, int, res);
311 xbt_dynar_push(reached_pairs_hash, &pair);
313 MC_free_snapshot(sn);
325 int visited(xbt_state_t st, int sc){
327 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
329 if(xbt_dynar_is_empty(visited_pairs)){
337 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
338 MC_take_snapshot_liveness(sn);
340 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
342 /* Get values of propositional symbols */
343 unsigned int cursor = 0;
344 xbt_propositional_symbol_t ps = NULL;
348 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
349 f = (int_f_void_t)ps->function;
351 xbt_dynar_push_as(prop_ato, int, res);
355 mc_pair_visited_t pair_test = NULL;
357 xbt_dynar_foreach(visited_pairs, cursor, pair_test){
358 if(pair_test->search_cycle == sc) {
359 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
360 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
361 if(snapshot_compare(pair_test->system_state, sn) == 0){
363 MC_free_snapshot(sn);
364 xbt_dynar_reset(prop_ato);
376 XBT_INFO("Different snapshot");
379 XBT_INFO("Different values of propositional symbols");
382 XBT_INFO("Different automaton state");
385 XBT_INFO("Different value of search_cycle");
390 MC_free_snapshot(sn);
391 xbt_dynar_reset(prop_ato);
406 int visited_hash(xbt_state_t st, int sc){
408 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
410 if(xbt_dynar_is_empty(visited_pairs_hash)){
418 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
419 MC_take_snapshot_liveness(sn);
422 unsigned int hash_regions[sn->num_reg];
423 for(j=0; j<sn->num_reg; j++){
424 hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
428 /* Get values of propositional symbols */
429 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
430 unsigned int cursor = 0;
431 xbt_propositional_symbol_t ps = NULL;
435 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
436 f = (int_f_void_t)ps->function;
438 xbt_dynar_push_as(prop_ato, int, res);
441 mc_pair_visited_hash_t pair_test = NULL;
446 xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
448 if(pair_test->search_cycle == sc) {
449 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
450 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
451 for(j=0 ; j< sn->num_reg ; j++){
452 if(hash_regions[j] != pair_test->hash_regions[j]){
456 if(region_diff == 0){
457 MC_free_snapshot(sn);
458 xbt_dynar_reset(prop_ato);
469 //XBT_INFO("Different snapshot");
472 //XBT_INFO("Different values of propositional symbols");
475 //XBT_INFO("Different automaton state");
478 //XBT_INFO("Different value of search_cycle");
484 MC_free_snapshot(sn);
485 xbt_dynar_reset(prop_ato);
499 void set_pair_visited_hash(xbt_state_t st, int sc){
501 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
505 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
506 MC_take_snapshot_liveness(sn);
508 mc_pair_visited_hash_t pair = NULL;
509 pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
510 pair->automaton_state = st;
511 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
512 pair->search_cycle = sc;
513 pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
517 for(i=0 ; i< sn->num_reg ; i++){
518 pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
521 /* Get values of propositional symbols */
522 unsigned int cursor = 0;
523 xbt_propositional_symbol_t ps = NULL;
527 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
528 f = (int_f_void_t)ps->function;
530 xbt_dynar_push_as(pair->prop_ato, int, res);
533 xbt_dynar_push(visited_pairs_hash, &pair);
535 MC_free_snapshot(sn);
546 void set_pair_visited(xbt_state_t st, int sc){
548 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
552 mc_pair_visited_t pair = NULL;
553 pair = xbt_new0(s_mc_pair_visited_t, 1);
554 pair->automaton_state = st;
555 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
556 pair->search_cycle = sc;
557 pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
558 MC_take_snapshot_liveness(pair->system_state);
561 /* Get values of propositional symbols */
562 unsigned int cursor = 0;
563 xbt_propositional_symbol_t ps = NULL;
567 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
568 f = (int_f_void_t)ps->function;
570 xbt_dynar_push_as(pair->prop_ato, int, res);
573 xbt_dynar_push(visited_pairs, &pair);
584 void MC_pair_delete(mc_pair_t pair){
585 xbt_free(pair->graph_state->proc_status);
586 xbt_free(pair->graph_state);
592 int MC_automaton_evaluate_label(xbt_exp_label_t l){
596 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
597 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
598 return (left_res || right_res);
601 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
602 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
603 return (left_res && right_res);
606 int res = MC_automaton_evaluate_label(l->u.exp_not);
610 unsigned int cursor = 0;
611 xbt_propositional_symbol_t p = NULL;
613 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
614 if(strcmp(p->pred, l->u.predicat) == 0){
615 f = (int_f_void_t)p->function;
630 /********************* Double-DFS stateless *******************/
632 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
633 xbt_free(pair->graph_state->proc_status);
634 xbt_free(pair->graph_state);
638 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
639 mc_pair_stateless_t p = NULL;
640 p = xbt_new0(s_mc_pair_stateless_t, 1);
641 p->automaton_state = st;
644 mc_stats_pair->expanded_pairs++;
648 void MC_ddfs_init(void){
650 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
652 XBT_INFO("**************************************************");
653 XBT_INFO("Double-DFS init");
654 XBT_INFO("**************************************************");
656 mc_pair_stateless_t mc_initial_pair = NULL;
657 mc_state_t initial_graph_state = NULL;
658 smx_process_t process;
661 MC_wait_for_requests();
665 initial_graph_state = MC_state_pair_new();
666 xbt_swag_foreach(process, simix_global->process_list){
667 if(MC_process_is_enabled(process)){
668 MC_state_interleave_process(initial_graph_state, process);
672 reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
673 //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
674 //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
675 //visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
676 successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
678 /* Save the initial state */
679 initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
680 MC_take_snapshot_liveness(initial_snapshot_liveness);
684 unsigned int cursor = 0;
687 xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
688 if(state->type == -1){
691 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
692 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
696 MC_restore_snapshot(initial_snapshot_liveness);
703 if(state->type == 2){
706 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
707 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
710 set_pair_reached(state);
711 //set_pair_reached_hash(state);
714 MC_restore_snapshot(initial_snapshot_liveness);
733 void MC_ddfs(int search_cycle){
735 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
737 smx_process_t process;
738 mc_pair_stateless_t current_pair = NULL;
740 if(xbt_fifo_size(mc_stack_liveness) == 0)
744 /* Get current pair */
745 current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
747 /* Update current state in buchi automaton */
748 _mc_property_automaton->current_state = current_pair->automaton_state;
751 XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
753 mc_stats_pair->visited_pairs++;
758 mc_state_t next_graph_state = NULL;
759 smx_simcall_t req = NULL;
762 xbt_transition_t transition_succ;
763 unsigned int cursor = 0;
766 mc_pair_stateless_t next_pair = NULL;
767 mc_pair_stateless_t pair_succ;
769 if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
771 //set_pair_visited(current_pair->automaton_state, search_cycle);
772 //set_pair_visited_hash(current_pair->automaton_state, search_cycle);
774 //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
775 //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
777 if(current_pair->requests > 0){
779 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
781 /* Debug information */
783 req_str = MC_request_to_string(req, value);
784 XBT_INFO("Execute: %s", req_str);
787 MC_state_set_executed_request(current_pair->graph_state, req, value);
789 /* Answer the request */
790 SIMIX_simcall_pre(req, value);
792 /* Wait for requests (schedules processes) */
793 MC_wait_for_requests();
798 /* Create the new expanded graph_state */
799 next_graph_state = MC_state_pair_new();
801 /* Get enabled process and insert it in the interleave set of the next graph_state */
802 xbt_swag_foreach(process, simix_global->process_list){
803 if(MC_process_is_enabled(process)){
804 MC_state_interleave_process(next_graph_state, process);
808 xbt_dynar_reset(successors);
814 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
816 res = MC_automaton_evaluate_label(transition_succ->label);
818 if(res == 1){ // enabled transition in automaton
820 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
821 xbt_dynar_push(successors, &next_pair);
829 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
831 res = MC_automaton_evaluate_label(transition_succ->label);
833 if(res == 2){ // true transition in automaton
835 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
836 xbt_dynar_push(successors, &next_pair);
844 xbt_dynar_foreach(successors, cursor, pair_succ){
846 if(search_cycle == 1){
848 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
850 if(reached(pair_succ->automaton_state)){
851 //if(reached_hash(pair_succ->automaton_state)){
853 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));
855 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
856 XBT_INFO("| ACCEPTANCE CYCLE |");
857 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
858 XBT_INFO("Counter-example that violates formula :");
859 MC_show_stack_liveness(mc_stack_liveness);
860 MC_dump_stack_liveness(mc_stack_liveness);
861 MC_print_statistics_pairs(mc_stats_pair);
866 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);
868 set_pair_reached(pair_succ->automaton_state);
869 //set_pair_reached_hash(pair_succ->automaton_state);
871 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
872 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
875 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
878 MC_ddfs(search_cycle);
884 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
885 //if(!visited(pair_succ->automaton_state, search_cycle)){
888 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
891 MC_ddfs(search_cycle);
895 XBT_INFO("Next pair already visited ! ");
903 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
905 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);
907 set_pair_reached(pair_succ->automaton_state);
908 //set_pair_reached_hash(pair_succ->automaton_state);
912 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
913 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
917 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
918 //if(!visited(pair_succ->automaton_state, search_cycle)){
921 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
924 MC_ddfs(search_cycle);
928 XBT_INFO("Next pair already visited ! ");
935 /* Restore system before checking others successors */
936 if(cursor != (xbt_dynar_length(successors) - 1))
937 MC_replay_liveness(mc_stack_liveness, 1);
942 if(MC_state_interleave_size(current_pair->graph_state) > 0){
943 XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
944 MC_replay_liveness(mc_stack_liveness, 0);
949 }else{ /*No request to execute, search evolution in Büchi automaton */
953 /* Create the new expanded graph_state */
954 next_graph_state = MC_state_pair_new();
956 xbt_dynar_reset(successors);
962 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
964 res = MC_automaton_evaluate_label(transition_succ->label);
966 if(res == 1){ // enabled transition in automaton
968 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
969 xbt_dynar_push(successors, &next_pair);
977 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
979 res = MC_automaton_evaluate_label(transition_succ->label);
981 if(res == 2){ // true transition in automaton
983 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
984 xbt_dynar_push(successors, &next_pair);
992 xbt_dynar_foreach(successors, cursor, pair_succ){
994 if(search_cycle == 1){
996 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
998 if(reached(pair_succ->automaton_state)){
999 //if(reached_hash(pair_succ->automaton_state)){
1001 XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
1003 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1004 XBT_INFO("| ACCEPTANCE CYCLE |");
1005 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1006 XBT_INFO("Counter-example that violates formula :");
1007 MC_show_stack_liveness(mc_stack_liveness);
1008 MC_dump_stack_liveness(mc_stack_liveness);
1009 MC_print_statistics_pairs(mc_stats_pair);
1014 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);
1016 set_pair_reached(pair_succ->automaton_state);
1017 //set_pair_reached_hash(pair_succ->automaton_state);
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);