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){
104 /* New pair reached */
105 xbt_dynar_push(reached_pairs, &new_pair);
116 mc_pair_reached_t pair_test = NULL;
118 xbt_dynar_foreach(reached_pairs, cursor, pair_test){
119 XBT_INFO("Pair reached #%d", pair_test->nb);
120 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
121 if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
122 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
132 XBT_INFO("Different values of propositional symbols");
135 XBT_INFO("Different automaton state");
139 //create_dump(xbt_dynar_length(reached_pairs));
141 /* New pair reached */
142 xbt_dynar_push(reached_pairs, &new_pair);
159 void set_pair_reached(xbt_state_t st){
161 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
165 mc_pair_reached_t pair = NULL;
166 pair = xbt_new0(s_mc_pair_reached_t, 1);
167 pair->nb = xbt_dynar_length(reached_pairs) + 1;
168 pair->automaton_state = st;
169 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
170 pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
171 MC_take_snapshot_liveness(pair->system_state);
173 /* Get values of propositional symbols */
174 unsigned int cursor = 0;
175 xbt_propositional_symbol_t ps = NULL;
179 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
180 f = (int_f_void_t)ps->function;
182 xbt_dynar_push_as(pair->prop_ato, int, res);
185 xbt_dynar_push(reached_pairs, &pair);
197 int reached_hash(xbt_state_t st){
199 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
201 if(xbt_dynar_is_empty(reached_pairs_hash)){
209 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
210 MC_take_snapshot_liveness(sn);
213 unsigned int hash_regions[sn->num_reg];
214 for(j=0; j<sn->num_reg; j++){
215 hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
219 /* Get values of propositional symbols */
220 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
221 unsigned int cursor = 0;
222 xbt_propositional_symbol_t ps = NULL;
226 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
227 f = (int_f_void_t)ps->function;
229 xbt_dynar_push_as(prop_ato, int, res);
232 mc_pair_reached_hash_t pair_test = NULL;
238 xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
240 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
241 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
242 for(j=0 ; j< sn->num_reg ; j++){
243 if(hash_regions[j] != pair_test->hash_regions[j]){
247 if(region_diff == 0){
248 MC_free_snapshot(sn);
249 xbt_dynar_reset(prop_ato);
260 XBT_INFO("Different snapshot");
263 XBT_INFO("Different values of propositional symbols");
266 XBT_INFO("Different automaton state");
272 MC_free_snapshot(sn);
273 xbt_dynar_reset(prop_ato);
287 void set_pair_reached_hash(xbt_state_t st){
289 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
293 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
294 MC_take_snapshot_liveness(sn);
296 mc_pair_reached_hash_t pair = NULL;
297 pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
298 pair->automaton_state = st;
299 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
300 pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
304 for(i=0 ; i< sn->num_reg ; i++){
305 pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
308 /* Get values of propositional symbols */
309 unsigned int cursor = 0;
310 xbt_propositional_symbol_t ps = NULL;
314 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
315 f = (int_f_void_t)ps->function;
317 xbt_dynar_push_as(pair->prop_ato, int, res);
320 xbt_dynar_push(reached_pairs_hash, &pair);
322 MC_free_snapshot(sn);
334 int visited(xbt_state_t st, int sc){
336 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
338 if(xbt_dynar_is_empty(visited_pairs)){
346 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
347 MC_take_snapshot_liveness(sn);
349 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
351 /* Get values of propositional symbols */
352 unsigned int cursor = 0;
353 xbt_propositional_symbol_t ps = NULL;
357 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
358 f = (int_f_void_t)ps->function;
360 xbt_dynar_push_as(prop_ato, int, res);
364 mc_pair_visited_t pair_test = NULL;
366 xbt_dynar_foreach(visited_pairs, cursor, pair_test){
367 if(pair_test->search_cycle == sc) {
368 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
369 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
370 if(snapshot_compare(pair_test->system_state, sn) == 0){
372 MC_free_snapshot(sn);
373 xbt_dynar_reset(prop_ato);
385 XBT_INFO("Different snapshot");
388 XBT_INFO("Different values of propositional symbols");
391 XBT_INFO("Different automaton state");
394 XBT_INFO("Different value of search_cycle");
399 MC_free_snapshot(sn);
400 xbt_dynar_reset(prop_ato);
415 int visited_hash(xbt_state_t st, int sc){
417 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
419 if(xbt_dynar_is_empty(visited_pairs_hash)){
427 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
428 MC_take_snapshot_liveness(sn);
431 unsigned int hash_regions[sn->num_reg];
432 for(j=0; j<sn->num_reg; j++){
433 hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
437 /* Get values of propositional symbols */
438 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
439 unsigned int cursor = 0;
440 xbt_propositional_symbol_t ps = NULL;
444 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
445 f = (int_f_void_t)ps->function;
447 xbt_dynar_push_as(prop_ato, int, res);
450 mc_pair_visited_hash_t pair_test = NULL;
455 xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
457 if(pair_test->search_cycle == sc) {
458 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
459 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
460 for(j=0 ; j< sn->num_reg ; j++){
461 if(hash_regions[j] != pair_test->hash_regions[j]){
465 if(region_diff == 0){
466 MC_free_snapshot(sn);
467 xbt_dynar_reset(prop_ato);
478 //XBT_INFO("Different snapshot");
481 //XBT_INFO("Different values of propositional symbols");
484 //XBT_INFO("Different automaton state");
487 //XBT_INFO("Different value of search_cycle");
493 MC_free_snapshot(sn);
494 xbt_dynar_reset(prop_ato);
508 void set_pair_visited_hash(xbt_state_t st, int sc){
510 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
514 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
515 MC_take_snapshot_liveness(sn);
517 mc_pair_visited_hash_t pair = NULL;
518 pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
519 pair->automaton_state = st;
520 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
521 pair->search_cycle = sc;
522 pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
526 for(i=0 ; i< sn->num_reg ; i++){
527 pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
530 /* Get values of propositional symbols */
531 unsigned int cursor = 0;
532 xbt_propositional_symbol_t ps = NULL;
536 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
537 f = (int_f_void_t)ps->function;
539 xbt_dynar_push_as(pair->prop_ato, int, res);
542 xbt_dynar_push(visited_pairs_hash, &pair);
544 MC_free_snapshot(sn);
555 void set_pair_visited(xbt_state_t st, int sc){
557 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
561 mc_pair_visited_t pair = NULL;
562 pair = xbt_new0(s_mc_pair_visited_t, 1);
563 pair->automaton_state = st;
564 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
565 pair->search_cycle = sc;
566 pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
567 MC_take_snapshot_liveness(pair->system_state);
570 /* Get values of propositional symbols */
571 unsigned int cursor = 0;
572 xbt_propositional_symbol_t ps = NULL;
576 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
577 f = (int_f_void_t)ps->function;
579 xbt_dynar_push_as(pair->prop_ato, int, res);
582 xbt_dynar_push(visited_pairs, &pair);
593 void MC_pair_delete(mc_pair_t pair){
594 xbt_free(pair->graph_state->proc_status);
595 xbt_free(pair->graph_state);
601 int MC_automaton_evaluate_label(xbt_exp_label_t l){
605 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
606 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
607 return (left_res || right_res);
610 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
611 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
612 return (left_res && right_res);
615 int res = MC_automaton_evaluate_label(l->u.exp_not);
619 unsigned int cursor = 0;
620 xbt_propositional_symbol_t p = NULL;
622 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
623 if(strcmp(p->pred, l->u.predicat) == 0){
624 f = (int_f_void_t)p->function;
639 /********************* Double-DFS stateless *******************/
641 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
642 xbt_free(pair->graph_state->proc_status);
643 xbt_free(pair->graph_state);
647 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
648 mc_pair_stateless_t p = NULL;
649 p = xbt_new0(s_mc_pair_stateless_t, 1);
650 p->automaton_state = st;
653 mc_stats_pair->expanded_pairs++;
657 void MC_ddfs_init(void){
659 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
661 XBT_INFO("**************************************************");
662 XBT_INFO("Double-DFS init");
663 XBT_INFO("**************************************************");
665 mc_pair_stateless_t mc_initial_pair = NULL;
666 mc_state_t initial_graph_state = NULL;
667 smx_process_t process;
670 MC_wait_for_requests();
674 initial_graph_state = MC_state_pair_new();
675 xbt_swag_foreach(process, simix_global->process_list){
676 if(MC_process_is_enabled(process)){
677 MC_state_interleave_process(initial_graph_state, process);
681 reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
682 //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
683 //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
684 //visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
685 successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
687 /* Save the initial state */
688 initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
689 MC_take_snapshot_liveness(initial_snapshot_liveness);
693 unsigned int cursor = 0;
696 xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
697 if(state->type == -1){
700 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
701 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
705 MC_restore_snapshot(initial_snapshot_liveness);
712 if(state->type == 2){
715 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
716 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
719 set_pair_reached(state);
720 //set_pair_reached_hash(state);
723 MC_restore_snapshot(initial_snapshot_liveness);
742 void MC_ddfs(int search_cycle){
744 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
746 smx_process_t process;
747 mc_pair_stateless_t current_pair = NULL;
749 if(xbt_fifo_size(mc_stack_liveness) == 0)
753 /* Get current pair */
754 current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
756 /* Update current state in buchi automaton */
757 _mc_property_automaton->current_state = current_pair->automaton_state;
760 XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
762 mc_stats_pair->visited_pairs++;
767 mc_state_t next_graph_state = NULL;
768 smx_simcall_t req = NULL;
771 xbt_transition_t transition_succ;
772 unsigned int cursor = 0;
775 mc_pair_stateless_t next_pair = NULL;
776 mc_pair_stateless_t pair_succ;
778 if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
780 //set_pair_visited(current_pair->automaton_state, search_cycle);
781 //set_pair_visited_hash(current_pair->automaton_state, search_cycle);
783 //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
784 //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
786 if(current_pair->requests > 0){
788 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
790 /* Debug information */
792 req_str = MC_request_to_string(req, value);
793 XBT_INFO("Execute: %s", req_str);
796 MC_state_set_executed_request(current_pair->graph_state, req, value);
798 /* Answer the request */
799 SIMIX_simcall_pre(req, value);
801 /* Wait for requests (schedules processes) */
802 MC_wait_for_requests();
807 /* Create the new expanded graph_state */
808 next_graph_state = MC_state_pair_new();
810 /* Get enabled process and insert it in the interleave set of the next graph_state */
811 xbt_swag_foreach(process, simix_global->process_list){
812 if(MC_process_is_enabled(process)){
813 MC_state_interleave_process(next_graph_state, process);
817 xbt_dynar_reset(successors);
823 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
825 res = MC_automaton_evaluate_label(transition_succ->label);
827 if(res == 1){ // enabled transition in automaton
829 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
830 xbt_dynar_push(successors, &next_pair);
838 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
840 res = MC_automaton_evaluate_label(transition_succ->label);
842 if(res == 2){ // true transition in automaton
844 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
845 xbt_dynar_push(successors, &next_pair);
853 xbt_dynar_foreach(successors, cursor, pair_succ){
855 if(search_cycle == 1){
857 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
859 if(reached(pair_succ->automaton_state)){
860 //if(reached_hash(pair_succ->automaton_state)){
862 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));
864 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
865 XBT_INFO("| ACCEPTANCE CYCLE |");
866 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
867 XBT_INFO("Counter-example that violates formula :");
868 MC_show_stack_liveness(mc_stack_liveness);
869 MC_dump_stack_liveness(mc_stack_liveness);
870 MC_print_statistics_pairs(mc_stats_pair);
875 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);
877 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
878 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
881 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
884 MC_ddfs(search_cycle);
890 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
891 //if(!visited(pair_succ->automaton_state, search_cycle)){
894 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
897 MC_ddfs(search_cycle);
901 XBT_INFO("Next pair already visited ! ");
909 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
911 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);
913 set_pair_reached(pair_succ->automaton_state);
914 //set_pair_reached_hash(pair_succ->automaton_state);
918 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
919 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
923 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
924 //if(!visited(pair_succ->automaton_state, search_cycle)){
927 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
930 MC_ddfs(search_cycle);
934 XBT_INFO("Next pair already visited ! ");
941 /* Restore system before checking others successors */
942 if(cursor != (xbt_dynar_length(successors) - 1))
943 MC_replay_liveness(mc_stack_liveness, 1);
948 if(MC_state_interleave_size(current_pair->graph_state) > 0){
949 XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
950 MC_replay_liveness(mc_stack_liveness, 0);
955 }else{ /*No request to execute, search evolution in Büchi automaton */
959 /* Create the new expanded graph_state */
960 next_graph_state = MC_state_pair_new();
962 xbt_dynar_reset(successors);
968 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
970 res = MC_automaton_evaluate_label(transition_succ->label);
972 if(res == 1){ // enabled transition in automaton
974 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
975 xbt_dynar_push(successors, &next_pair);
983 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
985 res = MC_automaton_evaluate_label(transition_succ->label);
987 if(res == 2){ // true transition in automaton
989 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
990 xbt_dynar_push(successors, &next_pair);
998 xbt_dynar_foreach(successors, cursor, pair_succ){
1000 if(search_cycle == 1){
1002 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
1004 if(reached(pair_succ->automaton_state)){
1005 //if(reached_hash(pair_succ->automaton_state)){
1007 XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
1009 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1010 XBT_INFO("| ACCEPTANCE CYCLE |");
1011 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1012 XBT_INFO("Counter-example that violates formula :");
1013 MC_show_stack_liveness(mc_stack_liveness);
1014 MC_dump_stack_liveness(mc_stack_liveness);
1015 MC_print_statistics_pairs(mc_stats_pair);
1020 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);
1022 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1023 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1026 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1029 MC_ddfs(search_cycle);
1035 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1036 //if(!visited(pair_succ->automaton_state, search_cycle)){
1039 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1042 MC_ddfs(search_cycle);
1046 XBT_INFO("Next pair already visited ! ");
1054 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1056 set_pair_reached(pair_succ->automaton_state);
1057 //set_pair_reached_hash(pair_succ->automaton_state);
1061 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1062 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1066 //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1067 //if(!visited(pair_succ->automaton_state, search_cycle)){
1070 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1073 MC_ddfs(search_cycle);
1077 XBT_INFO("Next pair already visited ! ");
1083 /* Restore system before checking others successors */
1084 if(cursor != xbt_dynar_length(successors) - 1)
1085 MC_replay_liveness(mc_stack_liveness, 1);
1094 XBT_INFO("Max depth reached");
1098 if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
1099 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) );
1101 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) );
1106 xbt_fifo_shift(mc_stack_liveness);
1107 if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
1108 xbt_dynar_pop(reached_pairs, NULL);
1109 //xbt_dynar_pop(reached_pairs_hash, NULL);